[Git][ghc/ghc][wip/T23923-mikolaj] Sketch the addition of DCoVarSet to UnivCo (#23923 (comment 543934))
Mikolaj Konarski (@Mikolaj)
gitlab at gitlab.haskell.org
Thu Jan 25 05:49:45 UTC 2024
Mikolaj Konarski pushed to branch wip/T23923-mikolaj at Glasgow Haskell Compiler / GHC
Commits:
b63e9414 by Mikolaj Konarski at 2024-01-25T06:49:21+01:00
Sketch the addition of DCoVarSet to UnivCo (#23923 (comment 543934))
- - - - -
20 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Coercion.hs-boot
- compiler/GHC/Core/Coercion/Opt.hs
- compiler/GHC/Core/FVs.hs
- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/TyCo/FVs.hs
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Core/TyCo/Subst.hs
- compiler/GHC/Core/TyCo/Tidy.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/CoreToIface.hs
- compiler/GHC/Iface/Rename.hs
- compiler/GHC/Iface/Syntax.hs
- compiler/GHC/Iface/Type.hs
- compiler/GHC/IfaceToCore.hs
- compiler/GHC/Tc/TyCl/Utils.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Types/Unique/DSet.hs
- compiler/GHC/Types/Var.hs
- compiler/GHC/Types/Var/Set.hs
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -43,7 +43,7 @@ module GHC.Core.Coercion (
mkNakedFunCo,
mkNakedForAllCo, mkForAllCo, mkHomoForAllCos,
mkPhantomCo,
- mkHoleCo, mkUnivCo, mkSubCo,
+ mkHoleCo, mkUnivCo, mkUnivCoCvs, mkSubCo,
mkAxiomInstCo, mkProofIrrelCo,
downgradeRole, mkAxiomRuleCo,
mkGReflRightCo, mkGReflLeftCo, mkCoherenceLeftCo, mkCoherenceRightCo,
@@ -149,6 +149,7 @@ import GHC.Types.Var.Set
import GHC.Types.Name hiding ( varName )
import GHC.Types.Basic
import GHC.Types.Unique
+import GHC.Types.Unique.DSet (emptyUniqDSet)
import GHC.Data.FastString
import GHC.Data.Pair
import GHC.Types.SrcLoc
@@ -1099,7 +1100,8 @@ mkUnbranchedAxInstLHS ax = mkAxInstLHS ax 0
mkHoleCo :: CoercionHole -> Coercion
mkHoleCo h = HoleCo h
--- | Make a universal coercion between two arbitrary types.
+-- | Make a universal coercion between two arbitrary types in the simple
+-- case where uc_fcvs is empty.
mkUnivCo :: UnivCoProvenance
-> Role -- ^ role of the built coercion, "r"
-> Type -- ^ t1 :: k1
@@ -1107,7 +1109,24 @@ mkUnivCo :: UnivCoProvenance
-> Coercion -- ^ :: t1 ~r t2
mkUnivCo prov role ty1 ty2
| ty1 `eqType` ty2 = mkReflCo role ty1
- | otherwise = UnivCo prov role ty1 ty2
+ | otherwise = UnivCo prov role ty1 ty2 emptyUniqDSet{-!!!-}
+-- !!! There are 19 occurrences of mkUnivCo. Shall I make them all take cvs
+-- and explicitly put emptyUniqDSet there and comment why it's correct?
+-- Regardless, I should go through all of them and verity it is correct,
+-- but about future GHC code, plugin writers? This is backward compat
+-- vs a forced change/review of a dogdy API element.
+
+-- | Make a universal coercion between two arbitrary types in the most
+-- general case with the 'DCoVarSet' argument.
+mkUnivCoCvs :: UnivCoProvenance
+ -> Role -- ^ role of the built coercion, "r"
+ -> Type -- ^ t1 :: k1
+ -> Type -- ^ t2 :: k2
+ -> DCoVarSet -- ^ !!! what's the comment here? "free coercion variables that a plugin made use of when constructing its proof"? anything more general?
+ -> Coercion -- ^ :: t1 ~r t2
+mkUnivCoCvs prov role ty1 ty2 cvs
+ | ty1 `eqType` ty2 = mkReflCo role ty1 -- !!! cvs not considered in this case?
+ | otherwise = UnivCo prov role ty1 ty2 cvs
-- | Create a symmetric version of the given 'Coercion' that asserts
-- equality between the same types but in the other "direction", so
@@ -1120,6 +1139,8 @@ mkSymCo co | isReflCo co = co
mkSymCo (SymCo co) = co
mkSymCo (SubCo (SymCo co)) = SubCo co
mkSymCo co = SymCo co
+-- !!! why is this case in !3792, but not on master branch? Just an optmization? Shall I include it? Are cvs unchanged in it? Similarly for mkSubCo.
+-- mkSymCo (UnivCo p r t1 t2 cvs) = UnivCo p r t2 t1 cvs
-- | Create a new 'Coercion' by composing the two given 'Coercion's transitively.
-- (co1 ; co2)
@@ -1269,8 +1290,8 @@ mkCoherenceRightCo r ty co co2
mkKindCo :: Coercion -> Coercion
mkKindCo co | Just (ty, _) <- isReflCo_maybe co = Refl (typeKind ty)
mkKindCo (GRefl _ _ (MCo co)) = co
-mkKindCo (UnivCo (PhantomProv h) _ _ _) = h
-mkKindCo (UnivCo (ProofIrrelProv h) _ _ _) = h
+mkKindCo (UnivCo (PhantomProv h) _ _ _ _) = h
+mkKindCo (UnivCo (ProofIrrelProv h) _ _ _ _) = h
mkKindCo co
| Pair ty1 ty2 <- coercionKind co
-- generally, calling coercionKind during coercion creation is a bad idea,
@@ -1394,11 +1415,11 @@ setNominalRole_maybe r co
pprPanic "setNominalRole_maybe: the coercion should already be nominal" (ppr co)
setNominalRole_maybe_helper (InstCo co arg)
= InstCo <$> setNominalRole_maybe_helper co <*> pure arg
- setNominalRole_maybe_helper (UnivCo prov _ co1 co2)
+ setNominalRole_maybe_helper (UnivCo prov _ co1 co2 cvs)
| case prov of PhantomProv _ -> False -- should always be phantom
ProofIrrelProv _ -> True -- it's always safe
PluginProv _ -> False -- who knows? This choice is conservative.
- = Just $ UnivCo prov Nominal co1 co2
+ = Just $ UnivCo prov Nominal co1 co2 cvs{-!!!-}
setNominalRole_maybe_helper _ = Nothing
-- | Make a phantom coercion between two types. The coercion passed
@@ -1520,9 +1541,9 @@ promoteCoercion co = case co of
AxiomInstCo {} -> mkKindCo co
AxiomRuleCo {} -> mkKindCo co
- UnivCo (PhantomProv kco) _ _ _ -> kco
- UnivCo (ProofIrrelProv kco) _ _ _ -> kco
- UnivCo (PluginProv _) _ _ _ -> mkKindCo co
+ UnivCo (PhantomProv kco) _ _ _ _cvs -> kco -- !!! is it fine to forget cvs?
+ UnivCo (ProofIrrelProv kco) _ _ _ _cvs -> kco
+ UnivCo (PluginProv _) _ _ _ _cvs -> mkKindCo co
SymCo g
-> mkSymCo (promoteCoercion g)
@@ -2340,8 +2361,8 @@ seqCo (FunCo r af1 af2 w co1 co2) = r `seq` af1 `seq` af2 `seq`
seqCo (CoVarCo cv) = cv `seq` ()
seqCo (HoleCo h) = coHoleCoVar h `seq` ()
seqCo (AxiomInstCo con ind cos) = con `seq` ind `seq` seqCos cos
-seqCo (UnivCo p r t1 t2)
- = seqProv p `seq` r `seq` seqType t1 `seq` seqType t2
+seqCo (UnivCo p r t1 t2 cvs)
+ = seqProv p `seq` r `seq` seqType t1 `seq` seqType t2 `seq` cvs `seq` () -- !!! no seqCo for a var set defined already elsewhere? What does "Sequencing on coercions" mean?
seqCo (SymCo co) = seqCo co
seqCo (TransCo co1 co2) = seqCo co1 `seq` seqCo co2
seqCo (SelCo n co) = n `seq` seqCo co
@@ -2405,7 +2426,7 @@ coercionLKind co
, ft_arg = go arg, ft_res = go res }
go (CoVarCo cv) = coVarLType cv
go (HoleCo h) = coVarLType (coHoleCoVar h)
- go (UnivCo _ _ ty1 _) = ty1
+ go (UnivCo _ _ ty1 _ _) = ty1
go (SymCo co) = coercionRKind co
go (TransCo co1 _) = go co1
go (LRCo lr co) = pickLR lr (splitAppTy (go co))
@@ -2466,7 +2487,7 @@ coercionRKind co
go (FunCo { fco_afr = af, fco_mult = mult, fco_arg = arg, fco_res = res})
{- See Note [FunCo] -} = FunTy { ft_af = af, ft_mult = go mult
, ft_arg = go arg, ft_res = go res }
- go (UnivCo _ _ _ ty2) = ty2
+ go (UnivCo _ _ _ ty2 _) = ty2
go (SymCo co) = coercionLKind co
go (TransCo _ co2) = go co2
go (LRCo lr co) = pickLR lr (splitAppTy (go co))
@@ -2576,7 +2597,7 @@ coercionRole = go
go (CoVarCo cv) = coVarRole cv
go (HoleCo h) = coVarRole (coHoleCoVar h)
go (AxiomInstCo ax _ _) = coAxiomRole ax
- go (UnivCo _ r _ _) = r
+ go (UnivCo _ r _ _ _) = r
go (SymCo co) = go co
go (TransCo co1 _co2) = go co1
go (SelCo SelForAll _co) = Nominal
=====================================
compiler/GHC/Core/Coercion.hs-boot
=====================================
@@ -10,6 +10,7 @@ import {-# SOURCE #-} GHC.Core.TyCon
import GHC.Types.Basic ( LeftOrRight )
import GHC.Core.Coercion.Axiom
import GHC.Types.Var
+import GHC.Types.Var.Set
import GHC.Data.Pair
import GHC.Utils.Misc
@@ -24,6 +25,7 @@ mkCoVarCo :: CoVar -> Coercion
mkAxiomInstCo :: CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion
mkPhantomCo :: Coercion -> Type -> Type -> Coercion
mkUnivCo :: UnivCoProvenance -> Role -> Type -> Type -> Coercion
+mkUnivCoCvs :: UnivCoProvenance -> Role -> Type -> Type -> DCoVarSet -> Coercion
mkSymCo :: Coercion -> Coercion
mkTransCo :: Coercion -> Coercion -> Coercion
mkSelCo :: HasDebugCallStack => CoSel -> Coercion -> Coercion
=====================================
compiler/GHC/Core/Coercion/Opt.hs
=====================================
@@ -24,6 +24,7 @@ import GHC.Core.Unify
import GHC.Types.Var
import GHC.Types.Var.Set
import GHC.Types.Var.Env
+import GHC.Types.Unique.DSet (emptyUniqDSet)
import GHC.Types.Unique.Set
import GHC.Data.Pair
@@ -351,9 +352,9 @@ opt_co4 env sym rep r (AxiomInstCo con ind cos)
cos)
-- Note that the_co does *not* have sym pushed into it
-opt_co4 env sym rep r (UnivCo prov _r t1 t2)
- = assert (r == _r )
- opt_univ env sym prov (chooseRole rep r) t1 t2
+opt_co4 env sym rep r (UnivCo prov _r t1 t2 cvs)
+ = assert (r == _r)
+ opt_univ env sym prov (chooseRole rep r) t1 t2 cvs
opt_co4 env sym rep r (TransCo co1 co2)
-- sym (g `o` h) = sym h `o` sym g
@@ -532,7 +533,7 @@ in GHC.Core.Coercion.
-- be a phantom, but the output sure will be.
opt_phantom :: LiftingContext -> SymFlag -> Coercion -> NormalCo
opt_phantom env sym co
- = opt_univ env sym (PhantomProv (mkKindCo co)) Phantom ty1 ty2
+ = opt_univ env sym (PhantomProv (mkKindCo co)) Phantom ty1 ty2 emptyUniqDSet{-!!!-}
where
Pair ty1 ty2 = coercionKind co
@@ -568,8 +569,8 @@ See #19509.
-}
opt_univ :: LiftingContext -> SymFlag -> UnivCoProvenance -> Role
- -> Type -> Type -> Coercion
-opt_univ env sym (PhantomProv h) _r ty1 ty2
+ -> Type -> Type -> DCoVarSet -> Coercion
+opt_univ env sym (PhantomProv h) _r ty1 ty2 _cvs{-!!!-}
| sym = mkPhantomCo h' ty2' ty1'
| otherwise = mkPhantomCo h' ty1' ty2'
where
@@ -577,7 +578,7 @@ opt_univ env sym (PhantomProv h) _r ty1 ty2
ty1' = substTy (lcSubstLeft env) ty1
ty2' = substTy (lcSubstRight env) ty2
-opt_univ env sym prov role oty1 oty2
+opt_univ env sym prov role oty1 oty2 cvs
| Just (tc1, tys1) <- splitTyConApp_maybe oty1
, Just (tc2, tys2) <- splitTyConApp_maybe oty2
, tc1 == tc2
@@ -607,7 +608,7 @@ opt_univ env sym prov role oty1 oty2
(env', tv1', eta') = optForAllCoBndr env sym tv1 eta
!(vis1', vis2') = swapSym sym (vis1, vis2)
in
- mkForAllCo tv1' vis1' vis2' eta' (opt_univ env' sym prov' role ty1 ty2')
+ mkForAllCo tv1' vis1' vis2' eta' (opt_univ env' sym prov' role ty1 ty2' cvs) -- !!! or (substDCoVarSet (lcTCvSubst env) cvs) ???
| Just (Bndr cv1 vis1, ty1) <- splitForAllForAllTyBinder_maybe oty1
, isCoVar cv1
@@ -628,7 +629,7 @@ opt_univ env sym prov role oty1 oty2
(env', cv1', eta') = optForAllCoBndr env sym cv1 eta
!(vis1', vis2') = swapSym sym (vis1, vis2)
in
- mkForAllCo cv1' vis1' vis2' eta' (opt_univ env' sym prov' role ty1 ty2')
+ mkForAllCo cv1' vis1' vis2' eta' (opt_univ env' sym prov' role ty1 ty2' cvs)
| otherwise
= let ty1 = substTyUnchecked (lcSubstLeft env) oty1
@@ -710,8 +711,8 @@ opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
= fireTransRule "TrPushInst" in_co1 in_co2 $
mkInstCo (opt_trans is co1 co2) ty1
-opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1)
- in_co2@(UnivCo p2 r2 _tyl2 tyr2)
+opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1 _cvs1{-!!!-})
+ in_co2@(UnivCo p2 r2 _tyl2 tyr2 _cvs2{-!!!-})
| Just prov' <- opt_trans_prov p1 p2
= assert (r1 == r2) $
fireTransRule "UnivCo" in_co1 in_co2 $
=====================================
compiler/GHC/Core/FVs.hs
=====================================
@@ -395,7 +395,7 @@ orphNamesOfCo (FunCo { fco_mult = co_mult, fco_arg = co1, fco_res = co2 })
`unionNameSet` orphNamesOfCo co2
orphNamesOfCo (CoVarCo _) = emptyNameSet
orphNamesOfCo (AxiomInstCo con _ cos) = orphNamesOfCoCon con `unionNameSet` orphNamesOfCos cos
-orphNamesOfCo (UnivCo p _ t1 t2) = orphNamesOfProv p `unionNameSet` orphNamesOfType t1
+orphNamesOfCo (UnivCo p _ t1 t2 _cvs{-!!!-}) = orphNamesOfProv p `unionNameSet` orphNamesOfType t1
`unionNameSet` orphNamesOfType t2
orphNamesOfCo (SymCo co) = orphNamesOfCo co
orphNamesOfCo (TransCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2
=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -2465,7 +2465,7 @@ lintCoercion co@(FunCo { fco_role = r, fco_afl = afl, fco_afr = afr
, text "res_co:" <+> ppr co2 ])
-- See Note [Bad unsafe coercion]
-lintCoercion co@(UnivCo prov r ty1 ty2)
+lintCoercion co@(UnivCo prov r ty1 ty2 cvs)
= do { ty1' <- lintType ty1
; ty2' <- lintType ty2
; let k1 = typeKind ty1'
@@ -2476,7 +2476,7 @@ lintCoercion co@(UnivCo prov r ty1 ty2)
&& isTYPEorCONSTRAINT k2)
(checkTypes ty1 ty2)
- ; return (UnivCo prov' r ty1' ty2') }
+ ; return (UnivCo prov' r ty1' ty2' cvs) } -- !!! shall I add and use checkTyCoVarInScope from !3792? If so, shall I use it also for the other constructors, as in !3792?
where
report s = hang (text $ "Unsafe coercion: " ++ s)
2 (vcat [ text "From:" <+> ppr ty1
=====================================
compiler/GHC/Core/TyCo/FVs.hs
=====================================
@@ -19,6 +19,7 @@ module GHC.Core.TyCo.FVs
tyCoVarsOfCoDSet,
tyCoFVsOfCo, tyCoFVsOfCos,
tyCoVarsOfCoList,
+ shallowCoVarsOfCosDSet,
almostDevoidCoVarOfCo,
@@ -48,7 +49,7 @@ module GHC.Core.TyCo.FVs
closeOverKinds,
-- * Raw materials
- Endo(..), runTyCoVars
+ TyCoAcc(..), Endo(..), runTyCoVars
) where
import GHC.Prelude
@@ -66,6 +67,7 @@ import GHC.Utils.FV
import GHC.Types.Var
import GHC.Types.Unique.FM
+import GHC.Types.Unique.DSet (emptyUniqDSet)
import GHC.Types.Unique.Set
import GHC.Types.Var.Set
@@ -281,6 +283,9 @@ runTyCoVars :: Endo TyCoVarSet -> TyCoVarSet
{-# INLINE runTyCoVars #-}
runTyCoVars f = appEndo f emptyVarSet
+type InScopeBndrs = TyCoVarSet
+newtype TyCoAcc acc = TCA' { runTCA :: InScopeBndrs -> acc -> acc }
+
{- *********************************************************************
* *
Deep free variables
@@ -446,6 +451,36 @@ deepCoVarFolder = TyCoFolder { tcf_view = noView
-- See Note [CoercionHoles and coercion free variables]
-- in GHC.Core.TyCo.Rep
+------- Same again, but for DCoVarSet ----------
+-- But this time the free vars are shallow
+shallowCoVarsOfCosDSet :: [Coercion] -> DCoVarSet
+shallowCoVarsOfCosDSet _cos = emptyUniqDSet -- !!! runTCA (shallow_dcv_cos cos) emptyVarSet emptyDVarSet
+
+{- TODO: !!! lots of other code and refactorings, partially bit-rotten, would need to be taken from !3792
+shallow_dcv_cos :: [Coercion] -> TyCoAcc DCoVarSet
+(_, _, _, shallow_dcv_cos) = foldTyCo shallowCoVarDSetFolder
+
+shallowCoVarDSetFolder :: TyCoFolder TyCoVarSet{-!!!-} (TyCoAcc DCoVarSet)
+shallowCoVarDSetFolder = TyCoFolder { tcf_view = noView
+ , tcf_tyvar = do_tyvar, tcf_covar = do_covar
+ , tcf_hole = do_hole, tcf_tycobinder = do_bndr }
+ where
+ do_tyvar _ = mempty
+ do_covar cv = shallowAddCoVarDSet cv
+
+ do_bndr tcv _vis fvs = extendInScope tcv fvs
+ do_hole hole = do_covar (coHoleCoVar hole)
+
+shallowAddCoVarDSet :: CoVar -> TyCoAcc DCoVarSet
+-- Add a variable to the free vars unless it is in the in-scope
+-- or is already in the in-scope set-
+shallowAddCoVarDSet cv = TCA add_it
+ where
+ add_it is acc | cv `elemVarSet` is = acc
+ | cv `elemDVarSet` acc = acc
+ | otherwise = acc `extendDVarSet` cv
+-}
+
{- *********************************************************************
* *
Closing over kinds
@@ -641,9 +676,10 @@ tyCoFVsOfCo (HoleCo h) fv_cand in_scope acc
= tyCoFVsOfCoVar (coHoleCoVar h) fv_cand in_scope acc
-- See Note [CoercionHoles and coercion free variables]
tyCoFVsOfCo (AxiomInstCo _ _ cos) fv_cand in_scope acc = tyCoFVsOfCos cos fv_cand in_scope acc
-tyCoFVsOfCo (UnivCo p _ t1 t2) fv_cand in_scope acc
+tyCoFVsOfCo (UnivCo p _ t1 t2 cvs) fv_cand in_scope acc
= (tyCoFVsOfProv p `unionFV` tyCoFVsOfType t1
- `unionFV` tyCoFVsOfType t2) fv_cand in_scope acc
+ `unionFV` tyCoFVsOfType t2
+ `unionFV` mkFVs (dVarSetElems cvs)) fv_cand in_scope acc
tyCoFVsOfCo (SymCo co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
tyCoFVsOfCo (TransCo co1 co2) fv_cand in_scope acc = (tyCoFVsOfCo co1 `unionFV` tyCoFVsOfCo co2) fv_cand in_scope acc
tyCoFVsOfCo (SelCo _ co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
@@ -696,10 +732,11 @@ almost_devoid_co_var_of_co (CoVarCo v) cv = v /= cv
almost_devoid_co_var_of_co (HoleCo h) cv = (coHoleCoVar h) /= cv
almost_devoid_co_var_of_co (AxiomInstCo _ _ cos) cv
= almost_devoid_co_var_of_cos cos cv
-almost_devoid_co_var_of_co (UnivCo p _ t1 t2) cv
+almost_devoid_co_var_of_co (UnivCo p _ t1 t2 cvs) cv
= almost_devoid_co_var_of_prov p cv
&& almost_devoid_co_var_of_type t1 cv
&& almost_devoid_co_var_of_type t2 cv
+ && not (cv `elemDVarSet` cvs)
almost_devoid_co_var_of_co (SymCo co) cv
= almost_devoid_co_var_of_co co cv
almost_devoid_co_var_of_co (TransCo co1 co2) cv
@@ -1112,7 +1149,7 @@ tyConsOfType ty
go_co (FunCo { fco_mult = m, fco_arg = a, fco_res = r })
= go_co m `unionUniqSets` go_co a `unionUniqSets` go_co r
go_co (AxiomInstCo ax _ args) = go_ax ax `unionUniqSets` go_cos args
- go_co (UnivCo p _ t1 t2) = go_prov p `unionUniqSets` go t1 `unionUniqSets` go t2
+ go_co (UnivCo p _ t1 t2 _cvs{-!!!-}) = go_prov p `unionUniqSets` go t1 `unionUniqSets` go t2
go_co (CoVarCo {}) = emptyUniqSet
go_co (HoleCo {}) = emptyUniqSet
go_co (SymCo co) = go_co co
@@ -1314,10 +1351,10 @@ occCheckExpand vs_to_avoid ty
go_co cxt (AxiomInstCo ax ind args) = do { args' <- mapM (go_co cxt) args
; return (AxiomInstCo ax ind args') }
- go_co cxt (UnivCo p r ty1 ty2) = do { p' <- go_prov cxt p
+ go_co cxt (UnivCo p r ty1 ty2 cvs) = do { p' <- go_prov cxt p
; ty1' <- go cxt ty1
; ty2' <- go cxt ty2
- ; return (UnivCo p' r ty1' ty2') }
+ ; return (UnivCo p' r ty1' ty2' cvs{-!!!-}) }
go_co cxt (SymCo co) = do { co' <- go_co cxt co
; return (SymCo co') }
go_co cxt (TransCo co1 co2) = do { co1' <- go_co cxt co1
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -1,4 +1,3 @@
-
{-# LANGUAGE DeriveDataTypeable #-}
{-# OPTIONS_HADDOCK not-home #-}
@@ -78,7 +77,7 @@ import {-# SOURCE #-} GHC.Core.Type( chooseFunTyFlag, typeKind, typeTypeOrConstr
-- friends:
import GHC.Types.Var
-import GHC.Types.Var.Set( elemVarSet )
+import GHC.Types.Var.Set( DCoVarSet, dVarSetElems, elemVarSet )
import GHC.Core.TyCon
import GHC.Core.Coercion.Axiom
@@ -885,7 +884,7 @@ data Coercion
| FunCo -- FunCo :: "e" -> N/P -> e -> e -> e
-- See Note [FunCo] for fco_afl, fco_afr
- { fco_role :: Role
+ { fco_role :: Role
, fco_afl :: FunTyFlag -- Arrow for coercionLKind
, fco_afr :: FunTyFlag -- Arrow for coercionRKind
, fco_mult :: CoercionN
@@ -912,10 +911,15 @@ data Coercion
-- The number coercions should match exactly the expectations
-- of the CoAxiomRule (i.e., the rule is fully saturated).
- | UnivCo UnivCoProvenance Role Type Type
- -- :: _ -> "e" -> _ -> _ -> e
+ | UnivCo -- :: _ -> "e" -> _ -> _ -> _ -> e
+ { uc_prov :: UnivCoProvenance
+ , uc_role :: Role
+ , uc_lhs :: Type
+ , uc_rhs :: Type
+ , uc_fcvs :: DCoVarSet }
| SymCo Coercion -- :: e -> e
+
| TransCo Coercion Coercion -- :: e -> e -> e
| SelCo CoSel Coercion -- See Note [SelCo]
@@ -1685,10 +1689,49 @@ Note that
co2 :: a2 ~ Bool
Here,
- co3 = UnivCo (ProofIrrelProv co5) Nominal (CoercionTy co1) (CoercionTy co2)
+ co3 = UnivCo (ProofIrrelProv co5) Nominal (CoercionTy co1) (CoercionTy co2) cvs
where
co5 :: (a1 ~ Bool) ~ (a2 ~ Bool)
co5 = TyConAppCo Nominal (~#) [<*>, <*>, co4, <Bool>]
+
+
+The importance of tracking free coercion variables
+--------------------------------------------------
+
+-- !!! Rewrite the below, explaining how plugins need the vars (any other reason to include it? future coersion zapping? any soundness issues apart of plugins?):
+
+It is vital that zapped coercions track their free coercion variables.
+To see why, consider this program:
+
+ data T a where
+ T1 :: Bool -> T Bool
+ T2 :: T Int
+
+ f :: T a -> a -> Bool
+ f = /\a (x:T a) (y:a).
+ case x of
+ T1 (c : a~Bool) (z : Bool) -> not (y |> c)
+ T2 -> True
+
+Now imagine that we zap the coercion `c`, replacing it with a generic UnivCo
+between `a` and Bool. If we didn't record the fact that this coercion was
+previously free in `c`, we may incorrectly float the expression `not (y |> c)`
+out of the case alternative which brings proof of `c` into scope. If this
+happened then `f T2 (I# 5)` would try to interpret `y` as a Bool, at
+which point we aren't far from a segmentation fault or much worse.
+
+Note that we don't need to track
+* the coercion's free *type* variables
+* coercion variables free in kinds (we only need the "shallow" free covars)
+
+This means that we may float past type variables which the original
+proof had as free variables. While surprising, this doesn't jeopardise
+the validity of the coercion, which only depends upon the scoping
+relative to the free coercion variables.
+
+(The free coercion variables are kept as a DCoVarSet in UnivCo,
+since these sets are included in interface files.)
+
-}
@@ -1833,8 +1876,9 @@ foldTyCo (TyCoFolder { tcf_view = view
go_co env (CoVarCo cv) = covar env cv
go_co env (AxiomInstCo _ _ args) = go_cos env args
go_co env (HoleCo hole) = cohole env hole
- go_co env (UnivCo p _ t1 t2) = go_prov env p `mappend` go_ty env t1
+ go_co env (UnivCo p _ t1 t2 cvs) = go_prov env p `mappend` go_ty env t1
`mappend` go_ty env t2
+ `mappend` go_cvs env (dVarSetElems cvs)
go_co env (SymCo co) = go_co env co
go_co env (TransCo c1 c2) = go_co env c1 `mappend` go_co env c2
go_co env (AxiomRuleCo _ cos) = go_cos env cos
@@ -1857,6 +1901,9 @@ foldTyCo (TyCoFolder { tcf_view = view
go_prov env (ProofIrrelProv co) = go_co env co
go_prov _ (PluginProv _) = mempty
+ go_cvs _ [] = mempty
+ go_cvs env (cv:cvs) = covar env cv `mappend` go_cvs env cvs
+
-- | A view function that looks through nothing.
noView :: Type -> Maybe Type
noView _ = Nothing
@@ -1908,7 +1955,8 @@ coercionSize (FunCo _ _ _ w c1 c2) = 1 + coercionSize c1 + coercionSize c2
coercionSize (CoVarCo _) = 1
coercionSize (HoleCo _) = 1
coercionSize (AxiomInstCo _ _ args) = 1 + sum (map coercionSize args)
-coercionSize (UnivCo p _ t1 t2) = 1 + provSize p + typeSize t1 + typeSize t2
+coercionSize (UnivCo p _ t1 t2 _)
+ = 1 + provSize p + typeSize t1 + typeSize t2
coercionSize (SymCo co) = 1 + coercionSize co
coercionSize (TransCo co1 co2) = 1 + coercionSize co1 + coercionSize co2
coercionSize (SelCo _ co) = 1 + coercionSize co
=====================================
compiler/GHC/Core/TyCo/Subst.hs
=====================================
@@ -41,7 +41,7 @@ module GHC.Core.TyCo.Subst
cloneTyVarBndr, cloneTyVarBndrs,
substVarBndr, substVarBndrs,
substTyVarBndr, substTyVarBndrs,
- substCoVarBndr,
+ substCoVarBndr, substDCoVarSet,
substTyVar, substTyVars, substTyVarToTyVar,
substTyCoVars,
substTyCoBndr, substForAllCoBndr,
@@ -56,7 +56,7 @@ import {-# SOURCE #-} GHC.Core.Type
import {-# SOURCE #-} GHC.Core.Coercion
( mkCoVarCo, mkKindCo, mkSelCo, mkTransCo
, mkNomReflCo, mkSubCo, mkSymCo
- , mkFunCo2, mkForAllCo, mkUnivCo
+ , mkFunCo2, mkForAllCo, mkUnivCoCvs
, mkAxiomInstCo, mkAppCo, mkGReflCo
, mkInstCo, mkLRCo, mkTyConAppCo
, mkCoercionType
@@ -895,8 +895,9 @@ subst_co subst co
go (FunCo r afl afr w co1 co2) = ((mkFunCo2 r afl afr $! go w) $! go co1) $! go co2
go (CoVarCo cv) = substCoVar subst cv
go (AxiomInstCo con ind cos) = mkAxiomInstCo con ind $! map go cos
- go (UnivCo p r t1 t2) = (((mkUnivCo $! go_prov p) $! r) $!
- (go_ty t1)) $! (go_ty t2)
+ go (UnivCo p r t1 t2 cvs)
+ = ((((mkUnivCoCvs $! go_prov p) $! r) $!
+ (go_ty t1)) $! (go_ty t2)) $! substDCoVarSet subst cvs
go (SymCo co) = mkSymCo $! (go co)
go (TransCo co1 co2) = (mkTransCo $! (go co1)) $! (go co2)
go (SelCo d co) = mkSelCo d $! (go co)
@@ -916,6 +917,12 @@ subst_co subst co
go_hole h@(CoercionHole { ch_co_var = cv })
= h { ch_co_var = updateVarType go_ty cv }
+-- | Perform a substitution within a 'DVarSet' of free variables.
+-- returning the shallow free coercion variables
+substDCoVarSet :: Subst -> DCoVarSet -> DCoVarSet
+substDCoVarSet subst cvs = shallowCoVarsOfCosDSet $ map (substCoVar subst) $
+ dVarSetElems cvs
+
substForAllCoBndr :: Subst -> TyCoVar -> KindCoercion
-> (Subst, TyCoVar, Coercion)
substForAllCoBndr subst
=====================================
compiler/GHC/Core/TyCo/Tidy.hs
=====================================
@@ -20,9 +20,11 @@ import GHC.Data.FastString
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.FVs (tyCoVarsOfTypesWellScoped, tyCoVarsOfTypeList)
+import GHC.Data.Maybe (orElse)
import GHC.Types.Name hiding (varName)
import GHC.Types.Var
import GHC.Types.Var.Env
+import GHC.Types.Var.Set
import GHC.Utils.Misc (strictMap)
import Data.List (mapAccumL)
@@ -238,8 +240,9 @@ tidyCo env@(_, subst) co
Just cv' -> CoVarCo cv'
go (HoleCo h) = HoleCo h
go (AxiomInstCo con ind cos) = AxiomInstCo con ind $! strictMap go cos
- go (UnivCo p r t1 t2) = (((UnivCo $! (go_prov p)) $! r) $!
- tidyType env t1) $! tidyType env t2
+ go (UnivCo p r t1 t2 cvs)
+ = ((((UnivCo $! (go_prov p)) $! r) $!
+ tidyType env t1) $! tidyType env t2) $! mapDVarSet go_cv cvs
go (SymCo co) = SymCo $! go co
go (TransCo co1 co2) = (TransCo $! go co1) $! go co2
go (SelCo d co) = SelCo d $! go co
@@ -249,6 +252,8 @@ tidyCo env@(_, subst) co
go (SubCo co) = SubCo $! go co
go (AxiomRuleCo ax cos) = AxiomRuleCo ax $ strictMap go cos
+ go_cv cv = lookupVarEnv subst cv `orElse` cv
+
go_prov (PhantomProv co) = PhantomProv $! go co
go_prov (ProofIrrelProv co) = ProofIrrelProv $! go co
go_prov p@(PluginProv _) = p
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -273,7 +273,7 @@ import GHC.Core.Coercion.Axiom
import {-# SOURCE #-} GHC.Core.Coercion
( mkNomReflCo, mkGReflCo, mkReflCo
, mkTyConAppCo, mkAppCo
- , mkForAllCo, mkFunCo2, mkAxiomInstCo, mkUnivCo
+ , mkForAllCo, mkFunCo2, mkAxiomInstCo, mkUnivCoCvs
, mkSymCo, mkTransCo, mkSelCo, mkLRCo, mkInstCo
, mkKindCo, mkSubCo, mkFunCo, funRole
, decomposePiCos, coercionKind
@@ -558,8 +558,8 @@ expandTypeSynonyms ty
= substCoVar subst cv
go_co subst (AxiomInstCo ax ind args)
= mkAxiomInstCo ax ind (map (go_co subst) args)
- go_co subst (UnivCo p r t1 t2)
- = mkUnivCo (go_prov subst p) r (go subst t1) (go subst t2)
+ go_co subst (UnivCo p r t1 t2 cvs)
+ = mkUnivCoCvs (go_prov subst p) r (go subst t1) (go subst t2) cvs
go_co subst (SymCo co)
= mkSymCo (go_co subst co)
go_co subst (TransCo co1 co2)
@@ -913,7 +913,8 @@ mapTyCo mapper
-> (go_ty (), go_tys (), go_co (), go_cos ())
{-# INLINE mapTyCoX #-} -- See Note [Specialising mappers]
-mapTyCoX :: Monad m => TyCoMapper env m
+mapTyCoX :: forall m env. Monad m
+ => TyCoMapper env m
-> ( env -> Type -> m Type
, env -> [Type] -> m [Type]
, env -> Coercion -> m Coercion
@@ -961,6 +962,7 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar
go_mco !_ MRefl = return MRefl
go_mco !env (MCo co) = MCo <$> (go_co env co)
+ go_co :: env -> Coercion -> m Coercion
go_co !env (Refl ty) = Refl <$> go_ty env ty
go_co !env (GRefl r ty mco) = mkGReflCo r <$> go_ty env ty <*> go_mco env mco
go_co !env (AppCo c1 c2) = mkAppCo <$> go_co env c1 <*> go_co env c2
@@ -968,8 +970,11 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar
<*> go_co env c1 <*> go_co env c2
go_co !env (CoVarCo cv) = covar env cv
go_co !env (HoleCo hole) = cohole env hole
- go_co !env (UnivCo p r t1 t2) = mkUnivCo <$> go_prov env p <*> pure r
+ go_co !env (UnivCo p r t1 t2 cvs) = mkUnivCoCvs <$> go_prov env p <*> pure r
<*> go_ty env t1 <*> go_ty env t2
+ <*> strictFoldDVarSet (do_cv env)
+ (return emptyDVarSet) cvs
+
go_co !env (SymCo co) = mkSymCo <$> go_co env co
go_co !env (TransCo c1 c2) = mkTransCo <$> go_co env c1 <*> go_co env c2
go_co !env (AxiomRuleCo r cos) = AxiomRuleCo r <$> go_cos env cos
@@ -1002,6 +1007,10 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar
go_prov !env (ProofIrrelProv co) = ProofIrrelProv <$> go_co env co
go_prov !_ p@(PluginProv _) = return p
+ do_cv :: env -> CoVar -> m DTyCoVarSet -> m DTyCoVarSet
+ do_cv env v mfvs = do { fvs <- mfvs
+ ; co <- covar env v
+ ; return (tyCoVarsOfCoDSet co `unionDVarSet` fvs) }
{- *********************************************************************
* *
=====================================
compiler/GHC/CoreToIface.hs
=====================================
@@ -88,6 +88,7 @@ import GHC.Utils.Panic
import GHC.Utils.Misc
import Data.Maybe ( isNothing, catMaybes )
+import Data.List ( partition )
{- Note [Avoiding space leaks in toIface*]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -298,9 +299,14 @@ toIfaceCoercionX fr co
go (SubCo co) = IfaceSubCo (go co)
go (AxiomRuleCo co cs) = IfaceAxiomRuleCo (coaxrName co) (map go cs)
go (AxiomInstCo c i cs) = IfaceAxiomInstCo (coAxiomName c) i (map go cs)
- go (UnivCo p r t1 t2) = IfaceUnivCo (go_prov p) r
+ go (UnivCo p r t1 t2 cvs)
+ = IfaceUnivCo (go_prov p) r
(toIfaceTypeX fr t1)
(toIfaceTypeX fr t2)
+ (map toIfaceCoVar bound_cvs) free_cvs
+ where
+ (free_cvs, bound_cvs) = partition (`elemVarSet` fr) (dVarSetElems cvs)
+
go co@(TyConAppCo r tc cos)
= assertPpr (isNothing (tyConAppFunCo_maybe r tc cos)) (ppr co) $
IfaceTyConAppCo r (toIfaceTyCon tc) (map go cos)
=====================================
compiler/GHC/Iface/Rename.hs
=====================================
@@ -676,8 +676,8 @@ rnIfaceCo (IfaceCoVarCo lcl) = IfaceCoVarCo <$> pure lcl
rnIfaceCo (IfaceHoleCo lcl) = IfaceHoleCo <$> pure lcl
rnIfaceCo (IfaceAxiomInstCo n i cs)
= IfaceAxiomInstCo <$> rnIfaceGlobal n <*> pure i <*> mapM rnIfaceCo cs
-rnIfaceCo (IfaceUnivCo s r t1 t2)
- = IfaceUnivCo s r <$> rnIfaceType t1 <*> rnIfaceType t2
+rnIfaceCo (IfaceUnivCo s r t1 t2 cvs fcvs)
+ = IfaceUnivCo s r <$> rnIfaceType t1 <*> rnIfaceType t2 <*> pure cvs{-!!!-} <*> pure fcvs{-!!!-}
rnIfaceCo (IfaceSymCo c)
= IfaceSymCo <$> rnIfaceCo c
rnIfaceCo (IfaceTransCo c1 c2)
=====================================
compiler/GHC/Iface/Syntax.hs
=====================================
@@ -1772,7 +1772,7 @@ freeNamesIfCoercion (IfaceCoVarCo _) = emptyNameSet
freeNamesIfCoercion (IfaceHoleCo _) = emptyNameSet
freeNamesIfCoercion (IfaceAxiomInstCo ax _ cos)
= unitNameSet ax &&& fnList freeNamesIfCoercion cos
-freeNamesIfCoercion (IfaceUnivCo p _ t1 t2)
+freeNamesIfCoercion (IfaceUnivCo p _ t1 t2 _cvs{-!!!-} _fcvs{-!!!-})
= freeNamesIfProv p &&& freeNamesIfType t1 &&& freeNamesIfType t2
freeNamesIfCoercion (IfaceSymCo c)
= freeNamesIfCoercion c
=====================================
compiler/GHC/Iface/Type.hs
=====================================
@@ -385,6 +385,7 @@ data IfaceCoercion
-- to use an IfaceLclName to distinguish them.
-- See Note [Adding built-in type families] in GHC.Builtin.Types.Literals
| IfaceUnivCo IfaceUnivCoProv Role IfaceType IfaceType
+ [IfLclName]{-!!!-} [Var]{-!!!-}
| IfaceSymCo IfaceCoercion
| IfaceTransCo IfaceCoercion IfaceCoercion
| IfaceSelCo CoSel IfaceCoercion
@@ -605,7 +606,8 @@ substIfaceType env ty
go_co (IfaceCoVarCo cv) = IfaceCoVarCo cv
go_co (IfaceHoleCo cv) = IfaceHoleCo cv
go_co (IfaceAxiomInstCo a i cos) = IfaceAxiomInstCo a i (go_cos cos)
- go_co (IfaceUnivCo prov r t1 t2) = IfaceUnivCo (go_prov prov) r (go t1) (go t2)
+ go_co (IfaceUnivCo prov r t1 t2 cvs fcvs)
+ = IfaceUnivCo (go_prov prov) r (go t1) (go t2) cvs{-!!!-} fcvs{-!!!-}
go_co (IfaceSymCo co) = IfaceSymCo (go_co co)
go_co (IfaceTransCo co1 co2) = IfaceTransCo (go_co co1) (go_co co2)
go_co (IfaceSelCo n co) = IfaceSelCo n (go_co co)
@@ -1867,10 +1869,11 @@ ppr_co _ (IfaceFreeCoVar covar) = ppr covar
ppr_co _ (IfaceCoVarCo covar) = ppr covar
ppr_co _ (IfaceHoleCo covar) = braces (ppr covar)
-ppr_co _ (IfaceUnivCo prov role ty1 ty2)
+ppr_co _ (IfaceUnivCo prov role ty1 ty2 cvs fcvs)
= text "Univ" <> (parens $
sep [ ppr role <+> pprIfaceUnivCoProv prov
- , dcolon <+> ppr ty1 <> comma <+> ppr ty2 ])
+ , dcolon <+> ppr ty1 <> comma <+> ppr ty2
+ , ppr cvs, ppr fcvs ])
ppr_co ctxt_prec (IfaceInstCo co ty)
= maybeParen ctxt_prec appPrec $
@@ -2178,12 +2181,14 @@ instance Binary IfaceCoercion where
put_ bh a
put_ bh b
put_ bh c
- put_ bh (IfaceUnivCo a b c d) = do
+ put_ bh (IfaceUnivCo a b c d cvs fcvs) = do
putByte bh 9
put_ bh a
put_ bh b
put_ bh c
put_ bh d
+ assertPpr (null fcvs) (ppr cvs $$ ppr fcvs) $
+ put_ bh cvs
put_ bh (IfaceSymCo a) = do
putByte bh 10
put_ bh a
@@ -2256,7 +2261,8 @@ instance Binary IfaceCoercion where
b <- get bh
c <- get bh
d <- get bh
- return $ IfaceUnivCo a b c d
+ e <- get bh
+ return $ IfaceUnivCo a b c d e []
10-> do a <- get bh
return $ IfaceSymCo a
11-> do a <- get bh
@@ -2342,7 +2348,7 @@ instance NFData IfaceCoercion where
IfaceCoVarCo f1 -> rnf f1
IfaceAxiomInstCo f1 f2 f3 -> rnf f1 `seq` rnf f2 `seq` rnf f3
IfaceAxiomRuleCo f1 f2 -> rnf f1 `seq` rnf f2
- IfaceUnivCo f1 f2 f3 f4 -> rnf f1 `seq` f2 `seq` rnf f3 `seq` rnf f4
+ IfaceUnivCo f1 f2 f3 f4 f5 f6 -> rnf f1 `seq` f2 `seq` rnf f3 `seq` rnf f4 `seq` rnf f5 `seq` rnf f6
IfaceSymCo f1 -> rnf f1
IfaceTransCo f1 f2 -> rnf f1 `seq` rnf f2
IfaceSelCo f1 f2 -> rnf f1 `seq` rnf f2
=====================================
compiler/GHC/IfaceToCore.hs
=====================================
@@ -1468,8 +1468,12 @@ tcIfaceCo = go
ForAllCo tv' visL visR k' <$> go c }
go (IfaceCoVarCo n) = CoVarCo <$> go_var n
go (IfaceAxiomInstCo n i cs) = AxiomInstCo <$> tcIfaceCoAxiom n <*> pure i <*> mapM go cs
- go (IfaceUnivCo p r t1 t2) = UnivCo <$> tcIfaceUnivCoProv p <*> pure r
- <*> tcIfaceType t1 <*> tcIfaceType t2
+ go (IfaceUnivCo p r t1 t2 cvs fcvs)
+ = assertPpr (null fcvs) (ppr fcvs) $ do
+ cvs' <- mapM tcIfaceLclId cvs
+ UnivCo <$> tcIfaceUnivCoProv p <*> pure r
+ <*> tcIfaceType t1 <*> tcIfaceType t2
+ <*> pure (mkDVarSet cvs')
go (IfaceSymCo c) = SymCo <$> go c
go (IfaceTransCo c1 c2) = TransCo <$> go c1
<*> go c2
=====================================
compiler/GHC/Tc/TyCl/Utils.hs
=====================================
@@ -144,7 +144,8 @@ synonymTyConsOfType ty
go_co (CoVarCo _) = emptyNameEnv
go_co (HoleCo {}) = emptyNameEnv
go_co (AxiomInstCo _ _ cs) = go_co_s cs
- go_co (UnivCo p _ ty ty') = go_prov p `plusNameEnv` go ty `plusNameEnv` go ty'
+ go_co (UnivCo p _ ty ty' _cvs)
+ = go_prov p `plusNameEnv` go ty `plusNameEnv` go ty'
go_co (SymCo co) = go_co co
go_co (TransCo co co') = go_co co `plusNameEnv` go_co co'
go_co (SelCo _ co) = go_co co
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -1557,9 +1557,11 @@ collect_cand_qtvs_co orig_ty cur_lvl bound = go_co
go_co dv (FunCo _ _ _ w co1 co2) = foldlM go_co dv [w, co1, co2]
go_co dv (AxiomInstCo _ _ cos) = foldlM go_co dv cos
go_co dv (AxiomRuleCo _ cos) = foldlM go_co dv cos
- go_co dv (UnivCo prov _ t1 t2) = do { dv1 <- go_prov dv prov
+ go_co dv (UnivCo prov _ t1 t2 cvs)
+ = do { dv1 <- go_prov dv prov
; dv2 <- collect_cand_qtvs orig_ty True cur_lvl bound dv1 t1
- ; collect_cand_qtvs orig_ty True cur_lvl bound dv2 t2 }
+ ; dv3 <- collect_cand_qtvs orig_ty True cur_lvl bound dv2 t2
+ ; strictFoldDVarSet zt_cv (return dv3) cvs }
go_co dv (SymCo co) = go_co dv co
go_co dv (TransCo co1 co2) = foldlM go_co dv [co1, co2]
go_co dv (SelCo _ co) = go_co dv co
@@ -1599,6 +1601,9 @@ collect_cand_qtvs_co orig_ty cur_lvl bound = go_co
is_bound tv = tv `elemVarSet` bound
+ zt_cv :: CoVar -> TcM CandidatesQTvs -> TcM CandidatesQTvs
+ zt_cv cv mdvs = do { dvs <- mdvs; go_cv dvs cv }
+
{- Note [Order of accumulation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
You might be tempted (like I was) to use unitDVarSet and mappend
=====================================
compiler/GHC/Types/Unique/DSet.hs
=====================================
@@ -33,7 +33,7 @@ module GHC.Types.Unique.DSet (
lookupUniqDSet,
uniqDSetToList,
partitionUniqDSet,
- mapUniqDSet
+ mapUniqDSet, strictFoldUniqDSet
) where
import GHC.Prelude
@@ -127,6 +127,10 @@ partitionUniqDSet p = coerce . partitionUDFM p . getUniqDSet
mapUniqDSet :: Uniquable b => (a -> b) -> UniqDSet a -> UniqDSet b
mapUniqDSet f = mkUniqDSet . map f . uniqDSetToList
+strictFoldUniqDSet :: (a -> r -> r) -> r -> UniqDSet a -> r
+strictFoldUniqDSet k r s = foldl' (\r e -> k e r) r $
+ uniqDSetToList s
+
-- Two 'UniqDSet's are considered equal if they contain the same
-- uniques.
instance Eq (UniqDSet a) where
=====================================
compiler/GHC/Types/Var.hs
=====================================
@@ -284,6 +284,9 @@ data ExportFlag -- See Note [ExportFlag on binders]
= NotExported -- ^ Not exported: may be discarded as dead code.
| Exported -- ^ Exported: kept alive
+instance NFData Var where
+ rnf x = seq x () {-!!!-}
+
{- Note [ExportFlag on binders]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
An ExportFlag of "Exported" on a top-level binder says "keep this
=====================================
compiler/GHC/Types/Var/Set.hs
=====================================
@@ -26,7 +26,7 @@ module GHC.Types.Var.Set (
nonDetStrictFoldVarSet,
-- * Deterministic Var set types
- DVarSet, DIdSet, DTyVarSet, DTyCoVarSet,
+ DVarSet, DIdSet, DTyVarSet, DCoVarSet, DTyCoVarSet,
-- ** Manipulating these sets
emptyDVarSet, unitDVarSet, mkDVarSet,
@@ -38,7 +38,7 @@ module GHC.Types.Var.Set (
isEmptyDVarSet, delDVarSet, delDVarSetList,
minusDVarSet,
nonDetStrictFoldDVarSet,
- filterDVarSet, mapDVarSet,
+ filterDVarSet, mapDVarSet, strictFoldDVarSet,
dVarSetMinusVarSet, anyDVarSet, allDVarSet,
transCloDVarSet,
sizeDVarSet, seqDVarSet,
@@ -232,6 +232,9 @@ type DIdSet = UniqDSet Id
-- | Deterministic Type Variable Set
type DTyVarSet = UniqDSet TyVar
+-- | Deterministic Coercion Variable Set
+type DCoVarSet = UniqDSet CoVar
+
-- | Deterministic Type or Coercion Variable Set
type DTyCoVarSet = UniqDSet TyCoVar
@@ -308,6 +311,9 @@ allDVarSet p = allUDFM p . getUniqDSet
mapDVarSet :: Uniquable b => (a -> b) -> UniqDSet a -> UniqDSet b
mapDVarSet = mapUniqDSet
+strictFoldDVarSet :: (a -> r -> r) -> r -> UniqDSet a -> r
+strictFoldDVarSet = strictFoldUniqDSet
+
filterDVarSet :: (Var -> Bool) -> DVarSet -> DVarSet
filterDVarSet = filterUniqDSet
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b63e941408566c9dd1895f1b0c6eae643fb2b0c0
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b63e941408566c9dd1895f1b0c6eae643fb2b0c0
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/20240125/7a5a3c73/attachment-0001.html>
More information about the ghc-commits
mailing list