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

8 files changed, 73 insertions, 58 deletions

diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs
index 9ffcabd3a3..21d537112e 100644
--- a/compiler/GHC/Core/Coercion.hs
+++ b/compiler/GHC/Core/Coercion.hs
@@ -39,8 +39,8 @@ module GHC.Core.Coercion (
         mkSymCo, mkTransCo,
         mkSelCo, getNthFun, getNthFromType, mkLRCo,
         mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo,
-        mkFunCo1, mkFunCo2, mkFunCoNoFTF, mkFunResCo,
-        mkNakedFunCo1, mkNakedFunCo2,
+        mkFunCo, mkFunCo2, mkFunCoNoFTF, mkFunResCo,
+        mkNakedFunCo,
         mkForAllCo, mkForAllCos, mkHomoForAllCos,
         mkPhantomCo,
         mkHoleCo, mkUnivCo, mkSubCo,
@@ -51,7 +51,7 @@ module GHC.Core.Coercion (
         castCoercionKind, castCoercionKind1, castCoercionKind2,
 
         mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
-        mkHeteroPrimEqPred, mkHeteroReprPrimEqPred,
+        mkNomPrimEqPred,
 
         -- ** Decomposition
         instNewTyCon_maybe,
@@ -811,29 +811,20 @@ mkFunCoNoFTF r w arg_co res_co
 -- or @(a => x) ~ (b => y)@, depending on the kind of @a@/@b@.
 -- This (most common) version takes a single FunTyFlag, which is used
 --   for both fco_afl and ftf_afr of the FunCo
-mkFunCo1 :: HasDebugCallStack => Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
-mkFunCo1 r af w arg_co res_co
+mkFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
+mkFunCo r af w arg_co res_co
   = mkFunCo2 r af af w arg_co res_co
 
-mkNakedFunCo1 :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
--- This version of mkFunCo1 does not check FunCo invariants (checkFunCo)
--- It is called during typechecking on un-zonked types;
--- in particular there may be un-zonked coercion variables.
-mkNakedFunCo1 r af w arg_co res_co
-  = mkNakedFunCo2 r af af w arg_co res_co
+mkNakedFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
+-- This version of mkFunCo does not check FunCo invariants (checkFunCo)
+-- It's a historical vestige; See Note [No assertion check on mkFunCo]
+mkNakedFunCo = mkFunCo
 
-mkFunCo2 :: HasDebugCallStack => Role -> FunTyFlag -> FunTyFlag
-                              -> CoercionN -> Coercion -> Coercion -> Coercion
+mkFunCo2 :: Role -> FunTyFlag -> FunTyFlag
+         -> CoercionN -> Coercion -> Coercion -> Coercion
 -- This is the smart constructor for FunCo; it checks invariants
 mkFunCo2 r afl afr w arg_co res_co
-  = assertPprMaybe (checkFunCo r afl afr w arg_co res_co) $
-    mkNakedFunCo2 r afl afr w arg_co res_co
-
-mkNakedFunCo2 :: Role -> FunTyFlag -> FunTyFlag
-              -> CoercionN -> Coercion -> Coercion -> Coercion
--- This is the smart constructor for FunCo
--- "Naked"; it does not check invariants
-mkNakedFunCo2 r afl afr w arg_co res_co
+  -- See Note [No assertion check on mkFunCo]
   | Just (ty1, _) <- isReflCo_maybe arg_co
   , Just (ty2, _) <- isReflCo_maybe res_co
   , Just (w, _)   <- isReflCo_maybe w
@@ -844,6 +835,19 @@ mkNakedFunCo2 r afl afr w arg_co res_co
           , fco_mult = w, fco_arg = arg_co, fco_res = res_co }
 
 
+{- Note [No assertion check on mkFunCo]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We used to have a checkFunCo assertion on mkFunCo, but during typechecking
+we can (legitimately) have not-full-zonked types or coercion variables, so
+the assertion spuriously fails (test T11480b is a case in point).  Lint
+checks all these things anyway.
+
+We used to get around the problem by calling mkNakedFunCo from within the
+typechecker, which dodged the assertion check.  But then mkAppCo calls
+mkTyConAppCo, which calls tyConAppFunCo_maybe, which calls mkFunCo.
+Duplicating this stack of calls with "naked" versions of each seems too much.
+
+-- Commented out: see Note [No assertion check on mkFunCo]
 checkFunCo :: Role -> FunTyFlag -> FunTyFlag
            -> CoercionN -> Coercion -> Coercion
            -> Maybe SDoc
@@ -875,6 +879,7 @@ checkFunCo _r afl afr _w arg_co res_co
     ok ty = isTYPEorCONSTRAINT (typeKind ty)
     pp_ty str ty = text str <> colon <+> hang (ppr ty)
                                             2 (dcolon <+> ppr (typeKind ty))
+-}
 
 -- | Apply a 'Coercion' to another 'Coercion'.
 -- The second coercion must be Nominal, unless the first is Phantom.
@@ -2077,7 +2082,7 @@ ty_co_subst !lc role ty
                               liftCoSubstTyVar lc r tv
     go r (AppTy ty1 ty2)    = mkAppCo (go r ty1) (go Nominal ty2)
     go r (TyConApp tc tys)  = mkTyConAppCo r tc (zipWith go (tyConRoleListX r tc) tys)
-    go r (FunTy af w t1 t2) = mkFunCo1 r af (go Nominal w) (go r t1) (go r t2)
+    go r (FunTy af w t1 t2) = mkFunCo r af (go Nominal w) (go r t1) (go r t2)
     go r t@(ForAllTy (Bndr v _) ty)
        = let (lc', v', h) = liftCoSubstVarBndr lc v
              body_co = ty_co_subst lc' r ty in
@@ -2606,7 +2611,8 @@ mkCoercionType Phantom          = \ty1 ty2 ->
   in
   TyConApp eqPhantPrimTyCon [ki1, ki2, ty1, ty2]
 
--- | Creates a primitive type equality predicate.
+-- | Creates a primitive nominal type equality predicate.
+--      t1 ~# t2
 -- Invariant: the types are not Coercions
 mkPrimEqPred :: Type -> Type -> Type
 mkPrimEqPred ty1 ty2
@@ -2615,22 +2621,9 @@ mkPrimEqPred ty1 ty2
     k1 = typeKind ty1
     k2 = typeKind ty2
 
--- | Makes a lifted equality predicate at the given role
-mkPrimEqPredRole :: Role -> Type -> Type -> PredType
-mkPrimEqPredRole Nominal          = mkPrimEqPred
-mkPrimEqPredRole Representational = mkReprPrimEqPred
-mkPrimEqPredRole Phantom          = panic "mkPrimEqPredRole phantom"
-
--- | Creates a primitive type equality predicate with explicit kinds
-mkHeteroPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
-mkHeteroPrimEqPred k1 k2 ty1 ty2 = mkTyConApp eqPrimTyCon [k1, k2, ty1, ty2]
-
--- | Creates a primitive representational type equality predicate
--- with explicit kinds
-mkHeteroReprPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
-mkHeteroReprPrimEqPred k1 k2 ty1 ty2
-  = mkTyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
-
+-- | Creates a primitive representational type equality predicate.
+--      t1 ~R# t2
+-- Invariant: the types are not Coercions
 mkReprPrimEqPred :: Type -> Type -> Type
 mkReprPrimEqPred ty1  ty2
   = mkTyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
@@ -2638,6 +2631,17 @@ mkReprPrimEqPred ty1  ty2
     k1 = typeKind ty1
     k2 = typeKind ty2
 
+-- | Makes a lifted equality predicate at the given role
+mkPrimEqPredRole :: Role -> Type -> Type -> PredType
+mkPrimEqPredRole Nominal          = mkPrimEqPred
+mkPrimEqPredRole Representational = mkReprPrimEqPred
+mkPrimEqPredRole Phantom          = panic "mkPrimEqPredRole phantom"
+
+-- | Creates a primitive nominal type equality predicate with an explicit
+--   (but homogeneous) kind: (~#) k k ty1 ty2
+mkNomPrimEqPred :: Kind -> Type -> Type -> Type
+mkNomPrimEqPred k ty1 ty2 = mkTyConApp eqPrimTyCon [k, k, ty1, ty2]
+
 -- | Assuming that two types are the same, ignoring coercions, find
 -- a nominal coercion between the types. This is useful when optimizing
 -- transitivity over coercion applications, where splitting two
@@ -2668,7 +2672,7 @@ buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2
     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 })
       = assert (af1 == af2) $
