[Git][ghc/ghc][wip/romes/splitting-id] Compile TyCo.FVs and more
Rodrigo Mesquita (@alt-romes)
gitlab at gitlab.haskell.org
Sun May 28 00:20:49 UTC 2023
Rodrigo Mesquita pushed to branch wip/romes/splitting-id at Glasgow Haskell Compiler / GHC
Commits:
c7b752c3 by Rodrigo Mesquita at 2023-05-28T01:20:37+01:00
Compile TyCo.FVs and more
- - - - -
8 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/TyCo/FVs.hs
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Core/TyCo/Rep.hs-boot
- compiler/GHC/Types/Unique.hs
- compiler/GHC/Types/Var.hs
- compiler/GHC/Types/Var/Env.hs
- compiler/GHC/Types/Var/Set.hs
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -591,11 +591,6 @@ coVarKindsTypesRole cv
= pprPanic "coVarKindsTypesRole, non coercion variable"
(ppr cv $$ ppr (varType cv))
-coVarKind :: CoVar -> Type
-coVarKind cv
- = assert (isCoVar cv )
- varType cv
-
coVarRole :: CoVar -> Role
coVarRole cv
= eqTyConRole (case tyConAppTyCon_maybe (varType cv) of
=====================================
compiler/GHC/Core/TyCo/FVs.hs
=====================================
@@ -1,4 +1,5 @@
{-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE LambdaCase #-}
module GHC.Core.TyCo.FVs
( shallowTyCoVarsOfType, shallowTyCoVarsOfTypes,
@@ -51,6 +52,7 @@ module GHC.Core.TyCo.FVs
Endo(..), runTyCoVars
) where
+import Data.Either
import GHC.Prelude
import {-# SOURCE #-} GHC.Core.Type( partitionInvisibleTypes, coreView, rewriterView )
@@ -102,7 +104,7 @@ Examples:
Type Shallow Deep
---------------------------------
(a : (k:Type)) {a} {a,k}
- forall (a:(k:Type)). a {k} {k}
+ forall (a:(k:Type)). a { } {k}
(a:k->Type) (b:k) {a,b} {a,b,k}
-}
@@ -317,18 +319,27 @@ deep_cos :: [Coercion] -> Endo TyCoVarSet
deepTcvFolder :: TyCoFolder TyCoVarSet (Endo TyCoVarSet)
deepTcvFolder = TyCoFolder { tcf_view = noView
- , tcf_tyvar = do_tcv, tcf_covar = do_tcv
+ , tcf_tyvar = do_tv, tcf_covar = do_cv
, tcf_hole = do_hole, tcf_tycobinder = do_bndr }
where
- do_tcv is v = Endo do_it
+ do_tv :: TyCoVarSet -> TyVar -> Endo TyCoVarSet
+ do_tv is v = Endo do_it
where
- do_it acc | v `elemVarSet` is = acc
- | v `elemVarSet` acc = acc
- | otherwise = appEndo (deep_ty (varType v)) $
- acc `extendVarSet` v
+ do_it acc | Left v `elemVarSet` is = acc
+ | Left v `elemVarSet` acc = acc
+ | otherwise = appEndo (deep_ty (varTypeTyVar v)) $
+ acc `extendVarSet` Left v
+
+ do_cv :: TyCoVarSet -> CoVar -> Endo TyCoVarSet
+ do_cv is v = Endo do_it
+ where
+ do_it acc | Right v `elemVarSet` is = acc
+ | Right v `elemVarSet` acc = acc
+ | otherwise = appEndo (deep_ty (varTypeId v)) $
+ acc `extendVarSet` Right v
do_bndr is tcv _ = extendVarSet is tcv
- do_hole is hole = do_tcv is (coHoleCoVar hole)
+ do_hole is hole = do_cv is (coHoleCoVar hole)
-- See Note [CoercionHoles and coercion free variables]
-- in GHC.Core.TyCo.Rep
@@ -375,14 +386,22 @@ shallow_cos :: [Coercion] -> Endo TyCoVarSet
shallowTcvFolder :: TyCoFolder TyCoVarSet (Endo TyCoVarSet)
shallowTcvFolder = TyCoFolder { tcf_view = noView
- , tcf_tyvar = do_tcv, tcf_covar = do_tcv
+ , tcf_tyvar = do_tv, tcf_covar = do_cv
, tcf_hole = do_hole, tcf_tycobinder = do_bndr }
where
- do_tcv is v = Endo do_it
+ do_tv :: TyCoVarSet -> TyVar -> Endo TyCoVarSet
+ do_tv is v = Endo do_it
where
- do_it acc | v `elemVarSet` is = acc
- | v `elemVarSet` acc = acc
- | otherwise = acc `extendVarSet` v
+ do_it acc | Left v `elemVarSet` is = acc
+ | Left v `elemVarSet` acc = acc
+ | otherwise = acc `extendVarSet` Left v
+
+ do_cv :: TyCoVarSet -> CoVar -> Endo TyCoVarSet
+ do_cv is v = Endo do_it
+ where
+ do_it acc | Right v `elemVarSet` is = acc
+ | Right v `elemVarSet` acc = acc
+ | otherwise = acc `extendVarSet` Right v
do_bndr is tcv _ = extendVarSet is tcv
do_hole _ _ = mempty -- Ignore coercion holes
@@ -411,10 +430,10 @@ coVarsOfTypes :: [Type] -> CoVarSet
coVarsOfCo :: Coercion -> CoVarSet
coVarsOfCos :: [Coercion] -> CoVarSet
-coVarsOfType ty = runTyCoVars (deep_cv_ty ty)
-coVarsOfTypes tys = runTyCoVars (deep_cv_tys tys)
-coVarsOfCo co = runTyCoVars (deep_cv_co co)
-coVarsOfCos cos = runTyCoVars (deep_cv_cos cos)
+coVarsOfType ty = rightsVarSet $ runTyCoVars (mapVarSet Right <$> deep_cv_ty ty)
+coVarsOfTypes tys = rightsVarSet $ runTyCoVars (mapVarSet Right <$> deep_cv_tys tys)
+coVarsOfCo co = rightsVarSet $ runTyCoVars (mapVarSet Right <$> deep_cv_co co)
+coVarsOfCos cos = rightsVarSet $ runTyCoVars (mapVarSet Right <$> deep_cv_cos cos)
deep_cv_ty :: Type -> Endo CoVarSet
deep_cv_tys :: [Type] -> Endo CoVarSet
@@ -436,9 +455,9 @@ deepCoVarFolder = TyCoFolder { tcf_view = noView
do_covar is v = Endo do_it
where
- do_it acc | v `elemVarSet` is = acc
+ do_it acc | Right v `elemVarSet` is = acc
| v `elemVarSet` acc = acc
- | otherwise = appEndo (deep_cv_ty (varType v)) $
+ | otherwise = appEndo (deep_cv_ty (varTypeId v)) $
acc `extendVarSet` v
do_bndr is tcv _ = extendVarSet is tcv
@@ -459,7 +478,7 @@ closeOverKinds :: TyCoVarSet -> TyCoVarSet
-- add the deep free variables of its kind
closeOverKinds vs = nonDetStrictFoldVarSet do_one vs vs
where
- do_one v acc = appEndo (deep_ty (varType v)) acc
+ do_one v acc = appEndo (deep_ty (varTypeTyCoVar v)) acc
{- --------------- Alternative version 1 (using FV) ------------
closeOverKinds = fvVarSet . closeOverKindsFV . nonDetEltsUniqSet
@@ -520,50 +539,60 @@ close_over_kinds wl acc
* *
********************************************************************* -}
+-- ROMES:TODO: In the following functions, the right thing to do is parametrize FV rather than converting to and from Var (the last being unsafe...)
+unsafeVarToTyVar :: [Var] -> [TyVar]
+unsafeVarToTyVar = map (\case TV v -> v; _ -> panic "unsafeVarToTyVar")
+unsafeVarToTyCoVar :: [Var] -> [TyCoVar]
+unsafeVarToTyCoVar = map (\case TV v -> Left v; I i -> Right i; _ -> panic "unsafeVarToTyCoVar")
+unsafeVarSetToTyVarSet :: DVarSet -> DTyVarSet
+unsafeVarSetToTyVarSet = mapDVarSet (\case TV v -> v; _ -> panic "unsafeVarSetToTyVarSet")
+unsafeVarSetToTyCoVarSet :: DVarSet -> DTyCoVarSet
+unsafeVarSetToTyCoVarSet = mapDVarSet (\case TV v -> Left v; I i -> Right i; _ -> panic "unsafeVarSetToTyCoVarSet")
+
-- | Given a list of tyvars returns a deterministic FV computation that
-- returns the given tyvars with the kind variables free in the kinds of the
-- given tyvars.
closeOverKindsFV :: [TyVar] -> FV
closeOverKindsFV tvs =
- mapUnionFV (tyCoFVsOfType . tyVarKind) tvs `unionFV` mkFVs tvs
+ mapUnionFV (tyCoFVsOfType . tyVarKind) tvs `unionFV` mkFVs (map TV tvs)
-- | Add the kind variables free in the kinds of the tyvars in the given set.
-- Returns a deterministically ordered list.
closeOverKindsList :: [TyVar] -> [TyVar]
-closeOverKindsList tvs = fvVarList $ closeOverKindsFV tvs
+closeOverKindsList tvs = unsafeVarToTyVar $ fvVarList $ closeOverKindsFV tvs
-- | Add the kind variables free in the kinds of the tyvars in the given set.
-- Returns a deterministic set.
closeOverKindsDSet :: DTyVarSet -> DTyVarSet
-closeOverKindsDSet = fvDVarSet . closeOverKindsFV . dVarSetElems
+closeOverKindsDSet = unsafeVarSetToTyVarSet . fvDVarSet . closeOverKindsFV . dVarSetElems
-- | `tyCoFVsOfType` that returns free variables of a type in a deterministic
-- set. For explanation of why using `VarSet` is not deterministic see
-- Note [Deterministic FV] in "GHC.Utils.FV".
tyCoVarsOfTypeDSet :: Type -> DTyCoVarSet
-- See Note [Free variables of types]
-tyCoVarsOfTypeDSet ty = fvDVarSet $ tyCoFVsOfType ty
+tyCoVarsOfTypeDSet ty = unsafeVarSetToTyCoVarSet $ fvDVarSet $ tyCoFVsOfType ty
-- | `tyCoFVsOfType` that returns free variables of a type in deterministic
-- order. For explanation of why using `VarSet` is not deterministic see
-- Note [Deterministic FV] in "GHC.Utils.FV".
tyCoVarsOfTypeList :: Type -> [TyCoVar]
-- See Note [Free variables of types]
-tyCoVarsOfTypeList ty = fvVarList $ tyCoFVsOfType ty
+tyCoVarsOfTypeList ty = unsafeVarToTyCoVar $ fvVarList $ tyCoFVsOfType ty
-- | Returns free variables of types, including kind variables as
-- a deterministic set. For type synonyms it does /not/ expand the
-- synonym.
tyCoVarsOfTypesDSet :: [Type] -> DTyCoVarSet
-- See Note [Free variables of types]
-tyCoVarsOfTypesDSet tys = fvDVarSet $ tyCoFVsOfTypes tys
+tyCoVarsOfTypesDSet tys = unsafeVarSetToTyCoVarSet $ fvDVarSet $ tyCoFVsOfTypes tys
-- | Returns free variables of types, including kind variables as
-- a deterministically ordered list. For type synonyms it does /not/ expand the
-- synonym.
tyCoVarsOfTypesList :: [Type] -> [TyCoVar]
-- See Note [Free variables of types]
-tyCoVarsOfTypesList tys = fvVarList $ tyCoFVsOfTypes tys
+tyCoVarsOfTypesList tys = unsafeVarToTyCoVar $ fvVarList $ tyCoFVsOfTypes tys
-- | The worker for `tyCoFVsOfType` and `tyCoFVsOfTypeList`.
-- The previous implementation used `unionVarSet` which is O(n+m) and can
@@ -577,12 +606,12 @@ tyCoVarsOfTypesList tys = fvVarList $ tyCoFVsOfTypes tys
tyCoFVsOfType :: Type -> FV
-- See Note [Free variables of types]
tyCoFVsOfType (TyVarTy v) f bound_vars (acc_list, acc_set)
- | not (f v) = (acc_list, acc_set)
- | v `elemVarSet` bound_vars = (acc_list, acc_set)
- | v `elemVarSet` acc_set = (acc_list, acc_set)
+ | not (f (TV v)) = (acc_list, acc_set)
+ | TV v `elemVarSet` bound_vars = (acc_list, acc_set)
+ | TV v `elemVarSet` acc_set = (acc_list, acc_set)
| otherwise = tyCoFVsOfType (tyVarKind v) f
emptyVarSet -- See Note [Closing over free variable kinds]
- (v:acc_list, extendVarSet acc_set v)
+ (TV v:acc_list, extendVarSet acc_set (TV v))
tyCoFVsOfType (TyConApp _ tys) f bound_vars acc = tyCoFVsOfTypes tys f bound_vars acc
tyCoFVsOfType (LitTy {}) f bound_vars acc = emptyFV f bound_vars acc
tyCoFVsOfType (AppTy fun arg) f bound_vars acc = (tyCoFVsOfType fun `unionFV` tyCoFVsOfType arg) f bound_vars acc
@@ -595,13 +624,13 @@ tyCoFVsBndr :: ForAllTyBinder -> FV -> FV
-- Free vars of (forall b. <thing with fvs>)
tyCoFVsBndr (Bndr tv _) fvs = tyCoFVsVarBndr tv fvs
-tyCoFVsVarBndrs :: [Var] -> FV -> FV
+tyCoFVsVarBndrs :: [TyCoVar] -> FV -> FV
tyCoFVsVarBndrs vars fvs = foldr tyCoFVsVarBndr fvs vars
-tyCoFVsVarBndr :: Var -> FV -> FV
-tyCoFVsVarBndr var fvs
- = tyCoFVsOfType (varType var) -- Free vars of its type/kind
- `unionFV` delFV var fvs -- Delete it from the thing-inside
+tyCoFVsVarBndr :: TyCoVar -> FV -> FV
+tyCoFVsVarBndr tycov fvs
+ = tyCoFVsOfType (varTypeTyCoVar tycov) -- Free vars of its type/kind
+ `unionFV` delFV (tyCoVarToVar tycov) fvs -- Delete it from the thing-inside
tyCoFVsOfTypes :: [Type] -> FV
-- See Note [Free variables of types]
@@ -611,11 +640,11 @@ tyCoFVsOfTypes [] fv_cand in_scope acc = emptyFV fv_cand in_scope acc
-- | Get a deterministic set of the vars free in a coercion
tyCoVarsOfCoDSet :: Coercion -> DTyCoVarSet
-- See Note [Free variables of types]
-tyCoVarsOfCoDSet co = fvDVarSet $ tyCoFVsOfCo co
+tyCoVarsOfCoDSet co = unsafeVarSetToTyCoVarSet $ fvDVarSet $ tyCoFVsOfCo co
tyCoVarsOfCoList :: Coercion -> [TyCoVar]
-- See Note [Free variables of types]
-tyCoVarsOfCoList co = fvVarList $ tyCoFVsOfCo co
+tyCoVarsOfCoList co = unsafeVarToTyCoVar $ fvVarList $ tyCoFVsOfCo co
tyCoFVsOfMCo :: MCoercion -> FV
tyCoFVsOfMCo MRefl = emptyFV
@@ -655,7 +684,7 @@ tyCoFVsOfCo (AxiomRuleCo _ cs) fv_cand in_scope acc = tyCoFVsOfCos cs fv_cand i
tyCoFVsOfCoVar :: CoVar -> FV
tyCoFVsOfCoVar v fv_cand in_scope acc
- = (unitFV v `unionFV` tyCoFVsOfType (varType v)) fv_cand in_scope acc
+ = (unitFV (I v) `unionFV` tyCoFVsOfType (varTypeId v)) fv_cand in_scope acc
tyCoFVsOfProv :: UnivCoProvenance -> FV
tyCoFVsOfProv (PhantomProv co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
@@ -688,7 +717,7 @@ almost_devoid_co_var_of_co (AppCo co arg) cv
&& almost_devoid_co_var_of_co arg cv
almost_devoid_co_var_of_co (ForAllCo v kind_co co) cv
= almost_devoid_co_var_of_co kind_co cv
- && (v == cv || almost_devoid_co_var_of_co co cv)
+ && (v == Right cv || almost_devoid_co_var_of_co co cv)
almost_devoid_co_var_of_co (FunCo { fco_mult = w, fco_arg = co1, fco_res = co2 }) cv
= almost_devoid_co_var_of_co w cv
&& almost_devoid_co_var_of_co co1 cv
@@ -747,8 +776,8 @@ almost_devoid_co_var_of_type (FunTy _ w arg res) cv
&& almost_devoid_co_var_of_type arg cv
&& almost_devoid_co_var_of_type res cv
almost_devoid_co_var_of_type (ForAllTy (Bndr v _) ty) cv
- = almost_devoid_co_var_of_type (varType v) cv
- && (v == cv || almost_devoid_co_var_of_type ty cv)
+ = almost_devoid_co_var_of_type (varTypeTyCoVar v) cv
+ && (v == (Right cv) || almost_devoid_co_var_of_type ty cv)
almost_devoid_co_var_of_type (CastTy ty co) cv
= almost_devoid_co_var_of_type ty cv
&& almost_devoid_co_var_of_co co cv
@@ -780,13 +809,13 @@ visVarsOfType orig_ty = Pair invis_vars vis_vars
Pair invis_vars1 vis_vars = go orig_ty
invis_vars = invis_vars1 `minusVarSet` vis_vars
- go (TyVarTy tv) = Pair (tyCoVarsOfType $ tyVarKind tv) (unitVarSet tv)
+ go (TyVarTy tv) = Pair (tyCoVarsOfType $ tyVarKind tv) (unitVarSet (Left tv))
go (AppTy t1 t2) = go t1 `mappend` go t2
go (TyConApp tc tys) = go_tc tc tys
go (FunTy _ w t1 t2) = go w `mappend` go t1 `mappend` go t2
go (ForAllTy (Bndr tv _) ty)
= ((`delVarSet` tv) <$> go ty) `mappend`
- (invisible (tyCoVarsOfType $ varType tv))
+ invisible (tyCoVarsOfType $ varTypeTyCoVar tv)
go (LitTy {}) = mempty
go (CastTy ty co) = go ty `mappend` invisible (tyCoVarsOfCo co)
go (CoercionTy co) = invisible $ tyCoVarsOfCo co
@@ -819,8 +848,10 @@ isInjectiveInType tv ty
go (AppTy f a) = go f || go a
go (FunTy _ w ty1 ty2) = go w || go ty1 || go ty2
go (TyConApp tc tys) = go_tc tc tys
- go (ForAllTy (Bndr tv' _) ty) = go (tyVarKind tv')
- || (tv /= tv' && go ty)
+ go (ForAllTy (Bndr (Left tv') _) ty) = go (tyVarKind tv')
+ || (tv /= tv' && go ty)
+ go (ForAllTy (Bndr (Right cv') _) ty) = go (coVarKind cv')
+ -- || (tv /= cv' && go ty) ROMES:TODO: Can never happen, right? How can a tyVar be == to a coVar
go LitTy{} = False
go (CastTy ty _) = go ty
go CoercionTy{} = False
@@ -859,11 +890,12 @@ injectiveVarsOfType :: Bool -- ^ Should we look under injective type families?
injectiveVarsOfType look_under_tfs = go
where
go ty | Just ty' <- rewriterView ty = go ty'
- go (TyVarTy v) = unitFV v `unionFV` go (tyVarKind v)
+ go (TyVarTy v) = unitFV (TV v) `unionFV` go (tyVarKind v)
go (AppTy f a) = go f `unionFV` go a
go (FunTy _ w ty1 ty2) = go w `unionFV` go ty1 `unionFV` go ty2
go (TyConApp tc tys) = go_tc tc tys
- go (ForAllTy (Bndr tv _) ty) = go (tyVarKind tv) `unionFV` delFV tv (go ty)
+ go (ForAllTy (Bndr (Left tv) _) ty) = go (tyVarKind tv) `unionFV` delFV (TV tv) (go ty)
+ go (ForAllTy (Bndr (Right tv) _) ty) = go (coVarKind tv) `unionFV` delFV (I tv) (go ty)
go LitTy{} = emptyFV
go (CastTy ty _) = go ty
go CoercionTy{} = emptyFV
@@ -944,10 +976,11 @@ invisibleVarsOfTypes = mapUnionFV invisibleVarsOfType
{-# INLINE afvFolder #-} -- so that specialization to (const True) works
afvFolder :: (TyCoVar -> Bool) -> TyCoFolder TyCoVarSet DM.Any
afvFolder check_fv = TyCoFolder { tcf_view = noView
- , tcf_tyvar = do_tcv, tcf_covar = do_tcv
+ , tcf_tyvar = do_tv, tcf_covar = do_cv
, tcf_hole = do_hole, tcf_tycobinder = do_bndr }
where
- do_tcv is tv = Any (not (tv `elemVarSet` is) && check_fv tv)
+ do_tv is tv = Any (not (Left tv `elemVarSet` is) && check_fv (Left tv))
+ do_cv is cv = Any (not (Right cv `elemVarSet` is) && check_fv (Right cv))
do_hole _ _ = Any False -- I'm unsure; probably never happens
do_bndr is tv _ = is `extendVarSet` tv
@@ -1055,7 +1088,7 @@ scopedSort = go [] []
-> [TyCoVar] -- sorted list, in reverse order
-> [TyCoVarSet] -- list of fvs, as above
-> ([TyCoVar], [TyCoVarSet]) -- augmented lists
- insert tv [] [] = ([tv], [tyCoVarsOfType (tyVarKind tv)])
+ insert tv [] [] = ([tv], [tyCoVarsOfType (tyCoVarKind tv)])
insert tv (a:as) (fvs:fvss)
| tv `elemVarSet` fvs
, (as', fvss') <- insert tv as fvss
@@ -1064,18 +1097,18 @@ scopedSort = go [] []
| otherwise
= (tv:a:as, fvs `unionVarSet` fv_tv : fvs : fvss)
where
- fv_tv = tyCoVarsOfType (tyVarKind tv)
+ fv_tv = tyCoVarsOfType (tyCoVarKind tv)
-- lists not in correspondence
insert _ _ _ = panic "scopedSort"
-- | Get the free vars of a type in scoped order
tyCoVarsOfTypeWellScoped :: Type -> [TyVar]
-tyCoVarsOfTypeWellScoped = scopedSort . tyCoVarsOfTypeList
+tyCoVarsOfTypeWellScoped = lefts . scopedSort . tyCoVarsOfTypeList
-- | Get the free vars of types in scoped order
tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
-tyCoVarsOfTypesWellScoped = scopedSort . tyCoVarsOfTypesList
+tyCoVarsOfTypesWellScoped = lefts . scopedSort . tyCoVarsOfTypesList
{-
************************************************************************
@@ -1101,7 +1134,7 @@ tyConsOfType ty
go (FunTy af w a b) = go w `unionUniqSets`
go a `unionUniqSets` go b
`unionUniqSets` go_tc (funTyFlagTyCon af)
- go (ForAllTy (Bndr tv _) ty) = go ty `unionUniqSets` go (varType tv)
+ go (ForAllTy (Bndr tv _) ty) = go ty `unionUniqSets` go (varTypeTyCoVar tv)
go (CastTy ty co) = go ty `unionUniqSets` go_co co
go (CoercionTy co) = go_co co
@@ -1212,7 +1245,7 @@ of occurrences. See bad_var_occ in occCheckExpand. And
see #18451 for more debate.
-}
-occCheckExpand :: [Var] -> Type -> Maybe Type
+occCheckExpand :: [TyCoVar] -> Type -> Maybe Type
-- See Note [Occurs check expansion]
-- We may have needed to do some type synonym unfolding in order to
-- get rid of the variable (or forall), so we also return the unfolded
@@ -1226,14 +1259,14 @@ occCheckExpand vs_to_avoid ty
| otherwise
= go (mkVarSet vs_to_avoid, emptyVarEnv) ty
where
- go :: (VarSet, VarEnv TyCoVar) -> Type -> Maybe Type
+ go :: (TyCoVarSet, TyCoVarEnv TyCoVar) -> Type -> Maybe Type
-- The VarSet is the set of variables we are trying to avoid
-- The VarEnv carries mappings necessary
-- because of kind expansion
go (as, env) ty@(TyVarTy tv)
- | Just tv' <- lookupVarEnv env tv = return (mkTyVarTy tv')
- | bad_var_occ as tv = Nothing
- | otherwise = return ty
+ | Just (Left tv') <- lookupVarEnv env (Left tv) = return (mkTyVarTy tv')
+ | bad_var_occ as (Left tv) = Nothing
+ | otherwise = return ty
go _ ty@(LitTy {}) = return ty
go cxt (AppTy ty1 ty2) = do { ty1' <- go cxt ty1
@@ -1245,8 +1278,8 @@ occCheckExpand vs_to_avoid ty
; ty2' <- go cxt ty2
; return (ty { ft_mult = w', ft_arg = ty1', ft_res = ty2' }) }
go cxt@(as, env) (ForAllTy (Bndr tv vis) body_ty)
- = do { ki' <- go cxt (varType tv)
- ; let tv' = setVarType tv ki'
+ = do { ki' <- go cxt (varTypeTyCoVar tv)
+ ; let tv' = setTyCoVarType tv ki'
env' = extendVarEnv env tv tv'
as' = as `delVarSet` tv
; body' <- go (as', env') body_ty
@@ -1270,12 +1303,12 @@ occCheckExpand vs_to_avoid ty
; return (CoercionTy co') }
------------------
- bad_var_occ :: VarSet -> Var -> Bool
+ bad_var_occ :: TyCoVarSet -> TyCoVar -> Bool
-- Works for TyVar and CoVar
-- See Note [Occurrence checking: look inside kinds]
bad_var_occ vs_to_avoid v
= v `elemVarSet` vs_to_avoid
- || tyCoVarsOfType (varType v) `intersectsVarSet` vs_to_avoid
+ || tyCoVarsOfType (varTypeTyCoVar v) `intersectsVarSet` vs_to_avoid
------------------
go_mco _ MRefl = return MRefl
@@ -1295,7 +1328,7 @@ occCheckExpand vs_to_avoid ty
; return (AppCo co' arg') }
go_co cxt@(as, env) (ForAllCo tv kind_co body_co)
= do { kind_co' <- go_co cxt kind_co
- ; let tv' = setVarType tv $
+ ; let tv' = setTyCoVarType tv $
coercionLKind kind_co'
env' = extendVarEnv env tv tv'
as' = as `delVarSet` tv
@@ -1308,13 +1341,13 @@ occCheckExpand vs_to_avoid ty
; return (co { fco_mult = w', fco_arg = co1', fco_res = co2' })}
go_co (as,env) co@(CoVarCo c)
- | Just c' <- lookupVarEnv env c = return (CoVarCo c')
- | bad_var_occ as c = Nothing
- | otherwise = return co
+ | Just (Right c') <- lookupVarEnv env (Right c) = return (CoVarCo c')
+ | bad_var_occ as (Right c) = Nothing
+ | otherwise = return co
go_co (as,_) co@(HoleCo h)
- | bad_var_occ as (ch_co_var h) = Nothing
- | otherwise = return co
+ | bad_var_occ as (Right (ch_co_var h)) = Nothing
+ | otherwise = return co
go_co cxt (AxiomInstCo ax ind args) = do { args' <- mapM (go_co cxt) args
; return (AxiomInstCo ax ind args') }
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -1,5 +1,6 @@
{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE LambdaCase #-}
{-# OPTIONS_HADDOCK not-home #-}
@@ -122,7 +123,7 @@ type FRRType = Type
-- See Note [GHC Formalism] in GHC.Core.Lint
data Type
-- See Note [Non-trivial definitional equality]
- = TyVarTy Var -- ^ Vanilla type or kind variable (*never* a coercion variable)
+ = TyVarTy TyVar -- ^ Vanilla type or kind variable (*never* a coercion variable)
| AppTy
Type
@@ -674,18 +675,15 @@ which in turn is imported by Type
-}
mkTyVarTy :: TyVar -> Type
-mkTyVarTy v = assertPpr (isTyVar v) (ppr v <+> dcolon <+> ppr (tyVarKind v)) $
- TyVarTy v
+mkTyVarTy v = TyVarTy v
mkTyVarTys :: [TyVar] -> [Type]
mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
mkTyCoVarTy :: TyCoVar -> Type
-mkTyCoVarTy v
- | isTyVar v
- = TyVarTy v
- | otherwise
- = CoercionTy (CoVarCo v)
+mkTyCoVarTy = \case
+ Left v -> TyVarTy v
+ Right v -> CoercionTy (CoVarCo v)
mkTyCoVarTys :: [TyCoVar] -> [Type]
mkTyCoVarTys = map mkTyCoVarTy
@@ -783,7 +781,7 @@ mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
-- | Wraps foralls over the type using the provided 'InvisTVBinder's from left to right
mkInvisForAllTys :: [InvisTVBinder] -> Type -> Type
-mkInvisForAllTys tyvars = mkForAllTys (tyVarSpecToBinders tyvars)
+mkInvisForAllTys tyvars = mkForAllTys $ mapVarBndrs Left (tyVarSpecToBinders tyvars)
mkPiTy :: PiTyBinder -> Type -> Type
mkPiTy (Anon ty1 af) ty2 = mkScaledFunTy af ty1 ty2
@@ -1727,7 +1725,7 @@ foldTyCo (TyCoFolder { tcf_view = view
go_ty env (TyConApp _ tys) = go_tys env tys
go_ty env (ForAllTy (Bndr tv vis) inner)
= let !env' = tycobinder env tv vis -- Avoid building a thunk here
- in go_ty env (varType tv) `mappend` go_ty env' inner
+ in go_ty env (varTypeTyCoVar 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
@@ -1761,7 +1759,7 @@ foldTyCo (TyCoFolder { tcf_view = view
= go_co env cw `mappend` go_co env c1 `mappend` go_co env c2
go_co env (ForAllCo tv kind_co co)
- = go_co env kind_co `mappend` go_ty env (varType tv)
+ = go_co env kind_co `mappend` go_ty env (varTypeTyCoVar tv)
`mappend` go_co env' co
where
env' = tycobinder env tv Inferred
@@ -1801,7 +1799,7 @@ typeSize (LitTy {}) = 1
typeSize (TyVarTy {}) = 1
typeSize (AppTy t1 t2) = typeSize t1 + typeSize t2
typeSize (FunTy _ _ t1 t2) = typeSize t1 + typeSize t2
-typeSize (ForAllTy (Bndr tv _) t) = typeSize (varType tv) + typeSize t
+typeSize (ForAllTy (Bndr tv _) t) = typeSize (varTypeTyCoVar tv) + typeSize t
typeSize (TyConApp _ ts) = 1 + typesSize ts
typeSize (CastTy ty co) = typeSize ty + coercionSize co
typeSize (CoercionTy co) = coercionSize co
=====================================
compiler/GHC/Core/TyCo/Rep.hs-boot
=====================================
@@ -3,7 +3,7 @@ module GHC.Core.TyCo.Rep where
import GHC.Utils.Outputable ( Outputable )
import Data.Data ( Data )
-import {-# SOURCE #-} GHC.Types.Var( Var, VarBndr, ForAllTyFlag, FunTyFlag )
+import {-# SOURCE #-} GHC.Types.Var( TyCoVar, VarBndr, ForAllTyFlag, FunTyFlag )
import {-# SOURCE #-} GHC.Core.TyCon ( TyCon )
data Type
@@ -26,7 +26,7 @@ type ThetaType = [PredType]
type CoercionN = Coercion
type MCoercionN = MCoercion
-mkForAllTy :: VarBndr Var ForAllTyFlag -> Type -> Type
+mkForAllTy :: VarBndr TyCoVar ForAllTyFlag -> Type -> Type
mkNakedTyConTy :: TyCon -> Type
mkNakedFunTy :: FunTyFlag -> Type -> Type -> Type
=====================================
compiler/GHC/Types/Unique.hs
=====================================
@@ -192,6 +192,9 @@ instance Uniquable Int where
instance Uniquable ModuleName where
getUnique (ModuleName nm) = getUnique nm
+instance (Uniquable a, Uniquable b) => Uniquable (Either a b) where
+ getUnique (Left x) = getUnique x
+ getUnique (Right x) = getUnique x
{-
************************************************************************
@@ -323,3 +326,4 @@ iToBase62 n_
{-# INLINE chooseChar62 #-}
chooseChar62 (I# n) = C# (indexCharOffAddr# chars62 n)
chars62 = "0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"#
+
=====================================
compiler/GHC/Types/Var.hs
=====================================
@@ -48,9 +48,13 @@ module GHC.Types.Var (
varMult, varMultMaybe,
varNameTyVar, varNameTcTyVar, varNameId,
varTypeTyVar, varTypeTcTyVar, varTypeId,
+
+ varTypeTyCoVar, tyCoVarToVar,
+ coVarKind, tyCoVarKind,
+
-- ** Modifying 'Var's
- setVarName, setVarUnique, setVarType,
+ setVarName, setVarUnique, setVarType, setTyCoVarType,
updateVarType, updateVarTypeM,
-- ** Constructing, taking apart, modifying 'Id's
@@ -273,6 +277,16 @@ data Id
id_details :: IdDetails, -- Stable, doesn't change
id_info :: IdInfo } -- Unstable, updated by simplifier
+varTypeTyCoVar :: TyCoVar -> Type
+varTypeTyCoVar = \case
+ Left v -> varTypeTyVar v
+ Right v -> varTypeId v
+
+tyCoVarToVar :: TyCoVar -> Var
+tyCoVarToVar = \case
+ Left x -> TV x
+ Right x -> I x
+
varName :: Var -> Name
varName = \case
TV TyVar{varNameTyVar} -> varNameTyVar
@@ -510,6 +524,11 @@ setVarType var ty = case var of
TV tv -> TV tv { varTypeTyVar = ty }
TTV ttv -> TTV ttv { varTypeTcTyVar = ty }
+setTyCoVarType :: TyCoVar -> Type -> TyCoVar
+setTyCoVarType var ty = case var of
+ Left tv -> Left tv { varTypeTyVar = ty }
+ Right id -> Right id { varTypeId = ty }
+
-- | Update a 'Var's type. Does not update the /multiplicity/
-- stored in an 'Id', if any. Because of the possibility for
-- abuse, ASSERTs that there is no multiplicity to update.
@@ -1151,6 +1170,14 @@ tyVarName = varNameTyVar
tyVarKind :: TyVar -> Kind
tyVarKind = varTypeTyVar
+coVarKind :: CoVar -> Type
+coVarKind cv = varTypeId cv
+
+tyCoVarKind :: TyCoVar -> Kind
+tyCoVarKind = \case
+ Left tv -> tyVarKind tv
+ Right cv -> coVarKind cv
+
setTyVarUnique :: TyVar -> Unique -> TyVar
setTyVarUnique tv uq = case setVarUnique (TV tv) uq of
TV tv -> tv
=====================================
compiler/GHC/Types/Var/Env.hs
=====================================
@@ -500,13 +500,14 @@ type TyCoVarEnv elt = UniqFM TyCoVar elt
-- | Coercion Variable Environment
type CoVarEnv elt = UniqFM CoVar elt
-emptyVarEnv :: VarEnv a
+emptyVarEnv :: UniqFM var a
mkVarEnv :: [(Var, a)] -> VarEnv a
mkVarEnv_Directly :: [(Unique, a)] -> VarEnv a
zipVarEnv :: [Var] -> [a] -> VarEnv a
unitVarEnv :: Var -> a -> VarEnv a
alterVarEnv :: (Maybe a -> Maybe a) -> VarEnv a -> Var -> VarEnv a
-extendVarEnv :: VarEnv a -> Var -> a -> VarEnv a
+extendVarEnv :: UniqFM var a -> var -> a -> UniqFM var a
+{-# SPECIALISE extendVarEnv :: VarEnv a -> Var -> a -> VarEnv a #-}
extendVarEnv_C :: (a->a->a) -> VarEnv a -> Var -> a -> VarEnv a
extendVarEnv_Acc :: (a->b->b) -> (a->b) -> VarEnv b -> Var -> a -> VarEnv b
plusVarEnv :: VarEnv a -> VarEnv a -> VarEnv a
@@ -527,7 +528,8 @@ mapVarEnv :: (a -> b) -> VarEnv a -> VarEnv b
modifyVarEnv :: (a -> a) -> VarEnv a -> Var -> VarEnv a
isEmptyVarEnv :: VarEnv a -> Bool
-lookupVarEnv :: VarEnv a -> Var -> Maybe a
+lookupVarEnv :: UniqFM var a -> var -> Maybe a
+{-# SPECIALISE lookupVarEnv :: VarEnv a -> Var -> Maybe a #-}
lookupVarEnv_Directly :: VarEnv a -> Unique -> Maybe a
filterVarEnv :: (a -> Bool) -> VarEnv a -> VarEnv a
anyVarEnv :: (elt -> Bool) -> UniqFM key elt -> Bool
=====================================
compiler/GHC/Types/Var/Set.hs
=====================================
@@ -3,7 +3,7 @@
(c) The GRASP/AQUA Project, Glasgow University, 1992-1998
-}
-
+{-# LANGUAGE LambdaCase #-}
module GHC.Types.Var.Set (
-- * Var, Id and TyVar set types
@@ -44,9 +44,12 @@ module GHC.Types.Var.Set (
sizeDVarSet, seqDVarSet,
partitionDVarSet,
dVarSetToVarSet,
+ leftsVarSet, rightsVarSet
) where
+import Data.Either
import GHC.Prelude
+import GHC.Utils.Panic
import GHC.Types.Var ( Var, TyVar, CoVar, TyCoVar, Id )
import GHC.Types.Unique
@@ -78,30 +81,39 @@ type CoVarSet = UniqSet CoVar
-- | Type or Coercion Variable Set
type TyCoVarSet = UniqSet TyCoVar
-emptyVarSet :: VarSet
-intersectVarSet :: VarSet -> VarSet -> VarSet
-unionVarSet :: VarSet -> VarSet -> VarSet
+emptyVarSet :: UniqSet a
+intersectVarSet :: UniqSet a -> UniqSet a -> UniqSet a
+{-# SPECIALISE intersectVarSet :: VarSet -> VarSet -> VarSet #-}
+unionVarSet :: UniqSet a -> UniqSet a -> UniqSet a
+{-# SPECIALISE unionVarSet :: VarSet -> VarSet -> VarSet #-}
unionVarSets :: [VarSet] -> VarSet
mapUnionVarSet :: (a -> VarSet) -> [a] -> VarSet
-- ^ map the function over the list, and union the results
-unitVarSet :: Var -> VarSet
-extendVarSet :: VarSet -> Var -> VarSet
+unitVarSet :: Uniquable a => a -> UniqSet a
+{-# SPECIALIZE unitVarSet :: Var -> VarSet #-}
+extendVarSet :: Uniquable a => UniqSet a -> a -> UniqSet a
+{-# SPECIALISE extendVarSet :: VarSet -> Var -> VarSet #-}
extendVarSetList:: VarSet -> [Var] -> VarSet
-elemVarSet :: Var -> VarSet -> Bool
-delVarSet :: VarSet -> Var -> VarSet
+elemVarSet :: Uniquable a => a -> UniqSet a -> Bool
+{-# SPECIALISE elemVarSet :: Var -> VarSet -> Bool #-}
+delVarSet :: Uniquable a => UniqSet a -> a -> UniqSet a
+{-# SPECIALISE delVarSet :: VarSet -> Var -> VarSet #-}
delVarSetList :: VarSet -> [Var] -> VarSet
-minusVarSet :: VarSet -> VarSet -> VarSet
+minusVarSet :: Uniquable a => UniqSet a -> UniqSet a -> UniqSet a
+{-# SPECIALISE minusVarSet :: VarSet -> VarSet -> VarSet #-}
isEmptyVarSet :: VarSet -> Bool
-mkVarSet :: [Var] -> VarSet
+mkVarSet :: Uniquable a => [a] -> UniqSet a
+{-# SPECIALISE mkVarSet :: [Var] -> VarSet #-}
lookupVarSet_Directly :: VarSet -> Unique -> Maybe Var
lookupVarSet :: VarSet -> Var -> Maybe Var
-- Returns the set element, which may be
-- (==) to the argument, but not the same as
lookupVarSetByName :: VarSet -> Name -> Maybe Var
sizeVarSet :: VarSet -> Int
-filterVarSet :: (Var -> Bool) -> VarSet -> VarSet
+filterVarSet :: Uniquable a => (a -> Bool) -> UniqSet a -> UniqSet a
+{-# SPECIALISE filterVarSet :: (Var -> Bool) -> VarSet -> VarSet #-}
delVarSetByKey :: VarSet -> Unique -> VarSet
elemVarSetByKey :: Unique -> VarSet -> Bool
@@ -113,7 +125,8 @@ extendVarSet = addOneToUniqSet
extendVarSetList= addListToUniqSet
intersectVarSet = intersectUniqSets
-intersectsVarSet:: VarSet -> VarSet -> Bool -- True if non-empty intersection
+intersectsVarSet:: UniqSet a -> UniqSet a -> Bool -- True if non-empty intersection
+{-# SPECIALISE intersectsVarSet :: VarSet -> VarSet -> Bool #-}
disjointVarSet :: VarSet -> VarSet -> Bool -- True if empty intersection
subVarSet :: VarSet -> VarSet -> Bool -- True if first arg is subset of second
-- (s1 `intersectsVarSet` s2) doesn't compute s2 if s1 is empty;
@@ -155,7 +168,8 @@ mapVarSet = mapUniqSet
-- See Note [Deterministic UniqFM] to learn about nondeterminism.
-- If you use this please provide a justification why it doesn't introduce
-- nondeterminism.
-nonDetStrictFoldVarSet :: (Var -> a -> a) -> a -> VarSet -> a
+nonDetStrictFoldVarSet :: (b -> a -> a) -> a -> UniqSet b -> a
+{-# SPECIALISE nonDetStrictFoldVarSet :: (Var -> a -> a) -> a -> VarSet -> a #-}
nonDetStrictFoldVarSet = nonDetStrictFoldUniqSet
fixVarSet :: (VarSet -> VarSet) -- Map the current set to a new set
@@ -251,7 +265,7 @@ extendDVarSet = addOneToUniqDSet
elemDVarSet :: Var -> DVarSet -> Bool
elemDVarSet = elementOfUniqDSet
-dVarSetElems :: DVarSet -> [Var]
+dVarSetElems :: UniqDSet a -> [a]
dVarSetElems = uniqDSetToList
subDVarSet :: DVarSet -> DVarSet -> Bool
@@ -358,3 +372,10 @@ transCloDVarSet fn seeds
| otherwise = go (acc `unionDVarSet` new_vs) new_vs
where
new_vs = fn candidates `minusDVarSet` acc
+
+leftsVarSet :: (Uniquable a, Uniquable b) => UniqSet (Either a b) -> UniqSet a
+leftsVarSet = mapVarSet (\case Left x -> x; Right _ -> panic "leftsVarSet") . filterVarSet isLeft
+
+rightsVarSet :: (Uniquable a, Uniquable b) => UniqSet (Either a b) -> UniqSet b
+rightsVarSet = mapVarSet (\case Right x -> x; Left _ -> panic "rightsVarSet") . filterVarSet isRight
+
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c7b752c31a0557c8bb097b721d367a325a63f4d3
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c7b752c31a0557c8bb097b721d367a325a63f4d3
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/20230527/de3a9d8d/attachment-0001.html>
More information about the ghc-commits
mailing list