Use the eager unifier in the constraint solver

This patch continues the refactoring of the constraint solver
described in #23070.

The Big Deal in this patch is to call the regular, eager unifier from the
constraint solver, when we want to create new equalities. This
replaces the existing, unifyWanted which amounted to
yet-another-unifier, so it reduces duplication of a rather subtle
piece of technology. See

  * Note [The eager unifier] in GHC.Tc.Utils.Unify
  * GHC.Tc.Solver.Monad.wrapUnifierTcS

I did lots of other refactoring along the way

* I simplified the treatment of right hand sides that contain CoercionHoles.
  Now, a constraint that contains a hetero-kind CoercionHole is non-canonical,
  and cannot be used for rewriting or unification alike.  This required me
  to add the ch_hertero_kind flag to CoercionHole, with consequent knock-on
  effects. See wrinkle (2) of `Note [Equalities with incompatible kinds]` in
  GHC.Tc.Solver.Equality.

* I refactored the StopOrContinue type to add StartAgain, so that after a
  fundep improvement (for example) we can simply start the pipeline again.

* I got rid of the unpleasant (and inefficient) rewriterSetFromType/Co functions.
  With Richard I concluded that they are never needed.

* I discovered Wrinkle (W1) in Note [Wanteds rewrite Wanteds] in
  GHC.Tc.Types.Constraint, and therefore now prioritise non-rewritten equalities.

Quite a few error messages change, I think always for the better.

Compiler runtime stays about the same, with one outlier: a 17% improvement in T17836

Metric Decrease:
    T17836
    T18223

1 files changed, 225 insertions, 210 deletions

diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index befc9e212e..91e20becf8 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -33,6 +33,7 @@ module GHC.Tc.Solver.Monad (
 
     -- The pipeline
     StopOrContinue(..), continueWith, stopWith, andWhenContinue,
+    startAgainWith,
 
     -- Tracing etc
     panicTcS, traceTcS,
@@ -51,7 +52,7 @@ module GHC.Tc.Solver.Monad (
     unifyTyVar, reportUnifications, touchabilityAndShapeTest,
     setEvBind, setWantedEq,
     setWantedEvTerm, setEvBindIfWanted,
-    newEvVar, newGivenEvVar, newGivenEvVars,
+    newEvVar, newGivenEvVar, emitNewGivens,
     checkReductionDepth,
     getSolvedDicts, setSolvedDicts,
 
@@ -95,7 +96,7 @@ module GHC.Tc.Solver.Monad (
     instDFunType,
 
     -- Unification
-    unifyWanted, unifyWanteds,
+    wrapUnifierTcS, unifyFunDeps, uPairsTcM,
 
     -- MetaTyVars
     newFlexiTcSTy, instFlexiX,
@@ -159,6 +160,7 @@ import GHC.Builtin.Names ( unsatisfiableClassNameKey )
 import GHC.Core.Type
 import GHC.Core.TyCo.Rep as Rep
 import GHC.Core.Coercion
+import GHC.Core.Coercion.Axiom( TypeEqn )
 import GHC.Core.Predicate
 import GHC.Core.Reduction
 import GHC.Core.Class
@@ -171,6 +173,7 @@ import GHC.Types.Name.Reader
 import GHC.Types.Var
 import GHC.Types.Var.Set
 import GHC.Types.Unique.Supply
+import GHC.Types.Unique.Set( elementOfUniqSet )
 
 import GHC.Unit.Module ( HasModule, getModule, extractModule )
 import qualified GHC.Rename.Env as TcM
@@ -184,12 +187,11 @@ import GHC.Data.Bag as Bag
 import GHC.Data.Pair
 
 import GHC.Utils.Monad
-import GHC.Utils.Misc( equalLength )
 
 import GHC.Exts (oneShot)
 import Control.Monad
 import Data.IORef
-import Data.List ( mapAccumL, zip4 )
+import Data.List ( mapAccumL )
 import Data.Foldable
 import qualified Data.Semigroup as S
 
@@ -205,7 +207,10 @@ import GHC.Data.Graph.Directed
 ********************************************************************* -}
 
 data StopOrContinue a
-  = ContinueWith a    -- The constraint was not solved, although it may have
+  = StartAgain a      -- Constraint is not solved, but some unifications
+                      --   happened, so go back to the beginning of the pipeline
+
+  | ContinueWith a    -- The constraint was not solved, although it may have
                       --   been rewritten
 
   | Stop CtEvidence   -- The (rewritten) constraint was solved
@@ -216,21 +221,25 @@ data StopOrContinue a
 instance Outputable a => Outputable (StopOrContinue a) where
   ppr (Stop ev s)      = text "Stop" <> parens s <+> ppr ev
   ppr (ContinueWith w) = text "ContinueWith" <+> ppr w
+  ppr (StartAgain w)   = text "StartAgain" <+> ppr w
+
+startAgainWith :: a -> TcS (StopOrContinue a)
+startAgainWith ct = return (StartAgain ct)
 
 continueWith :: a -> TcS (StopOrContinue a)
-continueWith = return . ContinueWith
+continueWith ct = return (ContinueWith ct)
 
 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)
+                -> (a -> TcS (StopOrContinue a))
+                -> TcS (StopOrContinue a)
 andWhenContinue tcs1 tcs2
   = do { r <- tcs1
        ; case r of
-           Stop ev s       -> return (Stop ev s)
-           ContinueWith ct -> tcs2 ct }
+           ContinueWith ct -> tcs2 ct
+           _               -> return r }
 infixr 0 `andWhenContinue`    -- allow chaining with ($)
 
 
