Make `tcCheckSatisfiability` incremental (#18645)

By taking and returning an `InertSet`.
Every new `TcS` session can then pick up where a prior session left with
`setTcSInerts`.

Since we don't want to unflatten the Givens (and because it leads to
infinite loops, see !3971), we introduced a new variant of `runTcS`,
`runTcSInerts`, that takes and returns the `InertSet` and makes
sure not to unflatten the Givens after running the `TcS` action.

Fixes #18645 and #17836.

Metric Decrease:
    T17977
    T18478

1 files changed, 28 insertions, 31 deletions

diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index 96fe5cbca2..f08622d8f1 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -718,22 +718,22 @@ simplifyDefault theta
        ; return () }
 
 ------------------
-tcCheckSatisfiability :: Bag EvVar -> TcM Bool
--- Return True if satisfiable, False if definitely contradictory
-tcCheckSatisfiability given_ids
-  = do { lcl_env <- TcM.getLclEnv
-       ; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
-       ; (res, _ev_binds) <- runTcS $
-             do { traceTcS "checkSatisfiability {" (ppr given_ids)
-                ; let given_cts = mkGivens given_loc (bagToList given_ids)
-                     -- See Note [Superclasses and satisfiability]
-                ; solveSimpleGivens given_cts
-                ; insols <- getInertInsols
-                ; insols <- try_harder insols
-                ; traceTcS "checkSatisfiability }" (ppr insols)
-                ; return (isEmptyBag insols) }
-       ; return res }
- where
+tcCheckSatisfiability :: InertSet -> Bag EvVar -> TcM (Maybe InertSet)
+-- Return (Just new_inerts) if satisfiable, Nothing if definitely contradictory
+tcCheckSatisfiability inerts given_ids = do
+  (sat, new_inerts) <- runTcSInerts inerts $ do
+    traceTcS "checkSatisfiability {" (ppr inerts <+> ppr given_ids)
+    lcl_env <- TcS.getLclEnv
+    let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
+    let given_cts = mkGivens given_loc (bagToList given_ids)
+    -- See Note [Superclasses and satisfiability]
+    solveSimpleGivens given_cts
+    insols <- getInertInsols
+    insols <- try_harder insols
+    traceTcS "checkSatisfiability }" (ppr insols)
+    return (isEmptyBag insols)
+  return $ if sat then Just new_inerts else Nothing
+  where
     try_harder :: Cts -> TcS Cts
     -- Maybe we have to search up the superclass chain to find
     -- an unsatisfiable constraint.  Example: pmcheck/T3927b.
@@ -749,15 +749,11 @@ tcCheckSatisfiability given_ids
 
 -- | Normalise a type as much as possible using the given constraints.
 -- See @Note [tcNormalise]@.
-tcNormalise :: Bag EvVar -> Type -> TcM Type
-tcNormalise given_ids ty
-  = do { lcl_env <- TcM.getLclEnv
-       ; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
-       ; norm_loc <- getCtLocM PatCheckOrigin Nothing
-       ; (res, _ev_binds) <- runTcS $
-             do { traceTcS "tcNormalise {" (ppr given_ids)
-                ; let given_cts = mkGivens given_loc (bagToList given_ids)
-                ; solveSimpleGivens given_cts
+tcNormalise :: InertSet -> Type -> TcM Type
+tcNormalise inerts ty
+  = do { norm_loc <- getCtLocM PatCheckOrigin Nothing
+       ; (res, _new_inerts) <- runTcSInerts inerts $
+             do { traceTcS "tcNormalise {" (ppr inerts)
                 ; ty' <- flattenType norm_loc ty
                 ; traceTcS "tcNormalise }" (ppr ty')
                 ; pure ty' }
@@ -788,8 +784,9 @@ Note [tcNormalise]
 tcNormalise is a rather atypical entrypoint to the constraint solver. Whereas
 most invocations of the constraint solver are intended to simplify a set of
 constraints or to decide if a particular set of constraints is satisfiable,
-the purpose of tcNormalise is to take a type, plus some local constraints, and
-normalise the type as much as possible with respect to those constraints.
+the purpose of tcNormalise is to take a type, plus some locally solved
+constraints in the form of an InertSet, and normalise the type as much as
+possible with respect to those constraints.
 
 It does *not* reduce type or data family applications or look through newtypes.
 
@@ -798,9 +795,9 @@ expression, it's possible that the type of the scrutinee will only reduce
 if some local equalities are solved for. See "Wrinkle: Local equalities"
 in Note [Type normalisation] in "GHC.HsToCore.PmCheck".
 
-To accomplish its stated goal, tcNormalise first feeds the local constraints
-into solveSimpleGivens, then uses flattenType to simplify the desired type
-with respect to the givens.
+To accomplish its stated goal, tcNormalise first initialises the solver monad
+with the given InertCans, then uses flattenType to simplify the desired type
+with respect to the Givens in the InertCans.
 
 ***********************************************************************************
 *                                                                                 *
@@ -893,7 +890,7 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
        ; psig_theta_vars <- mapM TcM.newEvVar psig_theta
        ; wanted_transformed_incl_derivs
             <- setTcLevel rhs_tclvl $
-               runTcSWithEvBinds ev_binds_var $
+               runTcSWithEvBinds ev_binds_var True $
                do { let loc         = mkGivenLoc rhs_tclvl UnkSkol $
                                       env_lcl tc_env
                         psig_givens = mkGivens loc psig_theta_vars