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.

2 files changed, 30 insertions, 24 deletions

diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index a90627091f..3e23756265 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 a92bc95aeb..b7faf153ca 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