[Git][ghc/ghc][wip/T24978] Put [Coercion] in UnivCo
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Wed Jun 12 12:57:35 UTC 2024
Simon Peyton Jones pushed to branch wip/T24978 at Glasgow Haskell Compiler / GHC
Commits:
e2142bf4 by Simon Peyton Jones at 2024-06-12T13:57:08+01:00
Put [Coercion] in UnivCo
- - - - -
19 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Coercion.hs-boot
- compiler/GHC/Core/Coercion/Opt.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/Utils/TcMType.hs
- 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
=====================================
@@ -1104,16 +1104,16 @@ mkHoleCo h = HoleCo h
-- | Make a universal coercion between two arbitrary types.
mkUnivCo :: UnivCoProvenance
- -> DCoVarSet -- Free coercion variables of the evidence for this coercion
+ -> [Coercion] -- ^ Coercions on which this depends
-> Role -- ^ role of the built coercion, "r"
-> Type -- ^ t1 :: k1
-> Type -- ^ t2 :: k2
-> Coercion -- ^ :: t1 ~r t2
-mkUnivCo prov cvs role ty1 ty2
+mkUnivCo prov deps role ty1 ty2
| ty1 `eqType` ty2 = mkReflCo role ty1
| otherwise = UnivCo { uco_prov = prov, uco_role = role
, uco_lty = ty1, uco_rty = ty2
- , uco_cvs = cvs }
+ , uco_deps = deps }
-- | Create a symmetric version of the given 'Coercion' that asserts
-- equality between the same types but in the other "direction", so
@@ -1400,8 +1400,7 @@ mkProofIrrelCo :: Role -- ^ role of the created coercion, "r"
-- the individual coercions are.
mkProofIrrelCo r co g _ | isGReflCo co = mkReflCo r (mkCoercionTy g)
-- kco is a kind coercion, thus @isGReflCo@ rather than @isReflCo@
-mkProofIrrelCo r kco g1 g2 = mkUnivCo ProofIrrelProv
- (coVarsOfCoDSet kco) r
+mkProofIrrelCo r kco g1 g2 = mkUnivCo ProofIrrelProv [kco] r
(mkCoercionTy g1) (mkCoercionTy g2)
{-
@@ -1469,7 +1468,7 @@ setNominalRole_maybe r co
-- types.
mkPhantomCo :: Coercion -> Type -> Type -> Coercion
mkPhantomCo h t1 t2
- = mkUnivCo PhantomProv (coVarsOfCoDSet h) Phantom t1 t2
+ = mkUnivCo PhantomProv [h] Phantom t1 t2
-- takes any coercion and turns it into a Phantom coercion
toPhantomCo :: Coercion -> Coercion
@@ -2404,8 +2403,8 @@ seqCo (CoVarCo cv) = cv `seq` ()
seqCo (HoleCo h) = coHoleCoVar h `seq` ()
seqCo (AxiomInstCo con ind cos) = con `seq` ind `seq` seqCos cos
seqCo (UnivCo { uco_prov = p, uco_role = r
- , uco_lty = t1, uco_rty = t2, uco_cvs = cvs })
- = p `seq` r `seq` seqType t1 `seq` seqType t2 `seq` seqDVarSet cvs
+ , uco_lty = t1, uco_rty = t2, uco_deps = deps })
+ = p `seq` r `seq` seqType t1 `seq` seqType t2 `seq` seqCos deps
seqCo (SymCo co) = seqCo co
seqCo (TransCo co1 co2) = seqCo co1 `seq` seqCo co2
seqCo (SelCo n co) = n `seq` seqCo co
=====================================
compiler/GHC/Core/Coercion.hs-boot
=====================================
@@ -10,7 +10,6 @@ import {-# SOURCE #-} GHC.Core.TyCon
import GHC.Types.Basic ( LeftOrRight )
import GHC.Core.Coercion.Axiom
import GHC.Types.Var
-import GHC.Types.Var.Set( DCoVarSet )
import GHC.Data.Pair
import GHC.Utils.Misc
@@ -24,7 +23,7 @@ mkFunCo2 :: Role -> FunTyFlag -> FunTyFlag -> CoercionN -> Coercion -> Coerc
mkCoVarCo :: CoVar -> Coercion
mkAxiomInstCo :: CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion
mkPhantomCo :: Coercion -> Type -> Type -> Coercion
-mkUnivCo :: UnivCoProvenance -> DCoVarSet -> Role -> Type -> Type -> Coercion
+mkUnivCo :: UnivCoProvenance -> [Coercion] -> Role -> Type -> Type -> Coercion
mkSymCo :: Coercion -> Coercion
mkTransCo :: Coercion -> Coercion -> Coercion
mkSelCo :: HasDebugCallStack => CoSel -> Coercion -> Coercion
=====================================
compiler/GHC/Core/Coercion/Opt.hs
=====================================
@@ -15,7 +15,6 @@ import GHC.Tc.Utils.TcType ( exactTyCoVarsOfType )
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Subst
import GHC.Core.TyCo.Compare( eqType, eqForAllVis )
-import GHC.Core.TyCo.FVs( coVarsOfCoDSet )
import GHC.Core.Coercion
import GHC.Core.Type as Type hiding( substTyVarBndr, substTy )
import GHC.Core.TyCon
@@ -372,8 +371,8 @@ opt_co4 env sym rep r (AxiomInstCo con ind cos)
-- Note that the_co does *not* have sym pushed into it
opt_co4 env sym rep r (UnivCo { uco_prov = prov, uco_lty = t1
- , uco_rty = t2, uco_cvs = cvs })
- = opt_univ env sym prov cvs (chooseRole rep r) t1 t2
+ , uco_rty = t2, uco_deps = deps })
+ = opt_univ env sym prov deps (chooseRole rep r) t1 t2
opt_co4 env sym rep r (TransCo co1 co2)
-- sym (g `o` h) = sym h `o` sym g
@@ -528,7 +527,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 (coVarsOfCoDSet co) Phantom ty1 ty2
+ = opt_univ env sym PhantomProv [mkKindCo co] Phantom ty1 ty2
where
Pair ty1 ty2 = coercionKind co
@@ -564,20 +563,19 @@ See #19509.
-}
opt_univ :: LiftingContext -> SymFlag -> UnivCoProvenance
- -> DCoVarSet -- Fully substituted by liftingContextSubst
+ -> [Coercion]
-> Role -> Type -> Type -> Coercion
-opt_univ env sym prov cvs role ty1 ty2
- | sym = opt_univ1 env prov cvs' role ty2 ty1
- | otherwise = opt_univ1 env prov cvs' role ty1 ty2
- where
- cvs' = substDCoVarSet (liftingContextSubst env) cvs
-
-opt_univ1 :: LiftingContext -> UnivCoProvenance
- -> DCoVarSet -- Fully substituted by liftingContextSubst
- -> Role -> Type -> Type
- -> Coercion
-opt_univ1 env PhantomProv cvs' _r ty1 ty2
- = mkUnivCo PhantomProv cvs' Phantom ty1' ty2'
+opt_univ env sym prov deps role ty1 ty2
+ = let ty1' = substTyUnchecked (lcSubstLeft env) ty1
+ ty2' = substTyUnchecked (lcSubstRight env) ty2
+ deps' = map (opt_co1 env sym) deps
+ (ty1'', ty2'') = swapSym sym (ty1', ty2')
+ in
+ mkUnivCo prov deps' role ty1'' ty2''
+
+{-
+opt_univ env PhantomProv cvs _r ty1 ty2
+ = mkUnivCo PhantomProv cvs Phantom ty1' ty2'
where
ty1' = substTy (lcSubstLeft env) ty1
ty2' = substTy (lcSubstRight env) ty2
@@ -638,6 +636,7 @@ opt_univ1 env prov cvs' role oty1 oty2
ty2 = substTyUnchecked (lcSubstRight env) oty2
in
mkUnivCo prov cvs' role ty1 ty2
+-}
-------------
opt_transList :: HasDebugCallStack => InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
@@ -724,12 +723,12 @@ opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
mkInstCo (opt_trans is co1 co2) ty1
opt_trans_rule _
- in_co1@(UnivCo { uco_prov = p1, uco_role = r1, uco_lty = tyl1, uco_cvs = cvs1 })
- in_co2@(UnivCo { uco_prov = p2, uco_role = r2, uco_rty = tyr2, uco_cvs = cvs2 })
+ in_co1@(UnivCo { uco_prov = p1, uco_role = r1, uco_lty = tyl1, uco_deps = deps1 })
+ in_co2@(UnivCo { uco_prov = p2, uco_role = r2, uco_rty = tyr2, uco_deps = deps2 })
| p1 == p2 -- If the provenances are different, opt'ing will be very confusing
= assert (r1 == r2) $
fireTransRule "UnivCo" in_co1 in_co2 $
- mkUnivCo p1 (cvs1 `unionDVarSet` cvs2) r1 tyl1 tyr2
+ mkUnivCo p1 (deps1 ++ deps2) r1 tyl1 tyr2
-- Push transitivity down through matching top-level constructors.
opt_trans_rule is in_co1@(TyConAppCo r1 tc1 cos1) in_co2@(TyConAppCo r2 tc2 cos2)
=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -2462,13 +2462,10 @@ lintCoercion co@(FunCo { fco_role = r, fco_afl = afl, fco_afr = afr
-- See Note [Bad unsafe coercion]
lintCoercion co@(UnivCo { uco_role = r
- , uco_lty = ty1, uco_rty = ty2, uco_cvs = cvs })
+ , uco_lty = ty1, uco_rty = ty2, uco_deps = deps })
= do { ty1' <- lintType ty1
; ty2' <- lintType ty2
- ; subst <- getSubst
- ; mapM_ (checkTyCoVarInScope subst) (dVarSetElems cvs)
- -- Don't bother to return substituted fvs;
- -- they don't matter to Lint
+ ; deps' <- mapM lintCoercion deps
; let k1 = typeKind ty1'
k2 = typeKind ty2'
@@ -2476,7 +2473,7 @@ lintCoercion co@(UnivCo { uco_role = r
&& isTYPEorCONSTRAINT k2)
(checkTypes ty1 ty2)
- ; return (co { uco_lty = ty1', uco_rty = ty2' }) }
+ ; return (co { uco_lty = ty1', uco_rty = ty2', uco_deps = deps' }) }
where
report s = hang (text $ "Unsafe coercion: " ++ s)
2 (vcat [ text "From:" <+> ppr ty1
=====================================
compiler/GHC/Core/TyCo/FVs.hs
=====================================
@@ -652,8 +652,8 @@ 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 { uco_lty = t1, uco_rty = t2, uco_cvs = cvs}) fv_cand in_scope acc
- = (tyCoFVsOfCVs cvs `unionFV` tyCoFVsOfType t1
+tyCoFVsOfCo (UnivCo { uco_lty = t1, uco_rty = t2, uco_deps = deps}) fv_cand in_scope acc
+ = (tyCoFVsOfCos deps `unionFV` tyCoFVsOfType t1
`unionFV` tyCoFVsOfType t2) 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
@@ -668,10 +668,6 @@ tyCoFVsOfCoVar :: CoVar -> FV
tyCoFVsOfCoVar v fv_cand in_scope acc
= (unitFV v `unionFV` tyCoFVsOfType (varType v)) fv_cand in_scope acc
-tyCoFVsOfCVs :: DCoVarSet -> FV
-tyCoFVsOfCVs 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
tyCoFVsOfCos (co:cos) fv_cand in_scope acc = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCos cos) fv_cand in_scope acc
@@ -706,8 +702,8 @@ 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 { uco_lty = t1, uco_rty = t2, uco_cvs = cvs }) cv
- = not (cv `elemDVarSet` cvs)
+almost_devoid_co_var_of_co (UnivCo { uco_lty = t1, uco_rty = t2, uco_deps = deps }) cv
+ = almost_devoid_co_var_of_cos deps cv
&& almost_devoid_co_var_of_type t1 cv
&& almost_devoid_co_var_of_type t2 cv
almost_devoid_co_var_of_co (SymCo co) cv
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -77,7 +77,7 @@ import {-# SOURCE #-} GHC.Core.Type( chooseFunTyFlag, typeKind, typeTypeOrConstr
-- friends:
import GHC.Types.Var
-import GHC.Types.Var.Set( DCoVarSet, dVarSetElems, elemVarSet )
+import GHC.Types.Var.Set( elemVarSet )
import GHC.Core.TyCon
import GHC.Core.Coercion.Axiom
@@ -915,9 +915,7 @@ data Coercion
| UnivCo { uco_prov :: UnivCoProvenance
, uco_role :: Role
, uco_lty, uco_rty :: Type
- , uco_cvs :: !DCoVarSet -- Free coercion variables
- -- The set must contain all the in-scope coercion variables
- -- that the the proof represented by the coercion makes use of.
+ , uco_deps :: [Coercion] -- Coercions on which it depends
-- See Note [The importance of tracking free coercion variables].
}
-- Of kind (lty ~role rty)
@@ -1956,9 +1954,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 { uco_lty = t1, uco_rty = t2, uco_cvs = cvs })
+ go_co env (UnivCo { uco_lty = t1, uco_rty = t2, uco_deps = deps })
= go_ty env t1 `mappend` go_ty env t2
- `mappend` go_cvs env cvs
+ `mappend` go_cos env deps
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
@@ -1977,10 +1975,6 @@ foldTyCo (TyCoFolder { tcf_view = view
where
env' = tycobinder env tv Inferred
- -- 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
noView _ = Nothing
=====================================
compiler/GHC/Core/TyCo/Subst.hs
=====================================
@@ -878,8 +878,7 @@ subst_co subst co
go :: Coercion -> Coercion
go (Refl ty) = mkNomReflCo $! (go_ty ty)
go (GRefl r ty mco) = (mkGReflCo r $! (go_ty ty)) $! (go_mco mco)
- go (TyConAppCo r tc args)= let args' = map go args
- in args' `seqList` mkTyConAppCo r tc args'
+ go (TyConAppCo r tc args)= mkTyConAppCo r tc $! go_cos args
go (AppCo co arg) = (mkAppCo $! go co) $! go arg
go (ForAllCo tv visL visR kind_co co)
= case substForAllCoBndrUnchecked subst tv kind_co of
@@ -889,8 +888,8 @@ subst_co subst co
go (CoVarCo cv) = substCoVar subst cv
go (AxiomInstCo con ind cos) = mkAxiomInstCo con ind $! map go cos
go (UnivCo { uco_prov = p, uco_role = r
- , uco_lty = t1, uco_rty = t2, uco_cvs = cvs })
- = ((((mkUnivCo $! p) $! go_cvs cvs) $! r) $!
+ , uco_lty = t1, uco_rty = t2, uco_deps = deps })
+ = ((((mkUnivCo $! p) $! go_cos deps) $! r) $!
(go_ty t1)) $! (go_ty t2)
go (SymCo co) = mkSymCo $! (go co)
go (TransCo co1 co2) = (mkTransCo $! (go co1)) $! (go co2)
@@ -903,7 +902,8 @@ subst_co subst co
in cs1 `seqList` AxiomRuleCo c cs1
go (HoleCo h) = HoleCo $! go_hole h
- go_cvs cvs = substDCoVarSet subst cvs
+ go_cos cos = let cos' = map go cos
+ in cos' `seqList` cos'
-- See Note [Substituting in a coercion hole]
go_hole h@(CoercionHole { ch_co_var = cv })
=====================================
compiler/GHC/Core/TyCo/Tidy.hs
=====================================
@@ -239,7 +239,7 @@ tidyCo env@(_, subst) co
go (AxiomInstCo con ind cos) = AxiomInstCo con ind $! strictMap go cos
go co@(UnivCo { uco_lty = t1, uco_rty = t2 })
= co { uco_lty = tidyType env t1, uco_rty = tidyType env t2 }
- -- Don't bother to tidy the uco_cvs field
+ -- Don't bother to tidy the uco_deps field
go (SymCo co) = SymCo $! go co
go (TransCo co1 co2) = (TransCo $! go co1) $! go co2
go (SelCo d co) = SelCo d $! go co
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -967,9 +967,9 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar
go_co !env (CoVarCo cv) = covar env cv
go_co !env (HoleCo hole) = cohole env hole
go_co !env (UnivCo { uco_prov = p, uco_role = r
- , uco_lty = t1, uco_rty = t2, uco_cvs = cvs })
+ , uco_lty = t1, uco_rty = t2, uco_deps = deps })
= mkUnivCo <$> pure p
- <*> go_fcvs env (dVarSetElems cvs)
+ <*> go_cos env deps
<*> pure r
<*> go_ty env t1 <*> go_ty env t2
go_co !env (SymCo co) = mkSymCo <$> go_co env co
@@ -1000,12 +1000,6 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar
; return $ mkForAllCo tv' visL visR kind_co' co' }
-- See Note [Efficiency for ForAllCo case of mapTyCoX]
- -- 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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
compiler/GHC/CoreToIface.hs
=====================================
@@ -88,7 +88,6 @@ import GHC.Utils.Panic
import GHC.Utils.Misc
import Data.Maybe ( isNothing, catMaybes )
-import Data.List ( partition )
{- Note [Avoiding space leaks in toIface*]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -299,12 +298,8 @@ toIfaceCoercionX fr co
go (SubCo co) = IfaceSubCo (go co)
go (AxiomRuleCo co cs) = IfaceAxiomRuleCo (mkIfLclName (coaxrName co)) (map go cs)
go (AxiomInstCo c i cs) = IfaceAxiomInstCo (coAxiomName c) i (map go cs)
- go (UnivCo { uco_prov = p, uco_role = r, uco_lty = t1, uco_rty = t2, uco_cvs = cvs })
- = IfaceUnivCo 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 (UnivCo { uco_prov = p, uco_role = r, uco_lty = t1, uco_rty = t2, uco_deps = deps })
+ = IfaceUnivCo p r (toIfaceTypeX fr t1) (toIfaceTypeX fr t2) (map go deps)
go co@(TyConAppCo r tc cos)
= assertPpr (isNothing (tyConAppFunCo_maybe r tc cos)) (ppr co) $
=====================================
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 cvs fcvs)
- = IfaceUnivCo s r <$> rnIfaceType t1 <*> rnIfaceType t2 <*> pure cvs <*> pure fcvs
+rnIfaceCo (IfaceUnivCo s r t1 t2 deps)
+ = IfaceUnivCo s r <$> rnIfaceType t1 <*> rnIfaceType t2 <*> mapM rnIfaceCo deps
-- Renaming affects only type constructors, not coercion variables,
-- so no need to recurse into the free-var fields
rnIfaceCo (IfaceSymCo c)
=====================================
compiler/GHC/Iface/Syntax.hs
=====================================
@@ -1783,9 +1783,9 @@ freeNamesIfCoercion (IfaceCoVarCo _) = emptyNameSet
freeNamesIfCoercion (IfaceHoleCo _) = emptyNameSet
freeNamesIfCoercion (IfaceAxiomInstCo ax _ cos)
= unitNameSet ax &&& fnList freeNamesIfCoercion cos
-freeNamesIfCoercion (IfaceUnivCo _ _ t1 t2 _ _)
+freeNamesIfCoercion (IfaceUnivCo _ _ t1 t2 _)
= freeNamesIfType t1 &&& freeNamesIfType t2
- -- Ignoring free-var fields, which are all local,
+ -- Ignoring uco_deps field, which are all local,
-- and don't contribute to dependency analysis
freeNamesIfCoercion (IfaceSymCo c)
= freeNamesIfCoercion c
=====================================
compiler/GHC/Iface/Type.hs
=====================================
@@ -481,9 +481,7 @@ data IfaceCoercion
-- ^ 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 UnivCoProvenance Role IfaceType IfaceType [IfLclName] [Var]
- -- ^ Local covars and open (free) covars resp
- -- See Note [Free TyVars and CoVars in IfaceType]
+ | IfaceUnivCo UnivCoProvenance Role IfaceType IfaceType [IfaceCoercion]
| IfaceSymCo IfaceCoercion
| IfaceTransCo IfaceCoercion IfaceCoercion
| IfaceSelCo CoSel IfaceCoercion
@@ -701,9 +699,7 @@ 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 cvs fvs) = IfaceUnivCo prov r (go t1) (go t2) cvs fvs
- -- Don't bother to substitute in free vars
- -- See Note [Substitution on IfaceType]
+ go_co (IfaceUnivCo p r t1 t2 ds) = IfaceUnivCo p r (go t1) (go t2) (go_cos ds)
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)
@@ -2003,9 +1999,9 @@ 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 cvs fvs)
+ppr_co _ (IfaceUnivCo prov role ty1 ty2 ds)
= text "Univ" <> (parens $
- sep [ ppr role <+> ppr prov <> ppr cvs <> ppr fvs
+ sep [ ppr role <+> ppr prov <> ppr ds
, dcolon <+> ppr ty1 <> comma <+> ppr ty2 ])
ppr_co ctxt_prec (IfaceInstCo co ty)
@@ -2370,15 +2366,13 @@ instance Binary IfaceCoercion where
put_ bh a
put_ bh b
put_ bh c
- put_ bh (IfaceUnivCo a b c d cvs fcvs) = do
+ put_ bh (IfaceUnivCo a b c d deps) = do
putByte bh 9
put_ bh a
put_ bh b
put_ bh c
put_ bh d
- assertPpr (null fcvs) (ppr cvs $$ ppr fcvs) $
- -- See Note [Free TyVars and CoVars in IfaceType]
- put_ bh cvs
+ put_ bh deps
put_ bh (IfaceSymCo a) = do
putByte bh 10
put_ bh a
@@ -2452,8 +2446,8 @@ instance Binary IfaceCoercion where
b <- get bh
c <- get bh
d <- get bh
- cvs <- get bh
- return $ IfaceUnivCo a b c d cvs []
+ deps <- get bh
+ return $ IfaceUnivCo a b c d deps
10-> do a <- get bh
return $ IfaceSymCo a
11-> do a <- get bh
@@ -2516,8 +2510,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 cvs fcvs -> rnf f1 `seq` f2 `seq` rnf f3 `seq` rnf f4
- `seq` rnf cvs `seq` rnf fcvs
+ IfaceUnivCo f1 f2 f3 f4 deps -> rnf f1 `seq` f2 `seq` rnf f3 `seq` rnf f4 `seq` rnf deps
IfaceSymCo f1 -> rnf f1
IfaceTransCo f1 f2 -> rnf f1 `seq` rnf f2
IfaceSelCo f1 f2 -> rnf f1 `seq` rnf f2
=====================================
compiler/GHC/IfaceToCore.hs
=====================================
@@ -1471,15 +1471,13 @@ tcIfaceCo = go
go (IfaceForAllCo tv visL visR k c) = do { k' <- go k
; bindIfaceBndr tv $ \ tv' ->
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 cvs fcvs)
- = do { t1' <- tcIfaceType t1; t2' <- tcIfaceType t2
- ; cvs' <- assertPpr (null fcvs) (ppr fcvs) $
- mapM tcIfaceLclId cvs
- ; return (UnivCo { uco_prov = p, uco_role = r
- , uco_lty = t1', uco_rty = t2'
- , uco_cvs = mkDVarSet cvs' }) }
+ 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 ds) = do { t1' <- tcIfaceType t1; t2' <- tcIfaceType t2
+ ; ds' <- mapM go ds
+ ; return (UnivCo { uco_prov = p, uco_role = r
+ , uco_lty = t1', uco_rty = t2'
+ , uco_deps = ds' }) }
go (IfaceSymCo c) = SymCo <$> go c
go (IfaceTransCo c1 c2) = TransCo <$> go c1
<*> go c2
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -1564,10 +1564,10 @@ 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 { uco_lty = t1, uco_rty = t2, uco_cvs = cvs })
+ go_co dv (UnivCo { uco_lty = t1, uco_rty = t2, uco_deps = deps })
= do { dv1 <- collect_cand_qtvs orig_ty True cur_lvl bound dv t1
; dv2 <- collect_cand_qtvs orig_ty True cur_lvl bound dv1 t2
- ; strictFoldDVarSet zt_cv (return dv2) cvs }
+ ; foldM go_co dv2 deps }
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
=====================================
testsuite/tests/pmcheck/should_compile/T11195.hs
=====================================
@@ -75,18 +75,10 @@ opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
| ty1 `eqCoercion` ty2
, co1 `compatible_co` co2 = undefined
-opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1 _fvs1)
- in_co2@(UnivCo p2 r2 _tyl2 tyr2 _fvs2)
- | Just prov' <- opt_trans_prov p1 p2 = undefined
- where
+opt_trans_rule is (UnivCo { uco_prov = p1 })
+ (UnivCo ( uco_prov = p2 })
+ | p1 == p2 = undefined
-- if the provenances are different, opt'ing will be very confusing
- opt_trans_prov PhantomProv PhantomProv
- = Just $ PhantomProv
- opt_trans_prov ProofIrrelProv ProofIrrelProv
- = Just $ ProofIrrelProv
- opt_trans_prov (PluginProv str1 _) (PluginProv str2 _)
- | str1 == str2 = Just p1
- opt_trans_prov _ _ = Nothing
-- Push transitivity down through matching top-level constructors.
opt_trans_rule is in_co1@(TyConAppCo r1 tc1 cos1)
=====================================
testsuite/tests/tcplugins/CtIdPlugin.hs
=====================================
@@ -42,7 +42,7 @@ solver :: [String]
-> PluginDefs -> EvBindsVar -> [Ct] -> [Ct]
-> TcPluginM TcPluginSolveResult
solver _args defs ev givens wanteds = do
- let pluginCo = mkUnivCo (PluginProv "CtIdPlugin" emptyUniqDSet) Representational -- Empty is fine. This plugin does not use "givens".
+ 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
=====================================
@@ -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".
+ co = mkUnivCo ( PluginProv "RewritePlugin") emptyUniqDSet Nominal -- Empty is fine. This plugin does not use "givens".
( mkTyConApp tyCon args ) res
=====================================
testsuite/tests/tcplugins/TyFamPlugin.hs
=====================================
@@ -80,6 +80,6 @@ solveCt ( PluginDefs {..} ) ct@( classifyPredType . ctPred -> EqPred NomEq lhs r
, let
evTerm :: EvTerm
evTerm = EvExpr . Coercion
- $ mkUnivCo ( PluginProv "TyFamPlugin" emptyUniqDSet) Nominal lhs rhs -- Empty is fine. This plugin does not use "givens".
+ $ 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/e2142bf459a39d1c9ac18c1719b4127ff314d840
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e2142bf459a39d1c9ac18c1719b4127ff314d840
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/20240612/a74cda8b/attachment-0001.html>
More information about the ghc-commits
mailing list