[Git][ghc/ghc][wip/T23923-mikolaj-take-2] 2 commits: Add DCoVarSet to PluginProv
Mikolaj Konarski (@Mikolaj)
gitlab at gitlab.haskell.org
Fri Mar 8 00:20:33 UTC 2024
Mikolaj Konarski pushed to branch wip/T23923-mikolaj-take-2 at Glasgow Haskell Compiler / GHC
Commits:
70f2d3ee by Mikolaj Konarski at 2024-03-07T00:34:41+01:00
Add DCoVarSet to PluginProv
Add the only remaining piece of feedback from git add src/Flavour.hs
Help CI check some more of the patch
Fix the 3 plugin tests that fail
Explain better how shallowCoVarsOfCosDSet is entangled with a hundreds of lines bit-rotten refactoring
Fix according to the first round of Simon's instruction
Fix according to the second round of Simon's instruction
Remove a question-comment that's probably absurd
Fix according to the third round of Simon's instruction
- - - - -
053fdb81 by Mikolaj Konarski at 2024-03-07T00:34:41+01:00
Make sure the foldl' accumulators are strict
- - - - -
23 changed files:
- compiler/GHC/Core/Coercion.hs
- 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/Set.hs
- compiler/GHC/Utils/FV.hs
- docs/users_guide/extending_ghc.rst
- testsuite/tests/tcplugins/CtIdPlugin.hs
- testsuite/tests/tcplugins/RewritePlugin.hs
- testsuite/tests/tcplugins/TyFamPlugin.hs
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -97,7 +97,7 @@ module GHC.Core.Coercion (
emptyLiftingContext, extendLiftingContext, extendLiftingContextAndInScope,
liftCoSubstVarBndrUsing, isMappedByLC, extendLiftingContextCvSubst,
- mkSubstLiftingContext, zapLiftingContext,
+ mkSubstLiftingContext, liftingContextSubst, zapLiftingContext,
substForAllCoBndrUsingLC, lcLookupCoVar, lcInScopeSet,
LiftCoEnv, LiftingContext(..), liftEnvSubstLeft, liftEnvSubstRight,
@@ -1397,7 +1397,7 @@ setNominalRole_maybe r co
setNominalRole_maybe_helper (UnivCo prov _ co1 co2)
| case prov of PhantomProv _ -> False -- should always be phantom
ProofIrrelProv _ -> True -- it's always safe
- PluginProv _ -> False -- who knows? This choice is conservative.
+ PluginProv _ _ -> False -- who knows? This choice is conservative.
= Just $ UnivCo prov Nominal co1 co2
setNominalRole_maybe_helper _ = Nothing
@@ -1522,7 +1522,7 @@ promoteCoercion co = case co of
UnivCo (PhantomProv kco) _ _ _ -> kco
UnivCo (ProofIrrelProv kco) _ _ _ -> kco
- UnivCo (PluginProv _) _ _ _ -> mkKindCo co
+ UnivCo (PluginProv _ _) _ _ _ -> mkKindCo co
SymCo g
-> mkSymCo (promoteCoercion g)
@@ -1979,6 +1979,9 @@ mkLiftingContext pairs
mkSubstLiftingContext :: Subst -> LiftingContext
mkSubstLiftingContext subst = LC subst emptyVarEnv
+liftingContextSubst :: LiftingContext -> Subst
+liftingContextSubst (LC subst _) = subst
+
-- | Extend a lifting context with a new mapping.
extendLiftingContext :: LiftingContext -- ^ original LC
-> TyCoVar -- ^ new variable to map...
@@ -2354,7 +2357,7 @@ seqCo (AxiomRuleCo _ cs) = seqCos cs
seqProv :: UnivCoProvenance -> ()
seqProv (PhantomProv co) = seqCo co
seqProv (ProofIrrelProv co) = seqCo co
-seqProv (PluginProv _) = ()
+seqProv (PluginProv _ cvs) = seqDVarSet cvs
seqCos :: [Coercion] -> ()
seqCos [] = ()
=====================================
compiler/GHC/Core/Coercion/Opt.hs
=====================================
@@ -641,7 +641,7 @@ opt_univ env sym prov role oty1 oty2
where
prov' = case prov of
ProofIrrelProv kco -> ProofIrrelProv $ opt_co4_wrap env sym False Nominal kco
- PluginProv _ -> prov
+ PluginProv s cvs -> PluginProv s $ substDCoVarSet (liftingContextSubst env) cvs
-------------
opt_transList :: HasDebugCallStack => InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
@@ -722,7 +722,8 @@ opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1)
= Just $ PhantomProv $ opt_trans is kco1 kco2
opt_trans_prov (ProofIrrelProv kco1) (ProofIrrelProv kco2)
= Just $ ProofIrrelProv $ opt_trans is kco1 kco2
- opt_trans_prov (PluginProv str1) (PluginProv str2) | str1 == str2 = Just p1
+ opt_trans_prov (PluginProv str1 cvs1) (PluginProv str2 cvs2)
+ | str1 == str2 = Just (PluginProv str1 (cvs1 `unionDVarSet` cvs2))
opt_trans_prov _ _ = Nothing
-- Push transitivity down through matching top-level constructors.
=====================================
compiler/GHC/Core/FVs.hs
=====================================
@@ -410,7 +410,7 @@ orphNamesOfCo (HoleCo _) = emptyNameSet
orphNamesOfProv :: UnivCoProvenance -> NameSet
orphNamesOfProv (PhantomProv co) = orphNamesOfCo co
orphNamesOfProv (ProofIrrelProv co) = orphNamesOfCo co
-orphNamesOfProv (PluginProv _) = emptyNameSet
+orphNamesOfProv (PluginProv _ _) = emptyNameSet
orphNamesOfCos :: [Coercion] -> NameSet
orphNamesOfCos = orphNamesOfThings orphNamesOfCo
=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -1931,6 +1931,13 @@ checkTyCon :: TyCon -> LintM ()
checkTyCon tc
= checkL (not (isTcTyCon tc)) (text "Found TcTyCon:" <+> ppr tc)
+-------------------
+checkTyCoVarInScope :: Subst -> TyCoVar -> LintM ()
+checkTyCoVarInScope subst tcv
+ = checkL (tcv `isInScope` subst) $
+ hang (text "The type or coercion variable" <+> pprBndr LetBind tcv)
+ 2 (text "is out of scope")
+
-------------------
lintType :: Type -> LintM LintedType
@@ -1948,12 +1955,8 @@ lintType (TyVarTy tv)
-- In GHCi we may lint an expression with a free
-- type variable. Then it won't be in the
-- substitution, but it should be in scope
- Nothing | tv `isInScope` subst
- -> return (TyVarTy tv)
- | otherwise
- -> failWithL $
- hang (text "The type variable" <+> pprBndr LetBind tv)
- 2 (text "is out of scope")
+ Nothing -> do { checkTyCoVarInScope subst tv
+ ; return (TyVarTy tv) }
}
lintType ty@(AppTy t1 t2)
@@ -2325,15 +2328,8 @@ lintCoercion (CoVarCo cv)
= do { subst <- getSubst
; case lookupCoVar subst cv of
Just linted_co -> return linted_co ;
- Nothing
- | cv `isInScope` subst
- -> return (CoVarCo cv)
- | otherwise
- ->
- -- lintCoBndr always extends the substitution
- failWithL $
- hang (text "The coercion variable" <+> pprBndr LetBind cv)
- 2 (text "is out of scope")
+ Nothing -> do { checkTyCoVarInScope subst cv
+ ; return (CoVarCo cv) }
}
@@ -2532,7 +2528,12 @@ lintCoercion co@(UnivCo prov r ty1 ty2)
; check_kinds kco k1 k2
; return (ProofIrrelProv kco') }
- lint_prov _ _ prov@(PluginProv _) = return prov
+ lint_prov _ _ (PluginProv s cvs)
+ = do { subst <- getSubst
+ ; mapM_ (checkTyCoVarInScope subst) (dVarSetElems cvs)
+ -- Don't bother to return substituted fvs;
+ -- they don't matter to Lint
+ ; return (PluginProv s cvs) }
check_kinds kco k1 k2
= do { let Pair k1' k2' = coercionKind kco
=====================================
compiler/GHC/Core/TyCo/FVs.hs
=====================================
@@ -19,6 +19,7 @@ module GHC.Core.TyCo.FVs
tyCoVarsOfCoDSet,
tyCoFVsOfCo, tyCoFVsOfCos,
tyCoVarsOfCoList,
+ coVarsOfCosDSet,
almostDevoidCoVarOfCo,
@@ -446,6 +447,13 @@ 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
+
+coVarsOfCosDSet :: [Coercion] -> DCoVarSet
+coVarsOfCosDSet cos = fvDVarSetSome isCoVar (tyCoFVsOfCos cos)
+
+
{- *********************************************************************
* *
Closing over kinds
@@ -660,7 +668,7 @@ tyCoFVsOfCoVar v fv_cand in_scope acc
tyCoFVsOfProv :: UnivCoProvenance -> FV
tyCoFVsOfProv (PhantomProv co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
tyCoFVsOfProv (ProofIrrelProv co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
-tyCoFVsOfProv (PluginProv _) fv_cand in_scope acc = emptyFV fv_cand in_scope acc
+tyCoFVsOfProv (PluginProv _ cvs) fv_cand in_scope acc = mkFVs (dVarSetElems cvs) fv_cand in_scope acc
tyCoFVsOfCos :: [Coercion] -> FV
tyCoFVsOfCos [] fv_cand in_scope acc = emptyFV fv_cand in_scope acc
@@ -730,7 +738,7 @@ almost_devoid_co_var_of_prov (PhantomProv co) cv
= almost_devoid_co_var_of_co co cv
almost_devoid_co_var_of_prov (ProofIrrelProv co) cv
= almost_devoid_co_var_of_co co cv
-almost_devoid_co_var_of_prov (PluginProv _) _ = True
+almost_devoid_co_var_of_prov (PluginProv _ cvs) cv = not (cv `elemDVarSet` cvs)
almost_devoid_co_var_of_type :: Type -> CoVar -> Bool
almost_devoid_co_var_of_type (TyVarTy _) _ = True
@@ -1129,7 +1137,7 @@ tyConsOfType ty
go_prov (PhantomProv co) = go_co co
go_prov (ProofIrrelProv co) = go_co co
- go_prov (PluginProv _) = emptyUniqSet
+ go_prov (PluginProv _ _) = emptyUniqSet
go_cos cos = foldr (unionUniqSets . go_co) emptyUniqSet cos
@@ -1340,4 +1348,4 @@ occCheckExpand vs_to_avoid ty
------------------
go_prov cxt (PhantomProv co) = PhantomProv <$> go_co cxt co
go_prov cxt (ProofIrrelProv co) = ProofIrrelProv <$> go_co cxt co
- go_prov _ p@(PluginProv _) = return p
+ go_prov _ p@(PluginProv _ _) = return p
=====================================
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
@@ -886,7 +885,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
@@ -1527,15 +1526,19 @@ data UnivCoProvenance
-- considered equivalent. See Note [ProofIrrelProv].
-- Can be used in Nominal or Representational coercions
- | PluginProv String -- ^ From a plugin, which asserts that this coercion
- -- is sound. The string is for the use of the plugin.
+ | PluginProv String !DCoVarSet
+ -- ^ From a plugin, which asserts that this coercion is sound.
+ -- The string and the variable set are for the use by the plugin.
+ -- E.g., the set may contain the in-scope coercion variables
+ -- that the the proof represented by the coercion makes use of.
+ -- See Note [The importance of tracking free coercion variables].
deriving Data.Data
instance Outputable UnivCoProvenance where
- ppr (PhantomProv _) = text "(phantom)"
- ppr (ProofIrrelProv _) = text "(proof irrel.)"
- ppr (PluginProv str) = parens (text "plugin" <+> brackets (text str))
+ ppr (PhantomProv _) = text "(phantom)"
+ ppr (ProofIrrelProv _) = text "(proof irrel.)"
+ ppr (PluginProv str cvs) = parens (text "plugin" <+> brackets (text str) <+> ppr cvs)
-- | A coercion to be filled in by the type-checker. See Note [Coercion holes]
data CoercionHole
@@ -1690,6 +1693,50 @@ Here,
where
co5 :: (a1 ~ Bool) ~ (a2 ~ Bool)
co5 = TyConAppCo Nominal (~#) [<*>, <*>, co4, <Bool>]
+
+
+Note [The importance of tracking free coercion variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It is vital that `UnivCo` (a coercion that lacks a proper proof)
+tracks its free coercion variables. To see why, consider this program:
+
+ type S :: Nat -> Nat
+
+ data T (a::Nat) where
+ T1 :: T 0
+ T2 :: ...
+
+ f :: T a -> S (a+1) -> S 1
+ f = /\a (x:T a) (y:a).
+ case x of
+ T1 (gco : a ~# 0) -> y |> wco
+
+For this to typecheck we need `wco :: S (a+1) ~# S 1`, given that `gco : a ~# 0`.
+To prove that we need to know that `a+1 = 1` if `a=0`, which a plugin might know.
+So it solves `wco` by providing a `UnivCo (PluginProv "my-plugin" gcvs) (a+1) 1`.
+
+ But the `gcvs` in `PluginProv` must mention `gco`.
+
+Why? Otherwise we might float the entire expression (y |> wco) out of the
+the case alternative for `T1` which brings `gco` into scope. If this
+happens then we aren't far from a segmentation fault or much worse.
+See #23923 for a real-world example of this happening.
+
+So it is /crucial/ for the `PluginProv` to mention, in `gcvs`, the coercion
+variables used by the plugin to justify the `UnivCo` that it builds.
+
+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.)
+
-}
@@ -1856,7 +1903,9 @@ foldTyCo (TyCoFolder { tcf_view = view
go_prov env (PhantomProv co) = go_co env co
go_prov env (ProofIrrelProv co) = go_co env co
- go_prov _ (PluginProv _) = mempty
+ go_prov _ (PluginProv _ cvs) = go_cvs env cvs
+
+ go_cvs env cvs = foldl' (\ !acc cv -> acc `mappend` covar env cv) mempty (dVarSetElems cvs)
-- | A view function that looks through nothing.
noView :: Type -> Maybe Type
@@ -1922,7 +1971,7 @@ coercionSize (AxiomRuleCo _ cs) = 1 + sum (map coercionSize cs)
provSize :: UnivCoProvenance -> Int
provSize (PhantomProv co) = 1 + coercionSize co
provSize (ProofIrrelProv co) = 1 + coercionSize co
-provSize (PluginProv _) = 1
+provSize (PluginProv _ _) = 1
{-
************************************************************************
=====================================
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,
@@ -910,12 +910,18 @@ subst_co subst co
go_prov (PhantomProv kco) = PhantomProv (go kco)
go_prov (ProofIrrelProv kco) = ProofIrrelProv (go kco)
- go_prov p@(PluginProv _) = p
+ go_prov (PluginProv s cvs) = PluginProv s $ substDCoVarSet subst cvs
-- See Note [Substituting in a coercion hole]
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 = coVarsOfCosDSet $ 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)
@@ -233,9 +235,7 @@ tidyCo env@(_, subst) co
-- the case above duplicates a bit of work in tidying h and the kind
-- of tv. But the alternative is to use coercionKind, which seems worse.
go (FunCo r afl afr w co1 co2) = ((FunCo r afl afr $! go w) $! go co1) $! go co2
- go (CoVarCo cv) = case lookupVarEnv subst cv of
- Nothing -> CoVarCo cv
- Just cv' -> CoVarCo cv'
+ go (CoVarCo cv) = CoVarCo $! go_cv 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) $!
@@ -249,9 +249,11 @@ 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
+ go_prov (PluginProv s cvs) = PluginProv s $ mapDVarSet go_cv cvs
tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
tidyCos env = strictMap (tidyCo env)
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -580,7 +580,7 @@ expandTypeSynonyms ty
go_prov subst (PhantomProv co) = PhantomProv (go_co subst co)
go_prov subst (ProofIrrelProv co) = ProofIrrelProv (go_co subst co)
- go_prov _ p@(PluginProv _) = p
+ go_prov _ p@(PluginProv _ _) = p
-- the "False" and "const" are to accommodate the type of
-- substForAllCoBndrUsing, which is general enough to
@@ -912,7 +912,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
@@ -960,6 +961,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
@@ -999,7 +1001,14 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar
go_prov !env (PhantomProv co) = PhantomProv <$> go_co env co
go_prov !env (ProofIrrelProv co) = ProofIrrelProv <$> go_co env co
- go_prov !_ p@(PluginProv _) = return p
+ go_prov !env (PluginProv s cvs) = PluginProv s <$> strictFoldDVarSet (do_cv env)
+ (return emptyDVarSet) cvs
+
+ 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*]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -318,9 +319,11 @@ toIfaceCoercionX fr co
fr' = fr `delVarSet` tv
go_prov :: UnivCoProvenance -> IfaceUnivCoProv
- go_prov (PhantomProv co) = IfacePhantomProv (go co)
- go_prov (ProofIrrelProv co) = IfaceProofIrrelProv (go co)
- go_prov (PluginProv str) = IfacePluginProv str
+ go_prov (PhantomProv co) = IfacePhantomProv (go co)
+ go_prov (ProofIrrelProv co) = IfaceProofIrrelProv (go co)
+ go_prov (PluginProv str cvs) = IfacePluginProv str (map toIfaceCoVar bound_cvs) free_cvs
+ where
+ (free_cvs, bound_cvs) = partition (`elemVarSet` fr) (dVarSetElems cvs)
toIfaceTcArgs :: TyCon -> [Type] -> IfaceAppArgs
toIfaceTcArgs = toIfaceTcArgsX emptyVarSet
=====================================
compiler/GHC/Iface/Rename.hs
=====================================
@@ -678,6 +678,8 @@ 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
+ -- Renaming affects only type constructors, not coercion variables,
+ -- so no need to recurs into the provenance.
rnIfaceCo (IfaceSymCo c)
= IfaceSymCo <$> rnIfaceCo c
rnIfaceCo (IfaceTransCo c1 c2)
=====================================
compiler/GHC/Iface/Syntax.hs
=====================================
@@ -1795,7 +1795,7 @@ freeNamesIfCoercion (IfaceAxiomRuleCo _ax cos)
freeNamesIfProv :: IfaceUnivCoProv -> NameSet
freeNamesIfProv (IfacePhantomProv co) = freeNamesIfCoercion co
freeNamesIfProv (IfaceProofIrrelProv co) = freeNamesIfCoercion co
-freeNamesIfProv (IfacePluginProv _) = emptyNameSet
+freeNamesIfProv (IfacePluginProv _ _ _) = emptyNameSet
freeNamesIfVarBndr :: VarBndr IfaceBndr vis -> NameSet
freeNamesIfVarBndr (Bndr bndr _) = freeNamesIfBndr bndr
=====================================
compiler/GHC/Iface/Type.hs
=====================================
@@ -399,7 +399,10 @@ data IfaceCoercion
data IfaceUnivCoProv
= IfacePhantomProv IfaceCoercion
| IfaceProofIrrelProv IfaceCoercion
- | IfacePluginProv String
+ | IfacePluginProv String [IfLclName] [Var]
+ -- Local covars and open (free) covars resp
+ -- See Note [Free tyvars in IfaceType]
+
{- Note [Holes in IfaceCoercion]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -620,7 +623,7 @@ substIfaceType env ty
go_prov (IfacePhantomProv co) = IfacePhantomProv (go_co co)
go_prov (IfaceProofIrrelProv co) = IfaceProofIrrelProv (go_co co)
- go_prov co@(IfacePluginProv _) = co
+ go_prov co@(IfacePluginProv _ _ _) = co
substIfaceAppArgs :: IfaceTySubst -> IfaceAppArgs -> IfaceAppArgs
substIfaceAppArgs env args
@@ -1954,8 +1957,8 @@ pprIfaceUnivCoProv (IfacePhantomProv co)
= text "phantom" <+> pprParendIfaceCoercion co
pprIfaceUnivCoProv (IfaceProofIrrelProv co)
= text "irrel" <+> pprParendIfaceCoercion co
-pprIfaceUnivCoProv (IfacePluginProv s)
- = text "plugin" <+> doubleQuotes (text s)
+pprIfaceUnivCoProv (IfacePluginProv s cvs fcvs)
+ = hang (text "plugin") 2 (sep [doubleQuotes (text s), ppr cvs, ppr fcvs])
-------------------
instance Outputable IfaceTyCon where
@@ -2324,9 +2327,11 @@ instance Binary IfaceUnivCoProv where
put_ bh (IfaceProofIrrelProv a) = do
putByte bh 2
put_ bh a
- put_ bh (IfacePluginProv a) = do
+ put_ bh (IfacePluginProv a cvs fcvs) = do
putByte bh 3
put_ bh a
+ assertPpr (null fcvs) (ppr cvs $$ ppr fcvs) $
+ put_ bh cvs
get bh = do
tag <- getByte bh
@@ -2336,7 +2341,8 @@ instance Binary IfaceUnivCoProv where
2 -> do a <- get bh
return $ IfaceProofIrrelProv a
3 -> do a <- get bh
- return $ IfacePluginProv a
+ cvs <- get bh
+ return $ IfacePluginProv a cvs []
_ -> panic ("get IfaceUnivCoProv " ++ show tag)
=====================================
compiler/GHC/IfaceToCore.hs
=====================================
@@ -1491,7 +1491,10 @@ tcIfaceCo = go
tcIfaceUnivCoProv :: IfaceUnivCoProv -> IfL UnivCoProvenance
tcIfaceUnivCoProv (IfacePhantomProv kco) = PhantomProv <$> tcIfaceCo kco
tcIfaceUnivCoProv (IfaceProofIrrelProv kco) = ProofIrrelProv <$> tcIfaceCo kco
-tcIfaceUnivCoProv (IfacePluginProv str) = return $ PluginProv str
+tcIfaceUnivCoProv (IfacePluginProv str cvs fcvs) =
+ assertPpr (null fcvs) (ppr fcvs) $ do
+ cvs' <- mapM tcIfaceLclId cvs
+ return $ PluginProv str $ mkDVarSet cvs'
{-
************************************************************************
=====================================
compiler/GHC/Tc/TyCl/Utils.hs
=====================================
@@ -156,7 +156,7 @@ synonymTyConsOfType ty
go_prov (PhantomProv co) = go_co co
go_prov (ProofIrrelProv co) = go_co co
- go_prov (PluginProv _) = emptyNameEnv
+ go_prov (PluginProv _ _) = emptyNameEnv
go_tc tc | isTypeSynonymTyCon tc = unitNameEnv (tyConName tc) tc
| otherwise = emptyNameEnv
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -1592,7 +1592,10 @@ collect_cand_qtvs_co orig_ty cur_lvl bound = go_co
go_prov dv (PhantomProv co) = go_co dv co
go_prov dv (ProofIrrelProv co) = go_co dv co
- go_prov dv (PluginProv _) = return dv
+ go_prov dv (PluginProv _ cvs) = strictFoldDVarSet zt_cv (return dv) cvs
+
+ zt_cv :: CoVar -> TcM CandidatesQTvs -> TcM CandidatesQTvs
+ zt_cv cv mdvs = do { dvs <- mdvs; go_cv dvs cv }
go_cv :: CandidatesQTvs -> CoVar -> TcM CandidatesQTvs
go_cv dv@(DV { dv_cvs = cvs }) cv
=====================================
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
@@ -125,7 +125,15 @@ partitionUniqDSet p = coerce . partitionUDFM p . getUniqDSet
-- See Note [UniqSet invariant] in GHC.Types.Unique.Set
mapUniqDSet :: Uniquable b => (a -> b) -> UniqDSet a -> UniqDSet b
-mapUniqDSet f = mkUniqDSet . map f . uniqDSetToList
+mapUniqDSet f (UniqDSet m) = UniqDSet $ unsafeCastUDFMKey $ mapUDFM f m
+-- Simply apply `f` to each element, retaining all the structure unchanged.
+-- The identification of keys and elements prevents a derived Functor
+-- instance, but `unsafeCastUDFMKey` makes it possible to apply the strict
+-- mapping from DFM.
+
+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.
=====================================
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
=====================================
compiler/GHC/Utils/FV.hs
=====================================
@@ -21,6 +21,7 @@ module GHC.Utils.FV (
delFVs,
filterFV,
mapUnionFV,
+ fvDVarSetSome,
) where
import GHC.Prelude
@@ -195,3 +196,7 @@ mkFVs :: [Var] -> FV
mkFVs vars fv_cand in_scope acc =
mapUnionFV unitFV vars fv_cand in_scope acc
{-# INLINE mkFVs #-}
+
+fvDVarSetSome :: InterestingVarFun -> FV -> DVarSet
+fvDVarSetSome interesting_var fv =
+ mkDVarSet $ fst $ fv interesting_var emptyVarSet ([], emptyVarSet)
=====================================
docs/users_guide/extending_ghc.rst
=====================================
@@ -760,10 +760,33 @@ This evidence is ignored for Given constraints, which GHC
"solves" simply by discarding them; typically this is used when they are
uninformative (e.g. reflexive equations). For Wanted constraints, the
evidence will form part of the Core term that is generated after
-typechecking, and can be checked by ``-dcore-lint``. It is possible for
-the plugin to create equality axioms for use in evidence terms, but GHC
-does not check their consistency, and inconsistent axiom sets may lead
-to segfaults or other runtime misbehaviour.
+typechecking, and can be checked by ``-dcore-lint``.
+
+When solving a Wanted equality constraint (of type ``t1 ~N# t2``
+or ``t1 ~R# t2`` for nominal and representation equalities respectively),
+the evidence (of type ``EvTerm``) will take the form ``EvExpr (Coercion co)``,
+where the coercion ``co`` has type ``co :: t1 ~N# t2`` or ``co :: t1 ~R# t2``
+respectively.
+
+It is up to the plugin to construct a suitable coercion ``co``.
+However, one possibility is to construct one of form ::
+
+ UnivCo (PluginProv "my-plugin" gcvs) role t1 t2
+
+A ``UnivCo`` of this form says "trust me: my-plugin has solved this Wanted
+using (only) ``gcvs``".
+
+Here
+
+* The ``role`` should be the role of the original equality constraint
+ (nominal or representational).
+* The ``gcvs`` is a set of "given coercion variables"; these are the coercion
+ variable bound by enclosing Given constraints, which the plugin has used
+ to justify solving the Wanted.
+
+For soundness, it is very important to include the ``gcvs``; otherwise
+GHC may transform the program into a form that seg-faults.
+See #23923 for a long dicussion.
Evidence is required also when creating new Given constraints, which are
usually implied by old ones. It is not uncommon that the evidence of a new
=====================================
testsuite/tests/tcplugins/CtIdPlugin.hs
=====================================
@@ -21,6 +21,7 @@ import GHC.Tc.Plugin
import GHC.Tc.Types
import GHC.Tc.Types.Constraint
import GHC.Tc.Types.Evidence
+import GHC.Types.Unique.DSet
-- common
import Common
@@ -41,7 +42,7 @@ solver :: [String]
-> PluginDefs -> EvBindsVar -> [Ct] -> [Ct]
-> TcPluginM TcPluginSolveResult
solver _args defs ev givens wanteds = do
- let pluginCo = mkUnivCo (PluginProv "CtIdPlugin") Representational
+ let pluginCo = mkUnivCo (PluginProv "CtIdPlugin" emptyUniqDSet) Representational -- Empty is fine. This plugin does not use "givens".
let substEvidence ct ct' =
evCast (ctEvExpr $ ctEvidence ct') $ pluginCo (ctPred ct') (ctPred ct)
=====================================
testsuite/tests/tcplugins/RewritePlugin.hs
=====================================
@@ -45,6 +45,8 @@ import GHC.Tc.Types.Constraint
)
import GHC.Tc.Types.Evidence
( EvTerm(EvExpr), Role(Nominal) )
+import GHC.Types.Unique.DSet
+ ( emptyUniqDSet )
import GHC.Types.Unique.FM
( UniqFM, listToUFM )
@@ -85,5 +87,5 @@ mkTyFamReduction :: TyCon -> [ Type ] -> Type -> Reduction
mkTyFamReduction tyCon args res = Reduction co res
where
co :: Coercion
- co = mkUnivCo ( PluginProv "RewritePlugin" ) Nominal
+ co = mkUnivCo ( PluginProv "RewritePlugin" emptyUniqDSet) Nominal -- Empty is fine. This plugin does not use "givens".
( mkTyConApp tyCon args ) res
=====================================
testsuite/tests/tcplugins/TyFamPlugin.hs
=====================================
@@ -39,6 +39,8 @@ import GHC.Tc.Types.Constraint
)
import GHC.Tc.Types.Evidence
( EvBindsVar, EvTerm(EvExpr), Role(Nominal) )
+import GHC.Types.Unique.DSet
+ ( emptyUniqDSet )
-- common
import Common
@@ -78,6 +80,6 @@ solveCt ( PluginDefs {..} ) ct@( classifyPredType . ctPred -> EqPred NomEq lhs r
, let
evTerm :: EvTerm
evTerm = EvExpr . Coercion
- $ mkUnivCo ( PluginProv "TyFamPlugin" ) Nominal lhs rhs
+ $ mkUnivCo ( PluginProv "TyFamPlugin" emptyUniqDSet) Nominal lhs rhs -- Empty is fine. This plugin does not use "givens".
= pure $ Just ( evTerm, ct )
solveCt _ ct = pure Nothing
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/d74bc7237300750eec8dc917bd86d1d4e1f2cde9...053fdb81f509cc6158c5d645ef2402e24ca3c115
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/d74bc7237300750eec8dc917bd86d1d4e1f2cde9...053fdb81f509cc6158c5d645ef2402e24ca3c115
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/20240307/0a5e2d89/attachment-0001.html>
More information about the ghc-commits
mailing list