[Git][ghc/ghc][master] Add DCoVarSet to PluginProv (!12037)
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Sat May 4 00:47:10 UTC 2024
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
d603f199 by Mikolaj Konarski at 2024-05-03T20:46:19-04:00
Add DCoVarSet to PluginProv (!12037)
- - - - -
28 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/Error/Codes.hs
- compiler/GHC/Types/RepType.hs
- compiler/GHC/Types/TyThing/Ppr.hs
- compiler/GHC/Types/Unique/DSet.hs
- compiler/GHC/Types/Var/Set.hs
- compiler/GHC/Utils/FV.hs
- docs/users_guide/9.12.1-notes.rst
- docs/users_guide/extending_ghc.rst
- testsuite/tests/pmcheck/should_compile/T11195.hs
- 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,
@@ -1456,9 +1456,9 @@ setNominalRole_maybe r co
setNominalRole_maybe_helper (InstCo co arg)
= InstCo <$> setNominalRole_maybe_helper co <*> pure arg
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.
+ | 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
setNominalRole_maybe_helper _ = Nothing
@@ -1583,7 +1583,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)
@@ -2040,6 +2040,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...
@@ -2415,7 +2418,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
=====================================
@@ -636,7 +636,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]
@@ -734,7 +734,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,8 @@ 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) _ _ (have, haveSet) =
+ (dVarSetElems cvs ++ have, dVarSetToVarSet cvs `unionVarSet` haveSet)
tyCoFVsOfCos :: [Coercion] -> FV
tyCoFVsOfCos [] fv_cand in_scope acc = emptyFV fv_cand in_scope acc
@@ -730,7 +739,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 +1138,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 +1349,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
@@ -1533,15 +1532,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.
+ -- The set must contain all 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
@@ -1696,6 +1699,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.)
+
-}
@@ -1755,7 +1802,6 @@ In particular, given
| tv `elemVarSet` acc = acc
| otherwise = acc `extendVarSet` tv
-
we want to end up with
fvs ty = go emptyVarSet ty emptyVarSet
where
@@ -1785,6 +1831,38 @@ Here deep_fvs and deep_tcf are mutually recursive, unlike fvs and tcf.
But, amazingly, we get good code here too. GHC is careful not to mark
TyCoFolder data constructor for deep_tcf as a loop breaker, so the
record selections still cancel. And eta expansion still happens too.
+
+Note [Use explicit recursion in foldTyCo]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In foldTyCo you'll see things like:
+ go_tys _ [] = mempty
+ go_tys env (t:ts) = go_ty env t `mappend` go_tys env ts
+where we use /explicit recursion/. You might wonder about using foldl instead:
+ go_tys env = foldl (\t acc -> go_ty env t `mappend` acc) mempty
+Or maybe foldl', or foldr.
+
+But don't do that for two reasons (see #24591)
+
+* We sometimes instantiate `a` to (Endo VarSet). Remembering
+ newtype Endo a = Endo (a->a)
+ after inlining `foldTyCo` bodily, the explicit recursion looks like
+ go_tys _ [] = \acc -> acc
+ go_tys env (t:ts) = \acc -> go_ty env t (go_tys env ts acc)
+ The strictness analyser has no problem spotting that this function is
+ strict in `acc`, provided `go_ty` is.
+
+ But in the foldl form that is /much/ less obvious, and the strictness
+ analyser fails utterly. Result: lots and lots of thunks get built. In
+ !12037, Mikolaj found that GHC allocated /six times/ as much heap
+ on test perf/compiler/T9198 as a result of this single problem!
+
+* Second, while I think that using `foldr` would be fine (simple experiments in
+ #24591 suggest as much), it builds a local loop (with env free) and I'm not 100%
+ confident it'll be lambda lifted in the end. It seems more direct just to write
+ the code we want.
+
+ On the other hand in `go_cvs` we might hope that the `foldr` will fuse with the
+ `dVarSetElems` so I have used `foldr`.
-}
data TyCoFolder env a
@@ -1823,12 +1901,11 @@ foldTyCo (TyCoFolder { tcf_view = view
= let !env' = tycobinder env tv vis -- Avoid building a thunk here
in go_ty env (varType tv) `mappend` go_ty env' inner
- -- Explicit recursion because using foldr builds a local
- -- loop (with env free) and I'm not confident it'll be
- -- lambda lifted in the end
+ -- See Note [Use explicit recursion in foldTyCo]
go_tys _ [] = mempty
go_tys env (t:ts) = go_ty env t `mappend` go_tys env ts
+ -- See Note [Use explicit recursion in foldTyCo]
go_cos _ [] = mempty
go_cos env (c:cs) = go_co env c `mappend` go_cos env cs
@@ -1862,7 +1939,11 @@ 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
+
+ -- See Note [Use explicit recursion in foldTyCo]
+ go_cvs env cvs = foldr (add_one env) mempty (dVarSetElems cvs)
+ add_one env cv acc = covar env cv `mappend` acc
-- | A view function that looks through nothing.
noView :: Type -> Maybe Type
@@ -1928,7 +2009,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,
@@ -903,12 +903,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
=====================================
@@ -579,7 +579,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
@@ -911,7 +911,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
@@ -923,6 +924,7 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar
, tcm_hole = cohole })
= (go_ty, go_tys, go_co, go_cos)
where
+ -- See Note [Use explicit recursion in mapTyCo]
go_tys !_ [] = return []
go_tys !env (ty:tys) = (:) <$> go_ty env ty <*> go_tys env tys
@@ -953,12 +955,14 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar
; inner' <- go_ty env' inner
; return $ ForAllTy (Bndr tv' vis) inner' }
+ -- See Note [Use explicit recursion in mapTyCo]
go_cos !_ [] = return []
go_cos !env (co:cos) = (:) <$> go_co env co <*> go_cos env cos
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
@@ -998,8 +1002,28 @@ 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 <$> go_fcvs env (dVarSetElems cvs)
+
+ -- See Note [Use explicit recursion in mapTyCo]
+ go_fcvs :: env -> [CoVar] -> m DTyCoVarSet
+ go_fcvs _ [] = return emptyDVarSet
+ go_fcvs env (cv:cvs) = do { co <- covar env cv
+ ; cvs' <- go_fcvs env cvs
+ ; return (tyCoVarsOfCoDSet co `unionDVarSet` cvs') }
+
+{- Note [Use explicit recursion in mapTyCo]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We use explicit recursion in `mapTyCo`, rather than calling, say, `strictFoldDVarSet`,
+for exactly the same reason as in Note [Use explicit recursion in foldTyCo] in
+GHC.Core.TyCo.Rep. We are in a monadic context, and using too-clever higher order
+functions makes the strictness analyser produce worse results.
+
+We could probably use `foldr`, since it is inlined bodily, fairly early; but
+I'm doing the simple thing and inlining it by hand.
+
+See !12037 for performance glitches caused by using `strictFoldDVarSet` (which is
+definitely not inlined bodily).
+-}
{- *********************************************************************
* *
=====================================
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*]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -176,7 +177,7 @@ toIfaceTypeX :: VarSet -> Type -> IfaceType
-- translates the tyvars in 'free' as IfaceFreeTyVars
--
-- Synonyms are retained in the interface type
-toIfaceTypeX fr (TyVarTy tv) -- See Note [Free tyvars in IfaceType] in GHC.Iface.Type
+toIfaceTypeX fr (TyVarTy tv) -- See Note [Free TyVars and CoVars in IfaceType] in GHC.Iface.Type
| tv `elemVarSet` fr = IfaceFreeTyVar tv
| otherwise = IfaceTyVar (toIfaceTyVar tv)
toIfaceTypeX fr ty@(AppTy {}) =
@@ -283,7 +284,7 @@ toIfaceCoercionX fr co
go (Refl ty) = IfaceReflCo (toIfaceTypeX fr ty)
go (GRefl r ty mco) = IfaceGReflCo r (toIfaceTypeX fr ty) (go_mco mco)
go (CoVarCo cv)
- -- See Note [Free tyvars in IfaceType] in GHC.Iface.Type
+ -- See Note [Free TyVars and CoVars in IfaceType] in GHC.Iface.Type
| cv `elemVarSet` fr = IfaceFreeCoVar cv
| otherwise = IfaceCoVarCo (toIfaceCoVar cv)
go (HoleCo h) = IfaceHoleCo (coHoleCoVar h)
@@ -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 recurse into the provenance.
rnIfaceCo (IfaceSymCo c)
= IfaceSymCo <$> rnIfaceCo c
rnIfaceCo (IfaceTransCo c1 c2)
=====================================
compiler/GHC/Iface/Syntax.hs
=====================================
@@ -1796,7 +1796,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
=====================================
@@ -154,7 +154,7 @@ type IfaceKind = IfaceType
-- Any time a 'Type' is pretty-printed, it is first converted to an 'IfaceType'
-- before being printed. See Note [Pretty printing via Iface syntax] in "GHC.Types.TyThing.Ppr"
data IfaceType
- = IfaceFreeTyVar TyVar -- See Note [Free tyvars in IfaceType]
+ = IfaceFreeTyVar TyVar -- See Note [Free TyVars and CoVars in IfaceType]
| IfaceTyVar IfLclName -- Type/coercion variable only, not tycon
| IfaceLitTy IfaceTyLit
| IfaceAppTy IfaceType IfaceAppArgs
@@ -284,7 +284,7 @@ instance Outputable IfaceTyConSort where
ppr (IfaceSumTyCon n) = text "sum:" <> ppr n
ppr IfaceEqualityTyCon = text "equality"
-{- Note [Free tyvars in IfaceType]
+{- Note [Free TyVars and CoVars in IfaceType]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Nowadays (since Nov 16, 2016) we pretty-print a Type by converting to
an IfaceType and pretty printing that. This eliminates a lot of
@@ -432,7 +432,7 @@ data IfaceCoercion
| IfaceCoVarCo IfLclName
| IfaceAxiomInstCo IfExtName BranchIndex [IfaceCoercion]
| IfaceAxiomRuleCo IfLclName [IfaceCoercion]
- -- There are only a fixed number of CoAxiomRules, so it suffices
+ -- ^ There are only a fixed number of CoAxiomRules, so it suffices
-- to use an IfaceLclName to distinguish them.
-- See Note [Adding built-in type families] in GHC.Builtin.Types.Literals
| IfaceUnivCo IfaceUnivCoProv Role IfaceType IfaceType
@@ -443,13 +443,16 @@ data IfaceCoercion
| IfaceInstCo IfaceCoercion IfaceCoercion
| IfaceKindCo IfaceCoercion
| IfaceSubCo IfaceCoercion
- | IfaceFreeCoVar CoVar -- See Note [Free tyvars in IfaceType]
+ | IfaceFreeCoVar CoVar -- ^ See Note [Free TyVars and CoVars in IfaceType]
| IfaceHoleCo CoVar -- ^ See Note [Holes in IfaceCoercion]
data IfaceUnivCoProv
= IfacePhantomProv IfaceCoercion
| IfaceProofIrrelProv IfaceCoercion
- | IfacePluginProv String
+ | IfacePluginProv String [IfLclName] [Var]
+ -- ^ Local covars and open (free) covars resp
+ -- See Note [Free TyVars and CoVars in IfaceType]
+
{- Note [Holes in IfaceCoercion]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -670,7 +673,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
@@ -1023,7 +1026,7 @@ ppr_ty ctxt_prec ty
| not (isIfaceRhoType ty) = ppr_sigma ShowForAllMust ctxt_prec ty
ppr_ty _ (IfaceForAllTy {}) = panic "ppr_ty" -- Covered by not.isIfaceRhoType
ppr_ty _ (IfaceFreeTyVar tyvar) = ppr tyvar -- This is the main reason for IfaceFreeTyVar!
-ppr_ty _ (IfaceTyVar tyvar) = ppr tyvar -- See Note [Free tyvars in IfaceType]
+ppr_ty _ (IfaceTyVar tyvar) = ppr tyvar -- See Note [Free TyVars and CoVars in IfaceType]
ppr_ty ctxt_prec (IfaceTyConApp tc tys) = pprTyTcApp ctxt_prec tc tys
ppr_ty ctxt_prec (IfaceTupleTy i p tys) = ppr_tuple ctxt_prec i p tys -- always fully saturated
ppr_ty _ (IfaceLitTy n) = pprIfaceTyLit n
@@ -1955,7 +1958,7 @@ ppr_co ctxt_prec co@(IfaceForAllCo {})
= let (tvs, co'') = split_co co' in ((name,kind_co,visL,visR):tvs,co'')
split_co co' = ([], co')
--- Why these three? See Note [Free tyvars in IfaceType]
+-- Why these three? See Note [Free TyVars and CoVars in IfaceType]
ppr_co _ (IfaceFreeCoVar covar) = ppr covar
ppr_co _ (IfaceCoVarCo covar) = ppr covar
ppr_co _ (IfaceHoleCo covar) = braces (ppr covar)
@@ -2010,8 +2013,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
@@ -2173,6 +2176,7 @@ ppr_parend_preds preds = parens (fsep (punctuate comma (map ppr preds)))
instance Binary IfaceType where
put_ _ (IfaceFreeTyVar tv)
= pprPanic "Can't serialise IfaceFreeTyVar" (ppr tv)
+ -- See Note [Free TyVars and CoVars in IfaceType]
put_ bh (IfaceForAllTy aa ab) = do
putByte bh 0
@@ -2321,9 +2325,10 @@ instance Binary IfaceCoercion where
put_ bh b
put_ _ (IfaceFreeCoVar cv)
= pprPanic "Can't serialise IfaceFreeCoVar" (ppr cv)
+ -- See Note [Free TyVars and CoVars in IfaceType]
put_ _ (IfaceHoleCo cv)
= pprPanic "Can't serialise IfaceHoleCo" (ppr cv)
- -- See Note [Holes in IfaceCoercion]
+ -- See Note [Holes in IfaceCoercion]
get bh = do
tag <- getByte bh
@@ -2393,9 +2398,12 @@ 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
+ -- See Note [Free TyVars and CoVars in IfaceType]
+ assertPpr (null fcvs) (ppr cvs $$ ppr fcvs) $
+ put_ bh cvs
get bh = do
tag <- getByte bh
@@ -2405,7 +2413,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
=====================================
@@ -1493,7 +1493,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/Error/Codes.hs
=====================================
@@ -1120,7 +1120,7 @@ To achieve this, we use a variant of the 'typed' lens from 'generic-lens'
first, and decide whether to recur into it using the
HasTypeQ type family.
- The two different behaviours are controlled by two main instances (*) and (**).
- - (*) recurs into a subtype, when we have a type family equation such as:
+ - (*) recurses into a subtype, when we have a type family equation such as:
ConRecursInto "TcRnCannotDeriveInstance" = 'Just DeriveInstanceErrReason
=====================================
compiler/GHC/Types/RepType.hs
=====================================
@@ -535,7 +535,7 @@ and returns the PrimRep IntRep. (See the definition of runtimeRepSimpleDataCons
GHC.Builtin.Types and its helper function mk_runtime_rep_dc.) Example 2 passes the promoted
list as the one argument to the extracted function. The extracted function is defined
as prim_rep_fun within tupleRepDataCon in GHC.Builtin.Types. It takes one argument, decomposes
-the promoted list (with extractPromotedList), and then recurs back to runtimeRepPrimRep
+the promoted list (with extractPromotedList), and then recurses back to runtimeRepPrimRep
to process the LiftedRep and WordRep, concatenating the results.
-}
=====================================
compiler/GHC/Types/TyThing/Ppr.hs
=====================================
@@ -98,7 +98,7 @@ Consequences:
(in GHC.IfaceToCore). For example, IfaceClosedSynFamilyTyCon
stores a [IfaceAxBranch] that is used only for pretty-printing.
-- See Note [Free tyvars in IfaceType] in GHC.Iface.Type
+- See Note [Free TyVars and CoVars in IfaceType] in GHC.Iface.Type
See #7730, #8776 for details -}
=====================================
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/9.12.1-notes.rst
=====================================
@@ -26,6 +26,14 @@ Language
Compiler
~~~~~~~~
+- Constructor ``PluginProv`` of type ``UnivCoProvenance``, relevant
+for typing plugins, gets an extra ``DCoVarSet`` argument.
+The argument is intended to 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]``
+in ``GHC.Core.TyCo.Rep``, :ref:`constraint-solving-with-plugins`
+and the migration guide.
+
GHCi
~~~~
=====================================
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/pmcheck/should_compile/T11195.hs
=====================================
@@ -84,7 +84,7 @@ 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)
+ opt_trans_prov (PluginProv str1 _) (PluginProv str2 _)
| str1 == str2 = Just p1
opt_trans_prov _ _ = Nothing
=====================================
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/-/commit/d603f1995f92eb14e533815f5e20e33e27a8ed6a
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d603f1995f92eb14e533815f5e20e33e27a8ed6a
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/20240503/a89ed70c/attachment-0001.html>
More information about the ghc-commits
mailing list