[Git][ghc/ghc][wip/T24359] 2 commits: Add mapMaybeTM to TrieMap
sheaf (@sheaf)
gitlab at gitlab.haskell.org
Fri Mar 7 18:32:18 UTC 2025
sheaf pushed to branch wip/T24359 at Glasgow Haskell Compiler / GHC
Commits:
ca89d176 by sheaf at 2025-03-07T19:31:58+01:00
Add mapMaybeTM to TrieMap
- - - - -
30049b74 by sheaf at 2025-03-07T19:31:58+01:00
new plan from March 7
- - - - -
17 changed files:
- compiler/GHC/Cmm/Dataflow/Label.hs
- compiler/GHC/Core/Map/Expr.hs
- compiler/GHC/Core/Map/Type.hs
- compiler/GHC/Data/TrieMap.hs
- compiler/GHC/Stg/CSE.hs
- 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/Solver/Types.hs
- compiler/GHC/Tc/Types/Evidence.hs
- compiler/GHC/Types/Var/Env.hs
- testsuite/tests/simplCore/should_compile/DsSpecPragmas.hs
- testsuite/tests/simplCore/should_compile/DsSpecPragmas.stderr
Changes:
=====================================
compiler/GHC/Cmm/Dataflow/Label.hs
=====================================
@@ -63,6 +63,7 @@ module GHC.Cmm.Dataflow.Label
, mapToList
, mapFromList
, mapFromListWith
+ , mapMapMaybe
) where
import GHC.Prelude
@@ -280,6 +281,9 @@ mapFromList assocs = LM (M.fromList [(lblToUnique k, v) | (k, v) <- assocs])
mapFromListWith :: (v -> v -> v) -> [(Label, v)] -> LabelMap v
mapFromListWith f assocs = LM (M.fromListWith f [(lblToUnique k, v) | (k, v) <- assocs])
+mapMapMaybe :: (a -> Maybe b) -> LabelMap a -> LabelMap b
+mapMapMaybe f (LM m) = LM (M.mapMaybe f m)
+
-----------------------------------------------------------------------------
-- Instances
@@ -298,7 +302,8 @@ instance TrieMap LabelMap where
lookupTM k m = mapLookup k m
alterTM k f m = mapAlter f k m
foldTM k m z = mapFoldr k z m
- filterTM f m = mapFilter f m
+ filterTM f = mapFilter f
+ mapMaybeTM f = mapMapMaybe f
-----------------------------------------------------------------------------
-- FactBase
=====================================
compiler/GHC/Core/Map/Expr.hs
=====================================
@@ -122,6 +122,7 @@ instance TrieMap CoreMap where
alterTM k f (CoreMap m) = CoreMap (alterTM (deBruijnize k) f m)
foldTM k (CoreMap m) = foldTM k m
filterTM f (CoreMap m) = CoreMap (filterTM f m)
+ mapMaybeTM f (CoreMap m) = CoreMap (mapMaybeTM f m)
-- | @CoreMapG a@ is a map from @DeBruijn CoreExpr@ to @a at . The extended
-- key makes it suitable for recursive traversal, since it can track binders,
@@ -271,6 +272,7 @@ instance TrieMap CoreMapX where
alterTM = xtE
foldTM = fdE
filterTM = ftE
+ mapMaybeTM = mpE
--------------------------
ftE :: (a->Bool) -> CoreMapX a -> CoreMapX a
@@ -287,6 +289,20 @@ ftE f (CM { cm_var = cvar, cm_lit = clit
, cm_letr = fmap (fmap (filterTM f)) cletr, cm_case = fmap (filterTM f) ccase
, cm_ecase = fmap (filterTM f) cecase, cm_tick = fmap (filterTM f) ctick }
+mpE :: (a -> Maybe b) -> CoreMapX a -> CoreMapX b
+mpE f (CM { cm_var = cvar, cm_lit = clit
+ , cm_co = cco, cm_type = ctype
+ , cm_cast = ccast , cm_app = capp
+ , cm_lam = clam, cm_letn = cletn
+ , cm_letr = cletr, cm_case = ccase
+ , cm_ecase = cecase, cm_tick = ctick })
+ = CM { cm_var = mapMaybeTM f cvar, cm_lit = mapMaybeTM f clit
+ , cm_co = mapMaybeTM f cco, cm_type = mapMaybeTM f ctype
+ , cm_cast = fmap (mapMaybeTM f) ccast, cm_app = fmap (mapMaybeTM f) capp
+ , cm_lam = fmap (mapMaybeTM f) clam, cm_letn = fmap (fmap (mapMaybeTM f)) cletn
+ , cm_letr = fmap (fmap (mapMaybeTM f)) cletr, cm_case = fmap (mapMaybeTM f) ccase
+ , cm_ecase = fmap (mapMaybeTM f) cecase, cm_tick = fmap (mapMaybeTM f) ctick }
+
--------------------------
lookupCoreMap :: CoreMap a -> CoreExpr -> Maybe a
lookupCoreMap cm e = lookupTM e cm
@@ -409,6 +425,7 @@ instance TrieMap AltMap where
alterTM = xtA emptyCME
foldTM = fdA
filterTM = ftA
+ mapMaybeTM = mpA
instance Eq (DeBruijn CoreAlt) where
D env1 a1 == D env2 a2 = go a1 a2 where
@@ -446,3 +463,9 @@ fdA :: (a -> b -> b) -> AltMap a -> b -> b
fdA k m = foldTM k (am_deflt m)
. foldTM (foldTM k) (am_data m)
. foldTM (foldTM k) (am_lit m)
+
+mpA :: (a -> Maybe b) -> AltMap a -> AltMap b
+mpA f (AM { am_deflt = adeflt, am_data = adata, am_lit = alit })
+ = AM { am_deflt = mapMaybeTM f adeflt
+ , am_data = fmap (mapMaybeTM f) adata
+ , am_lit = fmap (mapMaybeTM f) alit }
=====================================
compiler/GHC/Core/Map/Type.hs
=====================================
@@ -96,6 +96,7 @@ instance TrieMap CoercionMap where
alterTM k f (CoercionMap m) = CoercionMap (alterTM (deBruijnize k) f m)
foldTM k (CoercionMap m) = foldTM k m
filterTM f (CoercionMap m) = CoercionMap (filterTM f m)
+ mapMaybeTM f (CoercionMap m) = CoercionMap (mapMaybeTM f m)
type CoercionMapG = GenMap CoercionMapX
newtype CoercionMapX a = CoercionMapX (TypeMapX a)
@@ -112,6 +113,7 @@ instance TrieMap CoercionMapX where
alterTM = xtC
foldTM f (CoercionMapX core_tm) = foldTM f core_tm
filterTM f (CoercionMapX core_tm) = CoercionMapX (filterTM f core_tm)
+ mapMaybeTM f (CoercionMapX core_tm) = CoercionMapX (mapMaybeTM f core_tm)
instance Eq (DeBruijn Coercion) where
D env1 co1 == D env2 co2
@@ -189,6 +191,7 @@ instance TrieMap TypeMapX where
alterTM = xtT
foldTM = fdT
filterTM = filterT
+ mapMaybeTM = mpT
instance Eq (DeBruijn Type) where
(==) = eqDeBruijnType
@@ -380,6 +383,7 @@ instance TrieMap TyLitMap where
alterTM = xtTyLit
foldTM = foldTyLit
filterTM = filterTyLit
+ mapMaybeTM = mpTyLit
emptyTyLitMap :: TyLitMap a
emptyTyLitMap = TLM { tlm_number = Map.empty, tlm_string = emptyUFM, tlm_char = Map.empty }
@@ -407,6 +411,10 @@ filterTyLit :: (a -> Bool) -> TyLitMap a -> TyLitMap a
filterTyLit f (TLM { tlm_number = tn, tlm_string = ts, tlm_char = tc })
= TLM { tlm_number = Map.filter f tn, tlm_string = filterUFM f ts, tlm_char = Map.filter f tc }
+mpTyLit :: (a -> Maybe b) -> TyLitMap a -> TyLitMap b
+mpTyLit f (TLM { tlm_number = tn, tlm_string = ts, tlm_char = tc })
+ = TLM { tlm_number = Map.mapMaybe f tn, tlm_string = mapMaybeUFM f ts, tlm_char = Map.mapMaybe f tc }
+
-------------------------------------------------
-- | @TypeMap a@ is a map from 'Type' to @a at . If you are a client, this
-- is the type you want. The keys in this map may have different kinds.
@@ -435,6 +443,7 @@ instance TrieMap TypeMap where
alterTM k f m = xtTT (deBruijnize k) f m
foldTM k (TypeMap m) = foldTM (foldTM k) m
filterTM f (TypeMap m) = TypeMap (fmap (filterTM f) m)
+ mapMaybeTM f (TypeMap m) = TypeMap (fmap (mapMaybeTM f) m)
foldTypeMap :: (a -> b -> b) -> b -> TypeMap a -> b
foldTypeMap k z m = foldTM k m z
@@ -479,6 +488,7 @@ instance TrieMap LooseTypeMap where
alterTM k f (LooseTypeMap m) = LooseTypeMap (alterTM (deBruijnize k) f m)
foldTM f (LooseTypeMap m) = foldTM f m
filterTM f (LooseTypeMap m) = LooseTypeMap (filterTM f m)
+ mapMaybeTM f (LooseTypeMap m) = LooseTypeMap (mapMaybeTM f m)
{-
************************************************************************
@@ -558,10 +568,13 @@ instance TrieMap BndrMap where
alterTM = xtBndr emptyCME
foldTM = fdBndrMap
filterTM = ftBndrMap
+ mapMaybeTM = mpBndrMap
fdBndrMap :: (a -> b -> b) -> BndrMap a -> b -> b
fdBndrMap f (BndrMap tm) = foldTM (foldTM f) tm
+mpBndrMap :: (a -> Maybe b) -> BndrMap a -> BndrMap b
+mpBndrMap f (BndrMap tm) = BndrMap (fmap (mapMaybeTM f) tm)
-- We need to use 'BndrMap' for 'Coercion', 'CoreExpr' AND 'Type', since all
-- of these data types have binding forms.
@@ -594,6 +607,7 @@ instance TrieMap VarMap where
alterTM = xtVar emptyCME
foldTM = fdVar
filterTM = ftVar
+ mapMaybeTM = mpVar
lkVar :: CmEnv -> Var -> VarMap a -> Maybe a
lkVar env v
@@ -619,9 +633,24 @@ ftVar :: (a -> Bool) -> VarMap a -> VarMap a
ftVar f (VM { vm_bvar = bv, vm_fvar = fv })
= VM { vm_bvar = filterTM f bv, vm_fvar = filterTM f fv }
+mpVar :: (a -> Maybe b) -> VarMap a -> VarMap b
+mpVar f (VM { vm_bvar = bv, vm_fvar = fv })
+ = VM { vm_bvar = mapMaybeTM f bv, vm_fvar = mapMaybeTM f fv }
+
-------------------------------------------------
lkDNamed :: NamedThing n => n -> DNameEnv a -> Maybe a
lkDNamed n env = lookupDNameEnv env (getName n)
xtDNamed :: NamedThing n => n -> XT a -> DNameEnv a -> DNameEnv a
xtDNamed tc f m = alterDNameEnv f m (getName tc)
+
+mpT :: (a -> Maybe b) -> TypeMapX a -> TypeMapX b
+mpT f (TM { tm_var = tvar, tm_app = tapp, tm_tycon = ttycon
+ , tm_forall = tforall, tm_tylit = tlit
+ , tm_coerce = tcoerce })
+ = TM { tm_var = mapMaybeTM f tvar
+ , tm_app = fmap (mapMaybeTM f) tapp
+ , tm_tycon = mapMaybeTM f ttycon
+ , tm_forall = fmap (mapMaybeTM f) tforall
+ , tm_tylit = mapMaybeTM f tlit
+ , tm_coerce = tcoerce >>= f }
=====================================
compiler/GHC/Data/TrieMap.hs
=====================================
@@ -69,7 +69,7 @@ class Functor m => TrieMap m where
lookupTM :: forall b. Key m -> m b -> Maybe b
alterTM :: forall b. Key m -> XT b -> m b -> m b
filterTM :: (a -> Bool) -> m a -> m a
-
+ mapMaybeTM :: (a -> Maybe b) -> m a -> m b
foldTM :: (a -> b -> b) -> m a -> b -> b
-- The unusual argument order here makes
-- it easy to compose calls to foldTM;
@@ -146,6 +146,7 @@ instance TrieMap IntMap.IntMap where
alterTM = xtInt
foldTM k m z = IntMap.foldr k z m
filterTM f m = IntMap.filter f m
+ mapMaybeTM f m = IntMap.mapMaybe f m
xtInt :: Int -> XT a -> IntMap.IntMap a -> IntMap.IntMap a
xtInt k f m = IntMap.alter f k m
@@ -157,6 +158,7 @@ instance Ord k => TrieMap (Map.Map k) where
alterTM k f m = Map.alter f k m
foldTM k m z = Map.foldr k z m
filterTM f m = Map.filter f m
+ mapMaybeTM f m = Map.mapMaybe f m
{-
@@ -233,6 +235,7 @@ instance forall key. Uniquable key => TrieMap (UniqDFM key) where
alterTM k f m = alterUDFM f m k
foldTM k m z = foldUDFM k z m
filterTM f m = filterUDFM f m
+ mapMaybeTM f m = mapMaybeUDFM f m
{-
************************************************************************
@@ -259,6 +262,7 @@ instance TrieMap m => TrieMap (MaybeMap m) where
alterTM = xtMaybe alterTM
foldTM = fdMaybe
filterTM = ftMaybe
+ mapMaybeTM = mpMaybe
instance TrieMap m => Foldable (MaybeMap m) where
foldMap = foldMapTM
@@ -281,6 +285,10 @@ ftMaybe :: TrieMap m => (a -> Bool) -> MaybeMap m a -> MaybeMap m a
ftMaybe f (MM { mm_nothing = mn, mm_just = mj })
= MM { mm_nothing = filterMaybe f mn, mm_just = filterTM f mj }
+mpMaybe :: TrieMap m => (a -> Maybe b) -> MaybeMap m a -> MaybeMap m b
+mpMaybe f (MM { mm_nothing = mn, mm_just = mj })
+ = MM { mm_nothing = mn >>= f, mm_just = mapMaybeTM f mj }
+
foldMaybe :: (a -> b -> b) -> Maybe a -> b -> b
foldMaybe _ Nothing b = b
foldMaybe k (Just a) b = k a b
@@ -314,6 +322,7 @@ instance TrieMap m => TrieMap (ListMap m) where
alterTM = xtList alterTM
foldTM = fdList
filterTM = ftList
+ mapMaybeTM = mpList
instance TrieMap m => Foldable (ListMap m) where
foldMap = foldMapTM
@@ -340,6 +349,10 @@ ftList :: TrieMap m => (a -> Bool) -> ListMap m a -> ListMap m a
ftList f (LM { lm_nil = mnil, lm_cons = mcons })
= LM { lm_nil = filterMaybe f mnil, lm_cons = fmap (filterTM f) mcons }
+mpList :: TrieMap m => (a -> Maybe b) -> ListMap m a -> ListMap m b
+mpList f (LM { lm_nil = mnil, lm_cons = mcons })
+ = LM { lm_nil = mnil >>= f, lm_cons = fmap (mapMaybeTM f) mcons }
+
{-
************************************************************************
* *
@@ -395,6 +408,7 @@ instance (Eq (Key m), TrieMap m) => TrieMap (GenMap m) where
alterTM = xtG
foldTM = fdG
filterTM = ftG
+ mapMaybeTM = mpG
instance (Eq (Key m), TrieMap m) => Foldable (GenMap m) where
foldMap = foldMapTM
@@ -457,3 +471,11 @@ ftG f input@(SingletonMap _ v)
ftG f (MultiMap m) = MultiMap (filterTM f m)
-- we don't have enough information to reconstruct the key to make
-- a SingletonMap
+
+{-# INLINEABLE mpG #-}
+mpG :: TrieMap m => (a -> Maybe b) -> GenMap m a -> GenMap m b
+mpG _ EmptyMap = EmptyMap
+mpG f (SingletonMap k v) = case f v of
+ Just v' -> SingletonMap k v'
+ Nothing -> EmptyMap
+mpG f (MultiMap m) = MultiMap (mapMaybeTM f m)
=====================================
compiler/GHC/Stg/CSE.hs
=====================================
@@ -142,6 +142,8 @@ instance TrieMap StgArgMap where
foldTM k m = foldTM k (sam_var m) . foldTM k (sam_lit m)
filterTM f (SAM {sam_var = varm, sam_lit = litm}) =
SAM { sam_var = filterTM f varm, sam_lit = filterTM f litm }
+ mapMaybeTM f (SAM {sam_var = varm, sam_lit = litm}) =
+ SAM { sam_var = mapMaybeTM f varm, sam_lit = mapMaybeTM f litm }
newtype ConAppMap a = CAM { un_cam :: DNameEnv (ListMap StgArgMap a) }
@@ -158,6 +160,7 @@ instance TrieMap ConAppMap where
m { un_cam = un_cam m |> xtDNamed dataCon |>> alterTM args f }
foldTM k = un_cam >.> foldTM (foldTM k)
filterTM f = un_cam >.> fmap (filterTM f) >.> CAM
+ mapMaybeTM f = un_cam >.> fmap (mapMaybeTM f) >.> CAM
-----------------
-- The CSE Env --
=====================================
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
=====================================
@@ -231,7 +231,7 @@ simplifyAndEmitFlatConstraints wanted
-- it's OK to use unkSkol | we must increase the TcLevel,
-- because we don't bind | as explained in
-- any skolem variables here | Note [Wrapping failing kind equalities]
- ; emitImplication implic
+ ; TcM.emitImplication implic
; failM }
Just (simples, errs)
-> do { _ <- promoteTyVarSet (tyCoVarsOfCts simples)
=====================================
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 (Right dict_ct) $
+ 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,8 @@ module GHC.Tc.Solver.InertSet (
InertEqs,
foldTyEqs, delEq, findEq,
partitionInertEqs, partitionFunEqs,
+ filterInertEqs, filterFunEqs,
+ inertGivens,
foldFunEqs, addEqToCans,
-- * Inert Dicts
@@ -78,7 +80,6 @@ import Control.Monad ( forM_ )
import Data.List.NonEmpty ( NonEmpty(..), (<|) )
import Data.Function ( on )
-
{-
************************************************************************
* *
@@ -391,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"
@@ -1378,6 +1378,17 @@ addInertEqs :: EqCt -> InertEqs -> InertEqs
addInertEqs eq_ct@(EqCt { eq_lhs = TyVarLHS tv }) eqs = addTyEq eqs tv eq_ct
addInertEqs other _ = pprPanic "extendInertEqs" (ppr other)
+-- | Filter InertEqs according to a predicate
+filterInertEqs :: (EqCt -> Bool) -> InertEqs -> InertEqs
+filterInertEqs f = mapMaybeDVarEnv g
+ where
+ g xs =
+ let filtered = filter f xs
+ in
+ if null filtered
+ then Nothing
+ else Just filtered
+
------------------------
addCanFunEq :: InertFunEqs -> TyCon -> [TcType] -> EqCt -> InertFunEqs
@@ -1401,7 +1412,16 @@ addFunEqs eq_ct@(EqCt { eq_lhs = TyFamLHS tc args }) fun_eqs
= addCanFunEq fun_eqs tc args eq_ct
addFunEqs other _ = pprPanic "extendFunEqs" (ppr other)
-
+-- | Filter entries in InertFunEqs that satisfy the predicate
+filterFunEqs :: (EqCt -> Bool) -> InertFunEqs -> InertFunEqs
+filterFunEqs f = mapMaybeTcAppMap g
+ where
+ g xs =
+ let filtered = filter f xs
+ in
+ if null filtered
+ then Nothing
+ else Just filtered
{- *********************************************************************
* *
@@ -2215,3 +2235,44 @@ 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.)
-}
+
+{- *********************************************************************
+* *
+ Extracting Givens from the inert set
+* *
+********************************************************************* -}
+
+
+-- | Extract only Given constraints from the inert set.
+inertGivens :: InertSet -> InertSet
+inertGivens is@(IS { inert_cans = cans }) =
+ is { inert_cans = givens_cans
+ , inert_solved_dicts = emptyDictMap
+ }
+ where
+
+ isGivenEq :: EqCt -> Bool
+ isGivenEq eq = isGiven (ctEvidence (CEqCan eq))
+ isGivenDict :: DictCt -> Bool
+ isGivenDict dict = isGiven (ctEvidence (CDictCan dict))
+ isGivenIrred :: IrredCt -> Bool
+ isGivenIrred irred = isGiven (ctEvidence (CIrredCan irred))
+
+ -- Filter the inert constraints for Givens
+ (eq_givens_list, _) = partitionInertEqs isGivenEq (inert_eqs cans)
+ (funeq_givens_list, _) = partitionFunEqs isGivenEq (inert_funeqs cans)
+ dict_givens = filterDicts isGivenDict (inert_dicts cans)
+ safehask_givens = filterDicts isGivenDict (inert_safehask cans)
+ irreds_givens = filterBag isGivenIrred (inert_irreds cans)
+
+ eq_givens = foldr addInertEqs emptyTyEqs eq_givens_list
+ funeq_givens = foldr addFunEqs emptyFunEqs funeq_givens_list
+
+ givens_cans =
+ cans
+ { inert_eqs = eq_givens
+ , inert_funeqs = funeq_givens
+ , inert_dicts = dict_givens
+ , inert_safehask = safehask_givens
+ , inert_irreds = irreds_givens
+ }
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -14,11 +14,14 @@
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,
emitImplicationTcS, emitTvImplicationTcS,
+ emitImplication,
emitFunDepWanteds,
selectNextWorkItem,
@@ -210,6 +213,7 @@ 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 +709,7 @@ getUnsolvedInerts
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 +855,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 +899,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 +974,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 +1046,60 @@ runTcS tcs
runTcSEarlyAbort :: TcS a -> TcM a
runTcSEarlyAbort tcs
= do { ev_binds_var <- TcM.newTcEvBinds
- ; runTcSWithEvBinds' True True ev_binds_var tcs }
+ ; runTcSWithEvBinds' True TcSEarlyAbort ev_binds_var tcs }
+
+-- | Run the 'TcS' monad in 'TcSFullySolve' mode, which either fully solves
+-- each individual constraint or leaves it alone. See Note [TcSFullySolve].
+runTcSFullySolve :: EvBindsVar -> TcS a -> TcM a
+runTcSFullySolve ev_binds_var tcs
+ = runTcSWithEvBinds' True TcSFullySolve ev_binds_var tcs
+
+{- Note [TcSFullySolve]
+~~~~~~~~~~~~~~~~~~~~~~~
+The TcSFullySolve mode is a specialized constraint solving mode that guarantees
+each constraint is either:
+ - Fully solved with no free evidence variables, or
+ - Left completely untouched (no simplification at all)
+
+Examples:
+
+ * [W] Eq [a].
+
+ In TcSFullySolve mode, we **do not** simplify this constraint to [W] Eq a,
+ using the top-level Eq instance; instead we leave it alone as [W] Eq [a].
+
+ * [W] forall x. Eq x => Eq (f x).
+
+ In TcSFullySolve mode, we **do not** process this quantified constraint by
+ creating a new implication constraint; we leave it alone instead.
+
+ * [W] Eq (Maybe Int).
+
+ This constraint is solved fully, using two top-level Eq instances.
+
+ * [W] forall x. Eq x => Eq [x].
+
+ This constraint is solved fully as well, using the Eq instance for lists.
+
+The main observation is that, in TcSFullySolve mode, we should not take any
+**irreversible** steps. We can't run instances in reverse, nor recover the
+original quantified constraint from the generated implication, so in these
+two cases (and these two cases only), in the solver, we call the special
+function `solveCompletelyIfRequired`. This function recursively calls the
+solver but in TcSVanilla mode (i.e. full-blown solving, with no restrictions).
+If this recursive call manages to solve all the remaining constraints fully,
+then we proceed with that outcome (i.e. we continue with that inert set, etc).
+Otherwise, discard everything that happened in the recursive call, and continue
+with the original constraint unchanged.
+
+This functionality is crucially used by the specialiser, for which such
+irreversible constraint solving steps are actively harmful, as described in
+Note [Fully solving constraints for specialisation] in GHC.Tc.Gen.Sig.
+
+In the future, we could consider re-using this functionality for the short-cut
+solver (see Note [Shortcut solving] in GHC.Tc.Solver.Dict), but we would have to
+be wary of the performance implications.
+-}
-- | This can deal only with equality constraints.
runTcSEqualities :: TcS a -> TcM a
@@ -1031,7 +1112,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 +1121,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 +1142,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
@@ -1123,7 +1204,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 +1219,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 +1234,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_, traverse_ )
import qualified Data.Semigroup as S
import Data.Void( Void )
@@ -1217,6 +1220,12 @@ solveForAll ev@(CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_lo
-- This setSrcSpan is important: the emitImplicationTcS uses that
-- TcLclEnv for the implication, and that in turn sets the location
-- for the Givens when solving the constraint (#21006)
+
+ -- We are about to do something irreversible (turning a quantified constraint
+ -- into an implication), so wrap the inner call in solveCompletelyIfRequired
+ -- to ensure we can roll back if we can't solve the implication fully.
+ -- See Note [TcSFullySolve] in GHC.Tc.Solver.Monad.
+ solveCompletelyIfRequired (Left ev) $
do { let empty_subst = mkEmptySubst $ mkInScopeSet $
tyCoVarsOfTypes (pred:theta) `delVarSetList` tvs
is_qc = IsQC (ctLocOrigin loc)
@@ -1298,7 +1307,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 +1548,109 @@ 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 :: Either CtEvidence DictCt -> TcS (StopOrContinue a) -> TcS (StopOrContinue a)
+solveCompletelyIfRequired dict_or_qc (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 = inertGivens 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
+ }
+
+ -- Solve the constraint
+ ; let
+ ct = case dict_or_qc of
+ Left qci_ev -> mkNonCanonical qci_ev
+ Right dict_ct -> CDictCan dict_ct
+ wc = emptyWC { wc_simple = unitBag ct }
+ ; traceTc "solveCompletelyIfRequired solveWanteds" $
+ vcat [ text "ct:" <+> ppr ct
+ ]
+ ; solved_wc <- unTcS (solveWanteds wc) inner_env
+
+ ; if isSolvedWC solved_wc
+ then
+ do { -- The constraint was fully solved. Continue with
+ -- the inner solver state.
+ ; traceTc "solveCompletelyIfRequired: fully solved }" $
+ vcat [ text "ct:" <+> ppr ct
+ , 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
+
+ -- 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
+
+ -- Keep the outer inert set and work list: the inner work
+ -- list is empty, and there are no leftover unsolved
+ -- Wanteds.
+ -- However, we **must not** drop solved implications, due
+ -- to Note [Free vars of EvFun] in GHC.Tc.Types.Evidence.
+ ; traverse_ ( ( `unTcS` env ) . TcS.emitImplication ) $ wc_impl solved_wc
+ ; return $ Stop (ctEvidence ct) (text "Fully solved:" <+> ppr ct)
+ }
+ else
+ do { traceTc "solveCompletelyIfRequired: unsolved }" $
+ vcat [ text "ct:" <+> ppr ct
+ , text "solved_wc:" <+> ppr solved_wc ]
+ -- Failed to fully solve the constraint:
+ --
+ -- - discard the inner solver state,
+ -- - add the original constraint as an inert.
+ ; ( `unTcS` env ) $ case dict_or_qc of
+ Left qci_ev ->
+ updInertIrreds (IrredCt qci_ev IrredShapeReason)
+ Right dict_ct ->
+ updInertDicts dict_ct
+ ; return $ Stop (ctEvidence ct) (text "Not fully solved; kept as inert:" <+> ppr ct)
+ } }
+ _notFullySolveMode ->
+ thing_inside env
=====================================
compiler/GHC/Tc/Solver/Solve.hs-boot
=====================================
@@ -0,0 +1,11 @@
+module GHC.Tc.Solver.Solve where
+
+import GHC.Prelude
+ ( Either )
+import GHC.Tc.Solver.Monad
+ ( StopOrContinue, TcS )
+import GHC.Tc.Types.Constraint
+ ( CtEvidence, DictCt )
+
+solveCompletelyIfRequired
+ :: Either CtEvidence DictCt -> TcS (StopOrContinue a) -> TcS (StopOrContinue a)
=====================================
compiler/GHC/Tc/Solver/Types.hs
=====================================
@@ -14,6 +14,7 @@ module GHC.Tc.Solver.Types (
TcAppMap, emptyTcAppMap, isEmptyTcAppMap,
insertTcApp, alterTcApp, filterTcAppMap,
+ mapMaybeTcAppMap,
tcAppMapToBag, foldTcAppMap, delTcApp,
EqualCtList, filterEqualCtList, addToEqualCtList
@@ -114,6 +115,16 @@ filterTcAppMap f m = mapMaybeDTyConEnv one_tycon m
where
filtered_tm = filterTM f tm
+mapMaybeTcAppMap :: forall a b. (a -> Maybe b) -> TcAppMap a -> TcAppMap b
+mapMaybeTcAppMap f m = mapMaybeDTyConEnv one_tycon m
+ where
+ one_tycon :: ListMap LooseTypeMap a -> Maybe (ListMap LooseTypeMap b)
+ one_tycon tm
+ | isEmptyTM mapped_tm = Nothing
+ | otherwise = Just mapped_tm
+ where
+ mapped_tm = mapMaybeTM f tm
+
tcAppMapToBag :: TcAppMap a -> Bag a
tcAppMapToBag m = foldTcAppMap consBag m emptyBag
=====================================
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 }
+-- | Union two evidence binding maps
+unionEvBindMap :: EvBindMap -> EvBindMap -> EvBindMap
+unionEvBindMap (EvBindMap env1) (EvBindMap env2) =
+ EvBindMap { ev_bind_varenv = plusDVarEnv env1 env2 }
+
isEmptyEvBindMap :: EvBindMap -> Bool
isEmptyEvBindMap (EvBindMap m) = isEmptyDVarEnv m
=====================================
compiler/GHC/Types/Var/Env.hs
=====================================
@@ -74,7 +74,8 @@ module GHC.Types.Var.Env (
-- * TidyEnv and its operation
TidyEnv,
- emptyTidyEnv, mkEmptyTidyEnv, delTidyEnvList
+ emptyTidyEnv, mkEmptyTidyEnv, delTidyEnvList,
+ mapMaybeDVarEnv
) where
import GHC.Prelude
@@ -656,6 +657,9 @@ mapDVarEnv = mapUDFM
filterDVarEnv :: (a -> Bool) -> DVarEnv a -> DVarEnv a
filterDVarEnv = filterUDFM
+mapMaybeDVarEnv :: (a -> Maybe b) -> DVarEnv a -> DVarEnv b
+mapMaybeDVarEnv f = mapMaybeUDFM f
+
alterDVarEnv :: (Maybe a -> Maybe a) -> DVarEnv a -> Var -> DVarEnv a
alterDVarEnv = alterUDFM
=====================================
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 -> () #-}
--------------------------------------------------------------------------------
=====================================
testsuite/tests/simplCore/should_compile/DsSpecPragmas.stderr
=====================================
@@ -26,10 +26,17 @@
forall (@c) (df :: forall x. Eq x => Eq [x]) ($dEq :: Eq c).
f3 @c @[] $dEq df
= f3_$sf1 @c $dEq
-"USPEC f4 @(ST s) @_"
- forall (@b) (@s) ($dMonad :: Monad (ST s)).
- f4 @(ST s) @b $dMonad
+"USPEC f4 @_ @(ST s)"
+ forall (@s) (@b) ($dMonad :: Monad (ST s)) ($dEq :: Eq b).
+ f4 @b @(ST s) $dEq $dMonad
= $fApplicativeST_$cpure @s @b
+"USPEC f4_qc @Int @_ @_"
+ forall (@(n :: * -> *))
+ (@(r :: (* -> *) -> * -> *))
+ (df :: forall (m :: * -> *). Monad m => Monad (r m))
+ ($dEq :: Eq Int).
+ f4_qc @Int @r @n $dEq df
+ = \ _ [Occ=Dead] -> ()
"USPEC f5 @(D Int)"
forall ($dEq :: Eq (D Int)). f5 @(D Int) $dEq = f5_$sf5
"USPEC f5_qc @Int @D"
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/dbffc28b11f274baacae30224397fa09dce0bbbb...30049b74c302270ca4e0dfd18ef7eeaee815bd65
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/dbffc28b11f274baacae30224397fa09dce0bbbb...30049b74c302270ca4e0dfd18ef7eeaee815bd65
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/10c32ced/attachment-0001.html>
More information about the ghc-commits
mailing list