Implement a fast path for new constraints looking like (a~b), namely unifyWanted

Looking at some typechecker traces I could see places where we were laboriously
creating a Refl coercion.  This patch short-circuits the process.

See TcCanonical:
  Note [unifyWanted and unifyDerived]
  Note [Decomposing TyConApps]

I ended up with some refactoring, notably

  * I moved xCtEvidence, rewriteEvidence, rewriteEqEvidence
    from TcSMonad to TcCanonical

There are some knock-on effects, but only minor ones.

3 files changed, 436 insertions, 321 deletions

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 4042fe83c9..749748ff80 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -1,6 +1,11 @@
 {-# LANGUAGE CPP #-}
 
-module TcCanonical( canonicalize ) where
+module TcCanonical( 
+     canonicalize,
+     unifyDerived,
+
+     StopOrContinue(..), stopWith, continueWith
+  ) where
 
 #include "HsVersions.h"
 
@@ -18,12 +23,14 @@ import Var
 import Name( isSystemName )
 import OccName( OccName )
 import Outputable
-import Control.Monad    ( when )
+import Control.Monad
 import DynFlags( DynFlags )
 import VarSet
 
+import Pair
 import Util
 import BasicTypes
+import FastString
 
 {-
 ************************************************************************
@@ -427,7 +434,9 @@ can_eq_nc' ev (TyConApp tc1 _) ps_ty1 (FunTy {}) ps_ty2
   = canEqFailure ev ps_ty1 ps_ty2
 
 can_eq_nc' ev (FunTy s1 t1) _ (FunTy s2 t2) _
-  = canDecomposableTyConAppOK ev funTyCon [s1,t1] [s2,t2]
+  = do { canDecomposableTyConAppOK ev funTyCon [s1,t1] [s2,t2]
+       ; stopWith ev "Decomposed FunTyCon" }
+
 
 can_eq_nc' ev (FunTy {}) ps_ty1 (TyConApp tc2 _) ps_ty2
   | isDecomposableTyCon tc2
@@ -517,14 +526,11 @@ try_decompose_app ev ty1 ty2
        = do { emitNewDerived loc (mkTcEqPred t1 t2)
             ; try_decompose_app ev s1 s2 }
        | CtWanted { ctev_evar = evar, ctev_loc = loc } <- ev
-       = do { (ev_s,fr_s) <- newWantedEvVar loc (mkTcEqPred s1 s2)
-            ; (ev_t,fr_t) <- newWantedEvVar loc (mkTcEqPred t1 t2)
-            ; let co = mkTcAppCo (ctEvCoercion ev_s) (ctEvCoercion ev_t)
+       = do { ev_s <- newWantedEvVarNC loc (mkTcEqPred s1 s2)
+            ; co_t <- unifyWanted loc t1 t2
+            ; let co = mkTcAppCo (ctEvCoercion ev_s) co_t
             ; setEvBind evar (EvCoercion co)
-            ; when (isFresh fr_t) $ emitWorkNC [ev_t]
-            ; case fr_s of
-                Fresh  -> try_decompose_app ev_s s1 s2
-                Cached -> return (Stop ev (text "Decomposed app")) }
+            ; try_decompose_app ev_s s1 s2 }
        | CtGiven { ctev_evtm = ev_tm, ctev_loc = loc } <- ev
        = do { let co   = evTermCoercion ev_tm
                   co_s = mkTcLRCo CLeft  co
@@ -541,25 +547,38 @@ canDecomposableTyConApp :: CtEvidence
                         -> TyCon -> [TcType]
                         -> TyCon -> [TcType]
                         -> TcS (StopOrContinue Ct)
+-- See Note [Decomposing TyConApps]
 canDecomposableTyConApp ev tc1 tys1 tc2 tys2
   | tc1 /= tc2 || length tys1 /= length tys2
     -- Fail straight away for better error messages
   = canEqFailure ev (mkTyConApp tc1 tys1) (mkTyConApp tc2 tys2)
   | otherwise
   = do { traceTcS "canDecomposableTyConApp" (ppr ev $$ ppr tc1 $$ ppr tys1 $$ ppr tys2)
-       ; canDecomposableTyConAppOK ev tc1 tys1 tys2 }
+       ; canDecomposableTyConAppOK ev tc1 tys1 tys2
+       ; stopWith ev "Decomposed TyConApp" }
 
 canDecomposableTyConAppOK :: CtEvidence
                           -> TyCon -> [TcType] -> [TcType]
-                          -> TcS (StopOrContinue Ct)
-
+                          -> TcS ()
+-- Precondition: tys1 and tys2 are the same length, hence "OK"
 canDecomposableTyConAppOK ev tc1 tys1 tys2
-  = do { let xcomp xs  = EvCoercion (mkTcTyConAppCo Nominal tc1 (map evTermCoercion xs))
-             xdecomp x = zipWith (\_ i -> EvCoercion $ mkTcNthCo i (evTermCoercion x)) tys1 [0..]
-             xev = XEvTerm (zipWith mkTcEqPred tys1 tys2) xcomp xdecomp
-       ; xCtEvidence ev xev
-       ; stopWith ev "Decomposed TyConApp" }
+  = case ev of
+     CtDerived { ctev_loc = loc }
+        -> mapM_ (unifyDerived loc) (zipWith Pair tys1 tys2)
+
+     CtWanted { ctev_evar = evar, ctev_loc = loc }
+        -> do { cos <- zipWithM (unifyWanted loc) tys1 tys2
+              ; setEvBind evar (EvCoercion (mkTcTyConAppCo Nominal tc1 cos)) }
+
+     CtGiven { ctev_evtm = ev_tm, ctev_loc = loc }
+        -> do { given_evs <- newGivenEvVars loc $
+                             zipWith3 (mk_given ev_tm) tys1 tys2 [0..]
+              ; emitWorkNC given_evs }
+  where
+    mk_given ev_tm ty1 ty2 i
+       = (mkTcEqPred ty1 ty2, EvCoercion (mkTcNthCo i (evTermCoercion ev_tm)))
 
+--------------------
 canEqFailure :: CtEvidence -> TcType -> TcType -> TcS (StopOrContinue Ct)
 -- See Note [Make sure that insolubles are fully rewritten]
 canEqFailure ev ty1 ty2
@@ -572,6 +591,20 @@ canEqFailure ev ty1 ty2
            Stop ev s -> pprPanic "canEqFailure" (s $$ ppr ev $$ ppr ty1 $$ ppr ty2) }
 
 {-
+Note [Decomposing TyConApps]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If we see (T s1 t1 ~ T s2 t2), then we can just decompose to
+  (s1 ~ s2, t1 ~ t2)
+and push those back into the work list.  But if
+  s1 = K k1    s2 = K k2
+then we will jus decomopose s1~s2, and it might be better to
+do so on the spot.  An important special case is where s1=s2,
+and we get just Refl.
+
+So canDecomposableTyCon is a fast-path decomposition that uses
+unifyWanted etc to short-cut that work.
+
+
 Note [Canonicalising type applications]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Given (s1 t1) ~ ty2, how should we proceed?
@@ -1027,3 +1060,321 @@ we first try expanding each of the ti to types which no longer contain
 a.  If this turns out to be impossible, we next try expanding F
 itself, and so on.  See Note [Occurs check expansion] in TcType
 -}
+
+{-
+************************************************************************
+*                                                                      *
+                  Evidence transformation
+*                                                                      *
+************************************************************************
+-}
+
+{-
+Note [xCtEvidence]
+~~~~~~~~~~~~~~~~~~
+A call might look like this:
+
+    xCtEvidence ev evidence-transformer
+
+  ev is Given   => use ev_decomp to create new Givens for ev_preds,
+                   and return them
+
+  ev is Wanted  => create new wanteds for ev_preds,
+                   use ev_comp to bind ev,
+                   return fresh wanteds (ie ones not cached in inert_cans or solved)
+
+  ev is Derived => create new deriveds for ev_preds
+                      (unless cached in inert_cans or solved)
+
+Note: The [CtEvidence] returned is a subset of the subgoal-preds passed in
+      Ones that are already cached are not returned
+
+Example
+    ev : Tree a b ~ Tree c d
+    xCtEvidence ev [a~c, b~d] (XEvTerm { ev_comp = \[c1 c2]. <Tree> c1 c2
+                                       , ev_decomp = \c. [nth 1 c, nth 2 c] })
+              (\fresh-goals.  stuff)
+
+Note [Bind new Givens immediately]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+For Givens we make new EvVars and bind them immediately. We don't worry
+about caching, but we don't expect complicated calculations among Givens.
+It is important to bind each given:
+      class (a~b) => C a b where ....
+      f :: C a b => ....
+Then in f's Givens we have g:(C a b) and the superclass sc(g,0):a~b.
+But that superclass selector can't (yet) appear in a coercion
+(see evTermCoercion), so the easy thing is to bind it to an Id.
+
+See Note [Coercion evidence terms] in TcEvidence.
+-}
+
+xCtEvidence :: CtEvidence            -- Original evidence
+            -> XEvTerm               -- Instructions about how to manipulate evidence
+            -> TcS ()
+
+xCtEvidence (CtWanted { ctev_evar = evar, ctev_loc = loc })
+            (XEvTerm { ev_preds = ptys, ev_comp = comp_fn })
+  = do { new_evars <- mapM (newWantedEvVar loc) ptys
+       ; setEvBind evar (comp_fn (map (ctEvTerm . fst) new_evars))
+       ; emitWorkNC (freshGoals new_evars) }
+         -- Note the "NC": these are fresh goals, not necessarily canonical
+
+xCtEvidence (CtGiven { ctev_evtm = tm, ctev_loc = loc })
+            (XEvTerm { ev_preds = ptys, ev_decomp = decomp_fn })
+  = ASSERT( equalLength ptys (decomp_fn tm) )
+    do { given_evs <- newGivenEvVars loc (ptys `zip` decomp_fn tm)
+       ; emitWorkNC given_evs }
+
+xCtEvidence (CtDerived { ctev_loc = loc })
+            (XEvTerm { ev_preds = ptys })
+  = mapM_ (emitNewDerived loc) ptys
+
+-----------------------------
+data StopOrContinue a
+  = ContinueWith a    -- The constraint was not solved, although it may have
+                      --   been rewritten
+
+  | Stop CtEvidence   -- The (rewritten) constraint was solved
+         SDoc         -- Tells how it was solved
+                      -- Any new sub-goals have been put on the work list
+
+instance Functor StopOrContinue where
+  fmap f (ContinueWith x) = ContinueWith (f x)
+  fmap _ (Stop ev s)      = Stop ev s
+
+instance Outputable a => Outputable (StopOrContinue a) where
+  ppr (Stop ev s)      = ptext (sLit "Stop") <> parens s <+> ppr ev
+  ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
+
+continueWith :: a -> TcS (StopOrContinue a)
+continueWith = return . ContinueWith
+
+stopWith :: CtEvidence -> String -> TcS (StopOrContinue a)
+stopWith ev s = return (Stop ev (text s))
+
+andWhenContinue :: TcS (StopOrContinue a)
+                -> (a -> TcS (StopOrContinue b))
+                -> TcS (StopOrContinue b)
+andWhenContinue tcs1 tcs2
+  = do { r <- tcs1
+       ; case r of
+           Stop ev s       -> return (Stop ev s)
+           ContinueWith ct -> tcs2 ct }
+
+rewriteEvidence :: CtEvidence   -- old evidence
+                -> TcPredType   -- new predicate
+                -> TcCoercion   -- Of type :: new predicate ~ <type of old evidence>
+                -> TcS (StopOrContinue CtEvidence)
+-- Returns Just new_ev iff either (i)  'co' is reflexivity
+--                             or (ii) 'co' is not reflexivity, and 'new_pred' not cached
+-- In either case, there is nothing new to do with new_ev
+{-
+     rewriteEvidence old_ev new_pred co
+Main purpose: create new evidence for new_pred;
+              unless new_pred is cached already
+* Returns a new_ev : new_pred, with same wanted/given/derived flag as old_ev
+* If old_ev was wanted, create a binding for old_ev, in terms of new_ev
+* If old_ev was given, AND not cached, create a binding for new_ev, in terms of old_ev
+* Returns Nothing if new_ev is already cached
+
+        Old evidence    New predicate is               Return new evidence
+        flavour                                        of same flavor
+        -------------------------------------------------------------------
+        Wanted          Already solved or in inert     Nothing
+        or Derived      Not                            Just new_evidence
+
+        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 old_ev@(CtDerived { ctev_loc = loc }) new_pred _co
+  = -- If derived, don't even look at the coercion.
+    -- This is very important, DO NOT re-order the equations for
+    -- rewriteEvidence to put the isTcReflCo test first!
+    -- Why?  Because for *Derived* constraints, c, the coercion, which
+    -- was produced by flattening, may contain suspended calls to
+    -- (ctEvTerm c), which fails for Derived constraints.
+    -- (Getting this wrong caused Trac #7384.)
+    do { mb_ev <- newDerived loc new_pred
+       ; case mb_ev of
+           Just new_ev -> continueWith new_ev
+           Nothing     -> stopWith old_ev "Cached derived" }
+
+rewriteEvidence old_ev new_pred co
+  | isTcReflCo co -- See Note [Rewriting with Refl]
+  = return (ContinueWith (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]
+       ; return (ContinueWith new_ev) }
+  where
+    new_tm = mkEvCast old_tm (mkTcSubCo (mkTcSymCo co))  -- mkEvCast optimises ReflCo
+
+rewriteEvidence ev@(CtWanted { ctev_evar = evar, ctev_loc = loc }) new_pred co
+  = do { (new_ev, freshness) <- newWantedEvVar loc new_pred
+       ; MASSERT( tcCoercionRole co == Nominal )
+       ; setEvBind evar (mkEvCast (ctEvTerm new_ev) (mkTcSubCo co))
+       ; case freshness of
+            Fresh  -> continueWith new_ev
+            Cached -> stopWith ev "Cached wanted" }
+
+
+rewriteEqEvidence :: CtEvidence         -- Old evidence :: olhs ~ orhs (not swapped)
+                                        --              or orhs ~ olhs (swapped)
+                  -> SwapFlag
+                  -> TcType -> TcType   -- New predicate  nlhs ~ nrhs
+                                        -- Should be zonked, because we use typeKind on nlhs/nrhs
+                  -> TcCoercion         -- lhs_co, of type :: nlhs ~ olhs
+                  -> TcCoercion         -- rhs_co, of type :: nrhs ~ orhs
+                  -> TcS (StopOrContinue CtEvidence)  -- Of type nlhs ~ nrhs
+-- For (rewriteEqEvidence (Given g olhs orhs) False nlhs nrhs lhs_co rhs_co)
+-- we generate
+-- If not swapped
+--      g1 : nlhs ~ nrhs = lhs_co ; g ; sym rhs_co
+-- If 'swapped'
+--      g1 : nlhs ~ nrhs = lhs_co ; Sym g ; sym rhs_co
+--
+-- For (Wanted w) we do the dual thing.
+-- New  w1 : nlhs ~ nrhs
+-- If not swapped
+--      w : olhs ~ orhs = sym lhs_co ; w1 ; rhs_co
+-- If swapped
+--      w : orhs ~ olhs = sym rhs_co ; sym w1 ; lhs_co
+--
+-- It's all a form of rewwriteEvidence, specialised for equalities
+rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
+  | CtDerived { ctev_loc = loc } <- old_ev
+  = do { mb <- newDerived loc new_pred
+       ; case mb of
+           Just new_ev -> continueWith new_ev
+           Nothing     -> stopWith old_ev "Cached derived" }
+
+  | NotSwapped <- swapped
+  , isTcReflCo lhs_co      -- See Note [Rewriting with Refl]
+  , isTcReflCo rhs_co
+  = return (ContinueWith (old_ev { ctev_pred = new_pred }))
+
+  | CtGiven { ctev_evtm = old_tm , ctev_loc = loc } <- old_ev
+  = do { let new_tm = EvCoercion (lhs_co
+                                  `mkTcTransCo` maybeSym swapped (evTermCoercion old_tm)
+                                  `mkTcTransCo` mkTcSymCo rhs_co)
+       ; new_ev <- newGivenEvVar loc (new_pred, new_tm)  -- See Note [Bind new Givens immediately]
+       ; return (ContinueWith new_ev) }
+
+  | CtWanted { ctev_evar = evar, ctev_loc = loc } <- old_ev
+  = do { new_evar <- newWantedEvVarNC loc new_pred
+       ; let co = maybeSym swapped $
+                  mkTcSymCo lhs_co
+                  `mkTcTransCo` ctEvCoercion new_evar
+                  `mkTcTransCo` rhs_co
+       ; setEvBind evar (EvCoercion co)
+       ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co])
+       ; return (ContinueWith new_evar) }
+
+  | otherwise
+  = panic "rewriteEvidence"
+  where
+    new_pred = mkTcEqPred nlhs nrhs
+
+{- Note [unifyWanted and unifyDerived]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When decomposing equalities we often create new wanted constraints for
+(s ~ t).  But what if s=t?  Then it'd be faster to return Refl right away.
+Similar remarks apply for Derived.
+
+Rather than making an equality test (which traverses the structure of the
+type, perhaps fruitlessly, unifyWanted traverses the common structure, and
+bales out when it finds a difference by creating a new Wanted constraint.
+But where it succeeds in finding common structure, it just builds a coercion
+to reflect it.
+-}
+
+unifyWanted :: CtLoc -> TcType -> TcType -> TcS TcCoercion
+-- Return coercion witnessing the equality of the two types,
+-- emitting new work equalities where necessary to achieve that
+-- Very good short-cut when the two types are equal, or nearly so
+-- See Note [unifyWanted and unifyDerived]
+unifyWanted loc orig_ty1 orig_ty2
+  = go orig_ty1 orig_ty2
+  where
+    go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
+    go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
+
+    go (FunTy s1 t1) (FunTy s2 t2)
+      = do { co_s <- unifyWanted loc s1 s2
+           ; co_t <- unifyWanted loc t1 t2
+           ; return (mkTcTyConAppCo Nominal funTyCon [co_s,co_t]) }
+    go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
+      | tc1 == tc2, isDecomposableTyCon tc1, tys1 `equalLength` tys2
+      = do { cos <- zipWithM (unifyWanted loc) tys1 tys2
+           ; return (mkTcTyConAppCo Nominal tc1 cos) }
+    go (TyVarTy tv) ty2
+      = do { mb_ty <- isFilledMetaTyVar_maybe tv
+           ; case mb_ty of
+                Just ty1' -> go ty1' ty2
+                Nothing   -> bale_out }
+    go ty1 (TyVarTy tv)
+      = do { mb_ty <- isFilledMetaTyVar_maybe tv
+           ; case mb_ty of
+                Just ty2' -> go ty1 ty2'
+                Nothing   -> bale_out }
+    go _ _ = bale_out
+
+    bale_out = do { ev <- newWantedEvVarNC loc (mkTcEqPred orig_ty1 orig_ty2)
+                  ; emitWorkNC [ev]
+                  ; return (ctEvCoercion ev) }
+
+unifyDeriveds :: CtLoc -> [TcType] -> [TcType] -> TcS ()
+-- See Note [unifyWanted and unifyDerived]
+unifyDeriveds loc tys1 tys2 = zipWithM_ (unify_derived loc) tys1 tys2
+
+unifyDerived :: CtLoc -> Pair TcType -> TcS ()
+-- See Note [unifyWanted and unifyDerived]
+unifyDerived loc (Pair ty1 ty2) = unify_derived loc ty1 ty2
+
+unify_derived :: CtLoc -> TcType -> TcType -> TcS ()
+-- Create new Derived and put it in the work list
+-- Should do nothing if the two types are equal
+-- See Note [unifyWanted and unifyDerived]
+unify_derived loc orig_ty1 orig_ty2
+  = go orig_ty1 orig_ty2
+  where
+    go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
+    go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
+
+    go (FunTy s1 t1) (FunTy s2 t2)
+      = do { unify_derived loc s1 s2
+           ; unify_derived loc t1 t2 }
+    go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
+      | tc1 == tc2, isDecomposableTyCon tc1, tys1 `equalLength` tys2
+      = unifyDeriveds loc tys1 tys2
+    go (TyVarTy tv) ty2
+      = do { mb_ty <- isFilledMetaTyVar_maybe tv
+           ; case mb_ty of
+                Just ty1' -> go ty1' ty2
+                Nothing   -> bale_out }
+    go ty1 (TyVarTy tv)
+      = do { mb_ty <- isFilledMetaTyVar_maybe tv
+           ; case mb_ty of
+                Just ty2' -> go ty1 ty2'
+                Nothing   -> bale_out }
+    go _ _ = bale_out
+
+    bale_out = emitNewDerived loc (mkTcEqPred orig_ty1 orig_ty2)
+
+maybeSym :: SwapFlag -> TcCoercion -> TcCoercion
+maybeSym IsSwapped  co = mkTcSymCo co
+maybeSym NotSwapped co = co
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 47401ed829..e3ce77e29a 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -684,7 +684,7 @@ interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc
   = do { let matching_funeqs = findFunEqsByTyCon funeqs tc
        ; let interact = sfInteractInert ops args (lookupFlattenTyVar eqs fsk)
              do_one (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk, cc_ev = iev })
-                = mapM_ (emitNewDerivedEq (ctEvLoc iev))
+                = mapM_ (unifyDerived (ctEvLoc iev))
                         (interact iargs (lookupFlattenTyVar eqs ifsk))
              do_one ct = pprPanic "interactFunEq" (ppr ct)
        ; mapM_ do_one matching_funeqs
@@ -1496,7 +1496,7 @@ instFunDepEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = loc })
        ; mapM_ (do_one subst) eqs }
   where
     do_one subst (FDEq { fd_ty_left = ty1, fd_ty_right = ty2 })
