[Git][ghc/ghc][wip/T24359] new plan from March 7
sheaf (@sheaf)
gitlab at gitlab.haskell.org
Fri Mar 7 13:29:53 UTC 2025
sheaf pushed to branch wip/T24359 at Glasgow Haskell Compiler / GHC
Commits:
dbffc28b by sheaf at 2025-03-07T14:29:39+01:00
new plan from March 7
- - - - -
8 changed files:
- compiler/GHC/Tc/Gen/Sig.hs
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Solver/Solve.hs
- + compiler/GHC/Tc/Solver/Solve.hs-boot
- compiler/GHC/Tc/Types/Evidence.hs
- testsuite/tests/simplCore/should_compile/DsSpecPragmas.hs
Changes:
=====================================
compiler/GHC/Tc/Gen/Sig.hs
=====================================
@@ -39,7 +39,7 @@ import GHC.Tc.Gen.HsType
import GHC.Tc.Solver( reportUnsolvedEqualities, pushLevelAndSolveEqualitiesX
, emitResidualConstraints )
import GHC.Tc.Solver.Solve( solveWanteds )
-import GHC.Tc.Solver.Monad( runTcS, runTcSWithEvBinds )
+import GHC.Tc.Solver.Monad( runTcS, runTcSFullySolve )
import GHC.Tc.Validity ( checkValidType )
import GHC.Tc.Utils.Monad
@@ -761,16 +761,11 @@ This is done in three parts.
(1) Typecheck the expression, capturing its constraints
- (2) Clone these Wanteds, solve them, and zonk the original Wanteds.
- This is the same thing that we do for RULES: see Step 1 in
- Note [The SimplifyRule Plan].
+ (2) Solve these constraints, but in special TcSFullySolve mode which ensures
+ each original Wanted is either fully solved or left untouched.
+ See Note [Fully solving constraints for specialisation].
- (3) Compute the constraints to quantify over.
-
- a. 'getRuleQuantCts' computes the initial quantification candidates
- b. Filter out the fully soluble constraints; these are the constraints
- we are specialising away.
- See Note [Fully solving constraints for specialisation].
+ (3) Compute the constraints to quantify over, using `getRuleQuantCts`.
(4) Emit the residual (non-quantified) constraints, and wrap the
expression in a let binding for those constraints.
@@ -850,9 +845,8 @@ The conclusion is this:
- fully solved (no free evidence variables), or
- left untouched.
-To achieve this, we quantify over all constraints that are **not fully soluble**
-(see 'fullySolveCt_maybe'), although we still call 'mkMinimalBySCs' on this set
-to avoid e.g. quantifying over both `Eq a` and `Ord a`.
+To achieve this, we run the solver in a special "all-or-nothing" solving mode,
+described in Note [TcSFullySolve] in GHC.Tc.Solver.Monad.
Note [Handling old-form SPECIALISE pragmas]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1029,40 +1023,26 @@ tcSpecPrag poly_id (SpecSigE nm rule_bndrs spec_e inl)
<- tcRuleBndrs skol_info rule_bndrs $
tcInferRho spec_e
- -- (2) Clone these Wanteds, solve them, and zonk the original
- -- Wanteds, in order to benefit from any unifications.
-
- ; throwaway_ev_binds_var <- newTcEvBinds
- ; spec_e_wanted_clone <- cloneWC spec_e_wanted
- ; _ <- setTcLevel rhs_tclvl $
- runTcSWithEvBinds throwaway_ev_binds_var $
- solveWanteds spec_e_wanted_clone
+ -- (2) Solve the resulting wanteds in TcSFullySolve mode.
+ ; ev_binds_var <- newTcEvBinds
+ ; spec_e_wanted <- setTcLevel rhs_tclvl $
+ runTcSFullySolve ev_binds_var $
+ solveWanteds spec_e_wanted
; spec_e_wanted <- liftZonkM $ zonkWC spec_e_wanted
-- (3) Compute which constraints to quantify over.
- -- (a) Compute quantification candidates
- ; ev_binds_var <- newTcEvBinds
; (quant_cands, residual_wc) <- getRuleQuantCts spec_e_wanted
- -- (b) Compute fully soluble constraints
- -- See Note [Fully solving constraints for specialisation]
- ; traceTc "tcSpecPrag SpecSigE: computing fully soluble Wanteds {" empty
- ; fully_soluble_evids <-
- setTcLevel rhs_tclvl $
- mkVarSet <$>
- mapMaybeM fullySolveCt_maybe (bagToList quant_cands)
- ; let (fully_soluble_cts, quant_cts) = partitionBag ((`elemVarSet` fully_soluble_evids) . ctEvId) quant_cands
- -- (c) Compute constraints to quantify over using 'mkMinimalBySCs'
- qevs = map ctEvId (bagToList quant_cts)
- ; traceTc "tcSpecPrag SpecSigE: computed fully soluble Wanteds }" (ppr fully_soluble_cts)
-
-- (4) Emit the residual constraints (that we are not quantifying over)
; let tv_bndrs = filter isTyVar rule_bndrs'
+ qevs = map ctEvId (bagToList quant_cands)
; emitResidualConstraints rhs_tclvl skol_info_anon ev_binds_var
emptyVarSet tv_bndrs qevs
- (residual_wc `addSimples` fully_soluble_cts)
+ residual_wc
; let lhs_call = mkLHsWrap (WpLet (TcEvBinds ev_binds_var)) tc_spec_e
+ ; ev_binds <- getTcEvBindsMap ev_binds_var
+
; traceTc "tcSpecPrag SpecSigE }" $
vcat [ text "nm:" <+> ppr nm
, text "rule_bndrs':" <+> ppr rule_bndrs'
@@ -1070,9 +1050,11 @@ tcSpecPrag poly_id (SpecSigE nm rule_bndrs spec_e inl)
, text "spec_e:" <+> ppr tc_spec_e
, text "inl:" <+> ppr inl
, text "spec_e_wanted:" <+> ppr spec_e_wanted
- , text "quant_cts:" <+> ppr quant_cts
+ , text "quant_cands:" <+> ppr quant_cands
, text "residual_wc:" <+> ppr residual_wc
- , text "fully_soluble_wanteds:" <+> ppr fully_soluble_cts
+ , text (replicate 80 '-')
+ , text "ev_binds_var:" <+> ppr ev_binds_var
+ , text "ev_binds:" <+> ppr ev_binds
]
-- (5) Store the results in a SpecPragE record, which will be
@@ -1087,24 +1069,6 @@ tcSpecPrag poly_id (SpecSigE nm rule_bndrs spec_e inl)
tcSpecPrag _ prag = pprPanic "tcSpecPrag" (ppr prag)
--- | Try to fully solve a constraint.
-fullySolveCt_maybe :: Ct -> TcM (Maybe EvId)
-fullySolveCt_maybe ct = do
- throwaway_ev_binds_var <- newTcEvBinds
- res_wc <-
- runTcSWithEvBinds throwaway_ev_binds_var $
- solveWanteds $ emptyWC { wc_simple = unitBag ct }
- -- NB: don't use 'solveSimpleWanteds', as this will not
- -- fully solve quantified constraints.
- traceTc "fullySolveCt_maybe" $
- vcat [ text "ct:" <+> ppr ct
- , text "res_wc:" <+> ppr res_wc
- ]
- return $
- if isSolvedWC res_wc
- then Just $ ctEvId ct
- else Nothing
-
--------------
tcSpecWrapper :: UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
-- A simpler variant of tcSubType, used for SPECIALISE pragmas
=====================================
compiler/GHC/Tc/Solver/Dict.hs
=====================================
@@ -61,6 +61,7 @@ import Data.Void( Void )
import Control.Monad.Trans.Maybe( MaybeT, runMaybeT )
import Control.Monad.Trans.Class( lift )
import Control.Monad
+import {-# SOURCE #-} GHC.Tc.Solver.Solve (solveCompletelyIfRequired)
{- *********************************************************************
@@ -848,7 +849,13 @@ shortCutSolver dflags ev_w ev_i
tryInstances :: DictCt -> SolverStage ()
tryInstances dict_ct
= Stage $ do { inerts <- getInertSet
- ; try_instances inerts dict_ct }
+
+ -- We are about to do something irreversible (using an instance
+ -- declaration), so we wrap 'try_instances' in solveCompletelyIfRequired
+ -- to ensure we can roll back if we can't solve the constraint fully.
+ -- See Note [TcSFullySolve] in GHC.Tc.Solver.Monad.
+ ; solveCompletelyIfRequired (continueWith ()) $
+ try_instances inerts dict_ct }
try_instances :: InertSet -> DictCt -> TcS (StopOrContinue ())
-- Try to use type-class instance declarations to simplify the constraint
=====================================
compiler/GHC/Tc/Solver/InertSet.hs
=====================================
@@ -25,6 +25,7 @@ module GHC.Tc.Solver.InertSet (
InertEqs,
foldTyEqs, delEq, findEq,
partitionInertEqs, partitionFunEqs,
+ partitionInerts, andInertSet,
foldFunEqs, addEqToCans,
-- * Inert Dicts
@@ -75,6 +76,7 @@ import GHC.Utils.Panic
import GHC.Data.Bag
import Control.Monad ( forM_ )
+import Data.List ( partition )
import Data.List.NonEmpty ( NonEmpty(..), (<|) )
import Data.Function ( on )
@@ -391,7 +393,6 @@ emptyInert
, inert_famapp_cache = emptyFunEqs
, inert_solved_dicts = emptyDictMap }
-
{- Note [Solved dictionaries]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we apply a top-level instance declaration, we add the "solved"
@@ -2215,3 +2216,115 @@ Wrong! The level-check ensures that the inner implicit parameter wins.
(Actually I think that the order in which the work-list is processed means
that this chain of events won't happen, but that's very fragile.)
-}
+
+-- | Partition the inert set according to a predicate.
+partitionInerts :: (Ct -> Bool) -> InertSet -> (InertSet, InertSet)
+partitionInerts pred is@(IS { inert_cans = cans })
+ = (is { inert_cans = givens_cans }, is { inert_cans = wanteds_cans })
+ where
+ -- Helper functions to convert between Ct and specific constraint types
+ eqPred :: EqCt -> Bool
+ eqPred eq = pred (CEqCan eq)
+
+ dictPred :: DictCt -> Bool
+ dictPred dict = pred (CDictCan dict)
+
+ irredPred :: IrredCt -> Bool
+ irredPred irred = pred (CIrredCan irred)
+
+ qciPred :: QCInst -> Bool
+ qciPred qci = pred (CQuantCan qci)
+
+ -- Partition the inert constraints
+ (eq_givens_list, eq_wanteds) = partitionInertEqs eqPred (inert_eqs cans)
+ (funeq_givens_list, funeq_wanteds) = partitionFunEqs eqPred (inert_funeqs cans)
+ (dict_givens_bag, dict_wanteds) = partitionDicts dictPred (inert_dicts cans)
+ (safehask_givens_bag, safehask_wanteds) = partitionDicts dictPred (inert_safehask cans)
+ (insts_givens, insts_wanteds) = partition qciPred (inert_insts cans)
+ (irreds_givens, irreds_wanteds) = partitionBag irredPred (inert_irreds cans)
+
+ -- Convert lists to the appropriate container types
+ eq_givens = foldr addInertEqs emptyTyEqs eq_givens_list
+ funeq_givens = foldr addFunEqs emptyFunEqs funeq_givens_list
+
+ givens_cans = emptyInertCans {
+ inert_eqs = eq_givens,
+ inert_funeqs = funeq_givens,
+ inert_dicts = dictsToDictMap dict_givens_bag,
+ inert_safehask = dictsToDictMap safehask_givens_bag,
+ inert_insts = insts_givens,
+ inert_irreds = irreds_givens,
+ inert_given_eq_lvl = inert_given_eq_lvl cans,
+ inert_given_eqs = inert_given_eqs cans
+ }
+
+ wanteds_cans = emptyInertCans {
+ inert_eqs = eq_wanteds,
+ inert_funeqs = funeq_wanteds,
+ inert_dicts = dict_wanteds,
+ inert_safehask = safehask_wanteds,
+ inert_insts = insts_wanteds,
+ inert_irreds = irreds_wanteds,
+ inert_given_eq_lvl = inert_given_eq_lvl cans,
+ inert_given_eqs = inert_given_eqs cans
+ }
+
+-- | Convert a Bag of DictCts to a DictMap
+dictsToDictMap :: Bag DictCt -> DictMap DictCt
+dictsToDictMap = foldr addDict emptyDictMap . bagToList
+
+-- | Union two DictMaps
+unionDictMap :: DictMap DictCt -> DictMap DictCt -> DictMap DictCt
+unionDictMap dm1 dm2 = foldrTcAppMap addDict dm1 dm2
+
+-- | Union two InertEqs
+unionTyEqs :: InertEqs -> InertEqs -> InertEqs
+unionTyEqs eqs1 eqs2 = foldrTyEqs addInertEqs eqs1 eqs2
+
+-- | Union two InertFunEqs
+unionFunEqs :: InertFunEqs -> InertFunEqs -> InertFunEqs
+unionFunEqs feqs1 feqs2 = foldrFunEqs addFunEqs feqs1 feqs2
+
+-- | Union two FunEqMap Reductions
+unionFunEqMap :: FunEqMap Reduction -> FunEqMap Reduction -> FunEqMap Reduction
+unionFunEqMap m1 m2 = foldTcAppMap (\r acc ->
+ let ty = reductionReducedType r
+ in case tcSplitTyConApp_maybe ty of
+ Just (tc, args) -> insertTcApp acc tc args r
+ Nothing -> acc)
+ m1 m2
+
+-- | Fold over a TcAppMap with a function
+foldrTcAppMap :: (a -> b -> b) -> TcAppMap a -> b -> b
+foldrTcAppMap k m z = foldTcAppMap (\x acc -> k x acc) m z
+
+-- | Fold over FunEqs with a function
+foldrFunEqs :: (EqCt -> b -> b) -> InertFunEqs -> b -> b
+foldrFunEqs k feqs z = foldFunEqs (\eq acc -> k eq acc) feqs z
+
+-- | Fold over TyEqs with a function
+foldrTyEqs :: (EqCt -> b -> b) -> InertEqs -> b -> b
+foldrTyEqs k eqs z = foldTyEqs (\eq acc -> k eq acc) eqs z
+
+-- | Combine two 'InertSet's in a monoidal manner.
+andInertSet :: InertSet -> InertSet -> InertSet
+andInertSet is1 is2
+ = IS { inert_cans = combinedCans,
+ inert_cycle_breakers = inert_cycle_breakers is1, -- Keep the first one's cycle breakers
+ inert_famapp_cache = unionFunEqMap (inert_famapp_cache is1) (inert_famapp_cache is2),
+ inert_solved_dicts = unionDictMap (inert_solved_dicts is1) (inert_solved_dicts is2)
+ }
+ where
+ cans1 = inert_cans is1
+ cans2 = inert_cans is2
+
+ combinedCans = IC {
+ inert_eqs = unionTyEqs (inert_eqs cans1) (inert_eqs cans2),
+ inert_funeqs = unionFunEqs (inert_funeqs cans1) (inert_funeqs cans2),
+ inert_dicts = unionDictMap (inert_dicts cans1) (inert_dicts cans2),
+ inert_safehask = unionDictMap (inert_safehask cans1) (inert_safehask cans2),
+ inert_insts = inert_insts cans1 ++ inert_insts cans2,
+ inert_irreds = unionBags (inert_irreds cans1) (inert_irreds cans2),
+ inert_given_eq_lvl = maxTcLevel (inert_given_eq_lvl cans1) (inert_given_eq_lvl cans2),
+ inert_given_eqs = inert_given_eqs cans1 || inert_given_eqs cans2
+ }
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -14,7 +14,9 @@
module GHC.Tc.Solver.Monad (
-- The TcS monad
- TcS, runTcS, runTcSEarlyAbort, runTcSWithEvBinds, runTcSInerts,
+ TcS(..), TcSEnv(..), TcSMode(..),
+ runTcS, runTcSEarlyAbort, runTcSWithEvBinds, runTcSInerts,
+ runTcSFullySolve,
failTcS, warnTcS, addErrTcS, wrapTcS, ctLocWarnTcS,
runTcSEqualities,
nestTcS, nestImplicTcS, setEvBindsTcS,
@@ -71,7 +73,7 @@ module GHC.Tc.Solver.Monad (
getInertEqs, getInertCans, getInertGivens,
getInertInsols, getInnermostGivenEqLevel,
getInertSet, setInertSet,
- getUnsolvedInerts,
+ getUnsolvedInerts, getUnsolvedInerts2,
removeInertCts, getPendingGivenScs,
insertFunEq, addInertForAll,
updInertDicts, updInertIrreds,
@@ -203,13 +205,14 @@ import GHC.Exts (oneShot)
import Control.Monad
import Data.Foldable hiding ( foldr1 )
import Data.IORef
-import Data.List ( mapAccumL )
+import Data.List ( mapAccumL, unfoldr )
import Data.List.NonEmpty ( nonEmpty )
import qualified Data.List.NonEmpty as NE
import Data.Maybe ( isJust )
import qualified Data.Semigroup as S
import GHC.Types.SrcLoc
import GHC.Rename.Env
+--import GHC.Tc.Solver.Solve (solveWanteds)
#if defined(DEBUG)
import GHC.Types.Unique.Set (nonDetEltsUniqSet)
@@ -705,6 +708,45 @@ getUnsolvedInerts
where
ct = mk_ct thing
+getUnsolvedInerts2 :: TcS ( Bag Implication, Cts )
+getUnsolvedInerts2
+ = do { IC { inert_eqs = tv_eqs
+ , inert_funeqs = fun_eqs
+ , inert_irreds = irreds
+ , inert_dicts = idicts
+ } <- getInertCans
+
+ ; let unsolved_tv_eqs = foldTyEqs (add_if_unsolved CEqCan) tv_eqs emptyCts
+ unsolved_fun_eqs = foldFunEqs (add_if_unsolved CEqCan) fun_eqs emptyCts
+ unsolved_irreds = foldr (add_if_unsolved CIrredCan) emptyCts irreds
+ unsolved_dicts = foldDicts (add_if_unsolved CDictCan) idicts emptyCts
+
+ ; wl_var <- getTcSWorkListRef
+ ; wl_curr <- readTcRef wl_var
+ ; implics <- getWorkListImplics
+ ; let wl_simpls = listToBag $ unfoldr selectWorkItem wl_curr
+
+ ; traceTcS "getUnsolvedInerts" $
+ vcat [ text " tv eqs =" <+> ppr unsolved_tv_eqs
+ , text "fun eqs =" <+> ppr unsolved_fun_eqs
+ , text "dicts =" <+> ppr unsolved_dicts
+ , text "irreds =" <+> ppr unsolved_irreds
+ , text "implics =" <+> ppr implics ]
+
+ ; return ( implics, unsolved_tv_eqs `unionBags`
+ unsolved_fun_eqs `unionBags`
+ unsolved_irreds `unionBags`
+ unsolved_dicts `unionBags`
+ wl_simpls) }
+ where
+ add_if_unsolved :: (a -> Ct) -> a -> Cts -> Cts
+ add_if_unsolved mk_ct thing cts
+ | isWantedCt ct = ct `consCts` cts
+ | otherwise = cts
+ where
+ ct = mk_ct thing
+
+
getHasGivenEqs :: TcLevel -- TcLevel of this implication
-> TcS ( HasGivenEqs -- are there Given equalities?
, InertIrreds ) -- Insoluble equalities arising from givens
@@ -850,6 +892,31 @@ for it, so TcS carries a mutable location where the binding can be
added. This is initialised from the innermost implication constraint.
-}
+-- | See Note [TcSMode]
+data TcSMode
+ = TcSVanilla -- ^ Normal constraint solving
+ | TcSEarlyAbort -- ^ Abort early on insoluble constraints
+ | TcSFullySolve -- ^ Fully solve all constraints
+ deriving (Eq)
+
+{- Note [TcSMode]
+~~~~~~~~~~~~~~~~~
+The constraint solver can operate in different modes:
+
+* TcSVanilla: Normal constraint solving mode. This is the default.
+
+* TcSEarlyAbort: Abort (fail in the monad) as soon as we come across an
+ insoluble constraint. This is used to fail-fast when checking for hole-fits.
+ See Note [Speeding up valid hole-fits].
+
+* TcSFullySolve: Solve constraints fully or not at all. This is described in
+ Note [TcSFullySolve].
+
+ This mode is currently used in one place only: when solving constraints
+ arising from specialise pragmas.
+ See Note [Fully solving constraints for specialisation] in GHC.Tc.Gen.Sig.
+-}
+
data TcSEnv
= TcSEnv {
tcs_ev_binds :: EvBindsVar,
@@ -869,13 +936,11 @@ data TcSEnv
tcs_inerts :: IORef InertSet, -- Current inert set
- -- Whether to throw an exception if we come across an insoluble constraint.
- -- Used to fail-fast when checking for hole-fits. See Note [Speeding up
- -- valid hole-fits].
- tcs_abort_on_insoluble :: Bool,
+ -- | The mode of operation for the constraint solver.
+ -- See Note [TcSMode]
+ tcs_mode :: TcSMode,
- -- See Note [WorkList priorities] in GHC.Tc.Solver.InertSet
- tcs_worklist :: IORef WorkList -- Current worklist
+ tcs_worklist :: IORef WorkList
}
---------------
@@ -946,9 +1011,9 @@ addErrTcS = wrapTcS . TcM.addErr
panicTcS doc = pprPanic "GHC.Tc.Solver.Monad" doc
tryEarlyAbortTcS :: TcS ()
--- Abort (fail in the monad) if the abort_on_insoluble flag is on
+-- Abort (fail in the monad) if the mode is TcSEarlyAbort
tryEarlyAbortTcS
- = mkTcS (\env -> when (tcs_abort_on_insoluble env) TcM.failM)
+ = mkTcS (\env -> when (tcs_mode env == TcSEarlyAbort) TcM.failM)
-- | Emit a warning within the 'TcS' monad at the location given by the 'CtLoc'.
ctLocWarnTcS :: CtLoc -> TcRnMessage -> TcS ()
@@ -1018,7 +1083,60 @@ runTcS tcs
runTcSEarlyAbort :: TcS a -> TcM a
runTcSEarlyAbort tcs
= do { ev_binds_var <- TcM.newTcEvBinds
- ; runTcSWithEvBinds' True True ev_binds_var tcs }
+ ; runTcSWithEvBinds' True TcSEarlyAbort ev_binds_var tcs }
+
+-- | Run the 'TcS' monad in 'TcSFullySolve' mode, which either fully solves
+-- each individual constraint or leaves it alone. See Note [TcSFullySolve].
+runTcSFullySolve :: EvBindsVar -> TcS a -> TcM a
+runTcSFullySolve ev_binds_var tcs
+ = runTcSWithEvBinds' True TcSFullySolve ev_binds_var tcs
+
+{- Note [TcSFullySolve]
+~~~~~~~~~~~~~~~~~~~~~~~
+The TcSFullySolve mode is a specialized constraint solving mode that guarantees
+each constraint is either:
+ - Fully solved with no free evidence variables, or
+ - Left completely untouched (no simplification at all)
+
+Examples:
+
+ * [W] Eq [a].
+
+ In TcSFullySolve mode, we **do not** simplify this constraint to [W] Eq a,
+ using the top-level Eq instance; instead we leave it alone as [W] Eq [a].
+
+ * [W] forall x. Eq x => Eq (f x).
+
+ In TcSFullySolve mode, we **do not** process this quantified constraint by
+ creating a new implication constraint; we leave it alone instead.
+
+ * [W] Eq (Maybe Int).
+
+ This constraint is solved fully, using two top-level Eq instances.
+
+ * [W] forall x. Eq x => Eq [x].
+
+ This constraint is solved fully as well, using the Eq instance for lists.
+
+The main observation is that, in TcSFullySolve mode, we should not take any
+**irreversible** steps. We can't run instances in reverse, nor recover the
+original quantified constraint from the generated implication, so in these
+two cases (and these two cases only), in the solver, we call the special
+function `solveCompletelyIfRequired`. This function recursively calls the
+solver but in TcSVanilla mode (i.e. full-blown solving, with no restrictions).
+If this recursive call manages to solve all the remaining constraints fully,
+then we proceed with that outcome (i.e. we continue with that inert set, etc).
+Otherwise, discard everything that happened in the recursive call, and continue
+with the original constraint unchanged.
+
+This functionality is crucially used by the specialiser, for which such
+irreversible constraint solving steps are actively harmful, as described in
+Note [Fully solving constraints for specialisation] in GHC.Tc.Gen.Sig.
+
+In the future, we could consider re-using this functionality for the short-cut
+solver (see Note [Shortcut solving] in GHC.Tc.Solver.Dict), but we would have to
+be wary of the performance implications.
+-}
-- | This can deal only with equality constraints.
runTcSEqualities :: TcS a -> TcM a
@@ -1031,7 +1149,7 @@ runTcSEqualities thing_inside
runTcSInerts :: InertSet -> TcS a -> TcM (a, InertSet)
runTcSInerts inerts tcs = do
ev_binds_var <- TcM.newTcEvBinds
- runTcSWithEvBinds' False False ev_binds_var $ do
+ runTcSWithEvBinds' False TcSVanilla ev_binds_var $ do
setInertSet inerts
a <- tcs
new_inerts <- getInertSet
@@ -1040,17 +1158,17 @@ runTcSInerts inerts tcs = do
runTcSWithEvBinds :: EvBindsVar
-> TcS a
-> TcM a
-runTcSWithEvBinds = runTcSWithEvBinds' True False
+runTcSWithEvBinds = runTcSWithEvBinds' True TcSVanilla
-runTcSWithEvBinds' :: Bool -- ^ Restore type variable cycles afterwards?
+runTcSWithEvBinds' :: Bool -- True <=> restore type equality cycles
-- Don't if you want to reuse the InertSet.
-- See also Note [Type equality cycles]
-- in GHC.Tc.Solver.Equality
- -> Bool
+ -> TcSMode
-> EvBindsVar
-> TcS a
-> TcM a
-runTcSWithEvBinds' restore_cycles abort_on_insoluble ev_binds_var tcs
+runTcSWithEvBinds' restore_cycles mode ev_binds_var tcs
= do { unified_var <- TcM.newTcRef 0
; step_count <- TcM.newTcRef 0
; inert_var <- TcM.newTcRef emptyInert
@@ -1061,7 +1179,7 @@ runTcSWithEvBinds' restore_cycles abort_on_insoluble ev_binds_var tcs
, tcs_unif_lvl = unif_lvl_var
, tcs_count = step_count
, tcs_inerts = inert_var
- , tcs_abort_on_insoluble = abort_on_insoluble
+ , tcs_mode = mode
, tcs_worklist = wl_var }
-- Run the computation
@@ -1119,7 +1237,7 @@ nestImplicTcS ref inner_tclvl (TcS thing_inside)
, tcs_inerts = old_inert_var
, tcs_count = count
, tcs_unif_lvl = unif_lvl
- , tcs_abort_on_insoluble = abort_on_insoluble
+ , tcs_mode = mode
} ->
do { inerts <- TcM.readTcRef old_inert_var
; let nest_inert = inerts { inert_cycle_breakers = pushCycleBreakerVarStack
@@ -1134,7 +1252,7 @@ nestImplicTcS ref inner_tclvl (TcS thing_inside)
, tcs_ev_binds = ref
, tcs_unified = unified_var
, tcs_inerts = new_inert_var
- , tcs_abort_on_insoluble = abort_on_insoluble
+ , tcs_mode = mode
, tcs_worklist = new_wl_var }
; res <- TcM.setTcLevel inner_tclvl $
thing_inside nest_env
@@ -1149,7 +1267,7 @@ nestImplicTcS ref inner_tclvl (TcS thing_inside)
#endif
; return res }
-nestTcS :: TcS a -> TcS a
+nestTcS :: TcS a -> TcS a
-- Use the current untouchables, augmenting the current
-- evidence bindings, and solved dictionaries
-- But have no effect on the InertCans, or on the inert_famapp_cache
=====================================
compiler/GHC/Tc/Solver/Solve.hs
=====================================
@@ -1,3 +1,4 @@
+{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE RecursiveDo #-}
module GHC.Tc.Solver.Solve (
@@ -5,6 +6,7 @@ module GHC.Tc.Solver.Solve (
solveWanteds, -- Solves WantedConstraints
solveSimpleGivens, -- Solves [Ct]
solveSimpleWanteds, -- Solves Cts
+ solveCompletelyIfRequired,
setImplicationStatus
) where
@@ -51,6 +53,7 @@ import GHC.Driver.Session
import Data.List( deleteFirstsBy )
import Control.Monad
+import Data.Foldable ( for_ )
import qualified Data.Semigroup as S
import Data.Void( Void )
@@ -1217,6 +1220,12 @@ solveForAll ev@(CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_lo
-- This setSrcSpan is important: the emitImplicationTcS uses that
-- TcLclEnv for the implication, and that in turn sets the location
-- for the Givens when solving the constraint (#21006)
+
+ -- We are about to do something irreversible (turning a quantified constraint
+ -- into an implication), so wrap the inner call in solveCompletelyIfRequired
+ -- to ensure we can roll back if we can't solve the implication fully.
+ -- See Note [TcSFullySolve] in GHC.Tc.Solver.Monad.
+ solveCompletelyIfRequired add_inert_wanted_qc $
do { let empty_subst = mkEmptySubst $ mkInScopeSet $
tyCoVarsOfTypes (pred:theta) `delVarSetList` tvs
is_qc = IsQC (ctLocOrigin loc)
@@ -1251,6 +1260,10 @@ solveForAll ev@(CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_lo
; stopWith ev "Wanted forall-constraint" }
where
+ add_inert_wanted_qc =
+ do { updInertIrreds (IrredCt ev IrredShapeReason)
+ ; stopWith ev "Wanted QC not fully solved"
+ }
-- Getting the size of the head is a bit horrible
-- because of the special treament for class predicates
get_size pred = case classifyPredType pred of
@@ -1298,7 +1311,7 @@ Note [Solving a Given forall-constraint]
For a Given constraint
[G] df :: forall ab. (Eq a, Ord b) => C x a b
we just add it to TcS's local InstEnv of known instances,
-via addInertForall. Then, if we look up (C x Int Bool), say,
+via addInertForAll. Then, if we look up (C x Int Bool), say,
we'll find a match in the InstEnv.
@@ -1539,3 +1552,123 @@ runTcPluginSolvers solvers all_cts
CtWanted {} -> (givens, (ev,ct):wanteds)
+--------------------------------------------------------------------------------
+
+-- | If the mode is 'TcSFullySolve', attempt to fully solve the Wanted
+-- constraints that arise from 'thing_inside'; returning whether this was
+-- successful.
+--
+-- If not in 'TcSFullySolve' mode, simply run 'thing_inside'.
+--
+-- See Note [TcSFullySolve] in GHC.Tc.Solver.Monad.
+solveCompletelyIfRequired :: TcS (StopOrContinue a) -> TcS (StopOrContinue a) -> TcS (StopOrContinue a)
+solveCompletelyIfRequired not_fully_solved_action (TcS thing_inside)
+ = TcS $ \ env@(TcSEnv { tcs_ev_binds = outer_ev_binds_var
+ , tcs_unified = outer_unified_var
+ , tcs_inerts = outer_inert_var
+ , tcs_count = outer_count
+ , tcs_mode = mode
+ }) ->
+ case mode of
+ TcSFullySolve ->
+ do { traceTc "solveCompletelyIfRequired {" empty
+ -- Create a fresh environment for the inner computation
+ ; outer_inerts <- TcM.readTcRef outer_inert_var
+ ; let (outer_givens, outer_wanteds) =
+ partitionInerts isGivenCt outer_inerts
+ -- Keep the ambient Given inerts, but drop the Wanteds.
+ ; new_inert_var <- TcM.newTcRef outer_givens
+ ; new_wl_var <- TcM.newTcRef emptyWorkList
+ ; new_ev_binds_var <- TcM.newTcEvBinds
+ ; new_unified_var <- TcM.newTcRef 0
+ ; new_count <- TcM.newTcRef 0
+ ; new_unif_lvl <- TcM.newTcRef Nothing
+
+ ; let
+ inner_env =
+ TcSEnv
+ -- KEY part: recur with TcSVanilla
+ { tcs_mode = TcSVanilla
+
+ -- Use new variables for the inner computation, because
+ -- we may want to discard its state entirely.
+ , tcs_count = new_count
+ , tcs_unif_lvl = new_unif_lvl
+ , tcs_ev_binds = new_ev_binds_var
+ , tcs_unified = new_unified_var
+ , tcs_inerts = new_inert_var
+ , tcs_worklist = new_wl_var
+ }
+ -- Run the inner computation
+ ; traceTc "solveCompletelyIfRequired thing_inside {{" empty
+ ; r <- thing_inside inner_env
+ ; wl <- TcM.readTcRef new_wl_var
+ ; traceTc "solveCompletelyIfRequired thing_inside }}" $
+ vcat [ text "work list:" <+> ppr wl ]
+
+ -- Now attempt to solve the resulting constraints using 'solveWanteds'
+ ; (implics, simples) <- unTcS getUnsolvedInerts2 inner_env
+ ; let wc = emptyWC { wc_simple = simples, wc_impl = implics }
+ ; traceTc "solveCompletelyIfRequired solveWanteds" $
+ vcat [ text "wc:" <+> ppr wc
+ ]
+ ; solved_wc <- unTcS (solveWanteds wc) inner_env
+
+ ; traceTc "solveCompletelyIfRequired solveWanteds done" $
+ vcat [ text "wc:" <+> ppr wc
+ , text "solved_wc:" <+> ppr solved_wc
+ , text "outer_givens:" <+> ppr outer_givens
+ , text "outer_wanteds:" <+> ppr outer_wanteds
+ ]
+
+ ; if isSolvedWC solved_wc
+ then
+ do { -- The constraint was fully solved. Continue with
+ -- the inner solved state.
+ ; traceTc "solveCompletelyIfRequired: fully solved }" $
+ vcat [ text "wc:" <+> ppr wc
+ , text "solved_wc:" <+> ppr solved_wc ]
+
+ -- Add new evidence bindings to the existing ones
+ ; inner_ev_binds <- TcM.getTcEvBindsMap new_ev_binds_var
+ ; outer_ev_binds <- TcM.getTcEvBindsMap outer_ev_binds_var
+ ; let merged_ev_binds = outer_ev_binds `unionEvBindMap` inner_ev_binds
+ ; TcM.setTcEvBindsMap outer_ev_binds_var merged_ev_binds
+
+ -- Use the new inert set, adding back on the outer Wanteds
+ ; new_inerts <- TcM.readTcRef new_inert_var
+ ; let combined_cans = (new_inerts `andInertSet` outer_wanteds)
+ ; traceTc "solveCompletelyIfRequired: fully solved }" $
+ vcat [ text "outer_ev_binds_var:" <+> ppr outer_ev_binds_var
+ , text "inner_ev_binds_var:" <+> ppr new_ev_binds_var
+ , text "outer_inerts" <+> ppr outer_inerts
+ , text "new_inerts" <+> ppr new_inerts
+ , text "combined_cans:" <+> ppr combined_cans
+ , text "inner_ev_binds:" <+> ppr inner_ev_binds
+ , text "outer_ev_binds:" <+> ppr outer_ev_binds
+ , text "merged_ev_binds:" <+> ppr merged_ev_binds
+ ]
+ ; TcM.writeTcRef outer_inert_var combined_cans
+
+ -- Update the outer unified, count, and unif_lvl variables
+ ; inner_unified <- TcM.readTcRef new_unified_var
+ ; inner_count <- TcM.readTcRef new_count
+ ; inner_unif_lvl <- TcM.readTcRef new_unif_lvl
+ ; TcM.updTcRef outer_unified_var (+ inner_unified)
+ ; TcM.updTcRef outer_count (+ inner_count)
+ ; for_ inner_unif_lvl $ \inner_lvl ->
+ unTcS (setUnificationFlag inner_lvl) env
+
+ -- No need to update the outer work list: the inner work list
+ -- is empty by now (after 'solveWanteds').
+ ; return r }
+ else
+ do { traceTc "solveCompletelyIfRequired: unsolved }" $
+ vcat [ text "wc:" <+> ppr wc
+ , text "solved_wc:" <+> ppr solved_wc ]
+ ; -- Failed to fully solve the constraint.
+ -- Discard the inner solver state and continue.
+ ; unTcS not_fully_solved_action env
+ } }
+ _notFullySolveMode ->
+ thing_inside env
=====================================
compiler/GHC/Tc/Solver/Solve.hs-boot
=====================================
@@ -0,0 +1,6 @@
+module GHC.Tc.Solver.Solve where
+
+import GHC.Tc.Solver.Monad (StopOrContinue, TcS)
+
+solveCompletelyIfRequired
+ :: TcS (StopOrContinue a) -> TcS (StopOrContinue a) -> TcS (StopOrContinue a)
=====================================
compiler/GHC/Tc/Types/Evidence.hs
=====================================
@@ -15,7 +15,7 @@ module GHC.Tc.Types.Evidence (
-- * Evidence bindings
TcEvBinds(..), EvBindsVar(..),
- EvBindMap(..), emptyEvBindMap, extendEvBinds,
+ EvBindMap(..), emptyEvBindMap, extendEvBinds, unionEvBindMap,
lookupEvBind, evBindMapBinds,
foldEvBindMap, nonDetStrictFoldEvBindMap,
filterEvBindMap,
=====================================
testsuite/tests/simplCore/should_compile/DsSpecPragmas.hs
=====================================
@@ -17,7 +17,6 @@ import Data.Proxy
f1 :: ( Num a, Eq b ) => a -> b -> Int
f1 _ _ = 111
-
-- Make sure we don't generate a rule with an LHS of the form
--
-- forall @e (d :: Eq e). f1 @[e] ($fEqList d) = ...
@@ -56,12 +55,18 @@ f3 z = z == z
--------------------------------------------------------------------------------
-f4 :: Monad m => a -> m a
+f4 :: (Eq a, Monad m) => a -> m a
f4 = return
-- Check we can deal with locally quantified variables in constraints,
-- in this case 'Monad (ST s)'.
-{-# SPECIALISE f4 :: b -> ST s b #-}
+{-# SPECIALISE f4 :: forall s b. Eq b => b -> ST s b #-}
+
+f4_qc :: (Eq a, forall m. Monad m => Monad (t m)) => t m a -> ()
+f4_qc _ = ()
+
+-- Like 'f4' but with a quantified constraint.
+{-# SPECIALISE f4_qc :: forall r n b. (forall m. Monad m => Monad (r m)) => r n Int -> () #-}
--------------------------------------------------------------------------------
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/dbffc28b11f274baacae30224397fa09dce0bbbb
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/dbffc28b11f274baacae30224397fa09dce0bbbb
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/20250307/9895b6e8/attachment-0001.html>
More information about the ghc-commits
mailing list