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, 62 insertions, 40 deletions

diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 873ff2979a..7db80cfccb 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -44,7 +44,8 @@ module GHC.Tc.Utils.TcMType (
   newTcEvBinds, newNoTcEvBinds, addTcEvBind,
   emitNewExprHole,
 
-  newCoercionHole, fillCoercionHole, isFilledCoercionHole,
+  newCoercionHole, newCoercionHoleO, newVanillaCoercionHole,
+  fillCoercionHole, isFilledCoercionHole,
   unpackCoercionHole, unpackCoercionHole_maybe,
   checkCoercionHole,
 
@@ -103,7 +104,7 @@ module GHC.Tc.Utils.TcMType (
 
   ------------------------------
   -- Other
-  anyUnfilledCoercionHoles
+  zonkRewriterSet, zonkCtRewriterSet, zonkCtEvRewriterSet
   ) where
 
 import GHC.Prelude
@@ -111,6 +112,7 @@ import GHC.Prelude
 import GHC.Driver.Session
 import qualified GHC.LanguageExtensions as LangExt
 
+import {-# SOURCE #-} GHC.Tc.Utils.Unify( unifyInvisibleType )
 import GHC.Tc.Types.Origin
 import GHC.Tc.Types.Constraint
 import GHC.Tc.Types.Evidence
@@ -198,7 +200,7 @@ newEvVar ty = do { name <- newSysName (predTypeOccName ty)
 newWantedWithLoc :: CtLoc -> PredType -> TcM CtEvidence
 newWantedWithLoc loc pty
   = do dst <- case classifyPredType pty of
-                EqPred {} -> HoleDest  <$> newCoercionHole pty
+                EqPred {} -> HoleDest  <$> newCoercionHole loc pty
                 _         -> EvVarDest <$> newEvVar pty
        return $ CtWanted { ctev_dest      = dst
                          , ctev_pred      = pty
@@ -223,9 +225,9 @@ newWanteds orig = mapM (newWanted orig Nothing)
 ----------------------------------------------
 
 cloneWantedCtEv :: CtEvidence -> TcM CtEvidence
-cloneWantedCtEv ctev@(CtWanted { ctev_pred = pty, ctev_dest = HoleDest _ })
+cloneWantedCtEv ctev@(CtWanted { ctev_pred = pty, ctev_dest = HoleDest _, ctev_loc = loc })
   | isEqPrimPred pty
-  = do { co_hole <- newCoercionHole pty
+  = do { co_hole <- newCoercionHole loc pty
        ; return (ctev { ctev_dest = HoleDest co_hole }) }
   | otherwise
   = pprPanic "cloneWantedCtEv" (ppr pty)
@@ -273,13 +275,13 @@ emitWantedEqs origin pairs
 -- | Emits a new equality constraint
 emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion
 emitWantedEq origin t_or_k role ty1 ty2
-  = do { hole <- newCoercionHole pty
-       ; loc <- getCtLocM origin (Just t_or_k)
+  = do { hole <- newCoercionHoleO origin pty
+       ; loc  <- getCtLocM origin (Just t_or_k)
        ; emitSimple $ mkNonCanonical $
-         CtWanted { ctev_pred = pty
-                  , ctev_dest = HoleDest hole
-                  , ctev_loc = loc
-                  , ctev_rewriters = rewriterSetFromTypes [ty1, ty2] }
+         CtWanted { ctev_pred      = pty
+                  , ctev_dest      = HoleDest hole
+                  , ctev_loc       = loc
+                  , ctev_rewriters = emptyRewriterSet }
        ; return (HoleCo hole) }
   where
     pty = mkPrimEqPredRole role ty1 ty2
@@ -290,8 +292,8 @@ emitWantedEvVar :: CtOrigin -> TcPredType -> TcM EvVar
 emitWantedEvVar origin ty
   = do { new_cv <- newEvVar ty
        ; loc <- getCtLocM origin Nothing
-       ; let ctev = CtWanted { ctev_dest      = EvVarDest new_cv
-                             , ctev_pred      = ty
+       ; let ctev = CtWanted { ctev_pred      = ty
+                             , ctev_dest      = EvVarDest new_cv
                              , ctev_loc       = loc
                              , ctev_rewriters = emptyRewriterSet }
        ; emitSimple $ mkNonCanonical ctev
@@ -353,12 +355,23 @@ newImplication
 ************************************************************************
 -}
 
-newCoercionHole :: TcPredType -> TcM CoercionHole
-newCoercionHole pred_ty
+newVanillaCoercionHole :: TcPredType -> TcM CoercionHole
+newVanillaCoercionHole = new_coercion_hole False
+
+newCoercionHole :: CtLoc -> TcPredType -> TcM CoercionHole
+newCoercionHole loc = newCoercionHoleO (ctLocOrigin loc)
+
+newCoercionHoleO :: CtOrigin -> TcPredType -> TcM CoercionHole
+newCoercionHoleO (KindEqOrigin {}) = new_coercion_hole True
+newCoercionHoleO _                 = new_coercion_hole False
+
+new_coercion_hole :: Bool -> TcPredType -> TcM CoercionHole
+new_coercion_hole hetero_kind pred_ty
   = do { co_var <- newEvVar pred_ty
        ; traceTc "New coercion hole:" (ppr co_var <+> dcolon <+> ppr pred_ty)
        ; ref <- newMutVar Nothing
-       ; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref } }
+       ; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref
+                               , ch_hetero_kind = hetero_kind } }
 
 -- | Put a value in a coercion hole
 fillCoercionHole :: CoercionHole -> Coercion -> TcM ()
@@ -621,12 +634,7 @@ ensureMonoType res_ty
   = return ()
   | otherwise
   = do { mono_ty <- newOpenFlexiTyVarTy
-       ; let eq_orig = TypeEqOrigin { uo_actual   = res_ty
-                                    , uo_expected = mono_ty
-                                    , uo_thing    = Nothing
-                                    , uo_visible  = False }
-
-       ; _co <- emitWantedEq eq_orig TypeLevel Nominal res_ty mono_ty
+       ; _co <- unifyInvisibleType res_ty mono_ty
        ; return () }
 
 promoteTcType :: TcLevel -> TcType -> TcM (TcCoercionN, TcType)
@@ -652,12 +660,7 @@ promoteTcType dest_lvl ty
                 -- where alpha and rr are fresh and from level dest_lvl
       = do { rr      <- newMetaTyVarTyAtLevel dest_lvl runtimeRepTy
            ; prom_ty <- newMetaTyVarTyAtLevel dest_lvl (mkTYPEapp rr)
-           ; let eq_orig = TypeEqOrigin { uo_actual   = ty
-                                        , uo_expected = prom_ty
-                                        , uo_thing    = Nothing
-                                        , uo_visible  = False }
-
-           ; co <- emitWantedEq eq_orig TypeLevel Nominal ty prom_ty
+           ; co <- unifyInvisibleType ty prom_ty
            ; return (co, prom_ty) }
 
 {- Note [Promoting a type]
@@ -2471,8 +2474,7 @@ zonkCt ct
 zonkCtEvidence :: CtEvidence -> TcM CtEvidence
 zonkCtEvidence ctev
   = do { pred' <- zonkTcType (ctev_pred ctev)
-       ; return (setCtEvPredType ctev pred')
-       }
+       ; return (setCtEvPredType ctev pred') }
 
 zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
 zonkSkolemInfo (SkolemInfo u sk) = SkolemInfo u <$> zonkSkolemInfoAnon sk
@@ -2788,23 +2790,43 @@ naughtyQuantification orig_ty tv escapees
 ************************************************************************
 -}
 
+zonkCtRewriterSet :: Ct -> TcM Ct
+zonkCtRewriterSet ct
+  | isGiven ev = return ct
+  | otherwise
+  = case ct of
+      CQuantCan {}                    -> return ct
+      CEqCan eq@(EqCt { eq_ev = ev }) -> do { ev' <- zonkCtEvRewriterSet ev
+                                            ; return (CEqCan (eq { eq_ev = ev' })) }
+      _ ->  do { ev' <- zonkCtEvRewriterSet ev
+               ; return (ct { cc_ev = ev' }) }
+  where
+    ev = ctEvidence ct
+
+zonkCtEvRewriterSet :: CtEvidence -> TcM CtEvidence
+zonkCtEvRewriterSet ev@(CtGiven {})
+  = return ev
+zonkCtEvRewriterSet ev@(CtWanted { ctev_rewriters = rewriters })
+  = do { rewriters' <- zonkRewriterSet rewriters
+       ; return (ev { ctev_rewriters = rewriters' }) }
+
 -- | Check whether any coercion hole in a RewriterSet is still unsolved.
 -- Does this by recursively looking through filled coercion holes until
 -- one is found that is not yet filled in, at which point this aborts.
-anyUnfilledCoercionHoles :: RewriterSet -> TcM Bool
-anyUnfilledCoercionHoles (RewriterSet set)
-  = nonDetStrictFoldUniqSet go (return False) set
+zonkRewriterSet :: RewriterSet -> TcM RewriterSet
+zonkRewriterSet (RewriterSet set)
+  = nonDetStrictFoldUniqSet go (return emptyRewriterSet) set
      -- this does not introduce non-determinism, because the only
      -- monadic action is to read, and the combining function is
      -- commutative
   where
-    go :: CoercionHole -> TcM Bool -> TcM Bool
-    go hole m_acc = m_acc <||> check_hole hole
+    go :: CoercionHole -> TcM RewriterSet -> TcM RewriterSet
+    go hole m_acc = unionRewriterSet <$> (check_hole hole) <*> m_acc
 
-    check_hole :: CoercionHole -> TcM Bool
+    check_hole :: CoercionHole -> TcM RewriterSet
     check_hole hole = do { m_co <- unpackCoercionHole_maybe hole
                          ; case m_co of
-                             Nothing -> return True  -- unfilled hole
+                             Nothing -> return (unitRewriterSet hole)
                              Just co -> unUCHM (check_co co) }
 
     check_ty :: Type -> UnfilledCoercionHoleMonoid
@@ -2818,10 +2840,10 @@ anyUnfilledCoercionHoles (RewriterSet set)
                         , tcf_hole  = \ _ -> UCHM . check_hole
                         , tcf_tycobinder = \ _ _ _ -> () }
 
-newtype UnfilledCoercionHoleMonoid = UCHM { unUCHM :: TcM Bool }
+newtype UnfilledCoercionHoleMonoid = UCHM { unUCHM :: TcM RewriterSet }
 
 instance Semigroup UnfilledCoercionHoleMonoid where
-  UCHM l <> UCHM r = UCHM (l <||> r)
+  UCHM l <> UCHM r = UCHM (unionRewriterSet <$> l <*> r)
 
 instance Monoid UnfilledCoercionHoleMonoid where
-  mempty = UCHM (return False)
+  mempty = UCHM (return emptyRewriterSet)