summaryrefslogtreecommitdiff
path: root/compiler/GHC/Core/TyCo
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/GHC/Core/TyCo')
-rw-r--r--compiler/GHC/Core/TyCo/FVs.hs39
-rw-r--r--compiler/GHC/Core/TyCo/Rep.hs68
-rw-r--r--compiler/GHC/Core/TyCo/Rep.hs-boot1
-rw-r--r--compiler/GHC/Core/TyCo/Subst.hs8
-rw-r--r--compiler/GHC/Core/TyCo/Tidy.hs2
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'