@@ -340,8 +349,9 @@ addInertCan ct =
 maybeKickOut :: InertCans -> Ct -> TcS InertCans
 -- For a CEqCan, kick out any inert that can be rewritten by the CEqCan
 maybeKickOut ics ct
-  | CEqCan (EqCt { eq_lhs = lhs, eq_ev = ev, eq_eq_rel = eq_rel }) <- ct
-  = do { (_, ics') <- kickOutRewritable (ctEvFlavour ev, eq_rel) lhs ics
+  | CEqCan eq_ct <- ct
+  = do { (_, ics') <- kickOutRewritable (KOAfterAdding (eqCtLHS eq_ct))
+                                        (eqCtFlavourRole eq_ct) ics
        ; return ics' }
 
      -- See [Kick out existing binding for implicit parameter]
@@ -368,61 +378,73 @@ maybeKickOut ics ct
   = return ics
 
 -----------------------------------------
-kickOutRewritable  :: CtFlavourRole  -- Flavour/role of the equality that
-                                      -- is being added to the inert set
-                   -> CanEqLHS        -- The new equality is lhs ~ ty
-                   -> InertCans
-                   -> TcS (Int, InertCans)
-kickOutRewritable new_fr new_lhs ics
-  = do { let (kicked_out, ics') = kickOutRewritableLHS new_fr new_lhs ics
-             n_kicked = workListSize kicked_out
+kickOutRewritable  :: KickOutSpec -> CtFlavourRole
+                   -> InertCans -> TcS (Int, InertCans)
+kickOutRewritable ko_spec new_fr ics
+  = do { let (kicked_out, ics') = kickOutRewritableLHS ko_spec new_fr ics
+             n_kicked = lengthBag kicked_out
 
-       ; unless (n_kicked == 0) $
-         do { updWorkListTcS (appendWorkList kicked_out)
+       ; unless (isEmptyBag kicked_out) $
+         do { emitWork kicked_out
 
               -- The famapp-cache contains Given evidence from the inert set.
               -- If we're kicking out Givens, we need to remove this evidence
               -- from the cache, too.
-            ; let kicked_given_ev_vars =
-                    [ ev_var | ct <- wl_eqs kicked_out
-                             , CtGiven { ctev_evar = ev_var } <- [ctEvidence ct] ]
+            ; let kicked_given_ev_vars = foldr add_one emptyVarSet kicked_out
+                  add_one :: Ct -> VarSet -> VarSet
+                  add_one ct vs | CtGiven { ctev_evar = ev_var } <- ctEvidence ct
+                                = vs `extendVarSet` ev_var
+                                | otherwise = vs
+
             ; when (new_fr `eqCanRewriteFR` (Given, NomEq) &&
                    -- if this isn't true, no use looking through the constraints
-                    not (null kicked_given_ev_vars)) $
+                    not (isEmptyVarSet kicked_given_ev_vars)) $
               do { traceTcS "Given(s) have been kicked out; drop from famapp-cache"
                             (ppr kicked_given_ev_vars)
-                 ; dropFromFamAppCache (mkVarSet kicked_given_ev_vars) }
+                 ; dropFromFamAppCache kicked_given_ev_vars }
 
             ; csTraceTcS $
-              hang (text "Kick out, lhs =" <+> ppr new_lhs)
+              hang (text "Kick out")
                  2 (vcat [ text "n-kicked =" <+> int n_kicked
                          , text "kicked_out =" <+> ppr kicked_out
                          , text "Residual inerts =" <+> ppr ics' ]) }
 
        ; return (n_kicked, ics') }
 
-kickOutAfterUnification :: TcTyVar -> TcS Int
-kickOutAfterUnification new_tv
+kickOutAfterUnification :: [TcTyVar] -> TcS Int
+kickOutAfterUnification tvs
+  | null tvs
+  = return 0
+  | otherwise
   = do { ics <- getInertCans
-       ; (n_kicked, ics2) <- kickOutRewritable (Given,NomEq)
-                                               (TyVarLHS new_tv) ics
-                     -- Given because the tv := xi is given; NomEq because
-                     -- only nominal equalities are solved by unification
-
+       ; let tv_set = mkVarSet tvs
+       ; (n_kicked, ics2) <- kickOutRewritable (KOAfterUnify tv_set)
+                                               (Given, NomEq) ics
+                              -- Given because the tv := xi is given; NomEq because
+                              -- only nominal equalities are solved by unification
        ; setInertCans ics2
+
+       -- Set the unification flag if we have done outer unifications
+       -- that might affect an earlier implication constraint
+       ; let min_tv_lvl = foldr1 minTcLevel (map tcTyVarLevel tvs)
+       ; ambient_lvl <- getTcLevel
+       ; when (ambient_lvl `strictlyDeeperThan` min_tv_lvl) $
+         setUnificationFlag min_tv_lvl
+
+       ; traceTcS "kickOutAfterUnification" (ppr tvs $$ text "n_kicked =" <+> ppr n_kicked)
        ; return n_kicked }
 
--- See Wrinkle (2) in Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical
+kickOutAfterFillingCoercionHole :: CoercionHole -> TcS ()
+-- See Wrinkle (EIK2) in Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical
 -- It's possible that this could just go ahead and unify, but could there be occurs-check
 -- problems? Seems simpler just to kick out.
-kickOutAfterFillingCoercionHole :: CoercionHole -> TcS ()
 kickOutAfterFillingCoercionHole hole
   = do { ics <- getInertCans
        ; let (kicked_out, ics') = kick_out ics
-             n_kicked           = workListSize kicked_out
+             n_kicked           = lengthBag kicked_out
 
        ; unless (n_kicked == 0) $
-         do { updWorkListTcS (appendWorkList kicked_out)
+         do { updWorkListTcS (extendWorkListCts kicked_out)
             ; csTraceTcS $
               hang (text "Kick out, hole =" <+> ppr hole)
                  2 (vcat [ text "n-kicked =" <+> int n_kicked
@@ -431,19 +453,26 @@ kickOutAfterFillingCoercionHole hole
 
        ; setInertCans ics' }
   where
-    kick_out :: InertCans -> (WorkList, InertCans)
-    kick_out ics@(IC { inert_eqs = eqs, inert_funeqs = funeqs })
-      = (kicked_out, ics { inert_eqs = eqs_to_keep, inert_funeqs = funeqs_to_keep })
+    kick_out :: InertCans -> (Cts, InertCans)
+    kick_out ics@(IC { inert_irreds = irreds })
+      = -- We only care about irreds here, because any constraint blocked
+        -- by a coercion hole is an irred.  See wrinkle (EIK2a) in
+        -- Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical
+        (irreds_to_kick, ics { inert_irreds = irreds_to_keep })
       where
-        (eqs_to_kick, eqs_to_keep)       = partitionInertEqs kick_ct eqs
-        (funeqs_to_kick, funeqs_to_keep) = partitionFunEqs kick_ct funeqs
-        kicked_out = extendWorkListCts (map CEqCan (eqs_to_kick ++ funeqs_to_kick)) emptyWorkList
+        (irreds_to_kick, irreds_to_keep) = partitionBag kick_ct irreds
 
-    kick_ct :: EqCt -> Bool
+    kick_ct :: Ct -> Bool
          -- True: kick out; False: keep.
-    kick_ct (EqCt { eq_rhs = rhs, eq_ev = ctev })
-      = isWanted ctev &&    -- optimisation: givens don't have coercion holes anyway
-        rhs `hasThisCoercionHoleTy` hole
+    kick_ct ct
+      | CIrredCan { cc_ev = ev, cc_reason = reason } <- ct
+      , CtWanted { ctev_rewriters = RewriterSet rewriters } <- ev
+      , NonCanonicalReason ctyeq <- reason
+      , ctyeq `cterHasProblem` cteCoercionHole
+      , hole `elementOfUniqSet` rewriters
+      = True
+      | otherwise
+      = False
 
 --------------
 addInertSafehask :: InertCans -> Ct -> InertCans
@@ -1258,12 +1287,21 @@ emitWorkNC evs
   | null evs
   = return ()
   | otherwise
-  = emitWork (map mkNonCanonical evs)
+  = emitWork (listToBag (map mkNonCanonical evs))
 
-emitWork :: [Ct] -> TcS ()
-emitWork [] = return ()   -- avoid printing, among other work
+emitWork :: Cts -> TcS ()
 emitWork cts
-  = do { traceTcS "Emitting fresh work" (vcat (map ppr cts))
+  | isEmptyBag cts    -- Avoid printing, among other work
+  = return ()
+  | otherwise
+  = do { traceTcS "Emitting fresh work" (pprBag cts)
+         -- Zonk the rewriter set of Wanteds, because that affects
+         -- the prioritisation of the work-list. Suppose a constraint
+         -- c1 is rewritten by another, c2.  When c2 gets solved,
+         -- c1 has no rewriters, and can be prioritised; see
+         -- Note [Prioritise Wanteds with empty RewriterSet]
+         -- in GHC.Tc.Types.Constraint wrinkle (WRW1)
+       ; cts <- wrapTcS $ mapBagM TcM.zonkCtRewriterSet cts
        ; updWorkListTcS (extendWorkListCts cts) }
 
 emitImplication :: Implication -> TcS ()
@@ -1553,7 +1591,7 @@ track of
   - Whether any unifications at all have taken place (Nothing => no unifications)
   - If so, what is the outermost level that has seen a unification (Just lvl)
 
-The iteration done in the simplify_loop/maybe_simplify_again loop in GHC.Tc.Solver.
+The iteration is done in the simplify_loop/maybe_simplify_again loop in GHC.Tc.Solver.
 
 It helpful not to iterate unless there is a chance of progress.  #8474 is
 an example:
@@ -1627,20 +1665,22 @@ cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
 cloneMetaTyVar tv = wrapTcS (TcM.cloneMetaTyVar tv)
 
 instFlexiX :: Subst -> [TKVar] -> TcS Subst
-instFlexiX subst tvs
-  = wrapTcS (foldlM instFlexiHelper subst tvs)
+instFlexiX subst tvs = wrapTcS (instFlexiXTcM subst tvs)
 
-instFlexiHelper :: Subst -> TKVar -> TcM Subst
+instFlexiXTcM :: Subst -> [TKVar] -> TcM Subst
 -- Makes fresh tyvar, extends the substitution, and the in-scope set
-instFlexiHelper subst tv
+-- Takes account of the case [k::Type, a::k, ...],
+-- where we must substitute for k in a's kind
+instFlexiXTcM subst []
+  = return subst
+instFlexiXTcM subst (tv:tvs)
   = do { uniq <- TcM.newUnique
        ; details <- TcM.newMetaDetails TauTv
        ; let name   = setNameUnique (tyVarName tv) uniq
              kind   = substTyUnchecked subst (tyVarKind tv)
              tv'    = mkTcTyVar name kind details
              subst' = extendTvSubstWithClone subst tv tv'
-       ; TcM.traceTc "instFlexi" (ppr tv')
-       ; return (extendTvSubst subst' tv (mkTyVarTy tv')) }
+       ; instFlexiXTcM subst' tvs  }
 
 matchGlobalInst :: DynFlags
                 -> Bool      -- True <=> caller is the short-cut solver
@@ -1761,14 +1801,19 @@ newBoundEvVarId pred rhs
        ; setEvBind (mkGivenEvBind new_ev rhs)
        ; return new_ev }
 
-newGivenEvVars :: CtLoc -> [(TcPredType, EvTerm)] -> TcS [CtEvidence]
-newGivenEvVars loc pts = mapM (newGivenEvVar loc) pts
+emitNewGivens :: CtLoc -> [(Role,TcType,TcType,TcCoercion)] -> TcS ()
+emitNewGivens loc pts
+  = do { evs <- mapM (newGivenEvVar loc) $
+                [ (mkPrimEqPredRole role ty1 ty2, evCoercion co)
+                | (role, ty1, ty2, co) <- pts
+                , not (ty1 `tcEqType` ty2) ] -- Kill reflexive Givens at birth
+       ; emitWorkNC evs }
 
 emitNewWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType -> TcS Coercion
 -- | Emit a new Wanted equality into the work-list
 emitNewWantedEq loc rewriters role ty1 ty2
   = do { (ev, co) <- newWantedEq loc rewriters role ty1 ty2
-       ; updWorkListTcS (extendWorkListEq (mkNonCanonical ev))
+       ; updWorkListTcS (extendWorkListEq rewriters (mkNonCanonical ev))
        ; return co }
 
 -- | Create a new Wanted constraint holding a coercion hole
@@ -1776,8 +1821,7 @@ emitNewWantedEq loc rewriters role ty1 ty2
 newWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType
             -> TcS (CtEvidence, Coercion)
 newWantedEq loc rewriters role ty1 ty2
-  = do { hole <- wrapTcS $ TcM.newCoercionHole pty
-       ; traceTcS "Emitting new coercion hole" (ppr hole <+> dcolon <+> ppr pty)
+  = do { hole <- wrapTcS $ TcM.newCoercionHole loc pty
        ; return ( CtWanted { ctev_pred      = pty
                            , ctev_dest      = HoleDest hole
                            , ctev_loc       = loc
@@ -1906,43 +1950,47 @@ solverDepthError loc ty
 ************************************************************************
 -}
 
-emitFunDepWanteds :: RewriterSet  -- from the work item
-                  -> [FunDepEqn (CtLoc, RewriterSet)] -> TcS ()
+emitFunDepWanteds :: CtEvidence  -- The work item
+                  -> [FunDepEqn (CtLoc, RewriterSet)]
+                  -> TcS Bool  -- True <=> some unification happened
 
-emitFunDepWanteds _ [] = return () -- common case noop
+emitFunDepWanteds _ [] = return False -- common case noop
 -- See Note [FunDep and implicit parameter reactions]
 
-emitFunDepWanteds work_rewriters fd_eqns
-  = mapM_ do_one_FDEqn fd_eqns
+emitFunDepWanteds ev fd_eqns
+  = unifyFunDeps ev Nominal do_fundeps
   where
-    do_one_FDEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = (loc, rewriters) })
-     | null tvs  -- Common shortcut
-     = do { traceTcS "emitFunDepWanteds 1" (ppr (ctl_depth loc) $$ ppr eqs $$ ppr (isGivenLoc loc))
-          ; mapM_ (\(Pair ty1 ty2) -> unifyWanted all_rewriters loc Nominal ty1 ty2)
-                  (reverse eqs) }
-             -- See Note [Reverse order of fundep equations]
-
-     | otherwise
-     = do { traceTcS "emitFunDepWanteds 2" (ppr (ctl_depth loc) $$ ppr tvs $$ ppr eqs)
-          ; subst <- instFlexiX emptySubst tvs  -- Takes account of kind substitution
-          ; mapM_ (do_one_eq loc all_rewriters subst) (reverse eqs) }
-               -- See Note [Reverse order of fundep equations]
-     where
-       all_rewriters = work_rewriters S.<> rewriters
-
-    do_one_eq loc rewriters subst (Pair ty1 ty2)
-       = unifyWanted rewriters loc Nominal (substTyUnchecked subst' ty1) ty2
-         -- ty2 does not mention fd_qtvs, so no need to subst it.
-         -- See GHC.Tc.Instance.Fundeps Note [Improving against instances]
-         --     Wrinkle (1)
+    do_fundeps :: UnifyEnv -> TcM ()
+    do_fundeps env = mapM_ (do_one env) fd_eqns
+
+    do_one :: UnifyEnv -> FunDepEqn (CtLoc, RewriterSet) -> TcM ()
+    do_one uenv (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = (loc, rewriters) })
+      = do { eqs' <- instantiate_eqs tvs (reverse eqs)
+                     -- (reverse eqs): See Note [Reverse order of fundep equations]
+           ; uPairsTcM env_one eqs' }
       where
-         subst' = extendSubstInScopeSet subst (tyCoVarsOfType ty1)
-         -- The free vars of ty1 aren't just fd_qtvs: ty1 is the result
-         -- of matching with the [W] constraint. So we add its free
-         -- vars to InScopeSet, to satisfy substTy's invariants, even
-         -- though ty1 will never (currently) be a poytype, so this
-         -- InScopeSet will never be looked at.
+        env_one = uenv { u_rewriters = u_rewriters uenv S.<> rewriters
+                       , u_loc       = loc }
 
+    instantiate_eqs :: [TyVar] -> [TypeEqn] -> TcM [TypeEqn]
+    instantiate_eqs tvs eqs
+      | null tvs
+      = return eqs
+      | otherwise
+      = do { TcM.traceTc "emitFunDepWanteds 2" (ppr tvs $$ ppr eqs)
+           ; subst <- instFlexiXTcM emptySubst tvs  -- Takes account of kind substitution
+           ; return [ Pair (substTyUnchecked subst' ty1) ty2
+                           -- ty2 does not mention fd_qtvs, so no need to subst it.
+                           -- See GHC.Tc.Instance.Fundeps Note [Improving against instances]
+                           --     Wrinkle (1)
+                    | Pair ty1 ty2 <- eqs
+                    , let subst' = extendSubstInScopeSet subst (tyCoVarsOfType ty1) ]
+                          -- The free vars of ty1 aren't just fd_qtvs: ty1 is the result
+                          -- of matching with the [W] constraint. So we add its free
+                          -- vars to InScopeSet, to satisfy substTy's invariants, even
+                          -- though ty1 will never (currently) be a poytype, so this
+                          -- InScopeSet will never be looked at.
+           }
 
 {-
 ************************************************************************
@@ -1951,121 +1999,86 @@ emitFunDepWanteds work_rewriters fd_eqns
 *                                                                      *
 ************************************************************************
 
-Note [unifyWanted]
-~~~~~~~~~~~~~~~~~~
+Note [wrapUnifierTcS]
+~~~~~~~~~~~~~~~~~~~
 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.
 
-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.
+Rather than making an equality test (which traverses the structure of the type,
+perhaps fruitlessly), we call uType (via wrapUnifierTcS) to traverse the common
+structure, and bales out when it finds a difference by creating a new deferred
+Wanted constraint.  But where it succeeds in finding common structure, it just
+builds a coercion to reflect it.
+
+This is all much faster than creating a new constraint, putting it in the
+work list, picking it out, canonicalising it, etc etc.
+
+Note [unifyFunDeps]
+~~~~~~~~~~~~~~~~~~~
+The Bool returned by `unifyFunDeps` is True if we have unified a variable
+that occurs in the constraint we are trying to solve; it is not in the
+inert set so `wrapUnifierTcS` won't kick it out.  Instead we want to send it
+back to the start of the pipeline.  Hence the Bool.
+
+It's vital that we don't return (not (null unified)) because the fundeps
+may create fresh variables; unifying them (alone) should not make us send
+the constraint back to the start, or we'll get an infinite loop.  See
+Note [Fundeps with instances, and equality orientation] in GHC.Tc.Solver.Dict
+and Note [Improvement orientation] in GHC.Tc.Solver.Equality.
 -}
 
-unifyWanted :: RewriterSet -> CtLoc
-            -> Role -> TcType -> TcType -> TcS Coercion
--- 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]
--- The returned coercion's role matches the input parameter
-unifyWanted rewriters loc Phantom ty1 ty2
-  = do { kind_co <- unifyWanted rewriters loc Nominal (typeKind ty1) (typeKind ty2)
-       ; return (mkPhantomCo kind_co ty1 ty2) }
-
-unifyWanted rewriters loc role orig_ty1 orig_ty2
-  = go orig_ty1 orig_ty2
-  where
-    go ty1 ty2 | Just ty1' <- coreView ty1 = go ty1' ty2
-    go ty1 ty2 | Just ty2' <- coreView ty2 = go ty1 ty2'
-
-    go (FunTy af1 w1 s1 t1) (FunTy af2 w2 s2 t2)
-      | af1 == af2    -- Important!  See #21530
-      = do { co_s <- unifyWanted rewriters loc role s1 s2
-           ; co_t <- unifyWanted rewriters loc role t1 t2
-           ; co_w <- unifyWanted rewriters loc Nominal w1 w2
-           ; return (mkNakedFunCo1 role af1 co_w co_s co_t) }
-
-    go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
-      | tc1 == tc2, tys1 `equalLength` tys2
-      , isInjectiveTyCon tc1 role -- don't look under newtypes at Rep equality
-      = do { cos <- zipWith3M (unifyWanted rewriters loc)
-                              (tyConRoleListX role tc1) tys1 tys2
-           ; return (mkTyConAppCo role tc1 cos) }
-
-    go ty1@(TyVarTy tv) ty2
-      = do { mb_ty <- isFilledMetaTyVar_maybe tv
-           ; case mb_ty of
-                Just ty1' -> go ty1' ty2
-                Nothing   -> bale_out ty1 ty2}
-    go ty1 ty2@(TyVarTy tv)
-      = do { mb_ty <- isFilledMetaTyVar_maybe tv
-           ; case mb_ty of
-                Just ty2' -> go ty1 ty2'
-                Nothing   -> bale_out ty1 ty2 }
-
-    go ty1@(CoercionTy {}) (CoercionTy {})
-      = return (mkReflCo role ty1) -- we just don't care about coercions!
-
-    go ty1 ty2 = bale_out ty1 ty2
-
-    bale_out ty1 ty2
-       | ty1 `tcEqType` ty2 = return (mkReflCo role ty1)
-        -- Check for equality; e.g. a ~ a, or (m a) ~ (m a)
-       | otherwise = emitNewWantedEq loc rewriters role orig_ty1 orig_ty2
-
-
-{-
-Note [Decomposing Dependent TyCons and Processing Wanted Equalities]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When we decompose a dependent tycon we obtain a list of
-mixed wanted type and kind equalities. Ideally we want
-all the kind equalities to get solved first so that we avoid
-generating duplicate kind equalities
-
-For example, consider decomposing a TyCon equality
+uPairsTcM :: UnifyEnv -> [TypeEqn] -> TcM ()
+uPairsTcM uenv eqns = mapM_ (\(Pair ty1 ty2) -> uType uenv ty1 ty2) eqns
 
-    (0) [W] T k_fresh (t1::k_fresh) ~ T k1 (t2::k_fresh)
-
-This gives rise to 2 equalities in the solver worklist
+unifyFunDeps :: CtEvidence -> Role
+             -> (UnifyEnv -> TcM ())
+             -> TcS Bool
+unifyFunDeps ev role do_unifications
+  = do { (_, _, unified) <- wrapUnifierTcS ev role do_unifications
+       ; return (any (`elemVarSet` fvs) unified) }
+         -- See Note [unifyFunDeps]
+  where
+    fvs = tyCoVarsOfType (ctEvPred ev)
+
+wrapUnifierTcS :: CtEvidence -> Role
+               -> (UnifyEnv -> TcM a)  -- Some calls to uType
+               -> TcS (a, Bag Ct, [TcTyVar])
+-- Invokes the do_unifications argument, with a suitable UnifyEnv.
+-- Emit deferred equalities and kick-out from the inert set as a
+-- result of any unifications.
+-- Very good short-cut when the two types are equal, or nearly so
+-- See Note [wrapUnifierTcS]
+--
+-- The [TcTyVar] is the list of unification variables that were
+-- unified the process; the (Bag Ct) are the deferred constraints.
 
-    (1) [W] k_fresh ~ k1
-    (2) [W] t1::k_fresh ~ t2::k1
+wrapUnifierTcS ev role do_unifications
+  = do { (cos, unified, rewriters, cts) <- wrapTcS $
+             do { defer_ref   <- TcM.newTcRef emptyBag
+                ; unified_ref <- TcM.newTcRef []
+                ; rewriters <- TcM.zonkRewriterSet (ctEvRewriters ev)
+                ; let env = UE { u_role      = role
+                               , u_rewriters = rewriters
+                               , u_loc       = ctEvLoc ev
+                               , u_defer     = defer_ref
+                               , u_unified   = Just unified_ref}
 
-The solver worklist is processed in LIFO order:
-see GHC.Tc.Solver.InertSet.selectWorkItem.
-i.e. (2) is processed _before_ (1). Now, while solving (2)
-we would call `canEqCanLHSHetero` and that would emit a
-wanted kind equality
+                ; cos <- do_unifications env
 
-    (3) [W] k_fresh ~ k1
+                ; cts     <- TcM.readTcRef defer_ref
+                ; unified <- TcM.readTcRef unified_ref
+                ; return (cos, unified, rewriters, cts) }
 
-But (3) is exactly the same as (1)!
+       -- Emit the deferred constraints
+       -- See Note [Work-list ordering] in GHC.Tc.Solved.Equality
+       ; unless (isEmptyBag cts) $
+         updWorkListTcS (extendWorkListEqs rewriters cts)
 
-To avoid such duplicate wanted constraints from being added to the worklist,
-we ensure that (2) is processed before (1). Since we are processing
-the worklist in a LIFO ordering, we do it by emitting (1) before (2).
-This is exactly what we do in `unifyWanteds`.
+       -- And kick out any inert constraint that we have unified
+       ; _ <- kickOutAfterUnification unified
 
-NB: This ordering is not needed when we decompose FunTyCons as they are not dependently typed
--}
+       ; return (cos, cts, unified) }
 
--- NB: Length of [CtLoc] and [Roles] may be infinite
--- but list of RHS [TcType] and LHS [TcType] is finite and both are of equal length
-unifyWanteds :: RewriterSet -> [CtLoc] -> [Role]
-             -> [TcType] -- List of RHS types
-             -> [TcType] -- List of LHS types
-             -> TcS [Coercion]
-unifyWanteds rewriters ctlocs roles rhss lhss = unify_wanteds rewriters $ zip4 ctlocs roles rhss lhss
-  where
-    -- Order is important here
-    -- See Note [Decomposing Dependent TyCons and Processing Wanted Equalities]
-    unify_wanteds _ [] = return []
-    unify_wanteds rewriters ((new_loc, tc_role, ty1, ty2) : rest)
-       = do { cos <- unify_wanteds rewriters rest
-            ; co  <- unifyWanted rewriters new_loc tc_role ty1 ty2
-            ; return (co:cos) }
 
 {-
 ************************************************************************
@@ -2081,7 +2094,7 @@ checkTouchableTyVarEq
    -> TcType     -- The RHS
    -> TcS (PuResult () Reduction)
 -- Used for Nominal, Wanted equalities, with a touchable meta-tyvar on LHS
--- If checkTouchableTyVarEq tv ty = PuOK redn cts
+-- If checkTouchableTyVarEq tv ty = PuOK cts redn
 --   then we can unify
 --       tv := ty |> redn
 --   with extra wanteds 'cts'
@@ -2098,7 +2111,7 @@ checkTouchableTyVarEq ev lhs_tv rhs
        ; traceTcS "checkTouchableTyVarEq }" (ppr lhs_tv $$ ppr check_result)
        ; case check_result of
             PuFail reason -> return (PuFail reason)
-            PuOK redn cts -> do { emitWork (bagToList cts)
+            PuOK cts redn -> do { emitWork cts
                                 ; return (pure redn) } }
 
   where
@@ -2147,13 +2160,13 @@ checkTouchableTyVarEq ev lhs_tv rhs
                 _ -> TcM.newMetaTyVarTyAtLevel lhs_tv_lvl fam_app_kind
 
            ; let pty = mkPrimEqPredRole Nominal fam_app new_tv_ty
-           ; hole <- TcM.newCoercionHole pty
+           ; hole <- TcM.newVanillaCoercionHole pty
            ; let new_ev = CtWanted { ctev_pred      = pty
                                    , ctev_dest      = HoleDest hole
                                    , ctev_loc       = cb_loc
                                    , ctev_rewriters = ctEvRewriters ev }
-           ; return (PuOK (mkReduction (HoleCo hole) new_tv_ty)
-                          (singleCt (mkNonCanonical new_ev))) } }
+           ; return (PuOK (singleCt (mkNonCanonical new_ev))
+                          (mkReduction (HoleCo hole) new_tv_ty)) } }
 
     -- See Detail (7) of the Note
     cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin
@@ -2171,8 +2184,8 @@ checkTypeEq ev eq_rel lhs rhs
        ; traceTcS "checkTypeEq }" (ppr check_result)
        ; case check_result of
             PuFail reason -> return (PuFail reason)
-            PuOK redn prs -> do { new_givens <- mapBagM mk_new_given prs
-                                ; emitWorkNC (bagToList new_givens)
+            PuOK prs redn -> do { new_givens <- mapBagM mk_new_given prs
+                                ; emitWork new_givens
                                 ; updInertTcS (addCycleBreakerBindings prs)
                                 ; return (pure redn) } }
 
@@ -2180,9 +2193,10 @@ checkTypeEq ev eq_rel lhs rhs
   = do { check_result <- wrapTcS (checkTyEqRhs wanted_flags rhs)
        ; case check_result of
             PuFail reason -> return (PuFail reason)
-            PuOK redn cts -> do { emitWork (bagToList cts)
+            PuOK cts redn -> do { emitWork cts
                                 ; return (pure redn) } }
   where
+    check_given_rhs :: TcType -> TcM (PuResult (TcTyVar,TcType) Reduction)
     check_given_rhs rhs
        -- See Note [Special case for top-level of Given equality]
        | Just (TyFamLHS tc tys) <- canTyFamEqLHS_maybe rhs
@@ -2192,6 +2206,7 @@ checkTypeEq ev eq_rel lhs rhs
 
     arg_flags = famAppArgFlags given_flags
 
+    given_flags :: TyEqFlags (TcTyVar,TcType)
     given_flags = TEF { tef_lhs      = lhs
                       , tef_foralls  = False
                       , tef_unifying = NotUnifying
@@ -2215,14 +2230,14 @@ checkTypeEq ev eq_rel lhs rhs
     break_given :: TcType -> TcM (PuResult (TcTyVar,TcType) Reduction)
     break_given fam_app
       = do { new_tv <- TcM.newCycleBreakerTyVar (typeKind fam_app)
-           ; return (PuOK (mkReflRedn Nominal (mkTyVarTy new_tv))
-                          (unitBag (new_tv, fam_app))) }
+           ; return (PuOK (unitBag (new_tv, fam_app))
+                          (mkReflRedn Nominal (mkTyVarTy new_tv))) }
                     -- Why reflexive? See Detail (4) of the Note
 
     ---------------------------
-    mk_new_given :: (TcTyVar, TcType) -> TcS CtEvidence
+    mk_new_given :: (TcTyVar, TcType) -> TcS Ct
     mk_new_given (new_tv, fam_app)
-      = newGivenEvVar cb_loc (given_pred, given_term)
+      = mkNonCanonical <$> newGivenEvVar cb_loc (given_pred, given_term)
       where
         new_ty     = mkTyVarTy new_tv
         given_pred = mkPrimEqPred fam_app new_ty