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, 239 insertions, 170 deletions

diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index fc5728cc81..428eba5d69 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -20,9 +20,11 @@ module GHC.Tc.Utils.Unify (
   buildImplicationFor, buildTvImplication, emitResidualTvConstraint,
 
   -- Various unifications
-  unifyType, unifyKind, unifyExpectedType,
-  uType, promoteTcType,
+  unifyType, unifyKind, unifyInvisibleType, unifyExpectedType,
+  unifyTypeAndEmit, promoteTcType,
   swapOverTyVars, touchabilityAndShapeTest,
+  UnifyEnv(..), updUEnvLoc, setUEnvRole,
+  uType,
 
   --------------------------------
   -- Holes
@@ -1145,7 +1147,7 @@ tcEqMult origin w_actual w_expected = do
   {
   -- Note that here we do not call to `submult`, so we check
   -- for strict equality.
-  ; coercion <- uType TypeLevel origin w_actual w_expected
+  ; coercion <- unifyTypeAndEmit TypeLevel origin w_actual w_expected
   ; return $ if isReflCo coercion then WpHole else WpMultCoercion coercion }
 
 
@@ -1711,18 +1713,30 @@ unifyType :: Maybe TypedThing  -- ^ If present, the thing that has type ty1
 -- Actual and expected types
 -- Returns a coercion : ty1 ~ ty2
 unifyType thing ty1 ty2
-  = uType TypeLevel origin ty1 ty2
+  = unifyTypeAndEmit TypeLevel origin ty1 ty2
   where
     origin = TypeEqOrigin { uo_actual   = ty1
                           , uo_expected = ty2
                           , uo_thing    = thing
                           , uo_visible  = True }
 
+unifyInvisibleType :: TcTauType -> TcTauType    -- ty1 (actual), ty2 (expected)
+                   -> TcM TcCoercionN           -- :: ty1 ~# ty2
+-- Actual and expected types
+-- Returns a coercion : ty1 ~ ty2
+unifyInvisibleType ty1 ty2
+  = unifyTypeAndEmit TypeLevel origin ty1 ty2
+  where
+    origin = TypeEqOrigin { uo_actual   = ty1
+                          , uo_expected = ty2
+                          , uo_thing    = Nothing
+                          , uo_visible  = False }  -- This is the "invisible" bit
+
 unifyTypeET :: TcTauType -> TcTauType -> TcM CoercionN
 -- Like unifyType, but swap expected and actual in error messages
 -- This is used when typechecking patterns
 unifyTypeET ty1 ty2
-  = uType TypeLevel origin ty1 ty2
+  = unifyTypeAndEmit TypeLevel origin ty1 ty2
   where
     origin = TypeEqOrigin { uo_actual   = ty2   -- NB swapped
                           , uo_expected = ty1   -- NB swapped
@@ -1732,13 +1746,28 @@ unifyTypeET ty1 ty2
 
 unifyKind :: Maybe TypedThing -> TcKind -> TcKind -> TcM CoercionN
 unifyKind mb_thing ty1 ty2
-  = uType KindLevel origin ty1 ty2
+  = unifyTypeAndEmit KindLevel origin ty1 ty2
   where
     origin = TypeEqOrigin { uo_actual   = ty1
                           , uo_expected = ty2
                           , uo_thing    = mb_thing
                           , uo_visible  = True }
 
+unifyTypeAndEmit :: TypeOrKind -> CtOrigin -> TcType -> TcType -> TcM CoercionN
+-- Make a ref-cell, unify, emit the collected constraints
+unifyTypeAndEmit t_or_k orig ty1 ty2
+  = do { ref <- newTcRef emptyBag
+       ; loc <- getCtLocM orig (Just t_or_k)
+       ; let env = UE { u_loc = loc, u_role = Nominal
+                      , u_rewriters = emptyRewriterSet  -- ToDo: check this
+                      , u_defer = ref, u_unified = Nothing }
+
+       -- The hard work happens here
+       ; co <- uType env ty1 ty2
+
+       ; cts <- readTcRef ref
+       ; unless (null cts) (emitSimples cts)
+       ; return co }
 
 {-
 %************************************************************************
@@ -1747,45 +1776,110 @@ unifyKind mb_thing ty1 ty2
 %*                                                                      *
 %************************************************************************
 
-uType is the heart of the unifier.
+Note [The eager unifier]
+~~~~~~~~~~~~~~~~~~~~~~~~
+The eager unifier, `uType`, is called by
+
+  * The constraint generator (e.g. in GHC.Tc.Gen.Expr),
+    via the wrappers `unifyType`, `unifyKind` etc
+
+  * The constraint solver (e.g. in GHC.Tc.Solver.Equality),
+    via `GHC.Tc.Solver.Monad.wrapUnifierTcS`.
+
+`uType` runs in the TcM monad, but it carries a UnifyEnv that tells it
+what to do when unifying a variable or deferring a constraint. Specifically,
+  * it collects deferred constraints in `u_defer`, and
+  * it records which unification variables it has unified in `u_unified`
+Then it is up to the wrappers (one for the constraint generator, one for
+the constraint solver) to deal with these collected sets.
+
+Although `uType` runs in the TcM monad for convenience, really it could
+operate just with the ability to
+  * write to the accumulators of deferred constraints
+    and unification variables in UnifyEnv.
+  * read and update existing unification variables
+  * zonk types befire unifying (`zonkTcType` in `uUnfilledVar`, and
+    `zonkTyCoVarKind` in `uUnfilledVar1`
+  * create fresh coercion holes (`newCoercionHole`)
+  * emit tracing info for debugging
+  * look at the ambient TcLevel: `getTcLevel`
+A job for the future.
 -}
 
+data UnifyEnv
+  = UE { u_role      :: Role
+       , u_loc       :: CtLoc
+       , u_rewriters :: RewriterSet
+
+         -- Deferred constraints
+       , u_defer     :: TcRef (Bag Ct)
+
+         -- Which variables are unified;
+         -- if Nothing, we don't care
+       , u_unified :: Maybe (TcRef [TcTyVar])
+    }
+
+setUEnvRole :: UnifyEnv -> Role -> UnifyEnv
+setUEnvRole uenv role = uenv { u_role = role }
+
+updUEnvLoc :: UnifyEnv -> (CtLoc -> CtLoc) -> UnifyEnv
+updUEnvLoc uenv@(UE { u_loc = loc }) upd = uenv { u_loc = upd loc }
+
+mkKindEnv :: UnifyEnv -> TcType -> TcType -> UnifyEnv
+-- Modify the UnifyEnv to be right for unifing
+-- the kinds of these two types
+mkKindEnv env@(UE { u_loc = ctloc }) ty1 ty2
+  = env { u_role = Nominal, u_loc = mkKindEqLoc ty1 ty2 ctloc }
+
 uType, uType_defer
-  :: TypeOrKind
-  -> CtOrigin
+  :: UnifyEnv
   -> TcType    -- ty1 is the *actual* type
   -> TcType    -- ty2 is the *expected* type
   -> TcM CoercionN
 
---------------
 -- It is always safe to defer unification to the main constraint solver
 -- See Note [Deferred unification]
---    ty1 is "actual"
---    ty2 is "expected"
-uType_defer t_or_k origin ty1 ty2
-  = do { co <- emitWantedEq origin t_or_k Nominal ty1 ty2
+uType_defer (UE { u_loc = loc, u_defer = ref
+                , u_role = role, u_rewriters = rewriters })
+            ty1 ty2  -- ty1 is "actual", ty2 is "expected"
+  = do { let pred_ty = mkPrimEqPredRole role ty1 ty2
+       ; hole <- newCoercionHole loc pred_ty
+       ; let ct = mkNonCanonical $
+                  CtWanted { ctev_pred      = pred_ty
+                           , ctev_dest      = HoleDest hole
+                           , ctev_loc       = loc
+                           , ctev_rewriters = rewriters }
+             co = HoleCo hole
+       ; updTcRef ref (`snocBag` ct)
+         -- snocBag: see Note [Work-list ordering] in GHC.Tc.Solver.Equality
 
        -- Error trace only
        -- NB. do *not* call mkErrInfo unless tracing is on,
        --     because it is hugely expensive (#5631)
-       ; whenDOptM Opt_D_dump_tc_trace $ do
-            { ctxt <- getErrCtxt
-            ; doc <- mkErrInfo emptyTidyEnv ctxt
-            ; traceTc "utype_defer" (vcat [ debugPprType ty1
+       ; whenDOptM Opt_D_dump_tc_trace $
+         do { ctxt <- getErrCtxt
+            ; doc  <- mkErrInfo emptyTidyEnv ctxt
+            ; traceTc "utype_defer" (vcat [ ppr role
+                                          , debugPprType ty1
                                           , debugPprType ty2
-                                          , pprCtOrigin origin
                                           , doc])
-            ; traceTc "utype_defer2" (ppr co)
-            }
+            ; traceTc "utype_defer2" (ppr co) }
+
        ; return co }
 
+
 --------------
-uType t_or_k origin orig_ty1 orig_ty2
+uType env@(UE { u_role = role }) orig_ty1 orig_ty2
+  | Phantom <- role
+  = do { kind_co <- uType (mkKindEnv env orig_ty1 orig_ty2)
+                          (typeKind orig_ty1) (typeKind orig_ty2)
+       ; return (mkPhantomCo kind_co orig_ty1 orig_ty2) }
+
+  | otherwise
   = do { tclvl <- getTcLevel
        ; traceTc "u_tys" $ vcat
               [ text "tclvl" <+> ppr tclvl
-              , sep [ ppr orig_ty1, text "~", ppr orig_ty2]
-              , pprCtOrigin origin]
+              , sep [ ppr orig_ty1, text "~" <> ppr role, ppr orig_ty2] ]
        ; co <- go orig_ty1 orig_ty2
        ; if isReflCo co
             then traceTc "u_tys yields no coercion" Outputable.empty
@@ -1800,12 +1894,12 @@ uType t_or_k origin orig_ty1 orig_ty2
      -- recognize (t |> co) ~ (t |> co), which is nice. Previously, we
      -- didn't do it this way, and then the unification above was deferred.
     go (CastTy t1 co1) t2
-      = do { co_tys <- uType t_or_k origin t1 t2
-           ; return (mkCoherenceLeftCo Nominal t1 co1 co_tys) }
+      = do { co_tys <- uType env t1 t2
+           ; return (mkCoherenceLeftCo role t1 co1 co_tys) }
 
     go t1 (CastTy t2 co2)
-      = do { co_tys <- uType t_or_k origin t1 t2
-           ; return (mkCoherenceRightCo Nominal t2 co2 co_tys) }
+      = do { co_tys <- uType env t1 t2
+           ; return (mkCoherenceRightCo role t2 co2 co_tys) }
 
         -- Variables; go for uUnfilledVar
         -- Note that we pass in *original* (before synonym expansion),
@@ -1815,19 +1909,20 @@ uType t_or_k origin orig_ty1 orig_ty2
       = do { lookup_res <- isFilledMetaTyVar_maybe tv1
            ; case lookup_res of
                Just ty1 -> do { traceTc "found filled tyvar" (ppr tv1 <+> text ":->" <+> ppr ty1)
-                                ; go ty1 ty2 }
-               Nothing  -> uUnfilledVar origin t_or_k NotSwapped tv1 ty2 }
+                              ; uType env ty1 orig_ty2 }
+               Nothing -> uUnfilledVar env NotSwapped tv1 ty2 }
+
     go ty1 (TyVarTy tv2)
       = do { lookup_res <- isFilledMetaTyVar_maybe tv2
            ; case lookup_res of
                Just ty2 -> do { traceTc "found filled tyvar" (ppr tv2 <+> text ":->" <+> ppr ty2)
-                              ; go ty1 ty2 }
-               Nothing  -> uUnfilledVar origin t_or_k IsSwapped tv2 ty1 }
+                              ; uType env orig_ty1 ty2 }
+               Nothing -> uUnfilledVar env IsSwapped tv2 ty1 }
 
       -- See Note [Expanding synonyms during unification]
     go ty1@(TyConApp tc1 []) (TyConApp tc2 [])
       | tc1 == tc2
-      = return $ mkNomReflCo ty1
+      = return $ mkReflCo role ty1
 
         -- See Note [Expanding synonyms during unification]
         --
@@ -1842,14 +1937,14 @@ uType t_or_k origin orig_ty1 orig_ty2
       | Just ty2' <- coreView ty2 = go ty1  ty2'
 
     -- Functions (t1 -> t2) just check the two parts
-    -- Do not attempt (c => t); just defer
     go (FunTy { ft_af = af1, ft_mult = w1, ft_arg = arg1, ft_res = res1 })
        (FunTy { ft_af = af2, ft_mult = w2, ft_arg = arg2, ft_res = res2 })
-      | isVisibleFunArg af1, af1 == af2
-      = do { co_l <- uType t_or_k origin arg1 arg2
-           ; co_r <- uType t_or_k origin res1 res2
-           ; co_w <- uType t_or_k origin w1 w2
-           ; return $ mkNakedFunCo1 Nominal af1 co_w co_l co_r }
+      | isVisibleFunArg af1  -- Do not attempt (c => t); just defer
+      , af1 == af2           -- Important!  See #21530
+      = do { co_w <- uType (env { u_role = funRole role SelMult }) w1   w2
+           ; co_l <- uType (env { u_role = funRole role SelArg })  arg1 arg2
+           ; co_r <- uType (env { u_role = funRole role SelRes })  res1 res2
+           ; return $ mkNakedFunCo role af1 co_w co_l co_r }
 
         -- Always defer if a type synonym family (type function)
         -- is involved.  (Data families behave rigidly.)
@@ -1861,41 +1956,40 @@ uType t_or_k origin orig_ty1 orig_ty2
     go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
       -- See Note [Mismatched type lists and application decomposition]
       | tc1 == tc2, equalLength tys1 tys2
-      = assertPpr (isGenerativeTyCon tc1 Nominal) (ppr tc1) $
-        do { cos <- zipWith3M (uType t_or_k) origins' tys1 tys2
-           ; return $ mkTyConAppCo Nominal tc1 cos }
-      where
-        origins' = map (\is_vis -> if is_vis then origin else toInvisibleOrigin origin)
-                       (tcTyConVisibilities tc1)
+      , isInjectiveTyCon tc1 role -- don't look under newtypes at Rep equality
+      = assertPpr (isGenerativeTyCon tc1 role) (ppr tc1) $
+        do { traceTc "go-tycon" (ppr tc1 $$ ppr tys1 $$ ppr tys2 $$ ppr (take 10 (tyConRoleListX role tc1)))
+           ; cos <- zipWith4M u_tc_arg (tyConVisibilities tc1)   -- Infinite
+                                       (tyConRoleListX role tc1) -- Infinite
+                                       tys1 tys2
+           ; return $ mkTyConAppCo role tc1 cos }
 
     go (LitTy m) ty@(LitTy n)
       | m == n
-      = return $ mkNomReflCo ty
+      = return $ mkReflCo role ty
 
         -- See Note [Care with type applications]
         -- Do not decompose FunTy against App;
         -- it's often a type error, so leave it for the constraint solver
-    go (AppTy s1 t1) (AppTy s2 t2)
-      = go_app (isNextArgVisible s1) s1 t1 s2 t2
+    go ty1@(AppTy s1 t1) ty2@(AppTy s2 t2)
+      = go_app (isNextArgVisible s1) ty1 s1 t1 ty2 s2 t2
 
-    go (AppTy s1 t1) (TyConApp tc2 ts2)
+    go ty1@(AppTy s1 t1) ty2@(TyConApp tc2 ts2)
       | Just (ts2', t2') <- snocView ts2
       = assert (not (tyConMustBeSaturated tc2)) $
-        go_app (isNextTyConArgVisible tc2 ts2') s1 t1 (TyConApp tc2 ts2') t2'
+        go_app (isNextTyConArgVisible tc2 ts2')
+               ty1 s1 t1 ty2 (TyConApp tc2 ts2') t2'
 
-    go (TyConApp tc1 ts1) (AppTy s2 t2)
+    go ty1@(TyConApp tc1 ts1) ty2@(AppTy s2 t2)
       | Just (ts1', t1') <- snocView ts1
       = assert (not (tyConMustBeSaturated tc1)) $
-        go_app (isNextTyConArgVisible tc1 ts1') (TyConApp tc1 ts1') t1' s2 t2
+        go_app (isNextTyConArgVisible tc1 ts1')
+               ty1 (TyConApp tc1 ts1') t1' ty2 s2 t2
 
-    go (CoercionTy co1) (CoercionTy co2)
-      = do { let ty1 = coercionType co1
-                 ty2 = coercionType co2
-           ; kco <- uType KindLevel
-                          (KindEqOrigin orig_ty1 orig_ty2 origin
-                                        (Just t_or_k))
-                          ty1 ty2
-           ; return $ mkProofIrrelCo Nominal kco co1 co2 }
+    go ty1@(CoercionTy co1) ty2@(CoercionTy co2)
+      = do { kco <- uType (mkKindEnv env ty1 ty2)
+                          (coercionType co1) (coercionType co2)
+           ; return $ mkProofIrrelCo role kco co1 co2 }
 
         -- Anything else fails
         -- E.g. unifying for-all types, which is relative unusual
@@ -1903,17 +1997,33 @@ uType t_or_k origin orig_ty1 orig_ty2
 
     ------------------
     defer ty1 ty2   -- See Note [Check for equality before deferring]
-      | ty1 `tcEqType` ty2 = return (mkNomReflCo ty1)
-      | otherwise          = uType_defer t_or_k origin ty1 ty2
+      | ty1 `tcEqType` ty2 = return (mkReflCo role ty1)
+      | otherwise          = uType_defer env orig_ty1 orig_ty2
+
 
     ------------------
-    go_app vis s1 t1 s2 t2
-      = do { co_s <- uType t_or_k origin s1 s2
-           ; let arg_origin
-                   | vis       = origin
-                   | otherwise = toInvisibleOrigin origin
-           ; co_t <- uType t_or_k arg_origin t1 t2
+    u_tc_arg is_vis role ty1 ty2
+      = do { traceTc "u_tc_arg" (ppr role $$ ppr ty1 $$ ppr ty2)
+           ; uType env_arg ty1 ty2 }
+      where
+        env_arg = env { u_loc = adjustCtLoc is_vis False (u_loc env)
+                      , u_role = role }
+
+    ------------------
+    -- For AppTy, decompose only nominal equalities
+    -- See Note [Decomposing AppTy equalities] in GHC.Tc.Solver.Equality
+    go_app vis ty1 s1 t1 ty2 s2 t2
+      | Nominal <- role
+      = -- Unify arguments t1/t2 before function s1/s2, because
+        -- the former have smaller kinds, and hence simpler error messages
+        -- c.f. GHC.Tc.Solver.Equality.can_eq_app
+        -- Example: test T8603
+        do { let env_arg = env { u_loc = adjustCtLoc vis False (u_loc env) }
+           ; co_t <- uType env_arg t1 t2
+           ; co_s <- uType env s1 s2
            ; return $ mkAppCo co_s co_t }
+      | otherwise
+      = defer ty1 ty2
 
 {- Note [Check for equality before deferring]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2009,38 +2119,35 @@ back into @uTys@ if it turns out that the variable is already bound.
 -}
 
 ----------
-uUnfilledVar :: CtOrigin
-             -> TypeOrKind
-             -> SwapFlag
-             -> TcTyVar        -- Tyvar 1: not necessarily a meta-tyvar
-                               --    definitely not a /filled/ meta-tyvar
-             -> TcTauType      -- Type 2
-             -> TcM Coercion
+uUnfilledVar, uUnfilledVar1
+    :: UnifyEnv
+    -> SwapFlag
+    -> TcTyVar        -- Tyvar 1: not necessarily a meta-tyvar
+                      --    definitely not a /filled/ meta-tyvar
+    -> TcTauType      -- Type 2
+    -> TcM CoercionN
 -- "Unfilled" means that the variable is definitely not a filled-in meta tyvar
 --            It might be a skolem, or untouchable, or meta
-
-uUnfilledVar origin t_or_k swapped tv1 ty2
-  = do { ty2 <- zonkTcType ty2
-             -- Zonk to expose things to the
-             -- occurs check, and so that if ty2
-             -- looks like a type variable then it
-             -- /is/ a type variable
-       ; uUnfilledVar1 origin t_or_k swapped tv1 ty2 }
-
-----------
-uUnfilledVar1 :: CtOrigin
-              -> TypeOrKind
-              -> SwapFlag
-              -> TcTyVar        -- Tyvar 1: not necessarily a meta-tyvar
-                                --    definitely not a /filled/ meta-tyvar
-              -> TcTauType      -- Type 2, zonked
-              -> TcM Coercion
-uUnfilledVar1 origin t_or_k swapped tv1 ty2
+uUnfilledVar env swapped tv1 ty2
+  | Nominal <- u_role env
+  = do { ty2 <- zonkTcType ty2    -- Zonk to expose things to the occurs check, and so
+                                  -- that if ty2 looks like a type variable then it
+                                  -- /is/ a type variable
+       ; uUnfilledVar1 env swapped tv1 ty2 }
+
+  | otherwise  -- See Note [Do not unify representational equalities]
+               -- in GHC.Tc.Solver.Equality
+  = unSwap swapped (uType_defer env) (mkTyVarTy tv1) ty2
+
+uUnfilledVar1 env       -- Precondition: u_role==Nominal
+              swapped
+              tv1
+              ty2       -- ty2 is zonked
   | Just tv2 <- getTyVar_maybe ty2
   = go tv2
 
   | otherwise
-  = uUnfilledVar2 origin t_or_k swapped tv1 ty2
+  = uUnfilledVar2 env swapped tv1 ty2
 
   where
     -- 'go' handles the case where both are
@@ -2056,21 +2163,19 @@ uUnfilledVar1 origin t_or_k swapped tv1 ty2
                      -- not have happened yet, and it's an invariant of
                      -- uUnfilledTyVar2 that ty2 is fully zonked
                      -- Omitting this caused #16902
-                ; uUnfilledVar2 origin t_or_k (flipSwap swapped)
-                           tv2 (mkTyVarTy tv1) }
+                ; uUnfilledVar2 env (flipSwap swapped) tv2 (mkTyVarTy tv1) }
 
            | otherwise
-           = uUnfilledVar2 origin t_or_k swapped tv1 ty2
+           = uUnfilledVar2 env swapped tv1 ty2
 
 ----------
-uUnfilledVar2 :: CtOrigin
-              -> TypeOrKind
+uUnfilledVar2 :: UnifyEnv       -- Precondition: u_role==Nominal
               -> SwapFlag
               -> TcTyVar        -- Tyvar 1: not necessarily a meta-tyvar
                                 --    definitely not a /filled/ meta-tyvar
               -> TcTauType      -- Type 2, zonked
-              -> TcM Coercion
-uUnfilledVar2 origin t_or_k swapped tv1 ty2
+              -> TcM CoercionN
+uUnfilledVar2 env@(UE { u_defer = def_eq_ref }) swapped tv1 ty2
   = do { cur_lvl <- getTcLevel
            -- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles
            -- Here we don't know about given equalities here; so we treat
@@ -2079,7 +2184,10 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
                  && simpleUnifyCheck False tv1 ty2)
          then not_ok_so_defer
          else
-    do { co_k <- uType KindLevel kind_origin (typeKind ty2) (tyVarKind tv1)
+    do { def_eqs <- readTcRef def_eq_ref  -- Capture current state of def_eqs
+
+       -- Attempt to unify kinds
+       ; co_k <- uType (mkKindEnv env ty1 ty2) (typeKind ty2) (tyVarKind tv1)
        ; traceTc "uUnfilledVar2 ok" $
          vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
               , ppr ty2 <+> dcolon <+> ppr (typeKind  ty2)
@@ -2090,17 +2198,22 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
            -- NB: tv1 should still be unfilled, despite the kind unification
            --     because tv1 is not free in ty2' (or, hence, in its kind)
          then do { writeMetaTyVar tv1 ty2
-                 ; return (mkNomReflCo ty2) }
-
-         else defer  -- This cannot be solved now.  See GHC.Tc.Solver.Canonical
-                     -- Note [Equalities with incompatible kinds] for how
-                     -- this will be dealt with in the solver
+                 ; case u_unified env of
+                     Nothing -> return ()
+                     Just uref -> updTcRef uref (tv1 :)
+                 ; return (mkNomReflCo ty2) }  -- Unification is always Nominal
+
+         else -- The kinds don't match yet, so give up defer instead.
+              do { writeTcRef def_eq_ref def_eqs
+                     -- Since we are discarding co_k, also discard any constraints
+                     -- emitted by kind unification; they are just useless clutter.
+                     -- Do this dicarding by simply restoring the previous state
+                     -- of def_eqs; a bit imperative/yukky but works fine.
+                 ; defer }
          }}
   where
     ty1 = mkTyVarTy tv1
-    kind_origin = KindEqOrigin ty1 ty2 origin (Just t_or_k)
-
-    defer = unSwap swapped (uType_defer t_or_k origin) ty1 ty2
+    defer = unSwap swapped (uType_defer env) ty1 ty2
 
     not_ok_so_defer =
       do { traceTc "uUnfilledVar2 not ok" (ppr tv1 $$ ppr ty2)
@@ -2219,18 +2332,10 @@ There are five reasons not to unify:
 5. (COERCION-HOLE) Confusing coercion holes
    Suppose our equality is
      (alpha :: k) ~ (Int |> {co})
-   where co :: Type ~ k is an unsolved wanted. Note that this
-   equality is homogeneous; both sides have kind k. Unifying here
-   is sensible, but it can lead to very confusing error messages.
-   It's very much like a Wanted rewriting a Wanted. Even worse,
-   unifying a variable essentially turns an equality into a Given,
-   and so we could not use the tracking mechanism in
-   Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint.
-   We thus simply do not unify in this case.
-
-   This is expanded as Wrinkle (2) in Note [Equalities with incompatible kinds]
-   in GHC.Tc.Solver.Equality
-
+   where co :: Type ~ k is an unsolved wanted. Note that this equality
+   is homogeneous; both sides have kind k. We refrain from unifying here, because
+   of the coercion hole in the RHS -- see Wrinkle (EIK2) in
+   Note [Equalities with incompatible kinds] in GHC.Solver.Equality.
 
 Needless to say, all there are wrinkles:
 
@@ -2500,7 +2605,7 @@ matchExpectedFunKind hs_ty n k = go n k
     go n (FunTy { ft_af = af, ft_mult = w, ft_arg = arg, ft_res = res })
       | isVisibleFunArg af
       = do { co <- go (n-1) res
-           ; return (mkNakedFunCo1 Nominal af (mkNomReflCo w) (mkNomReflCo arg) co) }
+           ; return (mkNakedFunCo Nominal af (mkNomReflCo w) (mkNomReflCo arg) co) }
 
     go n other
      = defer n other
@@ -2514,7 +2619,7 @@ matchExpectedFunKind hs_ty n k = go n k
                                         , uo_thing    = Just hs_ty
                                         , uo_visible  = True
                                         }
-           ; uType KindLevel origin k new_fun }
+           ; unifyTypeAndEmit KindLevel origin k new_fun }
 
 {- *********************************************************************
 *                                                                      *
@@ -2523,40 +2628,6 @@ matchExpectedFunKind hs_ty n k = go n k
 *                                                                      *
 ********************************************************************* -}
 
-{- Commented out because I think we can just use the simple,
-   efficient simpleUnifyCheck instead; we can always defer.
-
-uTypeCheckTouchableTyVarEq :: TcTyVar -> TcType -> TcM (PuResult () TcType)
--- The check may expand type synonyms to avoid an occurs check,
--- so we must use the return type
---
--- Precondition: rhs is fully zonked
-uTypeCheckTouchableTyVarEq lhs_tv rhs
-  | simpleUnifyCheck False lhs_tv rhs  -- Do a fast-path check
-     -- False <=> See Note [Prevent unification with type families]
-  = return (pure rhs)
-
-  | otherwise
-  = do { traceTc "uTypeCheckTouchableTyVarEq {" (pprTyVar lhs_tv $$ ppr rhs)
-       ; check_result <- checkTyEqRhs flags rhs :: TcM (PuResult () Reduction)
-       ; traceTc "uTypeCheckTouchableTyVarEq }" (ppr check_result)
-       ; case check_result of
-            PuFail reason -> return (PuFail reason)
-            PuOK redn _   -> assertPpr (isReflCo (reductionCoercion redn))
-                                       (ppr lhs_tv $$ ppr rhs $$ ppr redn) $
-                             return (pure (reductionReducedType redn)) }
-  where
-    flags | MetaTv { mtv_info = tv_info, mtv_tclvl = tv_lvl } <- tcTyVarDetails lhs_tv
-          = TEF { tef_foralls  = isRuntimeUnkSkol lhs_tv
-                , tef_fam_app  = TEFA_Fail
-                , tef_unifying = Unifying tv_info tv_lvl LC_None
-                , tef_lhs      = TyVarLHS lhs_tv
-                , tef_occurs   = cteInsolubleOccurs }
-          | otherwise
-          = pprPanic "uTypeCheckTouchableTyVarEq" (ppr lhs_tv)
-          -- TEFA_Fail: See Note [Prevent unification with type families]
--}
-
 simpleUnifyCheck :: Bool -> TcTyVar -> TcType -> Bool
 -- A fast check: True <=> unification is OK
 -- If it says 'False' then unification might still be OK, but
@@ -2690,22 +2761,22 @@ reductionCoercion is Refl.  See `canEqCanLHSFinish_no_unification`.
 -}
 
 data PuResult a b = PuFail CheckTyEqResult
-                  | PuOK b (Bag a)
+                  | PuOK (Bag a) b
 
 instance Functor (PuResult a) where
   fmap _ (PuFail prob) = PuFail prob
-  fmap f (PuOK x cts)  = PuOK (f x) cts
+  fmap f (PuOK cts x)  = PuOK cts (f x)
 
 instance Applicative (PuResult a) where
-  pure x = PuOK x emptyBag
+  pure x = PuOK emptyBag x
   PuFail p1 <*> PuFail p2 = PuFail (p1 S.<> p2)
   PuFail p1 <*> PuOK {}   = PuFail p1
   PuOK {}   <*> PuFail p2 = PuFail p2
-  PuOK f c1 <*> PuOK x c2 = PuOK (f x) (c1 `unionBags` c2)
+  PuOK c1 f <*> PuOK c2 x = PuOK (c1 `unionBags` c2) (f x)
 
 instance (Outputable a, Outputable b) => Outputable (PuResult a b) where
   ppr (PuFail prob) = text "PuFail" <+> (ppr prob)
-  ppr (PuOK x cts)  = text "PuOK" <> braces
+  ppr (PuOK cts x)  = text "PuOK" <> braces
                         (vcat [ text "redn:" <+> ppr x
                               , text "cts:" <+> ppr cts ])
 
@@ -2715,7 +2786,7 @@ pprPur (PuFail prob) = text "PuFail:" <> ppr prob
 pprPur (PuOK {})     = text "PuOK"
 
 okCheckRefl :: TcType -> TcM (PuResult a Reduction)
-okCheckRefl ty = return (PuOK (mkReflRedn Nominal ty) emptyBag)
+okCheckRefl ty = return (PuOK emptyBag (mkReflRedn Nominal ty))
 
 failCheckWith :: CheckTyEqResult -> TcM (PuResult a b)
 failCheckWith p = return (PuFail p)
@@ -2851,15 +2922,14 @@ checkTyEqRhs flags ty
 checkCo :: TyEqFlags a -> Coercion -> TcM (PuResult a Coercion)
 -- See Note [checkCo]
 checkCo (TEF { tef_lhs = TyFamLHS {} }) co
-  = return (PuOK co emptyBag)
+  = return (pure co)
 
 checkCo (TEF { tef_lhs = TyVarLHS lhs_tv
              , tef_unifying = unifying
              , tef_occurs = occ_prob }) co
   -- Check for coercion holes, if unifying
   -- See (COERCION-HOLE) in Note [Unification preconditions]
-  | Unifying {} <- unifying
-  , hasCoercionHoleCo co
+  | hasCoercionHoleCo co
   = failCheckWith (cteProblem cteCoercionHole)
 
   -- Occurs check (can promote)
@@ -2874,7 +2944,7 @@ checkCo (TEF { tef_lhs = TyVarLHS lhs_tv
   = failCheckWith (cteProblem occ_prob)
 
   | otherwise
-  = return (PuOK co emptyBag)
+  = return (pure co)
 
 {- Note [checkCo]
 ~~~~~~~~~~~~~~~~~
@@ -3058,7 +3128,7 @@ checkFamApp flags@(TEF { tef_unifying = unifying, tef_occurs = occ_prob
       TEFA_Break breaker    -- Recurse; and break if there is a problem
         -> do { tys_res <- mapCheck (checkTyEqRhs arg_flags) tys
               ; case tys_res of
-                  PuOK redns cts -> return (PuOK (mkTyConAppRedn Nominal tc redns) cts)
+                  PuOK cts redns -> return (PuOK cts (mkTyConAppRedn Nominal tc redns))
                   PuFail {}      -> breaker fam_app }
   where
     arg_flags = famAppArgFlags flags
@@ -3228,4 +3298,3 @@ checkTopShape info xi
                         _                             -> False
       CycleBreakerTv -> False  -- We never unify these
       _ -> True
-