[Git][ghc/ghc][wip/T24359] 2 commits: Account for EvFun in evVarsOfTerm
sheaf (@sheaf)
gitlab at gitlab.haskell.org
Fri Mar 7 13:26:10 UTC 2025
sheaf pushed to branch wip/T24359 at Glasgow Haskell Compiler / GHC
Commits:
f9cec084 by sheaf at 2025-03-07T14:25:51+01:00
Account for EvFun in evVarsOfTerm
evVarsOfTerm used to return an empty set in the EvFun case. This was a hack that
worked around the fact that IO was required in order to collect bindings stored
within evidence binding variables. Note [Free vars of EvFun] (now deleted)
justified this behaviour with an explanation relating to bindings stored inside
implication constraints, but this is fragile and caused evidence bindings used
within EvFun bindings to be dropped in my work on implementing
[GHC proposal 493](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0493-specialise-expressions.rst)
- - - - -
e35aac40 by sheaf at 2025-03-07T14:25:52+01:00
new plan from March 7
- - - - -
10 changed files:
- compiler/GHC/Tc/Gen/Sig.hs
- compiler/GHC/Tc/Solver.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
- compiler/GHC/Types/Var/Set.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.hs
=====================================
@@ -70,6 +70,7 @@ import GHC.Data.Bag
import qualified GHC.LanguageExtensions as LangExt
import Control.Monad
+import Data.Functor.Identity (Identity(..))
import Data.List ( partition )
import GHC.Data.Maybe ( mapMaybe )
@@ -1909,7 +1910,7 @@ growThetaTyVars :: ThetaType -> TyCoVarSet -> TyCoVarSet
-- See Note [growThetaTyVars vs closeWrtFunDeps]
growThetaTyVars theta tcvs
| null theta = tcvs
- | otherwise = transCloVarSet mk_next seed_tcvs
+ | otherwise = runIdentity $ transCloVarSet (Identity . mk_next) seed_tcvs
where
seed_tcvs = tcvs `unionVarSet` tyCoVarsOfTypes ips
(ips, non_ips) = partition isIPLikePred theta
=====================================
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 [The shortcut solver] in GHC.Tc.Solver), 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
@@ -1085,29 +1203,25 @@ runTcSWithEvBinds' restore_cycles abort_on_insoluble ev_binds_var tcs
----------------------------
#if defined(DEBUG)
checkForCyclicBinds :: EvBindMap -> TcM ()
-checkForCyclicBinds ev_binds_map
- | null cycles
- = return ()
- | null coercion_cycles
- = TcM.traceTc "Cycle in evidence binds" $ ppr cycles
- | otherwise
- = pprPanic "Cycle in coercion bindings" $ ppr coercion_cycles
+checkForCyclicBinds ev_binds_map = do
+ edges <- liftIO $ traverse get_edge (bagToList $ evBindMapBinds ev_binds_map)
+ let cycles = [c | CyclicSCC c <- stronglyConnCompFromEdgedVerticesUniq edges]
+ coercion_cycles = [c | c <- cycles, any is_co_bind c]
+ is_co_bind (EvBind { eb_lhs = b }) = isEqPred (varType b)
+ if null cycles
+ then return ()
+ else if null coercion_cycles
+ then TcM.traceTc "Cycle in evidence binds" $ ppr cycles
+ else pprPanic "Cycle in coercion bindings" $ ppr coercion_cycles
where
- ev_binds = evBindMapBinds ev_binds_map
-
- cycles :: [[EvBind]]
- cycles = [c | CyclicSCC c <- stronglyConnCompFromEdgedVerticesUniq edges]
-
- coercion_cycles = [c | c <- cycles, any is_co_bind c]
- is_co_bind (EvBind { eb_lhs = b }) = isEqPred (varType b)
-
- edges :: [ Node EvVar EvBind ]
- edges = [ DigraphNode bind bndr (nonDetEltsUniqSet (evVarsOfTerm rhs))
- | bind@(EvBind { eb_lhs = bndr, eb_rhs = rhs}) <- bagToList ev_binds ]
- -- It's OK to use nonDetEltsUFM here as
- -- stronglyConnCompFromEdgedVertices is still deterministic even
- -- if the edges are in nondeterministic order as explained in
- -- Note [Deterministic SCC] in GHC.Data.Graph.Directed.
+ get_edge :: EvBind -> IO (Node EvVar EvBind)
+ get_edge bind@(EvBind { eb_lhs = bndr, eb_rhs = rhs}) = do
+ vars <- evVarsOfTerm rhs
+ return $ DigraphNode bind bndr (nonDetEltsUniqSet vars)
+ -- It's OK to use nonDetEltsUFM here as
+ -- stronglyConnCompFromEdgedVertices is still deterministic even
+ -- if the edges are in nondeterministic order as explained in
+ -- Note [Deterministic SCC] in GHC.Data.Graph.Directed.
#endif
----------------------------
@@ -1123,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
@@ -1138,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
@@ -1153,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 )
@@ -546,13 +549,13 @@ neededEvVars implic@(Implic { ic_given = givens
= do { ev_binds <- TcS.getTcEvBindsMap ev_binds_var
; tcvs <- TcS.getTcEvTyCoVars ev_binds_var
- ; let seeds1 = foldr add_implic_seeds old_needs implics
- seeds2 = nonDetStrictFoldEvBindMap add_wanted seeds1 ev_binds
- -- It's OK to use a non-deterministic fold here
- -- because add_wanted is commutative
- seeds3 = seeds2 `unionVarSet` tcvs
- need_inner = findNeededEvVars ev_binds seeds3
- live_ev_binds = filterEvBindMap (needed_ev_bind need_inner) ev_binds
+ ; let seeds1 = foldr add_implic_seeds old_needs implics
+ -- It's OK to use a non-deterministic fold here
+ -- because add_wanted is commutative
+ ; seeds2 <- wrapTcS $ foldEvBindMap add_wanted (pure seeds1) ev_binds
+ ; let seeds3 = seeds2 `unionVarSet` tcvs
+ ; need_inner <- liftIO $ findNeededEvVars ev_binds seeds3
+ ; let live_ev_binds = filterEvBindMap (needed_ev_bind need_inner) ev_binds
need_outer = varSetMinusEvBindMap need_inner live_ev_binds
`delVarSetList` givens
@@ -577,10 +580,10 @@ neededEvVars implic@(Implic { ic_given = givens
| EvBindGiven{} <- info = ev_var `elemVarSet` needed
| otherwise = True -- Keep all wanted bindings
- add_wanted :: EvBind -> VarSet -> VarSet
+ add_wanted :: EvBind -> TcM VarSet -> TcM VarSet
add_wanted (EvBind { eb_info = info, eb_rhs = rhs }) needs
| EvBindGiven{} <- info = needs -- Add the rhs vars of the Wanted bindings only
- | otherwise = evVarsOfTerm rhs `unionVarSet` needs
+ | otherwise = unionVarSet <$> liftIO (evVarsOfTerm rhs) <*> needs
-------------------------------------------------
simplifyDelayedErrors :: Bag DelayedError -> TcS (Bag DelayedError)
@@ -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,
@@ -79,14 +79,17 @@ import GHC.Utils.Outputable
import GHC.Data.Bag
import GHC.Data.FastString
-import qualified Data.Data as Data
import GHC.Types.SrcLoc
-import Data.IORef( IORef )
import GHC.Types.Unique.Set
import GHC.Core.Multiplicity
+import qualified Data.Data as Data
+
+import Control.Monad (foldM)
+import Data.IORef( IORef, readIORef )
import qualified Data.Semigroup as S
+
{-
Note [TcCoercions]
~~~~~~~~~~~~~~~~~~
@@ -433,6 +436,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
@@ -860,56 +868,68 @@ evTermCoercion tm = case evTermCoercion_maybe tm of
* *
********************************************************************* -}
-findNeededEvVars :: EvBindMap -> VarSet -> VarSet
+findNeededEvVars :: EvBindMap -> VarSet -> IO VarSet
-- Find all the Given evidence needed by seeds,
-- looking transitively through binds
findNeededEvVars ev_binds seeds
= transCloVarSet also_needs seeds
where
- also_needs :: VarSet -> VarSet
- also_needs needs = nonDetStrictFoldUniqSet add emptyVarSet needs
+ also_needs :: VarSet -> IO VarSet
+ also_needs needs = foldM add emptyVarSet (nonDetEltsUniqSet needs)
-- It's OK to use a non-deterministic fold here because we immediately
-- forget about the ordering by creating a set
- add :: Var -> VarSet -> VarSet
- add v needs
+ add :: VarSet -> Var -> IO VarSet
+ add needs v
| Just ev_bind <- lookupEvBind ev_binds v
, EvBind { eb_info = EvBindGiven, eb_rhs = rhs } <- ev_bind
- = evVarsOfTerm rhs `unionVarSet` needs
+ = do
+ rhs_vars <- evVarsOfTerm rhs
+ return (rhs_vars `unionVarSet` needs)
| otherwise
- = needs
+ = return needs
-evVarsOfTerm :: EvTerm -> VarSet
-evVarsOfTerm (EvExpr e) = exprSomeFreeVars isEvVar e
+evVarsOfTerm :: EvTerm -> IO VarSet
+evVarsOfTerm (EvExpr e) = pure $ exprSomeFreeVars isEvVar e
evVarsOfTerm (EvTypeable _ ev) = evVarsOfTypeable ev
-evVarsOfTerm (EvFun {}) = emptyVarSet -- See Note [Free vars of EvFun]
-
-evVarsOfTerms :: [EvTerm] -> VarSet
-evVarsOfTerms = mapUnionVarSet evVarsOfTerm
-
-evVarsOfTypeable :: EvTypeable -> VarSet
+evVarsOfTerm (EvFun { et_given = givens, et_binds = binds, et_body = body_id })
+ = do { rhs_binds <-
+ case binds of
+ TcEvBinds (EvBindsVar { ebv_binds = ev_binds_ref }) ->
+ eltsUDFM . ev_bind_varenv <$> readIORef ev_binds_ref
+ TcEvBinds (CoEvBindsVar {}) ->
+ pure []
+ EvBinds ev_bag ->
+ return $ bagToList ev_bag
+ ; let lhs_evvars = mkVarSet $ map eb_lhs rhs_binds
+ -- Get the RHS variables
+ ; rhs_evvars <- foldM (\acc bind -> do
+ vars <- evVarsOfTerm (eb_rhs bind)
+ pure (vars `unionVarSet` acc))
+ emptyVarSet rhs_binds
+ -- Variables needed by the body, excluding the given variables and LHS variables
+ ; let needed_vars = (unitVarSet body_id `unionVarSet` rhs_evvars)
+ `minusVarSet` mkVarSet givens
+ `minusVarSet` lhs_evvars
+ ; pure needed_vars }
+
+evVarsOfTerms :: [EvTerm] -> IO VarSet
+evVarsOfTerms [] = pure emptyVarSet
+evVarsOfTerms (t:ts) = do
+ vars1 <- evVarsOfTerm t
+ vars2 <- evVarsOfTerms ts
+ pure (vars1 `unionVarSet` vars2)
+
+evVarsOfTypeable :: EvTypeable -> IO VarSet
evVarsOfTypeable ev =
case ev of
- EvTypeableTyCon _ e -> mapUnionVarSet evVarsOfTerm e
+ EvTypeableTyCon _ e -> evVarsOfTerms e
EvTypeableTyApp e1 e2 -> evVarsOfTerms [e1,e2]
EvTypeableTrFun em e1 e2 -> evVarsOfTerms [em,e1,e2]
EvTypeableTyLit e -> evVarsOfTerm e
-{- Note [Free vars of EvFun]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Finding the free vars of an EvFun is made tricky by the fact the
-bindings et_binds may be a mutable variable. Fortunately, we
-can just squeeze by. Here's how.
-
-* evVarsOfTerm is used only by GHC.Tc.Solver.neededEvVars.
-* Each EvBindsVar in an et_binds field of an EvFun is /also/ in the
- ic_binds field of an Implication
-* So we can track usage via the processing for that implication,
- (see Note [Tracking redundant constraints] in GHC.Tc.Solver).
- We can ignore usage from the EvFun altogether.
-
-************************************************************************
+{- *********************************************************************
* *
Pretty printing
* *
=====================================
compiler/GHC/Types/Var/Set.hs
=====================================
@@ -168,31 +168,36 @@ fixVarSet fn vars
where
new_vars = fn vars
-transCloVarSet :: (VarSet -> VarSet)
- -- Map some variables in the set to
+-- | Compute the transitive closure of a set
+transCloVarSet :: forall m . Monad m
+ => (VarSet -> m VarSet)
+ -- ^ Map some variables in the set to
-- extra variables that should be in it
- -> VarSet -> VarSet
+ -> VarSet -> m VarSet
-- (transCloVarSet f s) repeatedly applies f to new candidates, adding any
-- new variables to s that it finds thereby, until it reaches a fixed point.
--
--- The function fn could be (Var -> VarSet), but we use (VarSet -> VarSet)
+-- The function fn could be (Var -> m VarSet), but we use (VarSet -> m VarSet)
-- for efficiency, so that the test can be batched up.
-- It's essential that fn will work fine if given new candidates
-- one at a time; ie fn {v1,v2} = fn v1 `union` fn v2
-- Use fixVarSet if the function needs to see the whole set all at once
-transCloVarSet fn seeds
- = go seeds seeds
+transCloVarSet fn seeds = go seeds seeds
where
go :: VarSet -- Accumulating result
-> VarSet -- Work-list; un-processed subset of accumulating result
- -> VarSet
+ -> m VarSet
-- Specification: go acc vs = acc `union` transClo fn vs
go acc candidates
- | isEmptyVarSet new_vs = acc
- | otherwise = go (acc `unionVarSet` new_vs) new_vs
- where
- new_vs = fn candidates `minusVarSet` acc
+ | isEmptyVarSet candidates = return acc
+ | otherwise = do
+ candidates' <- fn candidates
+ let new_vs = candidates' `minusVarSet` acc
+ if isEmptyVarSet new_vs
+ then return acc
+ else go (acc `unionVarSet` new_vs) new_vs
+{-# INLINEABLE transCloVarSet #-}
seqVarSet :: VarSet -> ()
seqVarSet s = s `seq` ()
=====================================
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/-/compare/34f8b5253dd1c7c8bdfe80dcfb52b2a3ceef0a94...e35aac40400eea45442a4315c97d1fba1f43edd0
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/34f8b5253dd1c7c8bdfe80dcfb52b2a3ceef0a94...e35aac40400eea45442a4315c97d1fba1f43edd0
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/fabd52d0/attachment-0001.html>
More information about the ghc-commits
mailing list