module GHC.Core.TyCo.FVs
( shallowTyCoVarsOfType, shallowTyCoVarsOfTypes,
tyCoVarsOfType, tyCoVarsOfTypes,
tyCoVarsOfTypeDSet, tyCoVarsOfTypesDSet,
tyCoFVsBndr, tyCoFVsVarBndr, tyCoFVsVarBndrs,
tyCoFVsOfType, tyCoVarsOfTypeList,
tyCoFVsOfTypes, tyCoVarsOfTypesList,
deepTcvFolder,
shallowTyCoVarsOfTyVarEnv, shallowTyCoVarsOfCoVarEnv,
shallowTyCoVarsOfCo, shallowTyCoVarsOfCos,
tyCoVarsOfCo, tyCoVarsOfCos, tyCoVarsOfMCo,
coVarsOfType, coVarsOfTypes,
coVarsOfCo, coVarsOfCos,
tyCoVarsOfCoDSet,
tyCoFVsOfCo, tyCoFVsOfCos,
tyCoVarsOfCoList,
almostDevoidCoVarOfCo,
injectiveVarsOfType, injectiveVarsOfTypes,
invisibleVarsOfType, invisibleVarsOfTypes,
anyFreeVarsOfType, anyFreeVarsOfTypes, anyFreeVarsOfCo,
noFreeVarsOfType, noFreeVarsOfTypes, noFreeVarsOfCo,
scopedSort, tyCoVarsOfTypeWellScoped,
tyCoVarsOfTypesWellScoped,
closeOverKindsDSet, closeOverKindsList,
closeOverKinds,
Endo(..), runTyCoVars
) where
import GHC.Prelude
import {-# SOURCE #-} GHC.Core.Type (coreView, partitionInvisibleTypes)
import Data.Monoid as DM ( Endo(..), Any(..) )
import GHC.Core.TyCo.Rep
import GHC.Core.TyCon
import GHC.Types.Var
import GHC.Utils.FV
import GHC.Types.Unique.FM
import GHC.Types.Var.Set
import GHC.Types.Var.Env
import GHC.Utils.Misc
import GHC.Utils.Panic
runTyCoVars :: Endo TyCoVarSet -> TyCoVarSet
{-# INLINE runTyCoVars #-}
runTyCoVars :: Endo VarSet -> VarSet
runTyCoVars Endo VarSet
f = Endo VarSet -> VarSet -> VarSet
forall a. Endo a -> a -> a
appEndo Endo VarSet
f VarSet
emptyVarSet
tyCoVarsOfType :: Type -> TyCoVarSet
tyCoVarsOfType :: Type -> VarSet
tyCoVarsOfType Type
ty = Endo VarSet -> VarSet
runTyCoVars (Type -> Endo VarSet
deep_ty Type
ty)
tyCoVarsOfTypes :: [Type] -> TyCoVarSet
tyCoVarsOfTypes :: [Type] -> VarSet
tyCoVarsOfTypes [Type]
tys = Endo VarSet -> VarSet
runTyCoVars ([Type] -> Endo VarSet
deep_tys [Type]
tys)
tyCoVarsOfCo :: Coercion -> TyCoVarSet
tyCoVarsOfCo :: Coercion -> VarSet
tyCoVarsOfCo Coercion
co = Endo VarSet -> VarSet
runTyCoVars (Coercion -> Endo VarSet
deep_co Coercion
co)
tyCoVarsOfMCo :: MCoercion -> TyCoVarSet
tyCoVarsOfMCo :: MCoercion -> VarSet
tyCoVarsOfMCo MCoercion
MRefl = VarSet
emptyVarSet
tyCoVarsOfMCo (MCo Coercion
co) = Coercion -> VarSet
tyCoVarsOfCo Coercion
co
tyCoVarsOfCos :: [Coercion] -> TyCoVarSet
tyCoVarsOfCos :: [Coercion] -> VarSet
tyCoVarsOfCos [Coercion]
cos = Endo VarSet -> VarSet
runTyCoVars ([Coercion] -> Endo VarSet
deep_cos [Coercion]
cos)
deep_ty :: Type -> Endo TyCoVarSet
deep_tys :: [Type] -> Endo TyCoVarSet
deep_co :: Coercion -> Endo TyCoVarSet
deep_cos :: [Coercion] -> Endo TyCoVarSet
(Type -> Endo VarSet
deep_ty, [Type] -> Endo VarSet
deep_tys, Coercion -> Endo VarSet
deep_co, [Coercion] -> Endo VarSet
deep_cos) = TyCoFolder VarSet (Endo VarSet)
-> VarSet
-> (Type -> Endo VarSet, [Type] -> Endo VarSet,
Coercion -> Endo VarSet, [Coercion] -> Endo VarSet)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo TyCoFolder VarSet (Endo VarSet)
deepTcvFolder VarSet
emptyVarSet
deepTcvFolder :: TyCoFolder TyCoVarSet (Endo TyCoVarSet)
deepTcvFolder :: TyCoFolder VarSet (Endo VarSet)
deepTcvFolder = TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view = Type -> Maybe Type
noView
, tcf_tyvar :: VarSet -> TyCoVar -> Endo VarSet
tcf_tyvar = VarSet -> TyCoVar -> Endo VarSet
do_tcv, tcf_covar :: VarSet -> TyCoVar -> Endo VarSet
tcf_covar = VarSet -> TyCoVar -> Endo VarSet
do_tcv
, tcf_hole :: VarSet -> CoercionHole -> Endo VarSet
tcf_hole = VarSet -> CoercionHole -> Endo VarSet
do_hole, tcf_tycobinder :: VarSet -> TyCoVar -> ArgFlag -> VarSet
tcf_tycobinder = VarSet -> TyCoVar -> ArgFlag -> VarSet
forall {p}. VarSet -> TyCoVar -> p -> VarSet
do_bndr }
where
do_tcv :: VarSet -> TyCoVar -> Endo VarSet
do_tcv VarSet
is TyCoVar
v = (VarSet -> VarSet) -> Endo VarSet
forall a. (a -> a) -> Endo a
Endo VarSet -> VarSet
do_it
where
do_it :: VarSet -> VarSet
do_it VarSet
acc | TyCoVar
v TyCoVar -> VarSet -> Bool
`elemVarSet` VarSet
is = VarSet
acc
| TyCoVar
v TyCoVar -> VarSet -> Bool
`elemVarSet` VarSet
acc = VarSet
acc
| Bool
otherwise = Endo VarSet -> VarSet -> VarSet
forall a. Endo a -> a -> a
appEndo (Type -> Endo VarSet
deep_ty (TyCoVar -> Type
varType TyCoVar
v)) (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$
VarSet
acc VarSet -> TyCoVar -> VarSet
`extendVarSet` TyCoVar
v
do_bndr :: VarSet -> TyCoVar -> p -> VarSet
do_bndr VarSet
is TyCoVar
tcv p
_ = VarSet -> TyCoVar -> VarSet
extendVarSet VarSet
is TyCoVar
tcv
do_hole :: VarSet -> CoercionHole -> Endo VarSet
do_hole VarSet
is CoercionHole
hole = VarSet -> TyCoVar -> Endo VarSet
do_tcv VarSet
is (CoercionHole -> TyCoVar
coHoleCoVar CoercionHole
hole)
shallowTyCoVarsOfType :: Type -> TyCoVarSet
shallowTyCoVarsOfType :: Type -> VarSet
shallowTyCoVarsOfType Type
ty = Endo VarSet -> VarSet
runTyCoVars (Type -> Endo VarSet
shallow_ty Type
ty)
shallowTyCoVarsOfTypes :: [Type] -> TyCoVarSet
shallowTyCoVarsOfTypes :: [Type] -> VarSet
shallowTyCoVarsOfTypes [Type]
tys = Endo VarSet -> VarSet
runTyCoVars ([Type] -> Endo VarSet
shallow_tys [Type]
tys)
shallowTyCoVarsOfCo :: Coercion -> TyCoVarSet
shallowTyCoVarsOfCo :: Coercion -> VarSet
shallowTyCoVarsOfCo Coercion
co = Endo VarSet -> VarSet
runTyCoVars (Coercion -> Endo VarSet
shallow_co Coercion
co)
shallowTyCoVarsOfCos :: [Coercion] -> TyCoVarSet
shallowTyCoVarsOfCos :: [Coercion] -> VarSet
shallowTyCoVarsOfCos [Coercion]
cos = Endo VarSet -> VarSet
runTyCoVars ([Coercion] -> Endo VarSet
shallow_cos [Coercion]
cos)
shallowTyCoVarsOfTyVarEnv :: TyVarEnv Type -> TyCoVarSet
shallowTyCoVarsOfTyVarEnv :: TyVarEnv Type -> VarSet
shallowTyCoVarsOfTyVarEnv TyVarEnv Type
tys = [Type] -> VarSet
shallowTyCoVarsOfTypes (TyVarEnv Type -> [Type]
forall key elt. UniqFM key elt -> [elt]
nonDetEltsUFM TyVarEnv Type
tys)
shallowTyCoVarsOfCoVarEnv :: CoVarEnv Coercion -> TyCoVarSet
shallowTyCoVarsOfCoVarEnv :: CoVarEnv Coercion -> VarSet
shallowTyCoVarsOfCoVarEnv CoVarEnv Coercion
cos = [Coercion] -> VarSet
shallowTyCoVarsOfCos (CoVarEnv Coercion -> [Coercion]
forall key elt. UniqFM key elt -> [elt]
nonDetEltsUFM CoVarEnv Coercion
cos)
shallow_ty :: Type -> Endo TyCoVarSet
shallow_tys :: [Type] -> Endo TyCoVarSet
shallow_co :: Coercion -> Endo TyCoVarSet
shallow_cos :: [Coercion] -> Endo TyCoVarSet
(Type -> Endo VarSet
shallow_ty, [Type] -> Endo VarSet
shallow_tys, Coercion -> Endo VarSet
shallow_co, [Coercion] -> Endo VarSet
shallow_cos) = TyCoFolder VarSet (Endo VarSet)
-> VarSet
-> (Type -> Endo VarSet, [Type] -> Endo VarSet,
Coercion -> Endo VarSet, [Coercion] -> Endo VarSet)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo TyCoFolder VarSet (Endo VarSet)
shallowTcvFolder VarSet
emptyVarSet
shallowTcvFolder :: TyCoFolder TyCoVarSet (Endo TyCoVarSet)
shallowTcvFolder :: TyCoFolder VarSet (Endo VarSet)
shallowTcvFolder = TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view = Type -> Maybe Type
noView
, tcf_tyvar :: VarSet -> TyCoVar -> Endo VarSet
tcf_tyvar = VarSet -> TyCoVar -> Endo VarSet
do_tcv, tcf_covar :: VarSet -> TyCoVar -> Endo VarSet
tcf_covar = VarSet -> TyCoVar -> Endo VarSet
do_tcv
, tcf_hole :: VarSet -> CoercionHole -> Endo VarSet
tcf_hole = VarSet -> CoercionHole -> Endo VarSet
forall {a} {p} {p}. Monoid a => p -> p -> a
do_hole, tcf_tycobinder :: VarSet -> TyCoVar -> ArgFlag -> VarSet
tcf_tycobinder = VarSet -> TyCoVar -> ArgFlag -> VarSet
forall {p}. VarSet -> TyCoVar -> p -> VarSet
do_bndr }
where
do_tcv :: VarSet -> TyCoVar -> Endo VarSet
do_tcv VarSet
is TyCoVar
v = (VarSet -> VarSet) -> Endo VarSet
forall a. (a -> a) -> Endo a
Endo VarSet -> VarSet
do_it
where
do_it :: VarSet -> VarSet
do_it VarSet
acc | TyCoVar
v TyCoVar -> VarSet -> Bool
`elemVarSet` VarSet
is = VarSet
acc
| TyCoVar
v TyCoVar -> VarSet -> Bool
`elemVarSet` VarSet
acc = VarSet
acc
| Bool
otherwise = VarSet
acc VarSet -> TyCoVar -> VarSet
`extendVarSet` TyCoVar
v
do_bndr :: VarSet -> TyCoVar -> p -> VarSet
do_bndr VarSet
is TyCoVar
tcv p
_ = VarSet -> TyCoVar -> VarSet
extendVarSet VarSet
is TyCoVar
tcv
do_hole :: p -> p -> a
do_hole p
_ p
_ = a
forall a. Monoid a => a
mempty
coVarsOfType :: Type -> CoVarSet
coVarsOfTypes :: [Type] -> CoVarSet
coVarsOfCo :: Coercion -> CoVarSet
coVarsOfCos :: [Coercion] -> CoVarSet
coVarsOfType :: Type -> VarSet
coVarsOfType Type
ty = Endo VarSet -> VarSet
runTyCoVars (Type -> Endo VarSet
deep_cv_ty Type
ty)
coVarsOfTypes :: [Type] -> VarSet
coVarsOfTypes [Type]
tys = Endo VarSet -> VarSet
runTyCoVars ([Type] -> Endo VarSet
deep_cv_tys [Type]
tys)
coVarsOfCo :: Coercion -> VarSet
coVarsOfCo Coercion
co = Endo VarSet -> VarSet
runTyCoVars (Coercion -> Endo VarSet
deep_cv_co Coercion
co)
coVarsOfCos :: [Coercion] -> VarSet
coVarsOfCos [Coercion]
cos = Endo VarSet -> VarSet
runTyCoVars ([Coercion] -> Endo VarSet
deep_cv_cos [Coercion]
cos)
deep_cv_ty :: Type -> Endo CoVarSet
deep_cv_tys :: [Type] -> Endo CoVarSet
deep_cv_co :: Coercion -> Endo CoVarSet
deep_cv_cos :: [Coercion] -> Endo CoVarSet
(Type -> Endo VarSet
deep_cv_ty, [Type] -> Endo VarSet
deep_cv_tys, Coercion -> Endo VarSet
deep_cv_co, [Coercion] -> Endo VarSet
deep_cv_cos) = TyCoFolder VarSet (Endo VarSet)
-> VarSet
-> (Type -> Endo VarSet, [Type] -> Endo VarSet,
Coercion -> Endo VarSet, [Coercion] -> Endo VarSet)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo TyCoFolder VarSet (Endo VarSet)
deepCoVarFolder VarSet
emptyVarSet
deepCoVarFolder :: TyCoFolder TyCoVarSet (Endo CoVarSet)
deepCoVarFolder :: TyCoFolder VarSet (Endo VarSet)
deepCoVarFolder = TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view = Type -> Maybe Type
noView
, tcf_tyvar :: VarSet -> TyCoVar -> Endo VarSet
tcf_tyvar = VarSet -> TyCoVar -> Endo VarSet
forall {a} {p} {p}. Monoid a => p -> p -> a
do_tyvar, tcf_covar :: VarSet -> TyCoVar -> Endo VarSet
tcf_covar = VarSet -> TyCoVar -> Endo VarSet
do_covar
, tcf_hole :: VarSet -> CoercionHole -> Endo VarSet
tcf_hole = VarSet -> CoercionHole -> Endo VarSet
do_hole, tcf_tycobinder :: VarSet -> TyCoVar -> ArgFlag -> VarSet
tcf_tycobinder = VarSet -> TyCoVar -> ArgFlag -> VarSet
forall {p}. VarSet -> TyCoVar -> p -> VarSet
do_bndr }
where
do_tyvar :: p -> p -> a
do_tyvar p
_ p
_ = a
forall a. Monoid a => a
mempty
do_covar :: VarSet -> TyCoVar -> Endo VarSet
do_covar VarSet
is TyCoVar
v = (VarSet -> VarSet) -> Endo VarSet
forall a. (a -> a) -> Endo a
Endo VarSet -> VarSet
do_it
where
do_it :: VarSet -> VarSet
do_it VarSet
acc | TyCoVar
v TyCoVar -> VarSet -> Bool
`elemVarSet` VarSet
is = VarSet
acc
| TyCoVar
v TyCoVar -> VarSet -> Bool
`elemVarSet` VarSet
acc = VarSet
acc
| Bool
otherwise = Endo VarSet -> VarSet -> VarSet
forall a. Endo a -> a -> a
appEndo (Type -> Endo VarSet
deep_cv_ty (TyCoVar -> Type
varType TyCoVar
v)) (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$
VarSet
acc VarSet -> TyCoVar -> VarSet
`extendVarSet` TyCoVar
v
do_bndr :: VarSet -> TyCoVar -> p -> VarSet
do_bndr VarSet
is TyCoVar
tcv p
_ = VarSet -> TyCoVar -> VarSet
extendVarSet VarSet
is TyCoVar
tcv
do_hole :: VarSet -> CoercionHole -> Endo VarSet
do_hole VarSet
is CoercionHole
hole = VarSet -> TyCoVar -> Endo VarSet
do_covar VarSet
is (CoercionHole -> TyCoVar
coHoleCoVar CoercionHole
hole)
closeOverKinds :: TyCoVarSet -> TyCoVarSet
closeOverKinds :: VarSet -> VarSet
closeOverKinds VarSet
vs = (TyCoVar -> VarSet -> VarSet) -> VarSet -> VarSet -> VarSet
forall a. (TyCoVar -> a -> a) -> a -> VarSet -> a
nonDetStrictFoldVarSet TyCoVar -> VarSet -> VarSet
do_one VarSet
vs VarSet
vs
where
do_one :: TyCoVar -> VarSet -> VarSet
do_one TyCoVar
v VarSet
acc = Endo VarSet -> VarSet -> VarSet
forall a. Endo a -> a -> a
appEndo (Type -> Endo VarSet
deep_ty (TyCoVar -> Type
varType TyCoVar
v)) VarSet
acc
closeOverKindsFV :: [TyVar] -> FV
closeOverKindsFV :: [TyCoVar] -> FV
closeOverKindsFV [TyCoVar]
tvs =
(TyCoVar -> FV) -> [TyCoVar] -> FV
forall a. (a -> FV) -> [a] -> FV
mapUnionFV (Type -> FV
tyCoFVsOfType (Type -> FV) -> (TyCoVar -> Type) -> TyCoVar -> FV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCoVar -> Type
tyVarKind) [TyCoVar]
tvs FV -> FV -> FV
`unionFV` [TyCoVar] -> FV
mkFVs [TyCoVar]
tvs
closeOverKindsList :: [TyVar] -> [TyVar]
closeOverKindsList :: [TyCoVar] -> [TyCoVar]
closeOverKindsList [TyCoVar]
tvs = FV -> [TyCoVar]
fvVarList (FV -> [TyCoVar]) -> FV -> [TyCoVar]
forall a b. (a -> b) -> a -> b
$ [TyCoVar] -> FV
closeOverKindsFV [TyCoVar]
tvs
closeOverKindsDSet :: DTyVarSet -> DTyVarSet
closeOverKindsDSet :: DTyVarSet -> DTyVarSet
closeOverKindsDSet = FV -> DTyVarSet
fvDVarSet (FV -> DTyVarSet) -> (DTyVarSet -> FV) -> DTyVarSet -> DTyVarSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TyCoVar] -> FV
closeOverKindsFV ([TyCoVar] -> FV) -> (DTyVarSet -> [TyCoVar]) -> DTyVarSet -> FV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DTyVarSet -> [TyCoVar]
dVarSetElems
tyCoVarsOfTypeDSet :: Type -> DTyCoVarSet
tyCoVarsOfTypeDSet :: Type -> DTyVarSet
tyCoVarsOfTypeDSet Type
ty = FV -> DTyVarSet
fvDVarSet (FV -> DTyVarSet) -> FV -> DTyVarSet
forall a b. (a -> b) -> a -> b
$ Type -> FV
tyCoFVsOfType Type
ty
tyCoVarsOfTypeList :: Type -> [TyCoVar]
tyCoVarsOfTypeList :: Type -> [TyCoVar]
tyCoVarsOfTypeList Type
ty = FV -> [TyCoVar]
fvVarList (FV -> [TyCoVar]) -> FV -> [TyCoVar]
forall a b. (a -> b) -> a -> b
$ Type -> FV
tyCoFVsOfType Type
ty
tyCoVarsOfTypesDSet :: [Type] -> DTyCoVarSet
tyCoVarsOfTypesDSet :: [Type] -> DTyVarSet
tyCoVarsOfTypesDSet [Type]
tys = FV -> DTyVarSet
fvDVarSet (FV -> DTyVarSet) -> FV -> DTyVarSet
forall a b. (a -> b) -> a -> b
$ [Type] -> FV
tyCoFVsOfTypes [Type]
tys
tyCoVarsOfTypesList :: [Type] -> [TyCoVar]
tyCoVarsOfTypesList :: [Type] -> [TyCoVar]
tyCoVarsOfTypesList [Type]
tys = FV -> [TyCoVar]
fvVarList (FV -> [TyCoVar]) -> FV -> [TyCoVar]
forall a b. (a -> b) -> a -> b
$ [Type] -> FV
tyCoFVsOfTypes [Type]
tys
tyCoFVsOfType :: Type -> FV
tyCoFVsOfType :: Type -> FV
tyCoFVsOfType (TyVarTy TyCoVar
v) InterestingVarFun
f VarSet
bound_vars ([TyCoVar]
acc_list, VarSet
acc_set)
| Bool -> Bool
not (InterestingVarFun
f TyCoVar
v) = ([TyCoVar]
acc_list, VarSet
acc_set)
| TyCoVar
v TyCoVar -> VarSet -> Bool
`elemVarSet` VarSet
bound_vars = ([TyCoVar]
acc_list, VarSet
acc_set)
| TyCoVar
v TyCoVar -> VarSet -> Bool
`elemVarSet` VarSet
acc_set = ([TyCoVar]
acc_list, VarSet
acc_set)
| Bool
otherwise = Type -> FV
tyCoFVsOfType (TyCoVar -> Type
tyVarKind TyCoVar
v) InterestingVarFun
f
VarSet
emptyVarSet
(TyCoVar
vTyCoVar -> [TyCoVar] -> [TyCoVar]
forall a. a -> [a] -> [a]
:[TyCoVar]
acc_list, VarSet -> TyCoVar -> VarSet
extendVarSet VarSet
acc_set TyCoVar
v)
tyCoFVsOfType (TyConApp TyCon
_ [Type]
tys) InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc = [Type] -> FV
tyCoFVsOfTypes [Type]
tys InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc
tyCoFVsOfType (LitTy {}) InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc = FV
emptyFV InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc
tyCoFVsOfType (AppTy Type
fun Type
arg) InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc = (Type -> FV
tyCoFVsOfType Type
fun FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType Type
arg) InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc
tyCoFVsOfType (FunTy AnonArgFlag
_ Type
w Type
arg Type
res) InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc = (Type -> FV
tyCoFVsOfType Type
w FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType Type
arg FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType Type
res) InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc
tyCoFVsOfType (ForAllTy TyCoVarBinder
bndr Type
ty) InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc = TyCoVarBinder -> FV -> FV
tyCoFVsBndr TyCoVarBinder
bndr (Type -> FV
tyCoFVsOfType Type
ty) InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc
tyCoFVsOfType (CastTy Type
ty Coercion
co) InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc = (Type -> FV
tyCoFVsOfType Type
ty FV -> FV -> FV
`unionFV` Coercion -> FV
tyCoFVsOfCo Coercion
co) InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc
tyCoFVsOfType (CoercionTy Coercion
co) InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co InterestingVarFun
f VarSet
bound_vars ([TyCoVar], VarSet)
acc
tyCoFVsBndr :: TyCoVarBinder -> FV -> FV
tyCoFVsBndr :: TyCoVarBinder -> FV -> FV
tyCoFVsBndr (Bndr TyCoVar
tv ArgFlag
_) FV
fvs = TyCoVar -> FV -> FV
tyCoFVsVarBndr TyCoVar
tv FV
fvs
tyCoFVsVarBndrs :: [Var] -> FV -> FV
tyCoFVsVarBndrs :: [TyCoVar] -> FV -> FV
tyCoFVsVarBndrs [TyCoVar]
vars FV
fvs = (TyCoVar -> FV -> FV) -> FV -> [TyCoVar] -> FV
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TyCoVar -> FV -> FV
tyCoFVsVarBndr FV
fvs [TyCoVar]
vars
tyCoFVsVarBndr :: Var -> FV -> FV
tyCoFVsVarBndr :: TyCoVar -> FV -> FV
tyCoFVsVarBndr TyCoVar
var FV
fvs
= Type -> FV
tyCoFVsOfType (TyCoVar -> Type
varType TyCoVar
var)
FV -> FV -> FV
`unionFV` TyCoVar -> FV -> FV
delFV TyCoVar
var FV
fvs
tyCoFVsOfTypes :: [Type] -> FV
tyCoFVsOfTypes :: [Type] -> FV
tyCoFVsOfTypes (Type
ty:[Type]
tys) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc = (Type -> FV
tyCoFVsOfType Type
ty FV -> FV -> FV
`unionFV` [Type] -> FV
tyCoFVsOfTypes [Type]
tys) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfTypes [] InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc = FV
emptyFV InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoVarsOfCoDSet :: Coercion -> DTyCoVarSet
tyCoVarsOfCoDSet :: Coercion -> DTyVarSet
tyCoVarsOfCoDSet Coercion
co = FV -> DTyVarSet
fvDVarSet (FV -> DTyVarSet) -> FV -> DTyVarSet
forall a b. (a -> b) -> a -> b
$ Coercion -> FV
tyCoFVsOfCo Coercion
co
tyCoVarsOfCoList :: Coercion -> [TyCoVar]
tyCoVarsOfCoList :: Coercion -> [TyCoVar]
tyCoVarsOfCoList Coercion
co = FV -> [TyCoVar]
fvVarList (FV -> [TyCoVar]) -> FV -> [TyCoVar]
forall a b. (a -> b) -> a -> b
$ Coercion -> FV
tyCoFVsOfCo Coercion
co
tyCoFVsOfMCo :: MCoercion -> FV
tyCoFVsOfMCo :: MCoercion -> FV
tyCoFVsOfMCo MCoercion
MRefl = FV
emptyFV
tyCoFVsOfMCo (MCo Coercion
co) = Coercion -> FV
tyCoFVsOfCo Coercion
co
tyCoFVsOfCo :: Coercion -> FV
tyCoFVsOfCo :: Coercion -> FV
tyCoFVsOfCo (Refl Type
ty) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
= Type -> FV
tyCoFVsOfType Type
ty InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfCo (GRefl Role
_ Type
ty MCoercion
mco) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
= (Type -> FV
tyCoFVsOfType Type
ty FV -> FV -> FV
`unionFV` MCoercion -> FV
tyCoFVsOfMCo MCoercion
mco) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfCo (TyConAppCo Role
_ TyCon
_ [Coercion]
cos) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc = [Coercion] -> FV
tyCoFVsOfCos [Coercion]
cos InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfCo (AppCo Coercion
co Coercion
arg) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
= (Coercion -> FV
tyCoFVsOfCo Coercion
co FV -> FV -> FV
`unionFV` Coercion -> FV
tyCoFVsOfCo Coercion
arg) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfCo (ForAllCo TyCoVar
tv Coercion
kind_co Coercion
co) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
= (TyCoVar -> FV -> FV
tyCoFVsVarBndr TyCoVar
tv (Coercion -> FV
tyCoFVsOfCo Coercion
co) FV -> FV -> FV
`unionFV` Coercion -> FV
tyCoFVsOfCo Coercion
kind_co) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfCo (FunCo Role
_ Coercion
w Coercion
co1 Coercion
co2) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
= (Coercion -> FV
tyCoFVsOfCo Coercion
co1 FV -> FV -> FV
`unionFV` Coercion -> FV
tyCoFVsOfCo Coercion
co2 FV -> FV -> FV
`unionFV` Coercion -> FV
tyCoFVsOfCo Coercion
w) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfCo (CoVarCo TyCoVar
v) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
= TyCoVar -> FV
tyCoFVsOfCoVar TyCoVar
v InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfCo (HoleCo CoercionHole
h) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
= TyCoVar -> FV
tyCoFVsOfCoVar (CoercionHole -> TyCoVar
coHoleCoVar CoercionHole
h) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfCo (AxiomInstCo CoAxiom Branched
_ BranchIndex
_ [Coercion]
cos) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc = [Coercion] -> FV
tyCoFVsOfCos [Coercion]
cos InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfCo (UnivCo UnivCoProvenance
p Role
_ Type
t1 Type
t2) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
= (UnivCoProvenance -> FV
tyCoFVsOfProv UnivCoProvenance
p FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType Type
t1
FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType Type
t2) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfCo (SymCo Coercion
co) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfCo (TransCo Coercion
co1 Coercion
co2) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc = (Coercion -> FV
tyCoFVsOfCo Coercion
co1 FV -> FV -> FV
`unionFV` Coercion -> FV
tyCoFVsOfCo Coercion
co2) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfCo (NthCo Role
_ BranchIndex
_ Coercion
co) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfCo (LRCo LeftOrRight
_ Coercion
co) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfCo (InstCo Coercion
co Coercion
arg) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc = (Coercion -> FV
tyCoFVsOfCo Coercion
co FV -> FV -> FV
`unionFV` Coercion -> FV
tyCoFVsOfCo Coercion
arg) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfCo (KindCo Coercion
co) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfCo (SubCo Coercion
co) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfCo (AxiomRuleCo CoAxiomRule
_ [Coercion]
cs) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc = [Coercion] -> FV
tyCoFVsOfCos [Coercion]
cs InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfCoVar :: CoVar -> FV
tyCoFVsOfCoVar :: TyCoVar -> FV
tyCoFVsOfCoVar TyCoVar
v InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
= (TyCoVar -> FV
unitFV TyCoVar
v FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType (TyCoVar -> Type
varType TyCoVar
v)) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfProv :: UnivCoProvenance -> FV
tyCoFVsOfProv :: UnivCoProvenance -> FV
tyCoFVsOfProv (PhantomProv Coercion
co) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfProv (ProofIrrelProv Coercion
co) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfProv (PluginProv String
_) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc = FV
emptyFV InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfProv (CorePrepProv Bool
_) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc = FV
emptyFV InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfCos :: [Coercion] -> FV
tyCoFVsOfCos :: [Coercion] -> FV
tyCoFVsOfCos [] InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc = FV
emptyFV InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
tyCoFVsOfCos (Coercion
co:[Coercion]
cos) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc = (Coercion -> FV
tyCoFVsOfCo Coercion
co FV -> FV -> FV
`unionFV` [Coercion] -> FV
tyCoFVsOfCos [Coercion]
cos) InterestingVarFun
fv_cand VarSet
in_scope ([TyCoVar], VarSet)
acc
almostDevoidCoVarOfCo :: CoVar -> Coercion -> Bool
almostDevoidCoVarOfCo :: TyCoVar -> Coercion -> Bool
almostDevoidCoVarOfCo TyCoVar
cv Coercion
co =
Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
cv
almost_devoid_co_var_of_co :: Coercion -> CoVar -> Bool
almost_devoid_co_var_of_co :: Coercion -> InterestingVarFun
almost_devoid_co_var_of_co (Refl {}) TyCoVar
_ = Bool
True
almost_devoid_co_var_of_co (GRefl {}) TyCoVar
_ = Bool
True
almost_devoid_co_var_of_co (TyConAppCo Role
_ TyCon
_ [Coercion]
cos) TyCoVar
cv
= [Coercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [Coercion]
cos TyCoVar
cv
almost_devoid_co_var_of_co (AppCo Coercion
co Coercion
arg) TyCoVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
cv
Bool -> Bool -> Bool
&& Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
arg TyCoVar
cv
almost_devoid_co_var_of_co (ForAllCo TyCoVar
v Coercion
kind_co Coercion
co) TyCoVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
kind_co TyCoVar
cv
Bool -> Bool -> Bool
&& (TyCoVar
v TyCoVar -> InterestingVarFun
forall a. Eq a => a -> a -> Bool
== TyCoVar
cv Bool -> Bool -> Bool
|| Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
cv)
almost_devoid_co_var_of_co (FunCo Role
_ Coercion
w Coercion
co1 Coercion
co2) TyCoVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
w TyCoVar
cv
Bool -> Bool -> Bool
&& Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co1 TyCoVar
cv
Bool -> Bool -> Bool
&& Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co2 TyCoVar
cv
almost_devoid_co_var_of_co (CoVarCo TyCoVar
v) TyCoVar
cv = TyCoVar
v TyCoVar -> InterestingVarFun
forall a. Eq a => a -> a -> Bool
/= TyCoVar
cv
almost_devoid_co_var_of_co (HoleCo CoercionHole
h) TyCoVar
cv = (CoercionHole -> TyCoVar
coHoleCoVar CoercionHole
h) TyCoVar -> InterestingVarFun
forall a. Eq a => a -> a -> Bool
/= TyCoVar
cv
almost_devoid_co_var_of_co (AxiomInstCo CoAxiom Branched
_ BranchIndex
_ [Coercion]
cos) TyCoVar
cv
= [Coercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [Coercion]
cos TyCoVar
cv
almost_devoid_co_var_of_co (UnivCo UnivCoProvenance
p Role
_ Type
t1 Type
t2) TyCoVar
cv
= UnivCoProvenance -> InterestingVarFun
almost_devoid_co_var_of_prov UnivCoProvenance
p TyCoVar
cv
Bool -> Bool -> Bool
&& Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
t1 TyCoVar
cv
Bool -> Bool -> Bool
&& Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
t2 TyCoVar
cv
almost_devoid_co_var_of_co (SymCo Coercion
co) TyCoVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
cv
almost_devoid_co_var_of_co (TransCo Coercion
co1 Coercion
co2) TyCoVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co1 TyCoVar
cv
Bool -> Bool -> Bool
&& Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co2 TyCoVar
cv
almost_devoid_co_var_of_co (NthCo Role
_ BranchIndex
_ Coercion
co) TyCoVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
cv
almost_devoid_co_var_of_co (LRCo LeftOrRight
_ Coercion
co) TyCoVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
cv
almost_devoid_co_var_of_co (InstCo Coercion
co Coercion
arg) TyCoVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
cv
Bool -> Bool -> Bool
&& Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
arg TyCoVar
cv
almost_devoid_co_var_of_co (KindCo Coercion
co) TyCoVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
cv
almost_devoid_co_var_of_co (SubCo Coercion
co) TyCoVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
cv
almost_devoid_co_var_of_co (AxiomRuleCo CoAxiomRule
_ [Coercion]
cs) TyCoVar
cv
= [Coercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [Coercion]
cs TyCoVar
cv
almost_devoid_co_var_of_cos :: [Coercion] -> CoVar -> Bool
almost_devoid_co_var_of_cos :: [Coercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [] TyCoVar
_ = Bool
True
almost_devoid_co_var_of_cos (Coercion
co:[Coercion]
cos) TyCoVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
cv
Bool -> Bool -> Bool
&& [Coercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [Coercion]
cos TyCoVar
cv
almost_devoid_co_var_of_prov :: UnivCoProvenance -> CoVar -> Bool
almost_devoid_co_var_of_prov :: UnivCoProvenance -> InterestingVarFun
almost_devoid_co_var_of_prov (PhantomProv Coercion
co) TyCoVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
cv
almost_devoid_co_var_of_prov (ProofIrrelProv Coercion
co) TyCoVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
cv
almost_devoid_co_var_of_prov (PluginProv String
_) TyCoVar
_ = Bool
True
almost_devoid_co_var_of_prov (CorePrepProv Bool
_) TyCoVar
_ = Bool
True
almost_devoid_co_var_of_type :: Type -> CoVar -> Bool
almost_devoid_co_var_of_type :: Type -> InterestingVarFun
almost_devoid_co_var_of_type (TyVarTy TyCoVar
_) TyCoVar
_ = Bool
True
almost_devoid_co_var_of_type (TyConApp TyCon
_ [Type]
tys) TyCoVar
cv
= [Type] -> InterestingVarFun
almost_devoid_co_var_of_types [Type]
tys TyCoVar
cv
almost_devoid_co_var_of_type (LitTy {}) TyCoVar
_ = Bool
True
almost_devoid_co_var_of_type (AppTy Type
fun Type
arg) TyCoVar
cv
= Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
fun TyCoVar
cv
Bool -> Bool -> Bool
&& Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
arg TyCoVar
cv
almost_devoid_co_var_of_type (FunTy AnonArgFlag
_ Type
w Type
arg Type
res) TyCoVar
cv
= Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
w TyCoVar
cv
Bool -> Bool -> Bool
&& Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
arg TyCoVar
cv
Bool -> Bool -> Bool
&& Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
res TyCoVar
cv
almost_devoid_co_var_of_type (ForAllTy (Bndr TyCoVar
v ArgFlag
_) Type
ty) TyCoVar
cv
= Type -> InterestingVarFun
almost_devoid_co_var_of_type (TyCoVar -> Type
varType TyCoVar
v) TyCoVar
cv
Bool -> Bool -> Bool
&& (TyCoVar
v TyCoVar -> InterestingVarFun
forall a. Eq a => a -> a -> Bool
== TyCoVar
cv Bool -> Bool -> Bool
|| Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
ty TyCoVar
cv)
almost_devoid_co_var_of_type (CastTy Type
ty Coercion
co) TyCoVar
cv
= Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
ty TyCoVar
cv
Bool -> Bool -> Bool
&& Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
cv
almost_devoid_co_var_of_type (CoercionTy Coercion
co) TyCoVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyCoVar
cv
almost_devoid_co_var_of_types :: [Type] -> CoVar -> Bool
almost_devoid_co_var_of_types :: [Type] -> InterestingVarFun
almost_devoid_co_var_of_types [] TyCoVar
_ = Bool
True
almost_devoid_co_var_of_types (Type
ty:[Type]
tys) TyCoVar
cv
= Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
ty TyCoVar
cv
Bool -> Bool -> Bool
&& [Type] -> InterestingVarFun
almost_devoid_co_var_of_types [Type]
tys TyCoVar
cv
injectiveVarsOfType :: Bool
-> Type -> FV
injectiveVarsOfType :: Bool -> Type -> FV
injectiveVarsOfType Bool
look_under_tfs = Type -> FV
go
where
go :: Type -> FV
go Type
ty | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty
= Type -> FV
go Type
ty'
go (TyVarTy TyCoVar
v) = TyCoVar -> FV
unitFV TyCoVar
v FV -> FV -> FV
`unionFV` Type -> FV
go (TyCoVar -> Type
tyVarKind TyCoVar
v)
go (AppTy Type
f Type
a) = Type -> FV
go Type
f FV -> FV -> FV
`unionFV` Type -> FV
go Type
a
go (FunTy AnonArgFlag
_ Type
w Type
ty1 Type
ty2) = Type -> FV
go Type
w FV -> FV -> FV
`unionFV` Type -> FV
go Type
ty1 FV -> FV -> FV
`unionFV` Type -> FV
go Type
ty2
go (TyConApp TyCon
tc [Type]
tys) =
case TyCon -> Injectivity
tyConInjectivityInfo TyCon
tc of
Injective [Bool]
inj
| Bool
look_under_tfs Bool -> Bool -> Bool
|| Bool -> Bool
not (TyCon -> Bool
isTypeFamilyTyCon TyCon
tc)
-> (Type -> FV) -> [Type] -> FV
forall a. (a -> FV) -> [a] -> FV
mapUnionFV Type -> FV
go ([Type] -> FV) -> [Type] -> FV
forall a b. (a -> b) -> a -> b
$
[Bool] -> [Type] -> [Type]
forall a. [Bool] -> [a] -> [a]
filterByList ([Bool]
inj [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ Bool -> [Bool]
forall a. a -> [a]
repeat Bool
True) [Type]
tys
Injectivity
_ -> FV
emptyFV
go (ForAllTy (Bndr TyCoVar
tv ArgFlag
_) Type
ty) = Type -> FV
go (TyCoVar -> Type
tyVarKind TyCoVar
tv) FV -> FV -> FV
`unionFV` TyCoVar -> FV -> FV
delFV TyCoVar
tv (Type -> FV
go Type
ty)
go LitTy{} = FV
emptyFV
go (CastTy Type
ty Coercion
_) = Type -> FV
go Type
ty
go CoercionTy{} = FV
emptyFV
injectiveVarsOfTypes :: Bool
-> [Type] -> FV
injectiveVarsOfTypes :: Bool -> [Type] -> FV
injectiveVarsOfTypes Bool
look_under_tfs = (Type -> FV) -> [Type] -> FV
forall a. (a -> FV) -> [a] -> FV
mapUnionFV (Bool -> Type -> FV
injectiveVarsOfType Bool
look_under_tfs)
invisibleVarsOfType :: Type -> FV
invisibleVarsOfType :: Type -> FV
invisibleVarsOfType = Type -> FV
go
where
go :: Type -> FV
go Type
ty | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty
= Type -> FV
go Type
ty'
go (TyVarTy TyCoVar
v) = Type -> FV
go (TyCoVar -> Type
tyVarKind TyCoVar
v)
go (AppTy Type
f Type
a) = Type -> FV
go Type
f FV -> FV -> FV
`unionFV` Type -> FV
go Type
a
go (FunTy AnonArgFlag
_ Type
w Type
ty1 Type
ty2) = Type -> FV
go Type
w FV -> FV -> FV
`unionFV` Type -> FV
go Type
ty1 FV -> FV -> FV
`unionFV` Type -> FV
go Type
ty2
go (TyConApp TyCon
tc [Type]
tys) = [Type] -> FV
tyCoFVsOfTypes [Type]
invisibles FV -> FV -> FV
`unionFV`
[Type] -> FV
invisibleVarsOfTypes [Type]
visibles
where ([Type]
invisibles, [Type]
visibles) = TyCon -> [Type] -> ([Type], [Type])
partitionInvisibleTypes TyCon
tc [Type]
tys
go (ForAllTy TyCoVarBinder
tvb Type
ty) = TyCoVarBinder -> FV -> FV
tyCoFVsBndr TyCoVarBinder
tvb (FV -> FV) -> FV -> FV
forall a b. (a -> b) -> a -> b
$ Type -> FV
go Type
ty
go LitTy{} = FV
emptyFV
go (CastTy Type
ty Coercion
co) = Coercion -> FV
tyCoFVsOfCo Coercion
co FV -> FV -> FV
`unionFV` Type -> FV
go Type
ty
go (CoercionTy Coercion
co) = Coercion -> FV
tyCoFVsOfCo Coercion
co
invisibleVarsOfTypes :: [Type] -> FV
invisibleVarsOfTypes :: [Type] -> FV
invisibleVarsOfTypes = (Type -> FV) -> [Type] -> FV
forall a. (a -> FV) -> [a] -> FV
mapUnionFV Type -> FV
invisibleVarsOfType
{-# INLINE afvFolder #-}
afvFolder :: (TyCoVar -> Bool) -> TyCoFolder TyCoVarSet DM.Any
afvFolder :: InterestingVarFun -> TyCoFolder VarSet Any
afvFolder InterestingVarFun
check_fv = TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view = Type -> Maybe Type
noView
, tcf_tyvar :: VarSet -> TyCoVar -> Any
tcf_tyvar = VarSet -> TyCoVar -> Any
do_tcv, tcf_covar :: VarSet -> TyCoVar -> Any
tcf_covar = VarSet -> TyCoVar -> Any
do_tcv
, tcf_hole :: VarSet -> CoercionHole -> Any
tcf_hole = VarSet -> CoercionHole -> Any
forall {p} {p}. p -> p -> Any
do_hole, tcf_tycobinder :: VarSet -> TyCoVar -> ArgFlag -> VarSet
tcf_tycobinder = VarSet -> TyCoVar -> ArgFlag -> VarSet
forall {p}. VarSet -> TyCoVar -> p -> VarSet
do_bndr }
where
do_tcv :: VarSet -> TyCoVar -> Any
do_tcv VarSet
is TyCoVar
tv = Bool -> Any
Any (Bool -> Bool
not (TyCoVar
tv TyCoVar -> VarSet -> Bool
`elemVarSet` VarSet
is) Bool -> Bool -> Bool
&& InterestingVarFun
check_fv TyCoVar
tv)
do_hole :: p -> p -> Any
do_hole p
_ p
_ = Bool -> Any
Any Bool
False
do_bndr :: VarSet -> TyCoVar -> p -> VarSet
do_bndr VarSet
is TyCoVar
tv p
_ = VarSet
is VarSet -> TyCoVar -> VarSet
`extendVarSet` TyCoVar
tv
anyFreeVarsOfType :: (TyCoVar -> Bool) -> Type -> Bool
anyFreeVarsOfType :: InterestingVarFun -> Type -> Bool
anyFreeVarsOfType InterestingVarFun
check_fv Type
ty = Any -> Bool
DM.getAny (Type -> Any
f Type
ty)
where (Type -> Any
f, [Type] -> Any
_, Coercion -> Any
_, [Coercion] -> Any
_) = TyCoFolder VarSet Any
-> VarSet
-> (Type -> Any, [Type] -> Any, Coercion -> Any, [Coercion] -> Any)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo (InterestingVarFun -> TyCoFolder VarSet Any
afvFolder InterestingVarFun
check_fv) VarSet
emptyVarSet
anyFreeVarsOfTypes :: (TyCoVar -> Bool) -> [Type] -> Bool
anyFreeVarsOfTypes :: InterestingVarFun -> [Type] -> Bool
anyFreeVarsOfTypes InterestingVarFun
check_fv [Type]
tys = Any -> Bool
DM.getAny ([Type] -> Any
f [Type]
tys)
where (Type -> Any
_, [Type] -> Any
f, Coercion -> Any
_, [Coercion] -> Any
_) = TyCoFolder VarSet Any
-> VarSet
-> (Type -> Any, [Type] -> Any, Coercion -> Any, [Coercion] -> Any)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo (InterestingVarFun -> TyCoFolder VarSet Any
afvFolder InterestingVarFun
check_fv) VarSet
emptyVarSet
anyFreeVarsOfCo :: (TyCoVar -> Bool) -> Coercion -> Bool
anyFreeVarsOfCo :: InterestingVarFun -> Coercion -> Bool
anyFreeVarsOfCo InterestingVarFun
check_fv Coercion
co = Any -> Bool
DM.getAny (Coercion -> Any
f Coercion
co)
where (Type -> Any
_, [Type] -> Any
_, Coercion -> Any
f, [Coercion] -> Any
_) = TyCoFolder VarSet Any
-> VarSet
-> (Type -> Any, [Type] -> Any, Coercion -> Any, [Coercion] -> Any)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo (InterestingVarFun -> TyCoFolder VarSet Any
afvFolder InterestingVarFun
check_fv) VarSet
emptyVarSet
noFreeVarsOfType :: Type -> Bool
noFreeVarsOfType :: Type -> Bool
noFreeVarsOfType Type
ty = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Any -> Bool
DM.getAny (Type -> Any
f Type
ty)
where (Type -> Any
f, [Type] -> Any
_, Coercion -> Any
_, [Coercion] -> Any
_) = TyCoFolder VarSet Any
-> VarSet
-> (Type -> Any, [Type] -> Any, Coercion -> Any, [Coercion] -> Any)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo (InterestingVarFun -> TyCoFolder VarSet Any
afvFolder (Bool -> InterestingVarFun
forall a b. a -> b -> a
const Bool
True)) VarSet
emptyVarSet
noFreeVarsOfTypes :: [Type] -> Bool
noFreeVarsOfTypes :: [Type] -> Bool
noFreeVarsOfTypes [Type]
tys = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Any -> Bool
DM.getAny ([Type] -> Any
f [Type]
tys)
where (Type -> Any
_, [Type] -> Any
f, Coercion -> Any
_, [Coercion] -> Any
_) = TyCoFolder VarSet Any
-> VarSet
-> (Type -> Any, [Type] -> Any, Coercion -> Any, [Coercion] -> Any)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo (InterestingVarFun -> TyCoFolder VarSet Any
afvFolder (Bool -> InterestingVarFun
forall a b. a -> b -> a
const Bool
True)) VarSet
emptyVarSet
noFreeVarsOfCo :: Coercion -> Bool
noFreeVarsOfCo :: Coercion -> Bool
noFreeVarsOfCo Coercion
co = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Any -> Bool
DM.getAny (Coercion -> Any
f Coercion
co)
where (Type -> Any
_, [Type] -> Any
_, Coercion -> Any
f, [Coercion] -> Any
_) = TyCoFolder VarSet Any
-> VarSet
-> (Type -> Any, [Type] -> Any, Coercion -> Any, [Coercion] -> Any)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo (InterestingVarFun -> TyCoFolder VarSet Any
afvFolder (Bool -> InterestingVarFun
forall a b. a -> b -> a
const Bool
True)) VarSet
emptyVarSet
scopedSort :: [TyCoVar] -> [TyCoVar]
scopedSort :: [TyCoVar] -> [TyCoVar]
scopedSort = [TyCoVar] -> [VarSet] -> [TyCoVar] -> [TyCoVar]
go [] []
where
go :: [TyCoVar]
-> [TyCoVarSet]
-> [TyCoVar]
-> [TyCoVar]
go :: [TyCoVar] -> [VarSet] -> [TyCoVar] -> [TyCoVar]
go [TyCoVar]
acc [VarSet]
_fv_list [] = [TyCoVar] -> [TyCoVar]
forall a. [a] -> [a]
reverse [TyCoVar]
acc
go [TyCoVar]
acc [VarSet]
fv_list (TyCoVar
tv:[TyCoVar]
tvs)
= [TyCoVar] -> [VarSet] -> [TyCoVar] -> [TyCoVar]
go [TyCoVar]
acc' [VarSet]
fv_list' [TyCoVar]
tvs
where
([TyCoVar]
acc', [VarSet]
fv_list') = TyCoVar -> [TyCoVar] -> [VarSet] -> ([TyCoVar], [VarSet])
insert TyCoVar
tv [TyCoVar]
acc [VarSet]
fv_list
insert :: TyCoVar
-> [TyCoVar]
-> [TyCoVarSet]
-> ([TyCoVar], [TyCoVarSet])
insert :: TyCoVar -> [TyCoVar] -> [VarSet] -> ([TyCoVar], [VarSet])
insert TyCoVar
tv [] [] = ([TyCoVar
tv], [Type -> VarSet
tyCoVarsOfType (TyCoVar -> Type
tyVarKind TyCoVar
tv)])
insert TyCoVar
tv (TyCoVar
a:[TyCoVar]
as) (VarSet
fvs:[VarSet]
fvss)
| TyCoVar
tv TyCoVar -> VarSet -> Bool
`elemVarSet` VarSet
fvs
, ([TyCoVar]
as', [VarSet]
fvss') <- TyCoVar -> [TyCoVar] -> [VarSet] -> ([TyCoVar], [VarSet])
insert TyCoVar
tv [TyCoVar]
as [VarSet]
fvss
= (TyCoVar
aTyCoVar -> [TyCoVar] -> [TyCoVar]
forall a. a -> [a] -> [a]
:[TyCoVar]
as', VarSet
fvs VarSet -> VarSet -> VarSet
`unionVarSet` VarSet
fv_tv VarSet -> [VarSet] -> [VarSet]
forall a. a -> [a] -> [a]
: [VarSet]
fvss')
| Bool
otherwise
= (TyCoVar
tvTyCoVar -> [TyCoVar] -> [TyCoVar]
forall a. a -> [a] -> [a]
:TyCoVar
aTyCoVar -> [TyCoVar] -> [TyCoVar]
forall a. a -> [a] -> [a]
:[TyCoVar]
as, VarSet
fvs VarSet -> VarSet -> VarSet
`unionVarSet` VarSet
fv_tv VarSet -> [VarSet] -> [VarSet]
forall a. a -> [a] -> [a]
: VarSet
fvs VarSet -> [VarSet] -> [VarSet]
forall a. a -> [a] -> [a]
: [VarSet]
fvss)
where
fv_tv :: VarSet
fv_tv = Type -> VarSet
tyCoVarsOfType (TyCoVar -> Type
tyVarKind TyCoVar
tv)
insert TyCoVar
_ [TyCoVar]
_ [VarSet]
_ = String -> ([TyCoVar], [VarSet])
forall a. String -> a
panic String
"scopedSort"
tyCoVarsOfTypeWellScoped :: Type -> [TyVar]
tyCoVarsOfTypeWellScoped :: Type -> [TyCoVar]
tyCoVarsOfTypeWellScoped = [TyCoVar] -> [TyCoVar]
scopedSort ([TyCoVar] -> [TyCoVar])
-> (Type -> [TyCoVar]) -> Type -> [TyCoVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [TyCoVar]
tyCoVarsOfTypeList
tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
tyCoVarsOfTypesWellScoped :: [Type] -> [TyCoVar]
tyCoVarsOfTypesWellScoped = [TyCoVar] -> [TyCoVar]
scopedSort ([TyCoVar] -> [TyCoVar])
-> ([Type] -> [TyCoVar]) -> [Type] -> [TyCoVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Type] -> [TyCoVar]
tyCoVarsOfTypesList