[Git][ghc/ghc][wip/T24359] new plan from March 7
sheaf (@sheaf)
gitlab at gitlab.haskell.org
Thu Mar 6 23:57:57 UTC 2025
sheaf pushed to branch wip/T24359 at Glasgow Haskell Compiler / GHC
Commits:
4a48dbec by sheaf at 2025-03-07T00:57:42+01:00
new plan from March 7
- - - - -
9 changed files:
- compiler/GHC/Tc/Gen/Sig.hs
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Solver/Irred.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
@@ -1029,38 +1029,22 @@ 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
; traceTc "tcSpecPrag SpecSigE }" $
@@ -1070,9 +1054,8 @@ 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
]
-- (5) Store the results in a SpecPragE record, which will be
@@ -1087,24 +1070,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)
{- *********************************************************************
@@ -101,26 +102,6 @@ solveDict dict_ct@(DictCt { di_ev = ev, di_cls = cls, di_tys = tys })
; simpleStage (updInertDicts dict_ct)
; stopWithStage (dictCtEvidence dict_ct) "Kept inert DictCt" }
-updInertDicts :: DictCt -> TcS ()
-updInertDicts dict_ct@(DictCt { di_cls = cls, di_ev = ev, di_tys = tys })
- = do { traceTcS "Adding inert dict" (ppr dict_ct $$ ppr cls <+> ppr tys)
-
- ; if | isGiven ev, Just (str_ty, _) <- isIPPred_maybe cls tys
- -> -- See (SIP1) and (SIP2) in Note [Shadowing of implicit parameters]
- -- Update /both/ inert_cans /and/ inert_solved_dicts.
- updInertSet $ \ inerts@(IS { inert_cans = ics, inert_solved_dicts = solved }) ->
- inerts { inert_cans = updDicts (filterDicts (not_ip_for str_ty)) ics
- , inert_solved_dicts = filterDicts (not_ip_for str_ty) solved }
- | otherwise
- -> return ()
-
- -- Add the new constraint to the inert set
- ; updInertCans (updDicts (addDict dict_ct)) }
- where
- not_ip_for :: Type -> DictCt -> Bool
- not_ip_for str_ty (DictCt { di_cls = cls, di_tys = tys })
- = not (mentionsIP str_ty cls tys)
-
canDictCt :: CtEvidence -> Class -> [Type] -> SolverStage DictCt
-- Once-only processing of Dict constraints:
-- * expand superclasses
@@ -868,7 +849,8 @@ shortCutSolver dflags ev_w ev_i
tryInstances :: DictCt -> SolverStage ()
tryInstances dict_ct
= Stage $ do { inerts <- getInertSet
- ; try_instances inerts dict_ct }
+ ; 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
=====================================
@@ -1,4 +1,5 @@
{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
@@ -16,6 +17,7 @@ module GHC.Tc.Solver.InertSet (
InertSet(..),
InertCans(..),
emptyInert,
+ partitionInerts, andInertSet,
noGivenNewtypeReprEqs, updGivenEqs,
prohibitedSuperClassSolve,
@@ -54,7 +56,7 @@ import GHC.Tc.Types.Constraint
import GHC.Tc.Types.Origin
import GHC.Tc.Types.CtLoc( CtLoc, ctLocOrigin, ctLocSpan, ctLocLevel )
import GHC.Tc.Solver.Types
-import GHC.Tc.Utils.TcType
+import GHC.Tc.Utils.TcType hiding () -- Make sure maxTcLevel is imported
import GHC.Types.Var
import GHC.Types.Var.Env
@@ -286,9 +288,9 @@ extendWorkListCts :: Cts -> WorkList -> WorkList
extendWorkListCts cts wl = foldr extendWorkListCt wl cts
isEmptyWorkList :: WorkList -> Bool
-isEmptyWorkList (WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X
+isEmptyWorkList (WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X, wl_rw_eqs = rw_eqs
, wl_rest = rest, wl_implics = implics })
- = null eqs_N && null eqs_X && null rest && isEmptyBag implics
+ = null eqs_N && null eqs_X && null rw_eqs && null rest && isEmptyBag implics
emptyWorkList :: WorkList
emptyWorkList = WL { wl_eqs_N = [], wl_eqs_X = []
@@ -390,7 +392,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"
@@ -2214,3 +2215,116 @@ 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 = filter qciPred (inert_insts cans)
+ insts_wanteds = filter (not . 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/Irred.hs
=====================================
@@ -39,10 +39,6 @@ solveIrred irred
; simpleStage (updInertIrreds irred)
; stopWithStage (irredCtEvidence irred) "Kept inert IrredCt" }
-updInertIrreds :: IrredCt -> TcS ()
-updInertIrreds irred
- = do { tc_lvl <- getTcLevel
- ; updInertCans $ addIrredToCans tc_lvl irred }
{- *********************************************************************
* *
=====================================
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,9 +73,10 @@ module GHC.Tc.Solver.Monad (
getInertEqs, getInertCans, getInertGivens,
getInertInsols, getInnermostGivenEqLevel,
getInertSet, setInertSet,
- getUnsolvedInerts,
+ getUnsolvedInerts, getUnsolvedInerts2,
removeInertCts, getPendingGivenScs,
insertFunEq, addInertForAll,
+ updInertDicts, updInertIrreds,
emitWorkNC, emitWork,
lookupInertDict,
@@ -202,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)
@@ -369,6 +373,31 @@ duplicates, is explained in Note [Use only the best matching quantified constrai
in GHC.Tc.Solver.Dict.
-}
+updInertDicts :: DictCt -> TcS ()
+updInertDicts dict_ct@(DictCt { di_cls = cls, di_ev = ev, di_tys = tys })
+ = do { traceTcS "Adding inert dict" (ppr dict_ct $$ ppr cls <+> ppr tys)
+
+ ; if | isGiven ev, Just (str_ty, _) <- isIPPred_maybe cls tys
+ -> -- See (SIP1) and (SIP2) in Note [Shadowing of implicit parameters]
+ -- Update /both/ inert_cans /and/ inert_solved_dicts.
+ updInertSet $ \ inerts@(IS { inert_cans = ics, inert_solved_dicts = solved }) ->
+ inerts { inert_cans = updDicts (filterDicts (not_ip_for str_ty)) ics
+ , inert_solved_dicts = filterDicts (not_ip_for str_ty) solved }
+ | otherwise
+ -> return ()
+
+ -- Add the new constraint to the inert set
+ ; updInertCans (updDicts (addDict dict_ct)) }
+ where
+ not_ip_for :: Type -> DictCt -> Bool
+ not_ip_for str_ty (DictCt { di_cls = cls, di_tys = tys })
+ = not (mentionsIP str_ty cls tys)
+
+updInertIrreds :: IrredCt -> TcS ()
+updInertIrreds irred
+ = do { tc_lvl <- getTcLevel
+ ; updInertCans $ addIrredToCans tc_lvl irred }
+
{- *********************************************************************
* *
Kicking out
@@ -579,7 +608,7 @@ getInertGivens :: TcS [Ct]
getInertGivens
= do { inerts <- getInertCans
; let all_cts = foldIrreds ((:) . CIrredCan) (inert_irreds inerts)
- $ foldDicts ((:) . CDictCan) (inert_dicts inerts)
+ $ foldDicts ((:) . CDictCan) (inert_dicts inerts)
$ foldFunEqs ((:) . CEqCan) (inert_funeqs inerts)
$ foldTyEqs ((:) . CEqCan) (inert_eqs inerts)
$ []
@@ -679,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
@@ -824,6 +892,27 @@ 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: Fully solve all constraints. This mode is not currently used
+ but is included for future extensions.
+-}
+
data TcSEnv
= TcSEnv {
tcs_ev_binds :: EvBindsVar,
@@ -843,13 +932,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
}
---------------
@@ -920,9 +1007,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 ()
@@ -992,7 +1079,15 @@ 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 attempts to fully solve all constraints.
+--
+-- See Note [Fully solving constraints for specialisation]
+runTcSFullySolve :: EvBindsVar -> TcS a -> TcM a
+runTcSFullySolve ev_binds_var tcs
+ = runTcSWithEvBinds' True TcSFullySolve ev_binds_var tcs
-- | This can deal only with equality constraints.
runTcSEqualities :: TcS a -> TcM a
@@ -1005,7 +1100,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
@@ -1014,17 +1109,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
@@ -1035,7 +1130,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
@@ -1097,7 +1192,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
@@ -1112,7 +1207,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
@@ -1127,7 +1222,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 )
@@ -1214,6 +1217,7 @@ solveForAll ev@(CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_lo
tvs theta pred _fuel
= -- See Note [Solving a Wanted forall-constraint]
TcS.setSrcSpan (getCtLocEnvLoc $ ctLocEnv loc) $
+ solveCompletelyIfRequired add_inert_wanted_qc $
-- 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)
@@ -1251,6 +1255,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 +1306,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 +1547,103 @@ 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'.
+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
+
+ ; 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
+ ; TcM.writeTcRef outer_inert_var (new_inerts `andInertSet` outer_wanteds)
+
+ -- 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,
@@ -433,6 +433,11 @@ extendEvBinds bs ev_bind
(eb_lhs ev_bind)
ev_bind }
+unionEvBindMap :: EvBindMap -> EvBindMap -> EvBindMap
+unionEvBindMap bs1 bs2
+ = EvBindMap { ev_bind_varenv = plusDVarEnv (ev_bind_varenv bs1)
+ (ev_bind_varenv bs2) }
+
isEmptyEvBindMap :: EvBindMap -> Bool
isEmptyEvBindMap (EvBindMap m) = isEmptyDVarEnv m
=====================================
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/4a48dbecf15ebd7f5d4dc80b63057cbb62e19c73
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/4a48dbecf15ebd7f5d4dc80b63057cbb62e19c73
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/20250306/3d37c7e7/attachment-0001.html>
More information about the ghc-commits
mailing list