diff options
Diffstat (limited to 'compiler/GHC/Core/TyCo')
-rw-r--r-- | compiler/GHC/Core/TyCo/FVs.hs | 39 | ||||
-rw-r--r-- | compiler/GHC/Core/TyCo/Rep.hs | 68 | ||||
-rw-r--r-- | compiler/GHC/Core/TyCo/Rep.hs-boot | 1 | ||||
-rw-r--r-- | compiler/GHC/Core/TyCo/Subst.hs | 8 | ||||
-rw-r--r-- | compiler/GHC/Core/TyCo/Tidy.hs | 2 |
5 files changed, 103 insertions, 15 deletions
diff --git a/compiler/GHC/Core/TyCo/FVs.hs b/compiler/GHC/Core/TyCo/FVs.hs index 9d9cd6b169..c2921ec057 100644 --- a/compiler/GHC/Core/TyCo/FVs.hs +++ b/compiler/GHC/Core/TyCo/FVs.hs @@ -16,11 +16,13 @@ module GHC.Core.TyCo.FVs tyCoVarsOfCo, tyCoVarsOfCos, tyCoVarsOfMCo, coVarsOfType, coVarsOfTypes, coVarsOfCo, coVarsOfCos, - coVarsOfCoDSet, coVarsOfCosDSet, + coVarsOfCosDSet, tyCoVarsOfCoDSet, tyCoVarsOfCosDSet, tyCoFVsOfCo, tyCoFVsOfCos, tyCoVarsOfCoList, + coVarsHolesOfCo, coVarsHolesOfCos, + almostDevoidCoVarOfCo, -- Injective free vars @@ -52,7 +54,7 @@ import GHC.Core.TyCo.Rep import GHC.Core.TyCon import GHC.Types.Var import GHC.Utils.FV - +import GHC.Types.Unique.DSet import GHC.Types.Unique.FM import GHC.Types.Var.Set import GHC.Types.Var.Env @@ -431,9 +433,6 @@ deepCoVarFolder = TyCoFolder { tcf_view = noView -- See Note [CoercionHoles and coercion free variables] -- in GHC.Core.TyCo.Rep -coVarsOfCoDSet :: Coercion -> DCoVarSet -coVarsOfCoDSet = fvDVarSet . filterFV isCoVar . tyCoFVsOfCo - coVarsOfCosDSet :: [Coercion] -> DCoVarSet coVarsOfCosDSet = fvDVarSet . filterFV isCoVar . tyCoFVsOfCos @@ -648,7 +647,11 @@ tyCoFVsOfCo (KindCo co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in tyCoFVsOfCo (SubCo co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc tyCoFVsOfCo (AxiomRuleCo _ cs) fv_cand in_scope acc = tyCoFVsOfCos cs fv_cand in_scope acc tyCoFVsOfCo (ZappedCo _ a b vs) fv_cand in_scope acc - = (tyCoFVsOfType a `unionFV` tyCoFVsOfType b `unionFV` mkFVs (dVarSetElems vs)) + = (tyCoFVsOfType a `unionFV` + tyCoFVsOfType b `unionFV` + mapUnionFV tyCoFVsOfCoVar (dVarSetElems (freeCoVars vs)) `unionFV` + mapUnionFV (tyCoFVsOfCoVar . coHoleCoVar) (uniqDSetToList (freeCoHoles vs))) + -- See Note [CoercionHoles and coercion free variables] fv_cand in_scope acc tyCoFVsOfCoVar :: CoVar -> FV @@ -717,10 +720,12 @@ almost_devoid_co_var_of_co (SubCo co) cv = almost_devoid_co_var_of_co co cv almost_devoid_co_var_of_co (AxiomRuleCo _ cs) cv = almost_devoid_co_var_of_cos cs cv -almost_devoid_co_var_of_co (ZappedCo _ t1 t2 cvs) cv +almost_devoid_co_var_of_co (ZappedCo _ t1 t2 vs) cv = almost_devoid_co_var_of_type t1 cv && almost_devoid_co_var_of_type t2 cv - && not (cv `elemDVarSet` cvs) + && not (cv `elemDVarSet` freeCoVars vs) + && not (cv `elemDVarSet` mapUniqDSet coHoleCoVar (freeCoHoles vs)) + -- there should be no holes here, anyway almost_devoid_co_var_of_cos :: [Coercion] -> CoVar -> Bool almost_devoid_co_var_of_cos [] _ = True @@ -1014,3 +1019,21 @@ tyCoVarsOfTypeWellScoped = scopedSort . tyCoVarsOfTypeList -- | Get the free vars of types in scoped order tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar] tyCoVarsOfTypesWellScoped = scopedSort . tyCoVarsOfTypesList + +{- ********************************************************************* +* * + Free coercion holes +* * +********************************************************************* -} + +coVarsHolesOfCo :: Coercion -> FreeCoVarsHoles +coVarsHolesOfCos :: [Coercion] -> FreeCoVarsHoles +(coVarsHolesOfCo, coVarsHolesOfCos) = (go_co, go_cos) + where + (go_ty, _, go_co, go_cos) = foldTyCo folder () + folder = TyCoFolder { tcf_view = noView + , tcf_tyvar = \ _ tv -> go_ty (varType tv) + , tcf_covar = \ _ cv -> mkFreeCoVarsHoles (unitDVarSet cv) mempty `mappend` + go_ty (varType cv) + , tcf_hole = \ _ h -> mkFreeCoVarsHoles mempty (unitUniqDSet h) + , tcf_tycobinder = const2 } diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs index 79dea31396..ee9712281e 100644 --- a/compiler/GHC/Core/TyCo/Rep.hs +++ b/compiler/GHC/Core/TyCo/Rep.hs @@ -41,6 +41,12 @@ module GHC.Core.TyCo.Rep ( CoercionN, CoercionR, CoercionP, KindCoercion, MCoercion(..), MCoercionR, MCoercionN, + FreeCoVarsHoles, + mkFreeCoVarsHoles, updateFreeCoVars, updateFreeCoVarsM, + sizeFreeCoVarsHoles, + freeCoVars, freeCoHoles, + + -- * Functions over types mkNakedTyConTy, mkTyVarTy, mkTyVarTys, mkTyCoVarTy, mkTyCoVarTys, @@ -98,6 +104,10 @@ import GHC.Utils.Panic -- libraries import qualified Data.Data as Data hiding ( TyCon ) import Data.IORef ( IORef ) -- for CoercionHole +import GHC.Types.Unique.DSet +import qualified Data.Semigroup -- for (<>) in a Semigroup instance only +import GHC.Utils.Panic.Plain + {- ********************************************************************** * * @@ -1209,7 +1219,7 @@ data Coercion | HoleCo CoercionHole -- ^ See Note [Coercion holes] -- Only present during typechecking - | ZappedCo Role Type Type DCoVarSet -- TODO (RAE): Comment + | ZappedCo Role Type Type !FreeCoVarsHoles -- TODO (RAE): Comment deriving Data.Data type CoercionN = Coercion -- always nominal @@ -1661,6 +1671,55 @@ instance Outputable CoercionHole where instance Uniquable CoercionHole where getUnique (CoercionHole { ch_co_var = cv }) = getUnique cv +-- | Stores the free covars and coercion holes from a type or coercion; +-- these are often needed together +data FreeCoVarsHoles = FCVH_Empty -- avoid allocating a new FCVH node at every <> + | FCVH !DCoVarSet !(UniqDSet CoercionHole) + deriving Data.Data + +mkFreeCoVarsHoles :: DCoVarSet -> UniqDSet CoercionHole -> FreeCoVarsHoles +mkFreeCoVarsHoles = FCVH + +-- this one preserves FCVH_Empty +-- Pre-condition: f empty == empty +updateFreeCoVars :: FreeCoVarsHoles -> (DCoVarSet -> DCoVarSet) -> FreeCoVarsHoles +updateFreeCoVars FCVH_Empty f = assert (isEmptyDVarSet (f emptyDVarSet)) + FCVH_Empty +updateFreeCoVars (FCVH cvs hs) f = FCVH (f cvs) hs + +-- this one preserves FCVH_Empty +-- Pre-condition: f empty == empty (and has no side effects) +updateFreeCoVarsM :: Applicative m => FreeCoVarsHoles -> (DCoVarSet -> m DCoVarSet) + -> m FreeCoVarsHoles +updateFreeCoVarsM FCVH_Empty _ = pure FCVH_Empty +updateFreeCoVarsM (FCVH cvs hs) f = FCVH <$> f cvs <*> pure hs + +freeCoVars :: FreeCoVarsHoles -> DCoVarSet +freeCoVars FCVH_Empty = emptyDVarSet +freeCoVars (FCVH cvs _) = cvs + +freeCoHoles :: FreeCoVarsHoles -> UniqDSet CoercionHole +freeCoHoles FCVH_Empty = emptyUniqDSet +freeCoHoles (FCVH _ hs) = hs + +sizeFreeCoVarsHoles :: FreeCoVarsHoles -> Int +sizeFreeCoVarsHoles FCVH_Empty = 0 +sizeFreeCoVarsHoles (FCVH cvs hs) = sizeDVarSet cvs + sizeUniqDSet hs + +instance Outputable FreeCoVarsHoles where + ppr FCVH_Empty = braces empty + ppr (FCVH vs hs) = braces (fcat (punctuate comma (map ppr (dVarSetElems vs))) <> vbar <> + fcat (punctuate comma (map ppr (uniqDSetToList hs)))) + +instance Semigroup FreeCoVarsHoles where + FCVH_Empty <> FCVH_Empty = FCVH_Empty + FCVH_Empty <> other = other + other <> FCVH_Empty = other + FCVH vs1 hs1 <> FCVH vs2 hs2 = FCVH (vs1 `mappend` vs2) (hs1 `mappend` hs2) + +instance Monoid FreeCoVarsHoles where + mempty = FCVH_Empty + {- Note [Phantom coercions] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider @@ -1936,9 +1995,10 @@ foldTyCo (TyCoFolder { tcf_view = view go_co env (InstCo co arg) = go_co env co `mappend` go_co env arg go_co env (KindCo co) = go_co env co go_co env (SubCo co) = go_co env co - go_co env (ZappedCo _ t1 t2 cvs) = go_ty env t1 `mappend` + go_co env (ZappedCo _ t1 t2 vs) = go_ty env t1 `mappend` go_ty env t2 `mappend` - foldMap (covar env) cvs + foldMap (covar env) (freeCoVars vs) `mappend` + foldMap (cohole env) (freeCoHoles vs) go_co env (ForAllCo tv kind_co co) = go_co env kind_co `mappend` go_ty env (varType tv) `mappend` go_co env' co @@ -2004,7 +2064,7 @@ coercionSize (InstCo co arg) = 1 + coercionSize co + coercionSize arg coercionSize (KindCo co) = 1 + coercionSize co coercionSize (SubCo co) = 1 + coercionSize co coercionSize (AxiomRuleCo _ cs) = 1 + sum (map coercionSize cs) -coercionSize (ZappedCo _ a b vs) = 1 + typeSize a + typeSize b + sizeDVarSet vs +coercionSize (ZappedCo _ a b vs) = 1 + typeSize a + typeSize b + sizeFreeCoVarsHoles vs provSize :: UnivCoProvenance -> Int provSize (PhantomProv co) = 1 + coercionSize co diff --git a/compiler/GHC/Core/TyCo/Rep.hs-boot b/compiler/GHC/Core/TyCo/Rep.hs-boot index f2e59d534f..89138ebf3a 100644 --- a/compiler/GHC/Core/TyCo/Rep.hs-boot +++ b/compiler/GHC/Core/TyCo/Rep.hs-boot @@ -8,6 +8,7 @@ import {-# SOURCE #-} GHC.Core.TyCon ( TyCon ) data Type data Coercion +data FreeCoVarsHoles data UnivCoProvenance data TyLit data TyCoBinder diff --git a/compiler/GHC/Core/TyCo/Subst.hs b/compiler/GHC/Core/TyCo/Subst.hs index defdad591c..e9a16d60e8 100644 --- a/compiler/GHC/Core/TyCo/Subst.hs +++ b/compiler/GHC/Core/TyCo/Subst.hs @@ -85,6 +85,7 @@ import GHC.Utils.Panic import GHC.Utils.Panic.Plain import Data.List (mapAccumL) +import GHC.Types.Unique.DSet {- %************************************************************************ @@ -859,8 +860,11 @@ subst_co subst co go (AxiomRuleCo c cs) = let cs1 = map go cs in cs1 `seqList` AxiomRuleCo c cs1 go (HoleCo h) = HoleCo $! go_hole h - go (ZappedCo r t1 t2 vs) = ((mkZappedCo r $! go_ty t1) $! go_ty t2) $! - coVarsOfCosDSet (map (substCoVar subst) (dVarSetElems vs)) + go (ZappedCo r t1 t2 vs) = ((mkZappedCo r $! go_ty t1) $! go_ty t2) $! new_vs + where + cos_from_vs = map (substCoVar subst) (dVarSetElems (freeCoVars vs)) + new_vs = coVarsHolesOfCos cos_from_vs `mappend` + mkFreeCoVarsHoles mempty (mapUniqDSet go_hole (freeCoHoles vs)) go_prov (PhantomProv kco) = PhantomProv (go kco) go_prov (ProofIrrelProv kco) = ProofIrrelProv (go kco) diff --git a/compiler/GHC/Core/TyCo/Tidy.hs b/compiler/GHC/Core/TyCo/Tidy.hs index 28f4a1f504..880dc3c725 100644 --- a/compiler/GHC/Core/TyCo/Tidy.hs +++ b/compiler/GHC/Core/TyCo/Tidy.hs @@ -248,7 +248,7 @@ tidyCo env@(_, subst) co go (SubCo co) = SubCo $! go co go (AxiomRuleCo ax cos) = AxiomRuleCo ax $ strictMap go cos go (ZappedCo r t1 t2 vs) = ((ZappedCo r $! tidyType env t1) $! tidyType env t2) $! - mapDVarSet go_covar vs + updateFreeCoVars vs (mapDVarSet go_covar) go_covar cv | Just cv' <- lookupVarEnv subst cv = cv' |