diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index bb0b27902adbd4efb0f0e21a52faeb7f98de36c0..6cd77b1c07ab72b79ac516828c9af63cc640da4a 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -475,14 +475,6 @@ flatten :: FlattenMode
--
-- Postcondition: Coercion :: Xi ~ TcType
-flatten f ctxt ty
- | Just ty' <- tcView ty
- = do { (xi, co) <- flatten f ctxt ty'
- ; if xi `tcEqType` ty' then return (ty,co)
- else return (xi,co) }
- -- Small tweak for better error messages
- -- by preserving type synonyms where possible
-
flatten _ _ xi@(LitTy {}) = return (xi, mkTcNomReflCo xi)
flatten f ctxt (TyVarTy tv)
@@ -500,7 +492,9 @@ flatten f ctxt (FunTy ty1 ty2)
; return (mkFunTy xi1 xi2, mkTcFunCo Nominal co1 co2) }
flatten f ctxt (TyConApp tc tys)
- -- For a normal type constructor or data family application,
+ -- For * a normal data type application
+ -- * type synonym application See Note [Flattening synonyms]
+ -- * data family application
-- we just recursively flatten the arguments.
| not (isSynFamilyTyCon tc)
= do { (xis,cos) <- flattenMany f ctxt tys
@@ -538,6 +532,17 @@ flatten _f ctxt ty@(ForAllTy {})
; return (mkForAllTys tvs rho', foldr mkTcForAllCo co tvs) }
\end{code}
+Note [Flattening synonyms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose
+ type T a = a -> a
+and we want to flatten the type (T (F a)). Then we can safely flatten
+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.
+
Note [Flattening under a forall]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Under a forall, we
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 1cc18d12893623f153cc793fa2b477bcc22502e4..0cb7c92be3aad1a3dd0bfdbf420fd09cb6a307b1 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -1724,7 +1724,18 @@ Main purpose: create new evidence for new_pred;
Given Already in inert Nothing
Not Just new_evidence
--}
+
+Note [Rewriting with Refl]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+If the coercion is just reflexivity then you may re-use the same
+variable. But be careful! Although the coercion is Refl, new_pred
+may reflect the result of unification alpha := ty, so new_pred might
+not _look_ the same as old_pred, and it's vital to proceed from now on
+using new_pred.
+
+The flattener preserves type synonyms, so they should appear in new_pred
+as well as in old_pred; that is important for good error messages.
+ -}
rewriteEvidence (CtDerived { ctev_loc = loc }) new_pred _co
@@ -1738,15 +1749,8 @@ rewriteEvidence (CtDerived { ctev_loc = loc }) new_pred _co
newDerived loc new_pred
rewriteEvidence old_ev new_pred co
- | isTcReflCo co -- If just reflexivity then you may re-use the same variable
- = return (Just (if ctEvPred old_ev `tcEqType` new_pred
- then old_ev
- else old_ev { ctev_pred = new_pred }))
- -- Even if the coercion is Refl, it might reflect the result of unification alpha := ty
- -- so old_pred and new_pred might not *look* the same, and it's vital to proceed from
- -- now on using new_pred.
- -- However, if they *do* look the same, we'd prefer to stick with old_pred
- -- then retain the old type, so that error messages come out mentioning synonyms
+ | isTcReflCo co -- See Note [Rewriting with Refl]
+ = return (Just (old_ev { ctev_pred = new_pred }))
rewriteEvidence (CtGiven { ctev_evtm = old_tm , ctev_loc = loc }) new_pred co
= do { new_ev <- newGivenEvVar loc (new_pred, new_tm) -- See Note [Bind new Givens immediately]
@@ -1789,12 +1793,9 @@ rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
= newDerived loc (mkEqPred nlhs nrhs)
| NotSwapped <- swapped
- , isTcReflCo lhs_co
+ , isTcReflCo lhs_co -- See Note [Rewriting with Refl]
, isTcReflCo rhs_co
- , let new_pred = mkTcEqPred nlhs nrhs
- = return (Just (if ctEvPred old_ev `tcEqType` new_pred
- then old_ev
- else old_ev { ctev_pred = new_pred }))
+ = return (Just (old_ev { ctev_pred = new_pred }))
| CtGiven { ctev_evtm = old_tm , ctev_loc = loc } <- old_ev
= do { let new_tm = EvCoercion (lhs_co
diff --git a/testsuite/tests/indexed-types/should_compile/T8913.hs b/testsuite/tests/indexed-types/should_compile/T8913.hs
new file mode 100644
index 0000000000000000000000000000000000000000..062a2521494a50cdc50f03dff64c8769711c4a94
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T8913.hs
@@ -0,0 +1,16 @@
+{-# OPTIONS_GHC -Wall #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE PolyKinds #-}
+
+module T8913 where
+
+class GCat f where
+ gcat :: f p -> Int
+
+cat :: (GCat (MyRep a), MyGeneric a) => a -> Int
+cat x = gcat (from x)
+
+class MyGeneric a where
+ type MyRep a :: * -> *
+ from :: a -> (MyRep a) p
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 5c156ec28e92f9d9008cb2cf17303a2ae70c4ecb..76682ad356cf2ca59f13122c10df865f8f5dcb7c 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -240,3 +240,4 @@ test('ClosedFam2', extra_clean(['ClosedFam2.o-boot', 'ClosedFam2.hi-boot']),
multimod_compile, ['ClosedFam2', '-v0'])
test('T8651', normal, compile, [''])
test('T8889', normal, compile, [''])
+test('T8913', normal, compile, [''])
diff --git a/testsuite/tests/simplCore/should_compile/simpl017.stderr b/testsuite/tests/simplCore/should_compile/simpl017.stderr
index b04dbb4ade51c4530bd270ce71f9465e707ebfcc..18b0a692ce97df2bae93feb3b351b86d1d16663e 100644
--- a/testsuite/tests/simplCore/should_compile/simpl017.stderr
+++ b/testsuite/tests/simplCore/should_compile/simpl017.stderr
@@ -12,11 +12,8 @@ simpl017.hs:44:12:
In a stmt of a 'do' block: return f
simpl017.hs:63:5:
- Couldn't match type ‘forall v.
- [E' RValue (ST s) Int] -> E' v (ST s) Int’
- with ‘[E (ST t0) Int] -> E' RValue (ST s) Int’
- Expected type: [E (ST t0) Int] -> E (ST s) Int
- Actual type: forall v. [E (ST s) Int] -> E' v (ST s) Int
+ Couldn't match expected type ‘[E (ST t0) Int] -> E (ST s) Int’
+ with actual type ‘forall v. [E (ST s) Int] -> E' v (ST s) Int’
Relevant bindings include
a :: forall v. [E (ST s) Int] -> E' v (ST s) Int
(bound at simpl017.hs:60:5)
@@ -28,11 +25,8 @@ simpl017.hs:63:5:
In a stmt of a 'do' block: a [one] `plus` a [one]
simpl017.hs:63:19:
- Couldn't match type ‘forall v.
- [E' RValue (ST s) Int] -> E' v (ST s) Int’
- with ‘[E (ST t1) Int] -> E' RValue (ST s) Int’
- Expected type: [E (ST t1) Int] -> E (ST s) Int
- Actual type: forall v. [E (ST s) Int] -> E' v (ST s) Int
+ Couldn't match expected type ‘[E (ST t1) Int] -> E (ST s) Int’
+ with actual type ‘forall v. [E (ST s) Int] -> E' v (ST s) Int’
Relevant bindings include
a :: forall v. [E (ST s) Int] -> E' v (ST s) Int
(bound at simpl017.hs:60:5)