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, 152 insertions, 74 deletions

diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index d99f9067df..78c1134475 100644
--- a/compiler/GHC/Tc/Types/Constraint.hs
+++ b/compiler/GHC/Tc/Types/Constraint.hs
@@ -10,7 +10,7 @@ module GHC.Tc.Types.Constraint (
         QCInst(..), pendingScInst_maybe,
 
         -- Canonical constraints
-        Xi, Ct(..), EqCt(..), Cts,
+        Xi, Ct(..), Cts,
         singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList,
         isEmptyCts, emptyCts, andCts, ctsPreds,
         isPendingScDict, pendingScDict_maybe,
@@ -43,6 +43,8 @@ module GHC.Tc.Types.Constraint (
         cterHasNoProblem, cterHasProblem, cterHasOnlyProblem, cterHasOnlyProblems,
         cterRemoveProblem, cterHasOccursCheck, cterFromKind,
 
+
+        EqCt(..), eqCtLHS, eqCtEvidence,
         CanEqLHS(..), canEqLHS_maybe, canTyFamEqLHS_maybe,
         canEqLHSKind, canEqLHSType, eqCanEqLHS,
 
@@ -68,11 +70,11 @@ module GHC.Tc.Types.Constraint (
         ctLocTypeOrKind_maybe,
         ctLocDepth, bumpCtLocDepth, isGivenLoc,
         setCtLocOrigin, updateCtLocOrigin, setCtLocEnv, setCtLocSpan,
-        pprCtLoc,
+        pprCtLoc, adjustCtLoc, adjustCtLocTyConBinder,
 
         -- CtEvidence
         CtEvidence(..), TcEvDest(..),
-        mkKindLoc, toKindLoc, mkGivenLoc,
+        mkKindEqLoc, toKindLoc, toInvisibleLoc, mkGivenLoc,
         isWanted, isGiven,
         ctEvRole, setCtEvPredType, setCtEvLoc, arisesFromGivens,
         tyCoVarsOfCtEvList, tyCoVarsOfCtEv, tyCoVarsOfCtEvsList,
@@ -80,8 +82,7 @@ module GHC.Tc.Types.Constraint (
 
         RewriterSet(..), emptyRewriterSet, isEmptyRewriterSet,
            -- exported concretely only for anyUnfilledCoercionHoles
-        rewriterSetFromType, rewriterSetFromTypes, rewriterSetFromCo,
-        addRewriterSet,
+        addRewriter, unitRewriterSet, unionRewriterSet, rewriterSetFromCts,
 
         wrapType,
 
@@ -132,7 +133,6 @@ import GHC.Utils.Constants (debugIsOn)
 import GHC.Types.Name.Reader
 
 import Data.Coerce
-import Data.Monoid ( Endo(..) )
 import qualified Data.Semigroup as S
 import Control.Monad ( msum, when )
 import Data.Maybe ( mapMaybe, isJust )
@@ -234,8 +234,8 @@ data Ct
       --     look like this, with the payload in an
       --     auxiliary type
 
-{- Note [Invariants of EqCt]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Canonical equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 An EqCt is a canonical equality constraint, one that can live in the inert set,
 and that can be used to rewrite other constrtaints. It satisfies these invariants:
   * (TyEq:OC) lhs does not occur in rhs (occurs check)
@@ -249,6 +249,9 @@ and that can be used to rewrite other constrtaints. It satisfies these invariant
     (Applies only when constructor of newtype is in scope.)
   * (TyEq:U) An EqCt is not immediately unifiable. If we can unify a:=ty, we
     will not form an EqCt (a ~ ty).
+  * (TyEq:CH) rhs does not mention any coercion holes that resulted from fixing up
+    a hetero-kinded equality.  See Note [Equalities with incompatible kinds] in
+    GHC.Tc.Solver.Equality, wrinkle (EIK2)
 
 These invariants ensure that the EqCts in inert_eqs constitute a terminating
 generalised substitution. See Note [inert_eqs: the inert equalities]
@@ -286,7 +289,7 @@ and forms condition T3 in Note [Extending the inert equalities]
 in GHC.Tc.Solver.InertSet.
 -}
 
-data EqCt -- An equality constraint; see Note [Invariants of EqCt]
+data EqCt -- An equality constraint; see Note [Canonical equalities]
   = EqCt {  -- CanEqLHS ~ rhs
       eq_ev     :: CtEvidence, -- See Note [Ct/evidence invariant]
       eq_lhs    :: CanEqLHS,
@@ -294,6 +297,12 @@ data EqCt -- An equality constraint; see Note [Invariants of EqCt]
       eq_eq_rel :: EqRel       -- INVARIANT: cc_eq_rel = ctEvEqRel cc_ev
     }
 
+eqCtEvidence :: EqCt -> CtEvidence
+eqCtEvidence = eq_ev
+
+eqCtLHS :: EqCt -> CanEqLHS
+eqCtLHS = eq_lhs
+
 ------------
 -- | A 'CanEqLHS' is a type that can appear on the left of a canonical
 -- equality: a type variable or /exactly-saturated/ type family application.
@@ -2083,41 +2092,26 @@ newtype RewriterSet = RewriterSet (UniqSet CoercionHole)
 emptyRewriterSet :: RewriterSet
 emptyRewriterSet = RewriterSet emptyUniqSet
 
+unitRewriterSet :: CoercionHole -> RewriterSet
+unitRewriterSet = coerce (unitUniqSet @CoercionHole)
+
+unionRewriterSet :: RewriterSet -> RewriterSet -> RewriterSet
+unionRewriterSet = coerce (unionUniqSets @CoercionHole)
+
 isEmptyRewriterSet :: RewriterSet -> Bool
-isEmptyRewriterSet (RewriterSet set) = isEmptyUniqSet set
-
-addRewriterSet :: RewriterSet -> CoercionHole -> RewriterSet
-addRewriterSet = coerce (addOneToUniqSet @CoercionHole)
-
--- | Makes a 'RewriterSet' from all the coercion holes that occur in the
--- given coercion.
-rewriterSetFromCo :: Coercion -> RewriterSet
-rewriterSetFromCo co = appEndo (rewriter_set_from_co co) emptyRewriterSet
-
--- | Makes a 'RewriterSet' from all the coercion holes that occur in the
--- given type.
-rewriterSetFromType :: Type -> RewriterSet
-rewriterSetFromType ty = appEndo (rewriter_set_from_ty ty) emptyRewriterSet
-
--- | Makes a 'RewriterSet' from all the coercion holes that occur in the
--- given types.
-rewriterSetFromTypes :: [Type] -> RewriterSet
-rewriterSetFromTypes tys = appEndo (rewriter_set_from_tys tys) emptyRewriterSet
-
-rewriter_set_from_ty :: Type -> Endo RewriterSet
-rewriter_set_from_tys :: [Type] -> Endo RewriterSet
-rewriter_set_from_co :: Coercion -> Endo RewriterSet
-(rewriter_set_from_ty, rewriter_set_from_tys, rewriter_set_from_co, _)
-  = foldTyCo folder ()
+isEmptyRewriterSet = coerce (isEmptyUniqSet @CoercionHole)
+
+addRewriter :: RewriterSet -> CoercionHole -> RewriterSet
+addRewriter = coerce (addOneToUniqSet @CoercionHole)
+
+rewriterSetFromCts :: Bag Ct -> RewriterSet
+-- Take a bag of Wanted equalities, and collect them as a RewriterSet
+rewriterSetFromCts cts
+  = foldr add emptyRewriterSet cts
   where
-    folder :: TyCoFolder () (Endo RewriterSet)
-    folder = TyCoFolder
-               { tcf_view  = noView
-               , tcf_tyvar = \ _ tv -> rewriter_set_from_ty (tyVarKind tv)
-               , tcf_covar = \ _ cv -> rewriter_set_from_ty (varType cv)
-               , tcf_hole  = \ _ hole -> coerce (`addOneToUniqSet` hole) S.<>
-                                         rewriter_set_from_ty (varType (coHoleCoVar hole))
-               , tcf_tycobinder = \ _ _ _ -> () }
+    add ct rw_set = case ctEvidence ct of
+         CtWanted { ctev_dest = HoleDest hole } -> rw_set `addRewriter` hole
+         _                                      -> rw_set
 
 {-
 ************************************************************************
@@ -2202,10 +2196,22 @@ TL;DR we want equality saturation.
 
 We thus want Wanteds to rewrite Wanteds in order to accept more programs,
 but we don't want Wanteds to rewrite Wanteds because doing so can create
-inscrutable error messages. We choose to allow the rewriting, but
-every Wanted tracks the set of Wanteds it has been rewritten by. This is
-called a RewriterSet, stored in the ctev_rewriters field of the CtWanted
-constructor of CtEvidence.  (Only Wanteds have RewriterSets.)
+inscrutable error messages. To solve this dilemma:
+
+* We allow Wanteds to rewrite Wanteds, but...
+
+* Each Wanted tracks the set of Wanteds it has been rewritten by, in its
+  RewriterSet, stored in the ctev_rewriters field of the CtWanted
+  constructor of CtEvidence.  (Only Wanteds have RewriterSets.)
+
+* In error reporting, we simply suppress any errors that have been rewritten
+  by /unsolved/ wanteds. This suppression happens in GHC.Tc.Errors.mkErrorItem,
+  which uses GHC.Tc.Utils.anyUnfilledCoercionHoles to look through any filled
+  coercion holes. The idea is that we wish to report the "root cause" -- the
+  error that rewrote all the others.
+
+* We prioritise Wanteds that have an empty RewriterSet:
+  see Note [Prioritise Wanteds with empty RewriterSet].
 
 Let's continue our first example above:
 
@@ -2219,25 +2225,72 @@ Because Wanteds can rewrite Wanteds, w1 will rewrite w2, yielding
 
 The {w1} in the second line of output is the RewriterSet of w1.
 
-A RewriterSet is just a set of unfilled CoercionHoles. This is
-sufficient because only equalities (evidenced by coercion holes) are
-used for rewriting; other (dictionary) constraints cannot ever
-rewrite. The rewriter (in e.g. GHC.Tc.Solver.Rewrite.rewrite) tracks
-and returns a RewriterSet, consisting of the evidence (a CoercionHole)
-for any Wanted equalities used in rewriting.  Then rewriteEvidence and
-rewriteEqEvidence (in GHC.Tc.Solver.Canonical) add this RewriterSet to
-the rewritten constraint's rewriter set.
-
-In error reporting, we simply suppress any errors that have been rewritten by
-/unsolved/ wanteds. This suppression happens in GHC.Tc.Errors.mkErrorItem, which
-uses GHC.Tc.Utils.anyUnfilledCoercionHoles to look through any filled coercion
-holes. The idea is that we wish to report the "root cause" -- the error that
-rewrote all the others.
-
-Wrinkle: In #22707, we have a case where all of the Wanteds have rewritten
-each other. In order to report /some/ error in this case, we simply report
-all the Wanteds. The user will get a perhaps-confusing error message, but
-they've written a confusing program!
+A RewriterSet is just a set of unfilled CoercionHoles. This is sufficient
+because only equalities (evidenced by coercion holes) are used for rewriting;
+other (dictionary) constraints cannot ever rewrite. The rewriter (in
+e.g. GHC.Tc.Solver.Rewrite.rewrite) tracks and returns a RewriterSet,
+consisting of the evidence (a CoercionHole) for any Wanted equalities used in
+rewriting.  Then rewriteEvidence and rewriteEqEvidence (in GHC.Tc.Solver.Canonical)
+add this RewriterSet to the rewritten constraint's arewriter set.
+
+Note [Prioritise Wanteds with empty RewriterSet]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When extending the WorkList, in GHC.Tc.Solver.InertSet.extendWorkListEq,
+we priorities constraints that have no rewriters. Here's why.
+
+Consider this, which came up in T22793:
+  inert: {}
+  work list: [W] co_ayf : awq ~ awo
+  work item: [W] co_ayb : awq ~ awp
+
+  ==> {just put work item in inert set}
+  inert: co_ayb : awq ~ awp
+  work list: {}
+  work: [W] co_ayf : awq ~ awo
+
+  ==> {rewrite ayf with co_ayb}
+  work list: {}
+  inert: co_ayb : awq ~ awp
+         co_aym{co_ayb} : awp ~ awo
+                ^ rewritten by ayb
+
+  ----- start again in simplify_loop in Solver.hs -----
+  inert: {}
+  work list: [W] co_ayb : awq ~ awp
+  work: co_aym{co_ayb} : awp ~ awo
+
+  ==> {add to inert set}
+  inert: co_aym{co_ayb} : awp ~ awo
+  work list: {}
+  work: co_ayb : awq ~ awp
+
+  ==> {rewrite co_ayb}
+  inert: co_aym{co_ayb} : awp ~ awo
+         co_ayp{co_aym} : awq ~ awo
+  work list: {}
+
+Now both wanteds have been rewriten by the other! This happened because
+in our simplify_loop iteration, we happened to start with co_aym. All would have
+been well if we'd started with the (not-rewritten) co_ayb and gotten it into the
+inert set.
+
+With that in mind, we /prioritise/ the work-list to put constraints
+with no rewriters first.  This prioritisation is done in
+GHC.Tc.Solver.InertSet.extendWorkListEq, and extendWorkListEqs.
+
+Wrinkles
+
+(WRW1) Before checking for an empty RewriterSet, we zonk the RewriterSet,
+  because some of those CoercionHoles may have been filled in since we last
+  looked: see GHC.Tc.Solver.Monad.emitWork.
+
+(WRW2) Despite the prioritisation, it is hard to be /certain/ that we can't end up
+  in a situation where all of the Wanteds have rewritten each other. In
+  order to report /some/ error in this case, we simply report all the
+  Wanteds. The user will get a perhaps-confusing error message, but they've
+  written a confusing program!  (T22707 and T22793 were close, but they do
+  not exhibit this behaviour.)  So belt and braces: see the `suppress`
+  stuff in GHC.Tc.Errors.mkErrorItem.
 
 Note [Avoiding rewriting cycles]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2416,10 +2469,11 @@ dictionaries don't appear in the original source code.
 
 -}
 
-data CtLoc = CtLoc { ctl_origin   :: CtOrigin
-                   , ctl_env      :: TcLclEnv
-                   , ctl_t_or_k   :: Maybe TypeOrKind  -- OK if we're not sure
-                   , ctl_depth    :: !SubGoalDepth }
+data CtLoc
+  = CtLoc { ctl_origin   :: CtOrigin
+          , ctl_env      :: TcLclEnv
+          , ctl_t_or_k   :: Maybe TypeOrKind  -- Used only to improve error messages
+          , ctl_depth    :: !SubGoalDepth }
 
   -- The TcLclEnv includes particularly
   --    source location:  tcl_loc   :: RealSrcSpan
@@ -2427,16 +2481,40 @@ data CtLoc = CtLoc { ctl_origin   :: CtOrigin
   --    binder stack:     tcl_bndrs :: TcBinderStack
   --    level:            tcl_tclvl :: TcLevel
 
-mkKindLoc :: TcType -> TcType   -- original *types* being compared
-          -> CtLoc -> CtLoc
-mkKindLoc s1 s2 loc = setCtLocOrigin (toKindLoc loc)
-                        (KindEqOrigin s1 s2 (ctLocOrigin loc)
-                                      (ctLocTypeOrKind_maybe loc))
+mkKindEqLoc :: TcType -> TcType   -- original *types* being compared
+            -> CtLoc -> CtLoc
+mkKindEqLoc s1 s2 ctloc
+  | CtLoc { ctl_t_or_k = t_or_k, ctl_origin = origin } <- ctloc
+  = ctloc { ctl_origin = KindEqOrigin s1 s2 origin t_or_k
+          , ctl_t_or_k = Just KindLevel }
+
+adjustCtLocTyConBinder :: TyConBinder -> CtLoc -> CtLoc
+-- Adjust the CtLoc when decomposing a type constructor
+adjustCtLocTyConBinder tc_bndr loc
+  = adjustCtLoc is_vis is_kind loc
+  where
+    is_vis  = isVisibleTyConBinder tc_bndr
+    is_kind = isNamedTyConBinder tc_bndr
+
+adjustCtLoc :: Bool    -- True <=> A visible argument
+            -> Bool    -- True <=> A kind argument
+            -> CtLoc -> CtLoc
+-- Adjust the CtLoc when decomposing a type constructor, application, etc
+adjustCtLoc is_vis is_kind loc
+  = loc2
+  where
+    loc1 | is_kind   = toKindLoc loc
+         | otherwise = loc
+    loc2 | is_vis    = loc1
+         | otherwise = toInvisibleLoc loc1
 
 -- | Take a CtLoc and moves it to the kind level
 toKindLoc :: CtLoc -> CtLoc
 toKindLoc loc = loc { ctl_t_or_k = Just KindLevel }
 
+toInvisibleLoc :: CtLoc -> CtLoc
+toInvisibleLoc loc = updateCtLocOrigin loc toInvisibleOrigin
+
 mkGivenLoc :: TcLevel -> SkolemInfoAnon -> TcLclEnv -> CtLoc
 mkGivenLoc tclvl skol_info env
   = CtLoc { ctl_origin   = GivenOrigin skol_info