[Git][ghc/ghc][wip/T24359] 4 commits: move updInertDicts, updInertIrreds
sheaf (@sheaf)
gitlab at gitlab.haskell.org
Fri Mar 7 13:11:06 UTC 2025
sheaf pushed to branch wip/T24359 at Glasgow Haskell Compiler / GHC
Commits:
63d03cf3 by sheaf at 2025-03-07T13:41:53+01:00
move updInertDicts, updInertIrreds
- - - - -
02627924 by sheaf at 2025-03-07T13:41:56+01:00
fix isEmptyWorkList
- - - - -
0d777eff by sheaf at 2025-03-07T13:42:16+01:00
fix EvVarsOfTerm
- - - - -
34f8b525 by sheaf at 2025-03-07T14:10:50+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
@@ -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)
{- *********************************************************************
@@ -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,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
=====================================
@@ -1,4 +1,5 @@
{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
@@ -24,6 +25,7 @@ module GHC.Tc.Solver.InertSet (
InertEqs,
foldTyEqs, delEq, findEq,
partitionInertEqs, partitionFunEqs,
+ partitionInerts, andInertSet,
foldFunEqs, addEqToCans,
-- * Inert Dicts
@@ -73,10 +75,11 @@ import GHC.Utils.Outputable
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 )
+import Data.Function ( on )
-import Control.Monad ( forM_ )
{-
************************************************************************
@@ -286,9 +289,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 +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"
@@ -2214,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/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,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,
@@ -843,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
}
---------------
@@ -920,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 ()
@@ -992,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
@@ -1005,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
@@ -1014,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
@@ -1035,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
@@ -1059,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
----------------------------
@@ -1097,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
@@ -1112,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
@@ -1127,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,37 +868,74 @@ 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
+ = transCloVarSetIO 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
-
-evVarsOfTerm :: EvTerm -> VarSet
-evVarsOfTerm (EvExpr e) = exprSomeFreeVars isEvVar e
+ = return needs
+
+-- | Compute the transitive closure of a set in a monad
+transCloVarSetIO :: (VarSet -> IO VarSet) -> VarSet -> IO VarSet
+transCloVarSetIO f vs
+ = do
+ vs' <- f vs
+ let vs_new = vs' `minusVarSet` vs
+ if isEmptyVarSet vs_new
+ then return vs
+ else do
+ vs_rest <- transCloVarSetIO f vs_new
+ return (vs `unionVarSet` vs_rest)
+
+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
=====================================
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/9a61f68527d79a21c09b09be09d336db459a6dc3...34f8b5253dd1c7c8bdfe80dcfb52b2a3ceef0a94
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/9a61f68527d79a21c09b09be09d336db459a6dc3...34f8b5253dd1c7c8bdfe80dcfb52b2a3ceef0a94
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/274586aa/attachment-0001.html>
More information about the ghc-commits
mailing list