-       = emitNewDerivedEq loc (Pair (Type.substTy subst ty1) (Type.substTy subst ty2))
+       = unifyDerived loc (Pair (Type.substTy subst ty1) (Type.substTy subst ty2))
 
 {-
 *********************************************************************************
@@ -1629,6 +1629,9 @@ doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
     | otherwise -- We must not assign ufsk := ...ufsk...!
     -> do { alpha_ty <- newFlexiTcSTy (tyVarKind fsk)
           ; new_ev <- newWantedEvVarNC loc (mkTcEqPred alpha_ty rhs_ty)
+          ; emitWorkNC [new_ev]
+              -- By emitting this as non-canonical, we deal with all
+              -- flattening, occurs-check, and ufsk := ufsk issues
           ; let final_co = ax_co `mkTcTransCo` mkTcSymCo (ctEvCoercion new_ev)
               --    ax_co :: fam_tc args ~ rhs_ty
               --       ev :: alpha ~ rhs_ty
@@ -1639,9 +1642,6 @@ doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
             vcat [ text "old_ev:" <+> ppr old_ev
                  , nest 2 (text ":=") <+> ppr final_co
                  , text "new_ev:" <+> ppr new_ev ]
-          ; emitWorkNC [new_ev]
-              -- By emitting this as non-canonical, we deal with all
-              -- flattening, occurs-check, and ufsk := ufsk issues
           ; stopWith old_ev "Fun/Top (wanted)" } } }
   where
     loc = ctEvLoc old_ev
