Flattener preserves synonyms, rewriteEvidence can drop buggy "optimisation"

There was a special case in rewriteEvidence, looking like:
  = return (Just (if ctEvPred old_ev `tcEqType` new_pred
                  then old_ev
                  else old_ev { ctev_pred = new_pred }))

But this was wrong: old_pred and new_pred might differ in the kind
of a TyVar occurrence, in which case tcEqType would not notice,
but we really, really want new_pred.  This caused Trac #8913.

I solved this by dropping the whole test, and instead making
the flattener preserve type synonyms. This was easy because
TcEvidence has TcTyConAppCo which (unlike) Coercion, handles
synonyms.

(cherry picked from commit 6ae678e31a5fdd3b0bd1f8613fe164012bb630f4)

5 files changed, 51 insertions, 34 deletions

diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index bb0b27902a..6cd77b1c07 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 1cc18d1289..0cb7c92be3 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 0000000000..062a252149
--- /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 5c156ec28e..76682ad356 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 b04dbb4ade..18b0a692ce 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)