diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index 6cd77b1c07ab72b79ac516828c9af63cc640da4a..f11c9d9ed92feef16ef14f959558ab8959a71cfb 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -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.
diff --git a/testsuite/tests/indexed-types/should_compile/T8978.hs b/testsuite/tests/indexed-types/should_compile/T8978.hs
new file mode 100644
index 0000000000000000000000000000000000000000..077a07db311ba97336da0cc23bae2502a8d42597
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T8978.hs
@@ -0,0 +1,12 @@
+{-# 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
diff --git a/testsuite/tests/indexed-types/should_compile/T8979.hs b/testsuite/tests/indexed-types/should_compile/T8979.hs
new file mode 100644
index 0000000000000000000000000000000000000000..85e13cee4e08ad07eeaf5a7bb67d344722b9380e
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T8979.hs
@@ -0,0 +1,10 @@
+{-# 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
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 76682ad356cf2ca59f13122c10df865f8f5dcb7c..5f304463c627be6d853e600f9a1927cd72f08312 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -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, [''])
diff --git a/testsuite/tests/indexed-types/should_fail/T5439.stderr b/testsuite/tests/indexed-types/should_fail/T5439.stderr
index d5f031898565a7db0c274840de66859f81b1b5f2..18af3fa7cf698fe60bfa49268c4e70e558025b63 100644
--- a/testsuite/tests/indexed-types/should_fail/T5439.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T5439.stderr
@@ -1,25 +1,26 @@
-
-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)’
diff --git a/testsuite/tests/indexed-types/should_fail/T5934.stderr b/testsuite/tests/indexed-types/should_fail/T5934.stderr
index cf7bf8784eea0851ba520954410ad348a76aa698..85ab1a1804e37f83e210f9a6cdb9bf6fcad66ccb 100644
--- a/testsuite/tests/indexed-types/should_fail/T5934.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T5934.stderr
@@ -1,7 +1,8 @@
-
-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