[Git][ghc/ghc][wip/T18645] Make `tcCheckSatisfiability` incremental (#18645)
Sebastian Graf
gitlab at gitlab.haskell.org
Mon Sep 7 10:49:50 UTC 2020
Sebastian Graf pushed to branch wip/T18645 at Glasgow Haskell Compiler / GHC
Commits:
d4347d90 by Sebastian Graf at 2020-09-07T12:47:10+02:00
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 (hopefully) #17836.
- - - - -
4 changed files:
- compiler/GHC/HsToCore/PmCheck/Oracle.hs
- compiler/GHC/HsToCore/PmCheck/Types.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Monad.hs
Changes:
=====================================
compiler/GHC/HsToCore/PmCheck/Oracle.hs
=====================================
@@ -523,13 +523,11 @@ nameTyCt pred_ty = do
tyOracle :: TyState -> Bag PredType -> DsM (Maybe TyState)
tyOracle (TySt inert) cts
= do { evs <- traverse nameTyCt cts
- ; let new_inert = inert `unionBags` evs
; tracePm "tyOracle" (ppr cts)
- ; ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability new_inert
+ ; ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability inert evs
; case res of
- Just True -> return (Just (TySt new_inert))
- Just False -> return Nothing
- Nothing -> pprPanic "tyOracle" (vcat $ pprErrMsgBagWithLoc errs) }
+ Just mb_new_inert -> return (TySt <$> mb_new_inert)
+ Nothing -> pprPanic "tyOracle" (vcat $ pprErrMsgBagWithLoc errs) }
-- | A 'SatisfiabilityCheck' based on new type-level constraints.
-- Returns a new 'Nabla' if the new constraints are compatible with existing
=====================================
compiler/GHC/HsToCore/PmCheck/Types.hs
=====================================
@@ -47,7 +47,6 @@ import GHC.Prelude
import GHC.Utils.Misc
import GHC.Data.Bag
import GHC.Data.FastString
-import GHC.Types.Var (EvVar)
import GHC.Types.Id
import GHC.Types.Var.Env
import GHC.Types.Unique.DSet
@@ -68,7 +67,7 @@ import GHC.Core.Utils (exprType)
import GHC.Builtin.Names
import GHC.Builtin.Types
import GHC.Builtin.Types.Prim
-import GHC.Tc.Utils.TcType (evVarPred)
+import GHC.Tc.Solver.Monad (InertSet, emptyInert)
import GHC.Driver.Types (ConLikeSet)
import Numeric (fromRat)
@@ -596,15 +595,14 @@ initTmState = TmSt emptySDIE emptyCoreMap
-- | The type oracle state. A poor man's 'GHC.Tc.Solver.Monad.InsertSet': The invariant is
-- that all constraints in there are mutually compatible.
-newtype TyState = TySt (Bag EvVar)
+newtype TyState = TySt InertSet
-- | Not user-facing.
instance Outputable TyState where
- ppr (TySt evs)
- = braces $ hcat $ punctuate comma $ map (ppr . evVarPred) $ bagToList evs
+ ppr (TySt inert) = ppr inert
initTyState :: TyState
-initTyState = TySt emptyBag
+initTyState = TySt emptyInert
-- | A normalised refinement type ∇ (\"nabla\"), comprised of an inert set of
-- canonical (i.e. mutually compatible) term and type constraints that form the
=====================================
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 InertCans, 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
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -15,7 +15,7 @@ module GHC.Tc.Solver.Monad (
getWorkList, updWorkListTcS, pushLevelNoWorkList,
-- The TcS monad
- TcS, runTcS, runTcSDeriveds, runTcSWithEvBinds,
+ TcS, runTcS, runTcSDeriveds, runTcSWithEvBinds, runTcSInerts,
failTcS, warnTcS, addErrTcS,
runTcSEqualities,
nestTcS, nestImplicTcS, setEvBindsTcS,
@@ -55,7 +55,7 @@ module GHC.Tc.Solver.Monad (
tcLookupClass, tcLookupId,
-- Inerts
- InertSet(..), InertCans(..),
+ InertSet(..), InertCans(..), emptyInert,
updInertTcS, updInertCans, updInertDicts, updInertIrreds,
getNoGivenEqs, setInertCans,
getInertEqs, getInertCans, getInertGivens,
@@ -2785,28 +2785,41 @@ runTcS :: TcS a -- What to run
-> TcM (a, EvBindMap)
runTcS tcs
= do { ev_binds_var <- TcM.newTcEvBinds
- ; res <- runTcSWithEvBinds ev_binds_var tcs
+ ; res <- runTcSWithEvBinds ev_binds_var True tcs
; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
; return (res, ev_binds) }
-
-- | This variant of 'runTcS' will keep solving, even when only Deriveds
-- are left around. It also doesn't return any evidence, as callers won't
-- need it.
runTcSDeriveds :: TcS a -> TcM a
runTcSDeriveds tcs
= do { ev_binds_var <- TcM.newTcEvBinds
- ; runTcSWithEvBinds ev_binds_var tcs }
+ ; runTcSWithEvBinds ev_binds_var True tcs }
-- | This can deal only with equality constraints.
runTcSEqualities :: TcS a -> TcM a
runTcSEqualities thing_inside
= do { ev_binds_var <- TcM.newNoTcEvBinds
- ; runTcSWithEvBinds ev_binds_var thing_inside }
+ ; runTcSWithEvBinds ev_binds_var True thing_inside }
+
+-- | A variant of 'runTcS' that takes and returns an 'InertSet' for
+-- later resumption of the 'TcS' session. Crucially, it doesn't
+-- 'unflattenGivens' when done.
+runTcSInerts :: InertSet -> TcS a -> TcM (a, InertSet)
+runTcSInerts inerts tcs = do
+ ev_binds_var <- TcM.newTcEvBinds
+ -- Passing False here to prohibit unflattening
+ runTcSWithEvBinds ev_binds_var False $ do
+ setTcSInerts inerts
+ a <- tcs
+ new_inerts <- getTcSInerts
+ return (a, new_inerts)
runTcSWithEvBinds :: EvBindsVar
+ -> Bool -- ^ Unflatten types afterwards? Don't if you want to reuse the InertSet.
-> TcS a
-> TcM a
-runTcSWithEvBinds ev_binds_var tcs
+runTcSWithEvBinds ev_binds_var unflatten tcs
= do { unified_var <- TcM.newTcRef 0
; step_count <- TcM.newTcRef 0
; inert_var <- TcM.newTcRef emptyInert
@@ -2824,7 +2837,7 @@ runTcSWithEvBinds ev_binds_var tcs
; when (count > 0) $
csTraceTcM $ return (text "Constraint solver steps =" <+> int count)
- ; unflattenGivens inert_var
+ ; when unflatten $ unflattenGivens inert_var
#if defined(DEBUG)
; ev_binds <- TcM.getTcEvBindsMap ev_binds_var
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d4347d90302566baf75d58e1885bec8a0b127654
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d4347d90302566baf75d58e1885bec8a0b127654
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200907/2bb398de/attachment-0001.html>
More information about the ghc-commits
mailing list