module TyCoFVs
(
tyCoVarsOfType, tyCoVarsOfTypeDSet, tyCoVarsOfTypes, tyCoVarsOfTypesDSet,
exactTyCoVarsOfType, exactTyCoVarsOfTypes,
tyCoFVsBndr, tyCoFVsVarBndr, tyCoFVsVarBndrs,
tyCoFVsOfType, tyCoVarsOfTypeList,
tyCoFVsOfTypes, tyCoVarsOfTypesList,
tyCoVarsOfTypesSet, tyCoVarsOfCosSet,
coVarsOfType, coVarsOfTypes,
coVarsOfCo, coVarsOfCos,
tyCoVarsOfCo, tyCoVarsOfCos,
tyCoVarsOfCoDSet,
tyCoFVsOfCo, tyCoFVsOfCos,
tyCoVarsOfCoList, tyCoVarsOfProv,
almostDevoidCoVarOfCo,
injectiveVarsOfType, injectiveVarsOfTypes,
invisibleVarsOfType, invisibleVarsOfTypes,
noFreeVarsOfType, noFreeVarsOfTypes, noFreeVarsOfCo,
mkTyCoInScopeSet,
scopedSort, tyCoVarsOfTypeWellScoped,
tyCoVarsOfTypesWellScoped,
) where
import GhcPrelude
import {-# SOURCE #-} Type (coreView, tcView, partitionInvisibleTypes)
import TyCoRep
import TyCon
import Var
import FV
import UniqFM
import VarSet
import VarEnv
import Util
import Panic
tyCoVarsOfType :: Type -> TyCoVarSet
tyCoVarsOfType :: Type -> TyCoVarSet
tyCoVarsOfType ty :: Type
ty = Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type Type
ty TyCoVarSet
emptyVarSet TyCoVarSet
emptyVarSet
tyCoVarsOfTypes :: [Type] -> TyCoVarSet
tyCoVarsOfTypes :: [Type] -> TyCoVarSet
tyCoVarsOfTypes tys :: [Type]
tys = [Type] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_types [Type]
tys TyCoVarSet
emptyVarSet TyCoVarSet
emptyVarSet
ty_co_vars_of_type :: Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type :: Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type (TyVarTy v :: Var
v) is :: TyCoVarSet
is acc :: TyCoVarSet
acc
| Var
v Var -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
is = TyCoVarSet
acc
| Var
v Var -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
acc = TyCoVarSet
acc
| Bool
otherwise = Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type (Var -> Type
tyVarKind Var
v)
TyCoVarSet
emptyVarSet
(TyCoVarSet -> Var -> TyCoVarSet
extendVarSet TyCoVarSet
acc Var
v)
ty_co_vars_of_type (TyConApp _ tys :: [Type]
tys) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = [Type] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_types [Type]
tys TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_type (LitTy {}) _ acc :: TyCoVarSet
acc = TyCoVarSet
acc
ty_co_vars_of_type (AppTy fun :: Type
fun arg :: Type
arg) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type Type
fun TyCoVarSet
is (Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type Type
arg TyCoVarSet
is TyCoVarSet
acc)
ty_co_vars_of_type (FunTy _ arg :: Type
arg res :: Type
res) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type Type
arg TyCoVarSet
is (Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type Type
res TyCoVarSet
is TyCoVarSet
acc)
ty_co_vars_of_type (ForAllTy (Bndr tv :: Var
tv _) ty :: Type
ty) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type (Var -> Type
varType Var
tv) TyCoVarSet
is (TyCoVarSet -> TyCoVarSet) -> TyCoVarSet -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$
Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type Type
ty (TyCoVarSet -> Var -> TyCoVarSet
extendVarSet TyCoVarSet
is Var
tv) TyCoVarSet
acc
ty_co_vars_of_type (CastTy ty :: Type
ty co :: KindCoercion
co) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type Type
ty TyCoVarSet
is (KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
is TyCoVarSet
acc)
ty_co_vars_of_type (CoercionTy co :: KindCoercion
co) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_types :: [Type] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_types :: [Type] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_types [] _ acc :: TyCoVarSet
acc = TyCoVarSet
acc
ty_co_vars_of_types (ty :: Type
ty:tys :: [Type]
tys) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type Type
ty TyCoVarSet
is ([Type] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_types [Type]
tys TyCoVarSet
is TyCoVarSet
acc)
tyCoVarsOfCo :: Coercion -> TyCoVarSet
tyCoVarsOfCo :: KindCoercion -> TyCoVarSet
tyCoVarsOfCo co :: KindCoercion
co = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
emptyVarSet TyCoVarSet
emptyVarSet
tyCoVarsOfCos :: [Coercion] -> TyCoVarSet
tyCoVarsOfCos :: [KindCoercion] -> TyCoVarSet
tyCoVarsOfCos cos :: [KindCoercion]
cos = [KindCoercion] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_cos [KindCoercion]
cos TyCoVarSet
emptyVarSet TyCoVarSet
emptyVarSet
ty_co_vars_of_co :: Coercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co :: KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co (Refl ty :: Type
ty) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type Type
ty TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (GRefl _ ty :: Type
ty mco :: MCoercionN
mco) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type Type
ty TyCoVarSet
is (TyCoVarSet -> TyCoVarSet) -> TyCoVarSet -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$
MCoercionN -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_mco MCoercionN
mco TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (TyConAppCo _ _ cos :: [KindCoercion]
cos) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = [KindCoercion] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_cos [KindCoercion]
cos TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (AppCo co :: KindCoercion
co arg :: KindCoercion
arg) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
is (TyCoVarSet -> TyCoVarSet) -> TyCoVarSet -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$
KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
arg TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (ForAllCo tv :: Var
tv kind_co :: KindCoercion
kind_co co :: KindCoercion
co) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
kind_co TyCoVarSet
is (TyCoVarSet -> TyCoVarSet) -> TyCoVarSet -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$
KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co (TyCoVarSet -> Var -> TyCoVarSet
extendVarSet TyCoVarSet
is Var
tv) TyCoVarSet
acc
ty_co_vars_of_co (FunCo _ co1 :: KindCoercion
co1 co2 :: KindCoercion
co2) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co1 TyCoVarSet
is (TyCoVarSet -> TyCoVarSet) -> TyCoVarSet -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$
KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co2 TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (CoVarCo v :: Var
v) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = Var -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co_var Var
v TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (HoleCo h :: CoercionHole
h) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = Var -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co_var (CoercionHole -> Var
coHoleCoVar CoercionHole
h) TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (AxiomInstCo _ _ cos :: [KindCoercion]
cos) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = [KindCoercion] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_cos [KindCoercion]
cos TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (UnivCo p :: UnivCoProvenance
p _ t1 :: Type
t1 t2 :: Type
t2) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = UnivCoProvenance -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_prov UnivCoProvenance
p TyCoVarSet
is (TyCoVarSet -> TyCoVarSet) -> TyCoVarSet -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$
Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type Type
t1 TyCoVarSet
is (TyCoVarSet -> TyCoVarSet) -> TyCoVarSet -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$
Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type Type
t2 TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (SymCo co :: KindCoercion
co) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (TransCo co1 :: KindCoercion
co1 co2 :: KindCoercion
co2) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co1 TyCoVarSet
is (TyCoVarSet -> TyCoVarSet) -> TyCoVarSet -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$
KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co2 TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (NthCo _ _ co :: KindCoercion
co) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (LRCo _ co :: KindCoercion
co) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (InstCo co :: KindCoercion
co arg :: KindCoercion
arg) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
is (TyCoVarSet -> TyCoVarSet) -> TyCoVarSet -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$
KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
arg TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (KindCo co :: KindCoercion
co) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (SubCo co :: KindCoercion
co) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co (AxiomRuleCo _ cs :: [KindCoercion]
cs) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = [KindCoercion] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_cos [KindCoercion]
cs TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_mco :: MCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_mco :: MCoercionN -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_mco MRefl _is :: TyCoVarSet
_is acc :: TyCoVarSet
acc = TyCoVarSet
acc
ty_co_vars_of_mco (MCo co :: KindCoercion
co) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_co_var :: CoVar -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co_var :: Var -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co_var v :: Var
v is :: TyCoVarSet
is acc :: TyCoVarSet
acc
| Var
v Var -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
is = TyCoVarSet
acc
| Var
v Var -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
acc = TyCoVarSet
acc
| Bool
otherwise = Type -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_type (Var -> Type
varType Var
v)
TyCoVarSet
emptyVarSet
(TyCoVarSet -> Var -> TyCoVarSet
extendVarSet TyCoVarSet
acc Var
v)
ty_co_vars_of_cos :: [Coercion] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_cos :: [KindCoercion] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_cos [] _ acc :: TyCoVarSet
acc = TyCoVarSet
acc
ty_co_vars_of_cos (co :: KindCoercion
co:cos :: [KindCoercion]
cos) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
is ([KindCoercion] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_cos [KindCoercion]
cos TyCoVarSet
is TyCoVarSet
acc)
tyCoVarsOfProv :: UnivCoProvenance -> TyCoVarSet
tyCoVarsOfProv :: UnivCoProvenance -> TyCoVarSet
tyCoVarsOfProv prov :: UnivCoProvenance
prov = UnivCoProvenance -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_prov UnivCoProvenance
prov TyCoVarSet
emptyVarSet TyCoVarSet
emptyVarSet
ty_co_vars_of_prov :: UnivCoProvenance -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_prov :: UnivCoProvenance -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_prov (PhantomProv co :: KindCoercion
co) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_prov (ProofIrrelProv co :: KindCoercion
co) is :: TyCoVarSet
is acc :: TyCoVarSet
acc = KindCoercion -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_co KindCoercion
co TyCoVarSet
is TyCoVarSet
acc
ty_co_vars_of_prov UnsafeCoerceProv _ acc :: TyCoVarSet
acc = TyCoVarSet
acc
ty_co_vars_of_prov (PluginProv _) _ acc :: TyCoVarSet
acc = TyCoVarSet
acc
mkTyCoInScopeSet :: [Type] -> [Coercion] -> InScopeSet
mkTyCoInScopeSet :: [Type] -> [KindCoercion] -> InScopeSet
mkTyCoInScopeSet tys :: [Type]
tys cos :: [KindCoercion]
cos
= TyCoVarSet -> InScopeSet
mkInScopeSet ([Type] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_types [Type]
tys TyCoVarSet
emptyVarSet (TyCoVarSet -> TyCoVarSet) -> TyCoVarSet -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$
[KindCoercion] -> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
ty_co_vars_of_cos [KindCoercion]
cos TyCoVarSet
emptyVarSet TyCoVarSet
emptyVarSet)
tyCoVarsOfTypeDSet :: Type -> DTyCoVarSet
tyCoVarsOfTypeDSet :: Type -> DTyCoVarSet
tyCoVarsOfTypeDSet ty :: Type
ty = FV -> DTyCoVarSet
fvDVarSet (FV -> DTyCoVarSet) -> FV -> DTyCoVarSet
forall a b. (a -> b) -> a -> b
$ Type -> FV
tyCoFVsOfType Type
ty
tyCoVarsOfTypeList :: Type -> [TyCoVar]
tyCoVarsOfTypeList :: Type -> [Var]
tyCoVarsOfTypeList ty :: Type
ty = FV -> [Var]
fvVarList (FV -> [Var]) -> FV -> [Var]
forall a b. (a -> b) -> a -> b
$ Type -> FV
tyCoFVsOfType Type
ty
tyCoVarsOfTypesSet :: TyVarEnv Type -> TyCoVarSet
tyCoVarsOfTypesSet :: TyVarEnv Type -> TyCoVarSet
tyCoVarsOfTypesSet tys :: TyVarEnv Type
tys = [Type] -> TyCoVarSet
tyCoVarsOfTypes ([Type] -> TyCoVarSet) -> [Type] -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$ TyVarEnv Type -> [Type]
forall elt. UniqFM elt -> [elt]
nonDetEltsUFM TyVarEnv Type
tys
tyCoVarsOfTypesDSet :: [Type] -> DTyCoVarSet
tyCoVarsOfTypesDSet :: [Type] -> DTyCoVarSet
tyCoVarsOfTypesDSet tys :: [Type]
tys = FV -> DTyCoVarSet
fvDVarSet (FV -> DTyCoVarSet) -> FV -> DTyCoVarSet
forall a b. (a -> b) -> a -> b
$ [Type] -> FV
tyCoFVsOfTypes [Type]
tys
tyCoVarsOfTypesList :: [Type] -> [TyCoVar]
tyCoVarsOfTypesList :: [Type] -> [Var]
tyCoVarsOfTypesList tys :: [Type]
tys = FV -> [Var]
fvVarList (FV -> [Var]) -> FV -> [Var]
forall a b. (a -> b) -> a -> b
$ [Type] -> FV
tyCoFVsOfTypes [Type]
tys
exactTyCoVarsOfType :: Type -> TyCoVarSet
exactTyCoVarsOfType :: Type -> TyCoVarSet
exactTyCoVarsOfType ty :: Type
ty
= Type -> TyCoVarSet
go Type
ty
where
go :: Type -> TyCoVarSet
go ty :: Type
ty | Just ty' :: Type
ty' <- Type -> Maybe Type
tcView Type
ty = Type -> TyCoVarSet
go Type
ty'
go (TyVarTy tv :: Var
tv) = Var -> TyCoVarSet
goVar Var
tv
go (TyConApp _ tys :: [Type]
tys) = [Type] -> TyCoVarSet
exactTyCoVarsOfTypes [Type]
tys
go (LitTy {}) = TyCoVarSet
emptyVarSet
go (AppTy fun :: Type
fun arg :: Type
arg) = Type -> TyCoVarSet
go Type
fun TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` Type -> TyCoVarSet
go Type
arg
go (FunTy _ arg :: Type
arg res :: Type
res) = Type -> TyCoVarSet
go Type
arg TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` Type -> TyCoVarSet
go Type
res
go (ForAllTy bndr :: VarBndr Var ArgFlag
bndr ty :: Type
ty) = TyCoVarSet -> VarBndr Var ArgFlag -> TyCoVarSet
delBinderVar (Type -> TyCoVarSet
go Type
ty) VarBndr Var ArgFlag
bndr TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` Type -> TyCoVarSet
go (VarBndr Var ArgFlag -> Type
forall argf. VarBndr Var argf -> Type
binderType VarBndr Var ArgFlag
bndr)
go (CastTy ty :: Type
ty co :: KindCoercion
co) = Type -> TyCoVarSet
go Type
ty TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` KindCoercion -> TyCoVarSet
goCo KindCoercion
co
go (CoercionTy co :: KindCoercion
co) = KindCoercion -> TyCoVarSet
goCo KindCoercion
co
goMCo :: MCoercionN -> TyCoVarSet
goMCo MRefl = TyCoVarSet
emptyVarSet
goMCo (MCo co :: KindCoercion
co) = KindCoercion -> TyCoVarSet
goCo KindCoercion
co
goCo :: KindCoercion -> TyCoVarSet
goCo (Refl ty :: Type
ty) = Type -> TyCoVarSet
go Type
ty
goCo (GRefl _ ty :: Type
ty mco :: MCoercionN
mco) = Type -> TyCoVarSet
go Type
ty TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` MCoercionN -> TyCoVarSet
goMCo MCoercionN
mco
goCo (TyConAppCo _ _ args :: [KindCoercion]
args)= [KindCoercion] -> TyCoVarSet
goCos [KindCoercion]
args
goCo (AppCo co :: KindCoercion
co arg :: KindCoercion
arg) = KindCoercion -> TyCoVarSet
goCo KindCoercion
co TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` KindCoercion -> TyCoVarSet
goCo KindCoercion
arg
goCo (ForAllCo tv :: Var
tv k_co :: KindCoercion
k_co co :: KindCoercion
co)
= KindCoercion -> TyCoVarSet
goCo KindCoercion
co TyCoVarSet -> Var -> TyCoVarSet
`delVarSet` Var
tv TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` KindCoercion -> TyCoVarSet
goCo KindCoercion
k_co
goCo (FunCo _ co1 :: KindCoercion
co1 co2 :: KindCoercion
co2) = KindCoercion -> TyCoVarSet
goCo KindCoercion
co1 TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` KindCoercion -> TyCoVarSet
goCo KindCoercion
co2
goCo (CoVarCo v :: Var
v) = Var -> TyCoVarSet
goVar Var
v
goCo (HoleCo h :: CoercionHole
h) = Var -> TyCoVarSet
goVar (CoercionHole -> Var
coHoleCoVar CoercionHole
h)
goCo (AxiomInstCo _ _ args :: [KindCoercion]
args) = [KindCoercion] -> TyCoVarSet
goCos [KindCoercion]
args
goCo (UnivCo p :: UnivCoProvenance
p _ t1 :: Type
t1 t2 :: Type
t2) = UnivCoProvenance -> TyCoVarSet
goProv UnivCoProvenance
p TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` Type -> TyCoVarSet
go Type
t1 TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` Type -> TyCoVarSet
go Type
t2
goCo (SymCo co :: KindCoercion
co) = KindCoercion -> TyCoVarSet
goCo KindCoercion
co
goCo (TransCo co1 :: KindCoercion
co1 co2 :: KindCoercion
co2) = KindCoercion -> TyCoVarSet
goCo KindCoercion
co1 TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` KindCoercion -> TyCoVarSet
goCo KindCoercion
co2
goCo (NthCo _ _ co :: KindCoercion
co) = KindCoercion -> TyCoVarSet
goCo KindCoercion
co
goCo (LRCo _ co :: KindCoercion
co) = KindCoercion -> TyCoVarSet
goCo KindCoercion
co
goCo (InstCo co :: KindCoercion
co arg :: KindCoercion
arg) = KindCoercion -> TyCoVarSet
goCo KindCoercion
co TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` KindCoercion -> TyCoVarSet
goCo KindCoercion
arg
goCo (KindCo co :: KindCoercion
co) = KindCoercion -> TyCoVarSet
goCo KindCoercion
co
goCo (SubCo co :: KindCoercion
co) = KindCoercion -> TyCoVarSet
goCo KindCoercion
co
goCo (AxiomRuleCo _ c :: [KindCoercion]
c) = [KindCoercion] -> TyCoVarSet
goCos [KindCoercion]
c
goCos :: [KindCoercion] -> TyCoVarSet
goCos cos :: [KindCoercion]
cos = (KindCoercion -> TyCoVarSet -> TyCoVarSet)
-> TyCoVarSet -> [KindCoercion] -> TyCoVarSet
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (TyCoVarSet -> TyCoVarSet -> TyCoVarSet
unionVarSet (TyCoVarSet -> TyCoVarSet -> TyCoVarSet)
-> (KindCoercion -> TyCoVarSet)
-> KindCoercion
-> TyCoVarSet
-> TyCoVarSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KindCoercion -> TyCoVarSet
goCo) TyCoVarSet
emptyVarSet [KindCoercion]
cos
goProv :: UnivCoProvenance -> TyCoVarSet
goProv UnsafeCoerceProv = TyCoVarSet
emptyVarSet
goProv (PhantomProv kco :: KindCoercion
kco) = KindCoercion -> TyCoVarSet
goCo KindCoercion
kco
goProv (ProofIrrelProv kco :: KindCoercion
kco) = KindCoercion -> TyCoVarSet
goCo KindCoercion
kco
goProv (PluginProv _) = TyCoVarSet
emptyVarSet
goVar :: Var -> TyCoVarSet
goVar v :: Var
v = Var -> TyCoVarSet
unitVarSet Var
v TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` Type -> TyCoVarSet
go (Var -> Type
varType Var
v)
exactTyCoVarsOfTypes :: [Type] -> TyVarSet
exactTyCoVarsOfTypes :: [Type] -> TyCoVarSet
exactTyCoVarsOfTypes tys :: [Type]
tys = (Type -> TyCoVarSet) -> [Type] -> TyCoVarSet
forall a. (a -> TyCoVarSet) -> [a] -> TyCoVarSet
mapUnionVarSet Type -> TyCoVarSet
exactTyCoVarsOfType [Type]
tys
tyCoFVsOfType :: Type -> FV
tyCoFVsOfType :: Type -> FV
tyCoFVsOfType (TyVarTy v :: Var
v) f :: InterestingVarFun
f bound_vars :: TyCoVarSet
bound_vars (acc_list :: [Var]
acc_list, acc_set :: TyCoVarSet
acc_set)
| Bool -> Bool
not (InterestingVarFun
f Var
v) = ([Var]
acc_list, TyCoVarSet
acc_set)
| Var
v Var -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
bound_vars = ([Var]
acc_list, TyCoVarSet
acc_set)
| Var
v Var -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
acc_set = ([Var]
acc_list, TyCoVarSet
acc_set)
| Bool
otherwise = Type -> FV
tyCoFVsOfType (Var -> Type
tyVarKind Var
v) InterestingVarFun
f
TyCoVarSet
emptyVarSet
(Var
vVar -> [Var] -> [Var]
forall a. a -> [a] -> [a]
:[Var]
acc_list, TyCoVarSet -> Var -> TyCoVarSet
extendVarSet TyCoVarSet
acc_set Var
v)
tyCoFVsOfType (TyConApp _ tys :: [Type]
tys) f :: InterestingVarFun
f bound_vars :: TyCoVarSet
bound_vars acc :: ([Var], TyCoVarSet)
acc = [Type] -> FV
tyCoFVsOfTypes [Type]
tys InterestingVarFun
f TyCoVarSet
bound_vars ([Var], TyCoVarSet)
acc
tyCoFVsOfType (LitTy {}) f :: InterestingVarFun
f bound_vars :: TyCoVarSet
bound_vars acc :: ([Var], TyCoVarSet)
acc = FV
emptyFV InterestingVarFun
f TyCoVarSet
bound_vars ([Var], TyCoVarSet)
acc
tyCoFVsOfType (AppTy fun :: Type
fun arg :: Type
arg) f :: InterestingVarFun
f bound_vars :: TyCoVarSet
bound_vars acc :: ([Var], TyCoVarSet)
acc = (Type -> FV
tyCoFVsOfType Type
fun FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType Type
arg) InterestingVarFun
f TyCoVarSet
bound_vars ([Var], TyCoVarSet)
acc
tyCoFVsOfType (FunTy _ arg :: Type
arg res :: Type
res) f :: InterestingVarFun
f bound_vars :: TyCoVarSet
bound_vars acc :: ([Var], TyCoVarSet)
acc = (Type -> FV
tyCoFVsOfType Type
arg FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType Type
res) InterestingVarFun
f TyCoVarSet
bound_vars ([Var], TyCoVarSet)
acc
tyCoFVsOfType (ForAllTy bndr :: VarBndr Var ArgFlag
bndr ty :: Type
ty) f :: InterestingVarFun
f bound_vars :: TyCoVarSet
bound_vars acc :: ([Var], TyCoVarSet)
acc = VarBndr Var ArgFlag -> FV -> FV
tyCoFVsBndr VarBndr Var ArgFlag
bndr (Type -> FV
tyCoFVsOfType Type
ty) InterestingVarFun
f TyCoVarSet
bound_vars ([Var], TyCoVarSet)
acc
tyCoFVsOfType (CastTy ty :: Type
ty co :: KindCoercion
co) f :: InterestingVarFun
f bound_vars :: TyCoVarSet
bound_vars acc :: ([Var], TyCoVarSet)
acc = (Type -> FV
tyCoFVsOfType Type
ty FV -> FV -> FV
`unionFV` KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co) InterestingVarFun
f TyCoVarSet
bound_vars ([Var], TyCoVarSet)
acc
tyCoFVsOfType (CoercionTy co :: KindCoercion
co) f :: InterestingVarFun
f bound_vars :: TyCoVarSet
bound_vars acc :: ([Var], TyCoVarSet)
acc = KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co InterestingVarFun
f TyCoVarSet
bound_vars ([Var], TyCoVarSet)
acc
tyCoFVsBndr :: TyCoVarBinder -> FV -> FV
tyCoFVsBndr :: VarBndr Var ArgFlag -> FV -> FV
tyCoFVsBndr (Bndr tv :: Var
tv _) fvs :: FV
fvs = Var -> FV -> FV
tyCoFVsVarBndr Var
tv FV
fvs
tyCoFVsVarBndrs :: [Var] -> FV -> FV
tyCoFVsVarBndrs :: [Var] -> FV -> FV
tyCoFVsVarBndrs vars :: [Var]
vars fvs :: FV
fvs = (Var -> FV -> FV) -> FV -> [Var] -> FV
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Var -> FV -> FV
tyCoFVsVarBndr FV
fvs [Var]
vars
tyCoFVsVarBndr :: Var -> FV -> FV
tyCoFVsVarBndr :: Var -> FV -> FV
tyCoFVsVarBndr var :: Var
var fvs :: FV
fvs
= Type -> FV
tyCoFVsOfType (Var -> Type
varType Var
var)
FV -> FV -> FV
`unionFV` Var -> FV -> FV
delFV Var
var FV
fvs
tyCoFVsOfTypes :: [Type] -> FV
tyCoFVsOfTypes :: [Type] -> FV
tyCoFVsOfTypes (ty :: Type
ty:tys :: [Type]
tys) fv_cand :: InterestingVarFun
fv_cand in_scope :: TyCoVarSet
in_scope acc :: ([Var], TyCoVarSet)
acc = (Type -> FV
tyCoFVsOfType Type
ty FV -> FV -> FV
`unionFV` [Type] -> FV
tyCoFVsOfTypes [Type]
tys) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfTypes [] fv_cand :: InterestingVarFun
fv_cand in_scope :: TyCoVarSet
in_scope acc :: ([Var], TyCoVarSet)
acc = FV
emptyFV InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoVarsOfCoDSet :: Coercion -> DTyCoVarSet
tyCoVarsOfCoDSet :: KindCoercion -> DTyCoVarSet
tyCoVarsOfCoDSet co :: KindCoercion
co = FV -> DTyCoVarSet
fvDVarSet (FV -> DTyCoVarSet) -> FV -> DTyCoVarSet
forall a b. (a -> b) -> a -> b
$ KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co
tyCoVarsOfCoList :: Coercion -> [TyCoVar]
tyCoVarsOfCoList :: KindCoercion -> [Var]
tyCoVarsOfCoList co :: KindCoercion
co = FV -> [Var]
fvVarList (FV -> [Var]) -> FV -> [Var]
forall a b. (a -> b) -> a -> b
$ KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co
tyCoFVsOfMCo :: MCoercion -> FV
tyCoFVsOfMCo :: MCoercionN -> FV
tyCoFVsOfMCo MRefl = FV
emptyFV
tyCoFVsOfMCo (MCo co :: KindCoercion
co) = KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co
tyCoVarsOfCosSet :: CoVarEnv Coercion -> TyCoVarSet
tyCoVarsOfCosSet :: CoVarEnv KindCoercion -> TyCoVarSet
tyCoVarsOfCosSet cos :: CoVarEnv KindCoercion
cos = [KindCoercion] -> TyCoVarSet
tyCoVarsOfCos ([KindCoercion] -> TyCoVarSet) -> [KindCoercion] -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$ CoVarEnv KindCoercion -> [KindCoercion]
forall elt. UniqFM elt -> [elt]
nonDetEltsUFM CoVarEnv KindCoercion
cos
tyCoFVsOfCo :: Coercion -> FV
tyCoFVsOfCo :: KindCoercion -> FV
tyCoFVsOfCo (Refl ty :: Type
ty) fv_cand :: InterestingVarFun
fv_cand in_scope :: TyCoVarSet
in_scope acc :: ([Var], TyCoVarSet)
acc
= Type -> FV
tyCoFVsOfType Type
ty InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (GRefl _ ty :: Type
ty mco :: MCoercionN
mco) fv_cand :: InterestingVarFun
fv_cand in_scope :: TyCoVarSet
in_scope acc :: ([Var], TyCoVarSet)
acc
= (Type -> FV
tyCoFVsOfType Type
ty FV -> FV -> FV
`unionFV` MCoercionN -> FV
tyCoFVsOfMCo MCoercionN
mco) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (TyConAppCo _ _ cos :: [KindCoercion]
cos) fv_cand :: InterestingVarFun
fv_cand in_scope :: TyCoVarSet
in_scope acc :: ([Var], TyCoVarSet)
acc = [KindCoercion] -> FV
tyCoFVsOfCos [KindCoercion]
cos InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (AppCo co :: KindCoercion
co arg :: KindCoercion
arg) fv_cand :: InterestingVarFun
fv_cand in_scope :: TyCoVarSet
in_scope acc :: ([Var], TyCoVarSet)
acc
= (KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co FV -> FV -> FV
`unionFV` KindCoercion -> FV
tyCoFVsOfCo KindCoercion
arg) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (ForAllCo tv :: Var
tv kind_co :: KindCoercion
kind_co co :: KindCoercion
co) fv_cand :: InterestingVarFun
fv_cand in_scope :: TyCoVarSet
in_scope acc :: ([Var], TyCoVarSet)
acc
= (Var -> FV -> FV
tyCoFVsVarBndr Var
tv (KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co) FV -> FV -> FV
`unionFV` KindCoercion -> FV
tyCoFVsOfCo KindCoercion
kind_co) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (FunCo _ co1 :: KindCoercion
co1 co2 :: KindCoercion
co2) fv_cand :: InterestingVarFun
fv_cand in_scope :: TyCoVarSet
in_scope acc :: ([Var], TyCoVarSet)
acc
= (KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co1 FV -> FV -> FV
`unionFV` KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co2) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (CoVarCo v :: Var
v) fv_cand :: InterestingVarFun
fv_cand in_scope :: TyCoVarSet
in_scope acc :: ([Var], TyCoVarSet)
acc
= Var -> FV
tyCoFVsOfCoVar Var
v InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (HoleCo h :: CoercionHole
h) fv_cand :: InterestingVarFun
fv_cand in_scope :: TyCoVarSet
in_scope acc :: ([Var], TyCoVarSet)
acc
= Var -> FV
tyCoFVsOfCoVar (CoercionHole -> Var
coHoleCoVar CoercionHole
h) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (AxiomInstCo _ _ cos :: [KindCoercion]
cos) fv_cand :: InterestingVarFun
fv_cand in_scope :: TyCoVarSet
in_scope acc :: ([Var], TyCoVarSet)
acc = [KindCoercion] -> FV
tyCoFVsOfCos [KindCoercion]
cos InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (UnivCo p :: UnivCoProvenance
p _ t1 :: Type
t1 t2 :: Type
t2) fv_cand :: InterestingVarFun
fv_cand in_scope :: TyCoVarSet
in_scope acc :: ([Var], TyCoVarSet)
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 TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (SymCo co :: KindCoercion
co) fv_cand :: InterestingVarFun
fv_cand in_scope :: TyCoVarSet
in_scope acc :: ([Var], TyCoVarSet)
acc = KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (TransCo co1 :: KindCoercion
co1 co2 :: KindCoercion
co2) fv_cand :: InterestingVarFun
fv_cand in_scope :: TyCoVarSet
in_scope acc :: ([Var], TyCoVarSet)
acc = (KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co1 FV -> FV -> FV
`unionFV` KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co2) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (NthCo _ _ co :: KindCoercion
co) fv_cand :: InterestingVarFun
fv_cand in_scope :: TyCoVarSet
in_scope acc :: ([Var], TyCoVarSet)
acc = KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (LRCo _ co :: KindCoercion
co) fv_cand :: InterestingVarFun
fv_cand in_scope :: TyCoVarSet
in_scope acc :: ([Var], TyCoVarSet)
acc = KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (InstCo co :: KindCoercion
co arg :: KindCoercion
arg) fv_cand :: InterestingVarFun
fv_cand in_scope :: TyCoVarSet
in_scope acc :: ([Var], TyCoVarSet)
acc = (KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co FV -> FV -> FV
`unionFV` KindCoercion -> FV
tyCoFVsOfCo KindCoercion
arg) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (KindCo co :: KindCoercion
co) fv_cand :: InterestingVarFun
fv_cand in_scope :: TyCoVarSet
in_scope acc :: ([Var], TyCoVarSet)
acc = KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (SubCo co :: KindCoercion
co) fv_cand :: InterestingVarFun
fv_cand in_scope :: TyCoVarSet
in_scope acc :: ([Var], TyCoVarSet)
acc = KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCo (AxiomRuleCo _ cs :: [KindCoercion]
cs) fv_cand :: InterestingVarFun
fv_cand in_scope :: TyCoVarSet
in_scope acc :: ([Var], TyCoVarSet)
acc = [KindCoercion] -> FV
tyCoFVsOfCos [KindCoercion]
cs InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCoVar :: CoVar -> FV
tyCoFVsOfCoVar :: Var -> FV
tyCoFVsOfCoVar v :: Var
v fv_cand :: InterestingVarFun
fv_cand in_scope :: TyCoVarSet
in_scope acc :: ([Var], TyCoVarSet)
acc
= (Var -> FV
unitFV Var
v FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType (Var -> Type
varType Var
v)) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfProv :: UnivCoProvenance -> FV
tyCoFVsOfProv :: UnivCoProvenance -> FV
tyCoFVsOfProv UnsafeCoerceProv fv_cand :: InterestingVarFun
fv_cand in_scope :: TyCoVarSet
in_scope acc :: ([Var], TyCoVarSet)
acc = FV
emptyFV InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfProv (PhantomProv co :: KindCoercion
co) fv_cand :: InterestingVarFun
fv_cand in_scope :: TyCoVarSet
in_scope acc :: ([Var], TyCoVarSet)
acc = KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfProv (ProofIrrelProv co :: KindCoercion
co) fv_cand :: InterestingVarFun
fv_cand in_scope :: TyCoVarSet
in_scope acc :: ([Var], TyCoVarSet)
acc = KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfProv (PluginProv _) fv_cand :: InterestingVarFun
fv_cand in_scope :: TyCoVarSet
in_scope acc :: ([Var], TyCoVarSet)
acc = FV
emptyFV InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCos :: [Coercion] -> FV
tyCoFVsOfCos :: [KindCoercion] -> FV
tyCoFVsOfCos [] fv_cand :: InterestingVarFun
fv_cand in_scope :: TyCoVarSet
in_scope acc :: ([Var], TyCoVarSet)
acc = FV
emptyFV InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
tyCoFVsOfCos (co :: KindCoercion
co:cos :: [KindCoercion]
cos) fv_cand :: InterestingVarFun
fv_cand in_scope :: TyCoVarSet
in_scope acc :: ([Var], TyCoVarSet)
acc = (KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co FV -> FV -> FV
`unionFV` [KindCoercion] -> FV
tyCoFVsOfCos [KindCoercion]
cos) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([Var], TyCoVarSet)
acc
getCoVarSet :: FV -> CoVarSet
getCoVarSet :: FV -> TyCoVarSet
getCoVarSet fv :: FV
fv = ([Var], TyCoVarSet) -> TyCoVarSet
forall a b. (a, b) -> b
snd (FV
fv InterestingVarFun
isCoVar TyCoVarSet
emptyVarSet ([], TyCoVarSet
emptyVarSet))
coVarsOfType :: Type -> CoVarSet
coVarsOfType :: Type -> TyCoVarSet
coVarsOfType ty :: Type
ty = FV -> TyCoVarSet
getCoVarSet (Type -> FV
tyCoFVsOfType Type
ty)
coVarsOfTypes :: [Type] -> TyCoVarSet
coVarsOfTypes :: [Type] -> TyCoVarSet
coVarsOfTypes tys :: [Type]
tys = FV -> TyCoVarSet
getCoVarSet ([Type] -> FV
tyCoFVsOfTypes [Type]
tys)
coVarsOfCo :: Coercion -> CoVarSet
coVarsOfCo :: KindCoercion -> TyCoVarSet
coVarsOfCo co :: KindCoercion
co = FV -> TyCoVarSet
getCoVarSet (KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co)
coVarsOfCos :: [Coercion] -> CoVarSet
coVarsOfCos :: [KindCoercion] -> TyCoVarSet
coVarsOfCos cos :: [KindCoercion]
cos = FV -> TyCoVarSet
getCoVarSet ([KindCoercion] -> FV
tyCoFVsOfCos [KindCoercion]
cos)
almostDevoidCoVarOfCo :: CoVar -> Coercion -> Bool
almostDevoidCoVarOfCo :: Var -> KindCoercion -> Bool
almostDevoidCoVarOfCo cv :: Var
cv co :: KindCoercion
co =
KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co Var
cv
almost_devoid_co_var_of_co :: Coercion -> CoVar -> Bool
almost_devoid_co_var_of_co :: KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co (Refl {}) _ = Bool
True
almost_devoid_co_var_of_co (GRefl {}) _ = Bool
True
almost_devoid_co_var_of_co (TyConAppCo _ _ cos :: [KindCoercion]
cos) cv :: Var
cv
= [KindCoercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [KindCoercion]
cos Var
cv
almost_devoid_co_var_of_co (AppCo co :: KindCoercion
co arg :: KindCoercion
arg) cv :: Var
cv
= KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co Var
cv
Bool -> Bool -> Bool
&& KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
arg Var
cv
almost_devoid_co_var_of_co (ForAllCo v :: Var
v kind_co :: KindCoercion
kind_co co :: KindCoercion
co) cv :: Var
cv
= KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
kind_co Var
cv
Bool -> Bool -> Bool
&& (Var
v Var -> InterestingVarFun
forall a. Eq a => a -> a -> Bool
== Var
cv Bool -> Bool -> Bool
|| KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co Var
cv)
almost_devoid_co_var_of_co (FunCo _ co1 :: KindCoercion
co1 co2 :: KindCoercion
co2) cv :: Var
cv
= KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co1 Var
cv
Bool -> Bool -> Bool
&& KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co2 Var
cv
almost_devoid_co_var_of_co (CoVarCo v :: Var
v) cv :: Var
cv = Var
v Var -> InterestingVarFun
forall a. Eq a => a -> a -> Bool
/= Var
cv
almost_devoid_co_var_of_co (HoleCo h :: CoercionHole
h) cv :: Var
cv = (CoercionHole -> Var
coHoleCoVar CoercionHole
h) Var -> InterestingVarFun
forall a. Eq a => a -> a -> Bool
/= Var
cv
almost_devoid_co_var_of_co (AxiomInstCo _ _ cos :: [KindCoercion]
cos) cv :: Var
cv
= [KindCoercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [KindCoercion]
cos Var
cv
almost_devoid_co_var_of_co (UnivCo p :: UnivCoProvenance
p _ t1 :: Type
t1 t2 :: Type
t2) cv :: Var
cv
= UnivCoProvenance -> InterestingVarFun
almost_devoid_co_var_of_prov UnivCoProvenance
p Var
cv
Bool -> Bool -> Bool
&& Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
t1 Var
cv
Bool -> Bool -> Bool
&& Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
t2 Var
cv
almost_devoid_co_var_of_co (SymCo co :: KindCoercion
co) cv :: Var
cv
= KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co Var
cv
almost_devoid_co_var_of_co (TransCo co1 :: KindCoercion
co1 co2 :: KindCoercion
co2) cv :: Var
cv
= KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co1 Var
cv
Bool -> Bool -> Bool
&& KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co2 Var
cv
almost_devoid_co_var_of_co (NthCo _ _ co :: KindCoercion
co) cv :: Var
cv
= KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co Var
cv
almost_devoid_co_var_of_co (LRCo _ co :: KindCoercion
co) cv :: Var
cv
= KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co Var
cv
almost_devoid_co_var_of_co (InstCo co :: KindCoercion
co arg :: KindCoercion
arg) cv :: Var
cv
= KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co Var
cv
Bool -> Bool -> Bool
&& KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
arg Var
cv
almost_devoid_co_var_of_co (KindCo co :: KindCoercion
co) cv :: Var
cv
= KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co Var
cv
almost_devoid_co_var_of_co (SubCo co :: KindCoercion
co) cv :: Var
cv
= KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co Var
cv
almost_devoid_co_var_of_co (AxiomRuleCo _ cs :: [KindCoercion]
cs) cv :: Var
cv
= [KindCoercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [KindCoercion]
cs Var
cv
almost_devoid_co_var_of_cos :: [Coercion] -> CoVar -> Bool
almost_devoid_co_var_of_cos :: [KindCoercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [] _ = Bool
True
almost_devoid_co_var_of_cos (co :: KindCoercion
co:cos :: [KindCoercion]
cos) cv :: Var
cv
= KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co Var
cv
Bool -> Bool -> Bool
&& [KindCoercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [KindCoercion]
cos Var
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 co :: KindCoercion
co) cv :: Var
cv
= KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co Var
cv
almost_devoid_co_var_of_prov (ProofIrrelProv co :: KindCoercion
co) cv :: Var
cv
= KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co Var
cv
almost_devoid_co_var_of_prov UnsafeCoerceProv _ = Bool
True
almost_devoid_co_var_of_prov (PluginProv _) _ = 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 _) _ = Bool
True
almost_devoid_co_var_of_type (TyConApp _ tys :: [Type]
tys) cv :: Var
cv
= [Type] -> InterestingVarFun
almost_devoid_co_var_of_types [Type]
tys Var
cv
almost_devoid_co_var_of_type (LitTy {}) _ = Bool
True
almost_devoid_co_var_of_type (AppTy fun :: Type
fun arg :: Type
arg) cv :: Var
cv
= Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
fun Var
cv
Bool -> Bool -> Bool
&& Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
arg Var
cv
almost_devoid_co_var_of_type (FunTy _ arg :: Type
arg res :: Type
res) cv :: Var
cv
= Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
arg Var
cv
Bool -> Bool -> Bool
&& Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
res Var
cv
almost_devoid_co_var_of_type (ForAllTy (Bndr v :: Var
v _) ty :: Type
ty) cv :: Var
cv
= Type -> InterestingVarFun
almost_devoid_co_var_of_type (Var -> Type
varType Var
v) Var
cv
Bool -> Bool -> Bool
&& (Var
v Var -> InterestingVarFun
forall a. Eq a => a -> a -> Bool
== Var
cv Bool -> Bool -> Bool
|| Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
ty Var
cv)
almost_devoid_co_var_of_type (CastTy ty :: Type
ty co :: KindCoercion
co) cv :: Var
cv
= Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
ty Var
cv
Bool -> Bool -> Bool
&& KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co Var
cv
almost_devoid_co_var_of_type (CoercionTy co :: KindCoercion
co) cv :: Var
cv
= KindCoercion -> InterestingVarFun
almost_devoid_co_var_of_co KindCoercion
co Var
cv
almost_devoid_co_var_of_types :: [Type] -> CoVar -> Bool
almost_devoid_co_var_of_types :: [Type] -> InterestingVarFun
almost_devoid_co_var_of_types [] _ = Bool
True
almost_devoid_co_var_of_types (ty :: Type
ty:tys :: [Type]
tys) cv :: Var
cv
= Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
ty Var
cv
Bool -> Bool -> Bool
&& [Type] -> InterestingVarFun
almost_devoid_co_var_of_types [Type]
tys Var
cv
injectiveVarsOfType :: Bool
-> Type -> FV
injectiveVarsOfType :: Bool -> Type -> FV
injectiveVarsOfType look_under_tfs :: Bool
look_under_tfs = Type -> FV
go
where
go :: Type -> FV
go ty :: Type
ty | Just ty' :: Type
ty' <- Type -> Maybe Type
coreView Type
ty
= Type -> FV
go Type
ty'
go (TyVarTy v :: Var
v) = Var -> FV
unitFV Var
v FV -> FV -> FV
`unionFV` Type -> FV
go (Var -> Type
tyVarKind Var
v)
go (AppTy f :: Type
f a :: Type
a) = Type -> FV
go Type
f FV -> FV -> FV
`unionFV` Type -> FV
go Type
a
go (FunTy _ ty1 :: Type
ty1 ty2 :: Type
ty2) = Type -> FV
go Type
ty1 FV -> FV -> FV
`unionFV` Type -> FV
go Type
ty2
go (TyConApp tc :: TyCon
tc tys :: [Type]
tys) =
case TyCon -> Injectivity
tyConInjectivityInfo TyCon
tc of
Injective inj :: [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
_ -> FV
emptyFV
go (ForAllTy (Bndr tv :: Var
tv _) ty :: Type
ty) = Type -> FV
go (Var -> Type
tyVarKind Var
tv) FV -> FV -> FV
`unionFV` Var -> FV -> FV
delFV Var
tv (Type -> FV
go Type
ty)
go LitTy{} = FV
emptyFV
go (CastTy ty :: Type
ty _) = Type -> FV
go Type
ty
go CoercionTy{} = FV
emptyFV
injectiveVarsOfTypes :: Bool
-> [Type] -> FV
injectiveVarsOfTypes :: Bool -> [Type] -> FV
injectiveVarsOfTypes look_under_tfs :: 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 ty :: Type
ty | Just ty' :: Type
ty' <- Type -> Maybe Type
coreView Type
ty
= Type -> FV
go Type
ty'
go (TyVarTy v :: Var
v) = Type -> FV
go (Var -> Type
tyVarKind Var
v)
go (AppTy f :: Type
f a :: Type
a) = Type -> FV
go Type
f FV -> FV -> FV
`unionFV` Type -> FV
go Type
a
go (FunTy _ ty1 :: Type
ty1 ty2 :: Type
ty2) = Type -> FV
go Type
ty1 FV -> FV -> FV
`unionFV` Type -> FV
go Type
ty2
go (TyConApp tc :: TyCon
tc tys :: [Type]
tys) = [Type] -> FV
tyCoFVsOfTypes [Type]
invisibles FV -> FV -> FV
`unionFV`
[Type] -> FV
invisibleVarsOfTypes [Type]
visibles
where (invisibles :: [Type]
invisibles, visibles :: [Type]
visibles) = TyCon -> [Type] -> ([Type], [Type])
partitionInvisibleTypes TyCon
tc [Type]
tys
go (ForAllTy tvb :: VarBndr Var ArgFlag
tvb ty :: Type
ty) = VarBndr Var ArgFlag -> FV -> FV
tyCoFVsBndr VarBndr Var ArgFlag
tvb (FV -> FV) -> FV -> FV
forall a b. (a -> b) -> a -> b
$ Type -> FV
go Type
ty
go LitTy{} = FV
emptyFV
go (CastTy ty :: Type
ty co :: KindCoercion
co) = KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co FV -> FV -> FV
`unionFV` Type -> FV
go Type
ty
go (CoercionTy co :: KindCoercion
co) = KindCoercion -> FV
tyCoFVsOfCo KindCoercion
co
invisibleVarsOfTypes :: [Type] -> FV
invisibleVarsOfTypes :: [Type] -> FV
invisibleVarsOfTypes = (Type -> FV) -> [Type] -> FV
forall a. (a -> FV) -> [a] -> FV
mapUnionFV Type -> FV
invisibleVarsOfType
noFreeVarsOfType :: Type -> Bool
noFreeVarsOfType :: Type -> Bool
noFreeVarsOfType (TyVarTy _) = Bool
False
noFreeVarsOfType (AppTy t1 :: Type
t1 t2 :: Type
t2) = Type -> Bool
noFreeVarsOfType Type
t1 Bool -> Bool -> Bool
&& Type -> Bool
noFreeVarsOfType Type
t2
noFreeVarsOfType (TyConApp _ tys :: [Type]
tys) = (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
noFreeVarsOfType [Type]
tys
noFreeVarsOfType ty :: Type
ty@(ForAllTy {}) = TyCoVarSet -> Bool
isEmptyVarSet (Type -> TyCoVarSet
tyCoVarsOfType Type
ty)
noFreeVarsOfType (FunTy _ t1 :: Type
t1 t2 :: Type
t2) = Type -> Bool
noFreeVarsOfType Type
t1 Bool -> Bool -> Bool
&& Type -> Bool
noFreeVarsOfType Type
t2
noFreeVarsOfType (LitTy _) = Bool
True
noFreeVarsOfType (CastTy ty :: Type
ty co :: KindCoercion
co) = Type -> Bool
noFreeVarsOfType Type
ty Bool -> Bool -> Bool
&& KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co
noFreeVarsOfType (CoercionTy co :: KindCoercion
co) = KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co
noFreeVarsOfMCo :: MCoercion -> Bool
noFreeVarsOfMCo :: MCoercionN -> Bool
noFreeVarsOfMCo MRefl = Bool
True
noFreeVarsOfMCo (MCo co :: KindCoercion
co) = KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co
noFreeVarsOfTypes :: [Type] -> Bool
noFreeVarsOfTypes :: [Type] -> Bool
noFreeVarsOfTypes = (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
noFreeVarsOfType
noFreeVarsOfCo :: Coercion -> Bool
noFreeVarsOfCo :: KindCoercion -> Bool
noFreeVarsOfCo (Refl ty :: Type
ty) = Type -> Bool
noFreeVarsOfType Type
ty
noFreeVarsOfCo (GRefl _ ty :: Type
ty co :: MCoercionN
co) = Type -> Bool
noFreeVarsOfType Type
ty Bool -> Bool -> Bool
&& MCoercionN -> Bool
noFreeVarsOfMCo MCoercionN
co
noFreeVarsOfCo (TyConAppCo _ _ args :: [KindCoercion]
args) = (KindCoercion -> Bool) -> [KindCoercion] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all KindCoercion -> Bool
noFreeVarsOfCo [KindCoercion]
args
noFreeVarsOfCo (AppCo c1 :: KindCoercion
c1 c2 :: KindCoercion
c2) = KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
c1 Bool -> Bool -> Bool
&& KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
c2
noFreeVarsOfCo co :: KindCoercion
co@(ForAllCo {}) = TyCoVarSet -> Bool
isEmptyVarSet (KindCoercion -> TyCoVarSet
tyCoVarsOfCo KindCoercion
co)
noFreeVarsOfCo (FunCo _ c1 :: KindCoercion
c1 c2 :: KindCoercion
c2) = KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
c1 Bool -> Bool -> Bool
&& KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
c2
noFreeVarsOfCo (CoVarCo _) = Bool
False
noFreeVarsOfCo (HoleCo {}) = Bool
True
noFreeVarsOfCo (AxiomInstCo _ _ args :: [KindCoercion]
args) = (KindCoercion -> Bool) -> [KindCoercion] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all KindCoercion -> Bool
noFreeVarsOfCo [KindCoercion]
args
noFreeVarsOfCo (UnivCo p :: UnivCoProvenance
p _ t1 :: Type
t1 t2 :: Type
t2) = UnivCoProvenance -> Bool
noFreeVarsOfProv UnivCoProvenance
p Bool -> Bool -> Bool
&&
Type -> Bool
noFreeVarsOfType Type
t1 Bool -> Bool -> Bool
&&
Type -> Bool
noFreeVarsOfType Type
t2
noFreeVarsOfCo (SymCo co :: KindCoercion
co) = KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co
noFreeVarsOfCo (TransCo co1 :: KindCoercion
co1 co2 :: KindCoercion
co2) = KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co1 Bool -> Bool -> Bool
&& KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co2
noFreeVarsOfCo (NthCo _ _ co :: KindCoercion
co) = KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co
noFreeVarsOfCo (LRCo _ co :: KindCoercion
co) = KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co
noFreeVarsOfCo (InstCo co1 :: KindCoercion
co1 co2 :: KindCoercion
co2) = KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co1 Bool -> Bool -> Bool
&& KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co2
noFreeVarsOfCo (KindCo co :: KindCoercion
co) = KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co
noFreeVarsOfCo (SubCo co :: KindCoercion
co) = KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co
noFreeVarsOfCo (AxiomRuleCo _ cs :: [KindCoercion]
cs) = (KindCoercion -> Bool) -> [KindCoercion] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all KindCoercion -> Bool
noFreeVarsOfCo [KindCoercion]
cs
noFreeVarsOfProv :: UnivCoProvenance -> Bool
noFreeVarsOfProv :: UnivCoProvenance -> Bool
noFreeVarsOfProv UnsafeCoerceProv = Bool
True
noFreeVarsOfProv (PhantomProv co :: KindCoercion
co) = KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co
noFreeVarsOfProv (ProofIrrelProv co :: KindCoercion
co) = KindCoercion -> Bool
noFreeVarsOfCo KindCoercion
co
noFreeVarsOfProv (PluginProv {}) = Bool
True
scopedSort :: [TyCoVar] -> [TyCoVar]
scopedSort :: [Var] -> [Var]
scopedSort = [Var] -> [TyCoVarSet] -> [Var] -> [Var]
go [] []
where
go :: [TyCoVar]
-> [TyCoVarSet]
-> [TyCoVar]
-> [TyCoVar]
go :: [Var] -> [TyCoVarSet] -> [Var] -> [Var]
go acc :: [Var]
acc _fv_list :: [TyCoVarSet]
_fv_list [] = [Var] -> [Var]
forall a. [a] -> [a]
reverse [Var]
acc
go acc :: [Var]
acc fv_list :: [TyCoVarSet]
fv_list (tv :: Var
tv:tvs :: [Var]
tvs)
= [Var] -> [TyCoVarSet] -> [Var] -> [Var]
go [Var]
acc' [TyCoVarSet]
fv_list' [Var]
tvs
where
(acc' :: [Var]
acc', fv_list' :: [TyCoVarSet]
fv_list') = Var -> [Var] -> [TyCoVarSet] -> ([Var], [TyCoVarSet])
insert Var
tv [Var]
acc [TyCoVarSet]
fv_list
insert :: TyCoVar
-> [TyCoVar]
-> [TyCoVarSet]
-> ([TyCoVar], [TyCoVarSet])
insert :: Var -> [Var] -> [TyCoVarSet] -> ([Var], [TyCoVarSet])
insert tv :: Var
tv [] [] = ([Var
tv], [Type -> TyCoVarSet
tyCoVarsOfType (Var -> Type
tyVarKind Var
tv)])
insert tv :: Var
tv (a :: Var
a:as :: [Var]
as) (fvs :: TyCoVarSet
fvs:fvss :: [TyCoVarSet]
fvss)
| Var
tv Var -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
fvs
, (as' :: [Var]
as', fvss' :: [TyCoVarSet]
fvss') <- Var -> [Var] -> [TyCoVarSet] -> ([Var], [TyCoVarSet])
insert Var
tv [Var]
as [TyCoVarSet]
fvss
= (Var
aVar -> [Var] -> [Var]
forall a. a -> [a] -> [a]
:[Var]
as', TyCoVarSet
fvs TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` TyCoVarSet
fv_tv TyCoVarSet -> [TyCoVarSet] -> [TyCoVarSet]
forall a. a -> [a] -> [a]
: [TyCoVarSet]
fvss')
| Bool
otherwise
= (Var
tvVar -> [Var] -> [Var]
forall a. a -> [a] -> [a]
:Var
aVar -> [Var] -> [Var]
forall a. a -> [a] -> [a]
:[Var]
as, TyCoVarSet
fvs TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` TyCoVarSet
fv_tv TyCoVarSet -> [TyCoVarSet] -> [TyCoVarSet]
forall a. a -> [a] -> [a]
: TyCoVarSet
fvs TyCoVarSet -> [TyCoVarSet] -> [TyCoVarSet]
forall a. a -> [a] -> [a]
: [TyCoVarSet]
fvss)
where
fv_tv :: TyCoVarSet
fv_tv = Type -> TyCoVarSet
tyCoVarsOfType (Var -> Type
tyVarKind Var
tv)
insert _ _ _ = String -> ([Var], [TyCoVarSet])
forall a. String -> a
panic "scopedSort"
tyCoVarsOfTypeWellScoped :: Type -> [TyVar]
tyCoVarsOfTypeWellScoped :: Type -> [Var]
tyCoVarsOfTypeWellScoped = [Var] -> [Var]
scopedSort ([Var] -> [Var]) -> (Type -> [Var]) -> Type -> [Var]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [Var]
tyCoVarsOfTypeList
tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
tyCoVarsOfTypesWellScoped :: [Type] -> [Var]
tyCoVarsOfTypesWellScoped = [Var] -> [Var]
scopedSort ([Var] -> [Var]) -> ([Type] -> [Var]) -> [Type] -> [Var]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Type] -> [Var]
tyCoVarsOfTypesList