-        mkFunCo1 Nominal af1 (go w1 w2) (go arg1 arg2) (go res1 res2)
+        mkFunCo Nominal af1 (go w1 w2) (go arg1 arg2) (go res1 res2)
 
     go (TyConApp tc1 args1) (TyConApp tc2 args2)
       = assert (tc1 == tc2) $
@@ -2749,15 +2753,17 @@ has_co_hole_co :: Coercion -> Monoid.Any
     folder = TyCoFolder { tcf_view  = noView
                         , tcf_tyvar = const2 (Monoid.Any False)
                         , tcf_covar = const2 (Monoid.Any False)
-                        , tcf_hole  = const2 (Monoid.Any True)
+                        , tcf_hole  = \_ hole -> Monoid.Any (isHeteroKindCoHole hole)
                         , tcf_tycobinder = const2
                         }
 
--- | Is there a coercion hole in this type?
+-- | Is there a hetero-kind coercion hole in this type?
+--   (That is, a coercion hole with ch_hetero_kind=True.)
+-- See wrinkle (EIK2) of Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality
 hasCoercionHoleTy :: Type -> Bool
 hasCoercionHoleTy = Monoid.getAny . has_co_hole_ty
 
--- | Is there a coercion hole in this coercion?
+-- | Is there a hetero-kind coercion hole in this coercion?
 hasCoercionHoleCo :: Coercion -> Bool
 hasCoercionHoleCo = Monoid.getAny . has_co_hole_co
 