@@ -1651,7 +1651,7 @@ doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
       | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
       = do { inert_eqs <- getInertEqs
            ; let eqns = sfInteractTop ops args (lookupFlattenTyVar inert_eqs fsk)
-           ; mapM_ (emitNewDerivedEq loc) eqns }
+           ; mapM_ (unifyDerived loc) eqns }
       | otherwise
       = return ()
 
@@ -2190,9 +2190,8 @@ requestCoercible :: CtLoc -> TcType -> TcType
                         , TcCoercion )      -- Coercion witnessing (Coercible t1 t2)
 requestCoercible loc ty1 ty2
   = ASSERT2( typeKind ty1 `tcEqKind` typeKind ty2, ppr ty1 <+> ppr ty2)
-    do { (new_ev, freshness) <- newWantedEvVar loc' (mkCoerciblePred ty1 ty2)
-       ; return ( case freshness of { Fresh -> [new_ev]; Cached -> [] }
-                , ctEvCoercion new_ev) }
+    do { new_ev <- newWantedEvVarNC loc' (mkCoerciblePred ty1 ty2)
+       ; return ( [new_ev], ctEvCoercion new_ev) }
            -- Evidence for a Coercible constraint is always a coercion t1 ~R t2
   where
      loc' = bumpCtLocDepth CountConstraints loc
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index cba8e24dd6..76200c5929 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -26,18 +26,11 @@ module TcSMonad (
     XEvTerm(..),
     Freshness(..), freshGoals, isFresh,
 
-    StopOrContinue(..), continueWith, stopWith, andWhenContinue,
-
-    xCtEvidence,        -- Transform a CtEvidence during a step
-    rewriteEvidence,    -- Specialized version of xCtEvidence for coercions
-    rewriteEqEvidence,  -- Yet more specialised, for equality coercions
-    maybeSym,
-
     newTcEvBinds, newWantedEvVar, newWantedEvVarNC,
     setWantedTyBind, reportUnifications,
     setEvBind,
-    newEvVar, newGivenEvVar,
-    emitNewDerived, emitNewDerivedEq,
+    newEvVar, newGivenEvVar, newGivenEvVars,
+    newDerived, emitNewDerived,
     instDFunConstraints,
 
     getInstEnvs, getFamInstEnvs,                -- Getting the environments
@@ -134,13 +127,12 @@ import Util
 import Id
 import TcRnTypes
 
-import BasicTypes
 import Unique
 import UniqFM
 import Maybes ( orElse, firstJusts )
 
 import TrieMap
-import Control.Monad( ap, when, unless )
+import Control.Monad( ap, when, unless, MonadPlus(..) )
 import MonadUtils
 import Data.IORef
 import Data.List ( partition, foldl' )
@@ -821,16 +813,12 @@ lookupFlatCache fam_tc tys
 lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
 -- Is this exact predicate type cached in the solved or canonicals of the InertSet?
 lookupInInerts loc pty
+  | ClassPred cls tys <- classifyPredType pty
   = do { inerts <- getTcSInerts
-       ; return $ case (classifyPredType pty) of
-           ClassPred cls tys
-              | Just ev <- lookupSolvedDict inerts loc cls tys
-              -> Just ev
-              | otherwise
-              -> lookupInertDict (inert_cans inerts) loc cls tys
-
-           _other -> Nothing -- NB: No caching for equalities, IPs, holes, or errors
-      }
+       ; return (lookupSolvedDict inerts loc cls tys `mplus`
+                 lookupInertDict (inert_cans inerts) loc cls tys) }
+  | otherwise -- NB: No caching for equalities, IPs, holes, or errors
+  = return Nothing
 
 lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
 lookupInertDict (IC { inert_dicts = dicts }) loc cls tys
@@ -1647,98 +1635,27 @@ newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
 -- Make a new variable of the given PredType,
 -- immediately bind it to the given term
 -- and return its CtEvidence
+-- Precondition: this is not a kind equality
+--               See Note [Do not create Given kind equalities]
 newGivenEvVar loc (pred, rhs)
-  = do { new_ev <- newEvVar pred
+  = ASSERT2( not (isKindEquality pred), ppr pred $$ pprCtOrigin (ctLocOrigin loc) )
+    do { new_ev <- newEvVar pred
        ; setEvBind new_ev rhs
        ; return (CtGiven { ctev_pred = pred, ctev_evtm = EvId new_ev, ctev_loc = loc }) }
 
-newWantedEvVarNC :: CtLoc -> TcPredType -> TcS CtEvidence
--- Don't look up in the solved/inerts; we know it's not there
-newWantedEvVarNC loc pty
-  = do { new_ev <- newEvVar pty
-       ; return (CtWanted { ctev_pred = pty, ctev_evar = new_ev, ctev_loc = loc })}
+newGivenEvVars :: CtLoc -> [(TcPredType, EvTerm)] -> TcS [CtEvidence]
+-- Like newGivenEvVar, but automatically discard kind equalities
+-- See Note [Do not create Given kind equalities]
+newGivenEvVars loc pts = mapM (newGivenEvVar loc) (filterOut (isKindEquality . fst) pts)
 
-newWantedEvVar :: CtLoc -> TcPredType -> TcS (CtEvidence, Freshness)
-newWantedEvVar loc pty
-  = do { mb_ct <- lookupInInerts loc pty
-       ; case mb_ct of
-            Just ctev | not (isDerived ctev)
-                      -> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
-                            ; return (ctev, Cached) }
-            _ -> do { ctev <- newWantedEvVarNC loc pty
-                    ; traceTcS "newWantedEvVar/cache miss" $ ppr ctev
-                    ; return (ctev, Fresh) } }
-
-emitNewDerivedEq :: CtLoc -> Pair TcType -> TcS ()
--- Create new Derived and put it in the work list
-emitNewDerivedEq loc (Pair ty1 ty2)
-  | ty1 `tcEqType` ty2   -- Quite common!
-  = return ()
-  | otherwise
-  = emitNewDerived loc (mkTcEqPred ty1 ty2)
-
-emitNewDerived :: CtLoc -> TcPredType -> TcS ()
--- Create new Derived and put it in the work list
-emitNewDerived loc pred
-  = do { mb_ev <- newDerived loc pred
-       ; case mb_ev of
-           Nothing -> return ()
-           Just ev -> do { traceTcS "Emitting [D]" (ppr ev)
-                         ; updWorkListTcS (extendWorkListCt (mkNonCanonical ev)) } }
-
-newDerived :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
--- Returns Nothing    if cached,
---         Just pred  if not cached
-newDerived loc pred
-  = do { mb_ct <- lookupInInerts loc pred
-       ; return (case mb_ct of
-                    Just {} -> Nothing
-                    Nothing -> Just (CtDerived { ctev_pred = pred, ctev_loc = loc })) }
-
-instDFunConstraints :: CtLoc -> TcThetaType -> TcS [(CtEvidence, Freshness)]
-instDFunConstraints loc = mapM (newWantedEvVar loc)
+isKindEquality :: TcPredType -> Bool
+-- See Note [Do not create Given kind equalities]
+isKindEquality pred = case classifyPredType pred of
+                        EqPred t1 _ -> isKind t1
+                        _           -> False
 
-{-
-Note [xCtEvidence]
-~~~~~~~~~~~~~~~~~~
-A call might look like this:
-
-    xCtEvidence ev evidence-transformer
-
-  ev is Given   => use ev_decomp to create new Givens for ev_preds,
-                   and return them
-
-  ev is Wanted  => create new wanteds for ev_preds,
-                   use ev_comp to bind ev,
-                   return fresh wanteds (ie ones not cached in inert_cans or solved)
-
-  ev is Derived => create new deriveds for ev_preds
-                      (unless cached in inert_cans or solved)
-
-Note: The [CtEvidence] returned is a subset of the subgoal-preds passed in
-      Ones that are already cached are not returned
-
-Example
-    ev : Tree a b ~ Tree c d
-    xCtEvidence ev [a~c, b~d] (XEvTerm { ev_comp = \[c1 c2]. <Tree> c1 c2
-                                       , ev_decomp = \c. [nth 1 c, nth 2 c] })
-              (\fresh-goals.  stuff)
-
-Note [Bind new Givens immediately]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-For Givens we make new EvVars and bind them immediately. We don't worry
-about caching, but we don't expect complicated calculations among Givens.
-It is important to bind each given:
-      class (a~b) => C a b where ....
-      f :: C a b => ....
-Then in f's Givens we have g:(C a b) and the superclass sc(g,0):a~b.
-But that superclass selector can't (yet) appear in a coercion
-(see evTermCoercion), so the easy thing is to bind it to an Id.
-
-See Note [Coercion evidence terms] in TcEvidence.
-
-Note [Do not create Given kind equalities]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Do not create Given kind equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We do not want to create a Given kind equality like
 
    [G]  kv ~ k   -- kv is a skolem kind variable
@@ -1772,198 +1689,45 @@ as an Irreducible (see Note [Equalities with incompatible kinds] in
 TcCanonical), and will do no harm.
 -}
 
-xCtEvidence :: CtEvidence            -- Original evidence
-            -> XEvTerm               -- Instructions about how to manipulate evidence
-            -> TcS ()
-
-xCtEvidence (CtWanted { ctev_evar = evar, ctev_loc = loc })
-            (XEvTerm { ev_preds = ptys, ev_comp = comp_fn })
-  = do { new_evars <- mapM (newWantedEvVar loc) ptys
-       ; setEvBind evar (comp_fn (map (ctEvTerm . fst) new_evars))
-       ; emitWorkNC (freshGoals new_evars) }
-         -- Note the "NC": these are fresh goals, not necessarily canonical
-
-xCtEvidence (CtGiven { ctev_evtm = tm, ctev_loc = loc })
-            (XEvTerm { ev_preds = ptys, ev_decomp = decomp_fn })
-  = ASSERT( equalLength ptys (decomp_fn tm) )
-    do { given_evs <- mapM (newGivenEvVar loc) $    -- See Note [Bind new Givens immediately]
-                      filterOut bad_given_pred (ptys `zip` decomp_fn tm)
-       ; emitWorkNC given_evs }
-  where
-    -- See Note [Do not create Given kind equalities]
-    bad_given_pred (pred_ty, _)
-      | EqPred t1 _ <- classifyPredType pred_ty
-      = isKind t1
-      | otherwise
-      = False
-
-xCtEvidence (CtDerived { ctev_loc = loc })
-            (XEvTerm { ev_preds = ptys })
-  = mapM_ (emitNewDerived loc) ptys
-
------------------------------
-data StopOrContinue a
-  = ContinueWith a    -- The constraint was not solved, although it may have
-                      --   been rewritten
-
-  | Stop CtEvidence   -- The (rewritten) constraint was solved
-         SDoc         -- Tells how it was solved
-                      -- Any new sub-goals have been put on the work list
-
-instance Functor StopOrContinue where
-  fmap f (ContinueWith x) = ContinueWith (f x)
-  fmap _ (Stop ev s)      = Stop ev s
-
-instance Outputable a => Outputable (StopOrContinue a) where
-  ppr (Stop ev s)      = ptext (sLit "Stop") <> parens s <+> ppr ev
-  ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
-
-continueWith :: a -> TcS (StopOrContinue a)
-continueWith = return . ContinueWith
-
-stopWith :: CtEvidence -> String -> TcS (StopOrContinue a)
-stopWith ev s = return (Stop ev (text s))
-
-andWhenContinue :: TcS (StopOrContinue a)
-                -> (a -> TcS (StopOrContinue b))
-                -> TcS (StopOrContinue b)
-andWhenContinue tcs1 tcs2
-  = do { r <- tcs1
-       ; case r of
-           Stop ev s       -> return (Stop ev s)
-           ContinueWith ct -> tcs2 ct }
-
-rewriteEvidence :: CtEvidence   -- old evidence
-                -> TcPredType   -- new predicate
-                -> TcCoercion   -- Of type :: new predicate ~ <type of old evidence>
-                -> TcS (StopOrContinue CtEvidence)
--- Returns Just new_ev iff either (i)  'co' is reflexivity
---                             or (ii) 'co' is not reflexivity, and 'new_pred' not cached
--- In either case, there is nothing new to do with new_ev
-{-
-     rewriteEvidence old_ev new_pred co
-Main purpose: create new evidence for new_pred;
-              unless new_pred is cached already
-* Returns a new_ev : new_pred, with same wanted/given/derived flag as old_ev
-* If old_ev was wanted, create a binding for old_ev, in terms of new_ev
-* If old_ev was given, AND not cached, create a binding for new_ev, in terms of old_ev
-* Returns Nothing if new_ev is already cached
-
-        Old evidence    New predicate is               Return new evidence
-        flavour                                        of same flavor
-        -------------------------------------------------------------------
-        Wanted          Already solved or in inert     Nothing
-        or Derived      Not                            Just new_evidence
-
-        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 old_ev@(CtDerived { ctev_loc = loc }) new_pred _co
-  = -- If derived, don't even look at the coercion.
-    -- This is very important, DO NOT re-order the equations for
-    -- rewriteEvidence to put the isTcReflCo test first!
-    -- Why?  Because for *Derived* constraints, c, the coercion, which
-    -- was produced by flattening, may contain suspended calls to
-    -- (ctEvTerm c), which fails for Derived constraints.
-    -- (Getting this wrong caused Trac #7384.)
-    do { mb_ev <- newDerived loc new_pred
-       ; case mb_ev of
-           Just new_ev -> continueWith new_ev
-           Nothing     -> stopWith old_ev "Cached derived" }
+newWantedEvVarNC :: CtLoc -> TcPredType -> TcS CtEvidence
+-- Don't look up in the solved/inerts; we know it's not there
+newWantedEvVarNC loc pty
+  = do { new_ev <- newEvVar pty
+       ; return (CtWanted { ctev_pred = pty, ctev_evar = new_ev, ctev_loc = loc })}
 
-rewriteEvidence old_ev new_pred co
-  | isTcReflCo co -- See Note [Rewriting with Refl]
-  = return (ContinueWith (old_ev { ctev_pred = new_pred }))
+newWantedEvVar :: CtLoc -> TcPredType -> TcS (CtEvidence, Freshness)
+-- For anything except ClassPred, this is the same as newWantedEvVarNC
+newWantedEvVar loc pty
+  = do { mb_ct <- lookupInInerts loc pty
+       ; case mb_ct of
+            Just ctev | not (isDerived ctev)
+                      -> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
+                            ; return (ctev, Cached) }
+            _ -> do { ctev <- newWantedEvVarNC loc pty
+                    ; traceTcS "newWantedEvVar/cache miss" $ ppr ctev
+                    ; return (ctev, Fresh) } }
 
-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]
-       ; return (ContinueWith new_ev) }
-  where
-    new_tm = mkEvCast old_tm (mkTcSubCo (mkTcSymCo co))  -- mkEvCast optimises ReflCo
-
-rewriteEvidence ev@(CtWanted { ctev_evar = evar, ctev_loc = loc }) new_pred co
-  = do { (new_ev, freshness) <- newWantedEvVar loc new_pred
-       ; MASSERT( tcCoercionRole co == Nominal )
-       ; setEvBind evar (mkEvCast (ctEvTerm new_ev) (mkTcSubCo co))
-       ; case freshness of
-            Fresh  -> continueWith new_ev
-            Cached -> stopWith ev "Cached wanted" }
-
-
-rewriteEqEvidence :: CtEvidence         -- Old evidence :: olhs ~ orhs (not swapped)
-                                        --              or orhs ~ olhs (swapped)
-                  -> SwapFlag
-                  -> TcType -> TcType   -- New predicate  nlhs ~ nrhs
-                                        -- Should be zonked, because we use typeKind on nlhs/nrhs
-                  -> TcCoercion         -- lhs_co, of type :: nlhs ~ olhs
-                  -> TcCoercion         -- rhs_co, of type :: nrhs ~ orhs
-                  -> TcS (StopOrContinue CtEvidence)  -- Of type nlhs ~ nrhs
--- For (rewriteEqEvidence (Given g olhs orhs) False nlhs nrhs lhs_co rhs_co)
--- we generate
--- If not swapped
---      g1 : nlhs ~ nrhs = lhs_co ; g ; sym rhs_co
--- If 'swapped'
---      g1 : nlhs ~ nrhs = lhs_co ; Sym g ; sym rhs_co
---
--- For (Wanted w) we do the dual thing.
--- New  w1 : nlhs ~ nrhs
--- If not swapped
---      w : olhs ~ orhs = sym lhs_co ; w1 ; rhs_co
--- If swapped
---      w : orhs ~ olhs = sym rhs_co ; sym w1 ; lhs_co
---
--- It's all a form of rewwriteEvidence, specialised for equalities
-rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
-  | CtDerived { ctev_loc = loc } <- old_ev
-  = do { mb <- newDerived loc (mkTcEqPred nlhs nrhs)
-       ; case mb of
-           Just new_ev -> continueWith new_ev
-           Nothing     -> stopWith old_ev "Cached derived" }
-
-  | NotSwapped <- swapped
-  , isTcReflCo lhs_co      -- See Note [Rewriting with Refl]
-  , isTcReflCo rhs_co
-  = return (ContinueWith (old_ev { ctev_pred = new_pred }))
-
-  | CtGiven { ctev_evtm = old_tm , ctev_loc = loc } <- old_ev
-  = do { let new_tm = EvCoercion (lhs_co
-                                  `mkTcTransCo` maybeSym swapped (evTermCoercion old_tm)
-                                  `mkTcTransCo` mkTcSymCo rhs_co)
-       ; new_ev <- newGivenEvVar loc (new_pred, new_tm)  -- See Note [Bind new Givens immediately]
-       ; return (ContinueWith new_ev) }
-
-  | CtWanted { ctev_evar = evar, ctev_loc = loc } <- old_ev
-  = do { new_evar <- newWantedEvVarNC loc new_pred
-                     -- Not much point in seeking exact-match equality evidence
-       ; let co = maybeSym swapped $
-                  mkTcSymCo lhs_co
-                  `mkTcTransCo` ctEvCoercion new_evar
-                  `mkTcTransCo` rhs_co
-       ; setEvBind evar (EvCoercion co)
-       ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co])
-       ; return (ContinueWith new_evar) }
+emitNewDerived :: CtLoc -> TcPredType -> TcS ()
+-- Create new Derived and put it in the work list
+emitNewDerived loc pred
+  = do { mb_ev <- newDerived loc pred
+       ; case mb_ev of
+           Nothing -> return ()
+           Just ev -> do { traceTcS "Emitting [D]" (ppr ev)
+                         ; updWorkListTcS (extendWorkListCt (mkNonCanonical ev)) } }
 
-  | otherwise
-  = panic "rewriteEvidence"
-  where
-    new_pred = mkTcEqPred nlhs nrhs
+newDerived :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
+-- Returns Nothing    if cached,
+--         Just pred  if not cached
+newDerived loc pred
+  = do { mb_ct <- lookupInInerts loc pred
+       ; return (case mb_ct of
+                    Just {} -> Nothing
+                    Nothing -> Just (CtDerived { ctev_pred = pred, ctev_loc = loc })) }
+
+instDFunConstraints :: CtLoc -> TcThetaType -> TcS [(CtEvidence, Freshness)]
+instDFunConstraints loc = mapM (newWantedEvVar loc)
 
-maybeSym :: SwapFlag -> TcCoercion -> TcCoercion
-maybeSym IsSwapped  co = mkTcSymCo co
-maybeSym NotSwapped co = co
 
 matchFam :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType))
 -- Given (F tys) return (ty, co), where co :: F tys ~ ty
@@ -2053,3 +1817,4 @@ deferTcSForAllEq role loc (tvs1,body1) (tvs2,body2)
                          ; return (TcLetCo ev_binds new_co) }
 
         ; return $ EvCoercion (foldr mkTcForAllCo coe_inside skol_tvs) }
+