[Git][ghc/ghc][wip/T23923-mikolaj-take-2] Fix according to the second round of Simon's instruction
Mikolaj Konarski (@Mikolaj)
gitlab at gitlab.haskell.org
Sun Feb 18 22:46:51 UTC 2024
Mikolaj Konarski pushed to branch wip/T23923-mikolaj-take-2 at Glasgow Haskell Compiler / GHC
Commits:
f11e2b5e by Mikolaj Konarski at 2024-02-18T23:45:39+01:00
Fix according to the second round of Simon's instruction
- - - - -
11 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Coercion/Opt.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/Iface/Rename.hs
- compiler/GHC/IfaceToCore.hs
- compiler/GHC/Utils/FV.hs
- docs/users_guide/extending_ghc.rst
- testsuite/tests/tcplugins/RewritePlugin.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,
@@ -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...
=====================================
compiler/GHC/Core/Coercion/Opt.hs
=====================================
@@ -641,9 +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 s cvs -> PluginProv s $! substDCoVarSet (undefined{-lcTCvSubst-} env) cvs
-
--- !!! neither lcTCvSubst nor lcSubst exist any more; what shall I use here? lcSubstLeft? lcSubstRight? leave the cvs alone?
+ PluginProv s cvs -> PluginProv s $ substDCoVarSet (liftingContextSubst env) cvs
-------------
opt_transList :: HasDebugCallStack => InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
@@ -725,11 +723,7 @@ opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1)
opt_trans_prov (ProofIrrelProv kco1) (ProofIrrelProv kco2)
= Just $ ProofIrrelProv $ opt_trans is kco1 kco2
opt_trans_prov (PluginProv str1 cvs1) (PluginProv str2 cvs2)
- | str1 == str2 && cvs1 == cvs2 = Just p1
--- !!! but Adam says "You'll want [...] the union of both sets of coercion variables.", so should we instead do
--- opt_trans_prov (PluginProv str1 cvs1) (PluginProv str2 cvs2)
--- | str1 == str2 = Just (PluginProv str1 (cvs1 `union` cvs2)
--- ??? maybe also concatenate the strings instead of comparing them?
+ | str1 == str2 = Just (PluginProv str1 (cvs1 `unionDVarSet` cvs2))
opt_trans_prov _ _ = Nothing
-- Push transitivity down through matching top-level constructors.
=====================================
compiler/GHC/Core/TyCo/FVs.hs
=====================================
@@ -19,7 +19,7 @@ module GHC.Core.TyCo.FVs
tyCoVarsOfCoDSet,
tyCoFVsOfCo, tyCoFVsOfCos,
tyCoVarsOfCoList,
- shallowCoVarsOfCosDSet,
+ coVarsOfCosDSet,
almostDevoidCoVarOfCo,
@@ -450,39 +450,8 @@ deepCoVarFolder = TyCoFolder { tcf_view = noView
------- Same again, but for DCoVarSet ----------
-- But this time the free vars are shallow
-shallowCoVarsOfCosDSet :: [Coercion] -> DCoVarSet
-shallowCoVarsOfCosDSet _cos = undefined -- !!! runTCA (shallow_dcv_cos cos) emptyVarSet emptyDVarSet
-{- TODO: !!! lots of other code and refactorings, partially bit-rotten, would need to be taken from !3792 --- in particular
-
-* should I port the removal of the `env` parameter from `TyCoFolder`, see https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3792/diffs#578c7c3857d66d963736ff6742f3433a0e8d01b7_1883_2076? That's 200 lines in the old GHC.Core.TyCo.Rep alone and who know how many lines in the new versions of these files. If not, what `env` to use in `shallowCoVarDSetFolder`, a couple of lines below in the place marked as {-!!!-}? Is this relatively shallow (e.g., if the env type-checks, it's likely to be correct?)?
-
-* should I introduce TyCoAcc, see https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3792/diffs#039e8f5676356ef05c90af828aae48aac7296e47_266_268 and then also use it for many other operations (e.g., instead of Endo)?
-
-
-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
--}
+coVarsOfCosDSet :: [Coercion] -> DCoVarSet
+coVarsOfCosDSet cos = fvDVarSetSome isCoVar (tyCoFVsOfCos cos)
{- *********************************************************************
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -1525,7 +1525,7 @@ data UnivCoProvenance
-- considered equivalent. See Note [ProofIrrelProv].
-- Can be used in Nominal or Representational coercions
- | PluginProv String DCoVarSet -- !!! shall we make the field(s) strict?
+ | PluginProv String !DCoVarSet
-- ^ From a plugin, which asserts that this coercion is sound.
-- The string and the variable set are for the use of the plugin.
-- E.g., the set may contain the in-scope coercion variables
=====================================
compiler/GHC/Core/TyCo/Subst.hs
=====================================
@@ -910,7 +910,7 @@ subst_co subst co
go_prov (PhantomProv kco) = PhantomProv (go kco)
go_prov (ProofIrrelProv kco) = ProofIrrelProv (go kco)
- go_prov (PluginProv s cvs) = PluginProv s $! substDCoVarSet subst cvs
+ 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 })
@@ -919,7 +919,7 @@ subst_co subst co
-- | 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) $
+substDCoVarSet subst cvs = coVarsOfCosDSet $ map (substCoVar subst) $
dVarSetElems cvs
substForAllCoBndr :: Subst -> TyCoVar -> KindCoercion
=====================================
compiler/GHC/Core/TyCo/Tidy.hs
=====================================
@@ -253,7 +253,7 @@ tidyCo env@(_, subst) co
go_prov (PhantomProv co) = PhantomProv $! go co
go_prov (ProofIrrelProv co) = ProofIrrelProv $! go co
- go_prov (PluginProv s cvs) = PluginProv s $! mapDVarSet go_cv cvs
+ go_prov (PluginProv s cvs) = PluginProv s $ mapDVarSet go_cv cvs
tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
tidyCos env = strictMap (tidyCo env)
=====================================
compiler/GHC/Iface/Rename.hs
=====================================
@@ -678,7 +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
- -- !!! do we need to rename the provenance `s` here?
+ -- 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/IfaceToCore.hs
=====================================
@@ -1494,7 +1494,7 @@ tcIfaceUnivCoProv (IfaceProofIrrelProv kco) = ProofIrrelProv <$> tcIfaceCo kco
tcIfaceUnivCoProv (IfacePluginProv str cvs fcvs) =
assertPpr (null fcvs) (ppr fcvs) $ do
cvs' <- mapM tcIfaceLclId cvs
- return $ PluginProv str $! mkDVarSet cvs'
+ return $ PluginProv str $ mkDVarSet cvs'
{-
************************************************************************
=====================================
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
=====================================
@@ -770,6 +770,8 @@ usually implied by old ones. It is not uncommon that the evidence of a new
Given constraint contains a removed constraint: the new one has replaced the
removed one.
+-- !!! Given that "Evidence" and "Given" is mentioned here, is this the right place to "explain when plugin authors need to record coercion variables in their PluginProv"? I think, ideally, we'd explaion this in a subsection about a relevant example plugin, but I can't spot any.
+
.. _type-family-rewriting-with-plugins:
Type family rewriting with plugins
=====================================
testsuite/tests/tcplugins/RewritePlugin.hs
=====================================
@@ -87,5 +87,5 @@ mkTyFamReduction :: TyCon -> [ Type ] -> Type -> Reduction
mkTyFamReduction tyCon args res = Reduction co res
where
co :: Coercion
- co = mkUnivCo ( PluginProv "RewritePlugin" emptyUniqDSet) Nominal -- Empty is fine. This plugin does not use "givens". -- !!! is it true for this plugin as well?
+ co = mkUnivCo ( PluginProv "RewritePlugin" emptyUniqDSet) Nominal -- Empty is fine. This plugin does not use "givens".
( mkTyConApp tyCon args ) res
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f11e2b5e080697b5374e8052d789ee0ce502a388
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f11e2b5e080697b5374e8052d789ee0ce502a388
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/20240218/974cdf05/attachment-0001.html>
More information about the ghc-commits
mailing list