diff --git a/compiler/GHC/Core/Coercion.hs-boot b/compiler/GHC/Core/Coercion.hs-boot
index 0d56cf628c..3143414feb 100644
--- a/compiler/GHC/Core/Coercion.hs-boot
+++ b/compiler/GHC/Core/Coercion.hs-boot
@@ -17,9 +17,9 @@ mkReflCo :: Role -> Type -> Coercion
 mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
 mkAppCo :: Coercion -> Coercion -> Coercion
 mkForAllCo :: TyCoVar -> Coercion -> Coercion -> Coercion
-mkFunCo1 :: HasDebugCallStack => Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
-mkNakedFunCo1 :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
-mkFunCo2 :: HasDebugCallStack => Role -> FunTyFlag -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
+mkFunCo      :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
+mkNakedFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
+mkFunCo2     :: Role -> FunTyFlag -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
 mkCoVarCo :: CoVar -> Coercion
 mkAxiomInstCo :: CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion
 mkPhantomCo :: Coercion -> Type -> Type -> Coercion
diff --git a/compiler/GHC/Core/Predicate.hs b/compiler/GHC/Core/Predicate.hs
index c8d280259a..2fc07e1be1 100644
--- a/compiler/GHC/Core/Predicate.hs
+++ b/compiler/GHC/Core/Predicate.hs
@@ -16,7 +16,7 @@ module GHC.Core.Predicate (
   getEqPredTys, getEqPredTys_maybe, getEqPredRole,
   predTypeEqRel,
   mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
-  mkHeteroPrimEqPred, mkHeteroReprPrimEqPred,
+  mkNomPrimEqPred,
 
   -- Class predicates
   mkClassPred, isDictTy, typeDeterminesValue,
diff --git a/compiler/GHC/Core/Reduction.hs b/compiler/GHC/Core/Reduction.hs
index 07d7a93748..a4f1df4f70 100644
--- a/compiler/GHC/Core/Reduction.hs
+++ b/compiler/GHC/Core/Reduction.hs
@@ -361,8 +361,8 @@ mkFunRedn r af
   (Reduction arg_co arg_ty)
   (Reduction res_co res_ty)
     = mkReduction
-        (mkFunCo1 r af w_co arg_co res_co)
-        (mkFunTy    af w_ty arg_ty res_ty)
+        (mkFunCo r af w_co arg_co res_co)
+        (mkFunTy   af w_ty arg_ty res_ty)
 {-# INLINE mkFunRedn #-}
 
 -- | Create a 'Reduction' associated to a Π type,
diff --git a/compiler/GHC/Core/TyCo/Compare.hs b/compiler/GHC/Core/TyCo/Compare.hs
index 4ef9d04eb8..9c32675d3e 100644
--- a/compiler/GHC/Core/TyCo/Compare.hs
+++ b/compiler/GHC/Core/TyCo/Compare.hs
@@ -379,7 +379,7 @@ We perform this optimisation in a number of places:
  * GHC.Core.Types.eqType
  * GHC.Core.Types.nonDetCmpType
  * GHC.Core.Unify.unify_ty
- * TcCanonical.can_eq_nc'
+ * GHC.Tc.Solver.Equality.can_eq_nc'
  * TcUnify.uType
 
 This optimisation is especially helpful for the ubiquitous GHC.Types.Type,
diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs
index 8417ded123..245a1c507b 100644
--- a/compiler/GHC/Core/TyCo/Rep.hs
+++ b/compiler/GHC/Core/TyCo/Rep.hs
@@ -38,7 +38,7 @@ module GHC.Core.TyCo.Rep (
         -- * Coercions
         Coercion(..), CoSel(..), FunSel(..),
         UnivCoProvenance(..),
-        CoercionHole(..), coHoleCoVar, setCoHoleCoVar,
+        CoercionHole(..), coHoleCoVar, setCoHoleCoVar, isHeteroKindCoHole,
         CoercionN, CoercionR, CoercionP, KindCoercion,
         MCoercion(..), MCoercionR, MCoercionN,
 
@@ -1454,12 +1454,20 @@ data CoercionHole
   = CoercionHole { ch_co_var  :: CoVar
                        -- See Note [CoercionHoles and coercion free variables]
 
-                 , ch_ref     :: IORef (Maybe Coercion)
+                 , ch_ref :: IORef (Maybe Coercion)
+
+                 , ch_hetero_kind :: Bool
+                       -- True <=> arises from a kind-level equality
+                       -- See Note [Equalities with incompatible kinds]
+                       --     in GHC.Tc.Solver.Equality, wrinkle (EIK2)
                  }
 
 coHoleCoVar :: CoercionHole -> CoVar
 coHoleCoVar = ch_co_var
 
+isHeteroKindCoHole :: CoercionHole -> Bool
+isHeteroKindCoHole = ch_hetero_kind
+
 setCoHoleCoVar :: CoercionHole -> CoVar -> CoercionHole
 setCoHoleCoVar h cv = h { ch_co_var = cv }
 
@@ -1470,7 +1478,8 @@ instance Data.Data CoercionHole where
   dataTypeOf _ = mkNoRepType "CoercionHole"
 
 instance Outputable CoercionHole where
-  ppr (CoercionHole { ch_co_var = cv }) = braces (ppr cv)
+  ppr (CoercionHole { ch_co_var = cv, ch_hetero_kind = hk })
+    = braces (ppr cv <> ppWhen hk (text "[hk]"))
 
 instance Uniquable CoercionHole where
   getUnique (CoercionHole { ch_co_var = cv }) = getUnique cv
diff --git a/compiler/GHC/Core/TyCo/Subst.hs b/compiler/GHC/Core/TyCo/Subst.hs
index ebf87dae94..4224bd127b 100644
--- a/compiler/GHC/Core/TyCo/Subst.hs
+++ b/compiler/GHC/Core/TyCo/Subst.hs
@@ -387,9 +387,9 @@ extendTvSubstWithClone :: Subst -> TyVar -> TyVar -> Subst
 --   those variables should be in scope already
 extendTvSubstWithClone (Subst in_scope idenv tenv cenv) tv tv'
   = Subst (extendInScopeSet in_scope tv')
-             idenv
-             (extendVarEnv tenv tv (mkTyVarTy tv'))
-             cenv
+          idenv
+          (extendVarEnv tenv tv (mkTyVarTy tv'))
+          cenv
 
 -- | Add a substitution from a 'CoVar' to a 'Coercion' to the 'Subst':
 -- you must ensure that the in-scope set satisfies
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 796fb5aecd..5e4be72a34 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -274,7 +274,7 @@ import {-# SOURCE #-} GHC.Core.Coercion
    , mkTyConAppCo, mkAppCo
    , mkForAllCo, mkFunCo2, mkAxiomInstCo, mkUnivCo
    , mkSymCo, mkTransCo, mkSelCo, mkLRCo, mkInstCo
-   , mkKindCo, mkSubCo, mkFunCo1
+   , mkKindCo, mkSubCo, mkFunCo
    , decomposePiCos, coercionKind
    , coercionRKind, coercionType
    , isReflexiveCo, seqCo
@@ -1332,7 +1332,7 @@ tyConAppFunCo_maybe :: HasDebugCallStack => Role -> TyCon -> [Coercion]
 -- ^ Return Just if this TyConAppCo should be represented as a FunCo
 tyConAppFunCo_maybe r tc cos
   | Just (af, mult, arg, res) <- ty_con_app_fun_maybe (mkReflCo r manyDataConTy) tc cos
-            = Just (mkFunCo1 r af mult arg res)
+            = Just (mkFunCo r af mult arg res)
   | otherwise = Nothing
 
 ty_con_app_fun_maybe :: (HasDebugCallStack, Outputable a) => a -> TyCon -> [a]