Commit b8132a9d authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Fix egregious blunder in the type flattener

In tidying up the flattener I introduced an error that no
regression test caught, giving rise to Trac #8978, #8979.
It shows up if you have a type synonym whose RHS mentions
type functions, such sas
     type family F a
     type T a = (F a, a)   -- This synonym isn't properly flattened

The fix is easy, but sadly the bug is in the released GHC 7.8.1
parent b4dd5667
......@@ -492,13 +492,21 @@ flatten f ctxt (FunTy ty1 ty2)
; return (mkFunTy xi1 xi2, mkTcFunCo Nominal co1 co2) }
flatten f ctxt (TyConApp tc tys)
-- Expand type synonyms that mention type families
-- on the RHS; see Note [Flattening synonyms]
| Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys
, any isSynFamilyTyCon (tyConsOfType rhs)
= flatten f ctxt (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
-- For * a normal data type application
-- * type synonym application See Note [Flattening synonyms]
-- * data family application
-- * type synonym application whose RHS does not mention type families
-- See Note [Flattening synonyms]
-- we just recursively flatten the arguments.
| not (isSynFamilyTyCon tc)
= do { (xis,cos) <- flattenMany f ctxt tys
; return (mkTyConApp tc xis, mkTcTyConAppCo Nominal tc cos) }
= do { (xis,cos) <- flattenMany f ctxt tys
; return (mkTyConApp tc xis, mkTcTyConAppCo Nominal tc cos) }
-- Otherwise, it's a type function application, and we have to
-- flatten it away as well, and generate a new given equality constraint
......@@ -534,6 +542,9 @@ flatten _f ctxt ty@(ForAllTy {})
Note [Flattening synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~
Not expanding synonyms aggressively improves error messages, and
keeps types smaller. But we need to take care.
Suppose
type T a = a -> a
and we want to flatten the type (T (F a)). Then we can safely flatten
......@@ -541,12 +552,16 @@ the (F a) to a skolem, and return (T fsk). We don't need to expand the
synonym. This works because TcTyConAppCo can deal with synonyms
(unlike TyConAppCo), see Note [TcCoercions] in TcEvidence.
Not expanding synonyms aggressively improves error messages.
But (Trac #8979) for
type T a = (F a, a) where F is a type function
we must expand the synonym in (say) T Int, to expose the type functoin
to the flattener.
Note [Flattening under a forall]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Under a forall, we
(a) MUST apply the inert subsitution
(a) MUST apply the inert substitution
(b) MUST NOT flatten type family applications
Hence FMSubstOnly.
......
{-# LANGUAGE FlexibleContexts, TypeFamilies #-}
module T8978 where
type Syn a = Associated a
class Eq (Associated a) => Foo a where
type Associated a :: *
foo :: a -> Syn a -> Bool
instance Foo () where
type Associated () = Int
foo _ x = x == x
{-# LANGUAGE TypeFamilies #-}
module T8979 where
type family F a
type family G a
type H a = G a
f :: F (G Char) -> F (H Char)
f a = a
......@@ -241,3 +241,5 @@ test('ClosedFam2', extra_clean(['ClosedFam2.o-boot', 'ClosedFam2.hi-boot']),
test('T8651', normal, compile, [''])
test('T8889', normal, compile, [''])
test('T8913', normal, compile, [''])
test('T8978', normal, compile, [''])
test('T8979', normal, compile, [''])
T5439.hs:83:28:
Couldn't match type ‘Attempt (HNth n0 l0) -> Attempt (HElemOf l0)’
with ‘Attempt (WaitOpResult (WaitOps rs))’
Expected type: f (Attempt (HNth n0 l0) -> Attempt (HElemOf l0))
Actual type: f (Attempt (WaitOpResult (WaitOps rs)))
Relevant bindings include
register :: Bool -> Peano n -> WaitOps (HDrop n rs) -> IO Bool
(bound at T5439.hs:65:9)
ev :: f (Attempt (WaitOpResult (WaitOps rs)))
(bound at T5439.hs:62:22)
ops :: WaitOps rs (bound at T5439.hs:62:18)
registerWaitOp :: WaitOps rs
-> f (Attempt (WaitOpResult (WaitOps rs))) -> IO Bool
(bound at T5439.hs:62:3)
In the first argument of ‘complete’, namely ‘ev’
In the expression: complete ev
T5439.hs:83:39:
Couldn't match expected type ‘Peano n0’
with actual type ‘Attempt α0’
In the second argument of ‘($)’, namely
‘Failure (e :: SomeException)’
In the second argument of ‘($)’, namely
‘inj $ Failure (e :: SomeException)’
T5439.hs:83:28:
Couldn't match type ‘Attempt (HHead (HDrop n0 l0))
-> Attempt (HElemOf l0)’
with ‘Attempt (WaitOpResult (WaitOps rs))’
Expected type: f (Attempt (HNth n0 l0) -> Attempt (HElemOf l0))
Actual type: f (Attempt (WaitOpResult (WaitOps rs)))
Relevant bindings include
register :: Bool -> Peano n -> WaitOps (HDrop n rs) -> IO Bool
(bound at T5439.hs:65:9)
ev :: f (Attempt (WaitOpResult (WaitOps rs)))
(bound at T5439.hs:62:22)
ops :: WaitOps rs (bound at T5439.hs:62:18)
registerWaitOp :: WaitOps rs
-> f (Attempt (WaitOpResult (WaitOps rs))) -> IO Bool
(bound at T5439.hs:62:3)
In the first argument of ‘complete’, namely ‘ev’
In the expression: complete ev
T5439.hs:83:39:
Couldn't match expected type ‘Peano n0’
with actual type ‘Attempt α0’
In the second argument of ‘($)’, namely
‘Failure (e :: SomeException)’
In the second argument of ‘($)’, namely
‘inj $ Failure (e :: SomeException)’
T5934.hs:12:7:
Cannot instantiate unification variable ‘a0’
with a type involving foralls: (forall s. GenST s) -> Int
Perhaps you want ImpredicativeTypes
In the expression: 0
In an equation for ‘run’: run = 0
T5934.hs:12:7:
Cannot instantiate unification variable ‘a0’
with a type involving foralls:
(forall s. Gen (PrimState (ST s))) -> Int
Perhaps you want ImpredicativeTypes
In the expression: 0
In an equation for ‘run’: run = 0
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment