{-# LANGUAGE CPP #-}
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,
coVarsOfType, coVarsOfTypes,
coVarsOfCo, coVarsOfCos,
tyCoVarsOfCoDSet,
tyCoFVsOfCo, tyCoFVsOfCos,
tyCoVarsOfCoList,
almostDevoidCoVarOfCo,
injectiveVarsOfType, injectiveVarsOfTypes,
invisibleVarsOfType, invisibleVarsOfTypes,
noFreeVarsOfType, noFreeVarsOfTypes, noFreeVarsOfCo,
scopedSort, tyCoVarsOfTypeWellScoped,
tyCoVarsOfTypesWellScoped,
closeOverKindsDSet, closeOverKindsList,
closeOverKinds,
Endo(..), runTyCoVars
) where
#include "GhclibHsVersions.h"
import GHC.Prelude
import {-# SOURCE #-} GHC.Core.Type (coreView, partitionInvisibleTypes)
import Data.Monoid as DM ( Endo(..), All(..) )
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 TyCoVarSet -> TyCoVarSet
runTyCoVars Endo TyCoVarSet
f = Endo TyCoVarSet -> TyCoVarSet -> TyCoVarSet
forall a. Endo a -> a -> a
appEndo Endo TyCoVarSet
f TyCoVarSet
emptyVarSet
noView :: Type -> Maybe Type
noView :: Type -> Maybe Type
noView Type
_ = Maybe Type
forall a. Maybe a
Nothing
tyCoVarsOfType :: Type -> TyCoVarSet
tyCoVarsOfType :: Type -> TyCoVarSet
tyCoVarsOfType Type
ty = Endo TyCoVarSet -> TyCoVarSet
runTyCoVars (Type -> Endo TyCoVarSet
deep_ty Type
ty)
tyCoVarsOfTypes :: [Type] -> TyCoVarSet
tyCoVarsOfTypes :: [Type] -> TyCoVarSet
tyCoVarsOfTypes [Type]
tys = Endo TyCoVarSet -> TyCoVarSet
runTyCoVars ([Type] -> Endo TyCoVarSet
deep_tys [Type]
tys)
tyCoVarsOfCo :: Coercion -> TyCoVarSet
tyCoVarsOfCo :: Coercion -> TyCoVarSet
tyCoVarsOfCo Coercion
co = Endo TyCoVarSet -> TyCoVarSet
runTyCoVars (Coercion -> Endo TyCoVarSet
deep_co Coercion
co)
tyCoVarsOfCos :: [Coercion] -> TyCoVarSet
tyCoVarsOfCos :: [Coercion] -> TyCoVarSet
tyCoVarsOfCos [Coercion]
cos = Endo TyCoVarSet -> TyCoVarSet
runTyCoVars ([Coercion] -> Endo TyCoVarSet
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 TyCoVarSet
deep_ty, [Type] -> Endo TyCoVarSet
deep_tys, Coercion -> Endo TyCoVarSet
deep_co, [Coercion] -> Endo TyCoVarSet
deep_cos) = TyCoFolder TyCoVarSet (Endo TyCoVarSet)
-> TyCoVarSet
-> (Type -> Endo TyCoVarSet, [Type] -> Endo TyCoVarSet,
Coercion -> Endo TyCoVarSet, [Coercion] -> Endo TyCoVarSet)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo TyCoFolder TyCoVarSet (Endo TyCoVarSet)
deepTcvFolder TyCoVarSet
emptyVarSet
deepTcvFolder :: TyCoFolder TyCoVarSet (Endo TyCoVarSet)
deepTcvFolder :: TyCoFolder TyCoVarSet (Endo TyCoVarSet)
deepTcvFolder = TyCoFolder :: forall env a.
(Type -> Maybe Type)
-> (env -> TyVar -> a)
-> (env -> TyVar -> a)
-> (env -> CoercionHole -> a)
-> (env -> TyVar -> ArgFlag -> env)
-> TyCoFolder env a
TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view = Type -> Maybe Type
noView
, tcf_tyvar :: TyCoVarSet -> TyVar -> Endo TyCoVarSet
tcf_tyvar = TyCoVarSet -> TyVar -> Endo TyCoVarSet
do_tcv, tcf_covar :: TyCoVarSet -> TyVar -> Endo TyCoVarSet
tcf_covar = TyCoVarSet -> TyVar -> Endo TyCoVarSet
do_tcv
, tcf_hole :: TyCoVarSet -> CoercionHole -> Endo TyCoVarSet
tcf_hole = TyCoVarSet -> CoercionHole -> Endo TyCoVarSet
do_hole, tcf_tycobinder :: TyCoVarSet -> TyVar -> ArgFlag -> TyCoVarSet
tcf_tycobinder = TyCoVarSet -> TyVar -> ArgFlag -> TyCoVarSet
forall p. TyCoVarSet -> TyVar -> p -> TyCoVarSet
do_bndr }
where
do_tcv :: TyCoVarSet -> TyVar -> Endo TyCoVarSet
do_tcv TyCoVarSet
is TyVar
v = (TyCoVarSet -> TyCoVarSet) -> Endo TyCoVarSet
forall a. (a -> a) -> Endo a
Endo TyCoVarSet -> TyCoVarSet
do_it
where
do_it :: TyCoVarSet -> TyCoVarSet
do_it TyCoVarSet
acc | TyVar
v TyVar -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
is = TyCoVarSet
acc
| TyVar
v TyVar -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
acc = TyCoVarSet
acc
| Bool
otherwise = Endo TyCoVarSet -> TyCoVarSet -> TyCoVarSet
forall a. Endo a -> a -> a
appEndo (Type -> Endo TyCoVarSet
deep_ty (TyVar -> Type
varType TyVar
v)) (TyCoVarSet -> TyCoVarSet) -> TyCoVarSet -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$
TyCoVarSet
acc TyCoVarSet -> TyVar -> TyCoVarSet
`extendVarSet` TyVar
v
do_bndr :: TyCoVarSet -> TyVar -> p -> TyCoVarSet
do_bndr TyCoVarSet
is TyVar
tcv p
_ = TyCoVarSet -> TyVar -> TyCoVarSet
extendVarSet TyCoVarSet
is TyVar
tcv
do_hole :: TyCoVarSet -> CoercionHole -> Endo TyCoVarSet
do_hole TyCoVarSet
is CoercionHole
hole = TyCoVarSet -> TyVar -> Endo TyCoVarSet
do_tcv TyCoVarSet
is (CoercionHole -> TyVar
coHoleCoVar CoercionHole
hole)
shallowTyCoVarsOfType :: Type -> TyCoVarSet
shallowTyCoVarsOfType :: Type -> TyCoVarSet
shallowTyCoVarsOfType Type
ty = Endo TyCoVarSet -> TyCoVarSet
runTyCoVars (Type -> Endo TyCoVarSet
shallow_ty Type
ty)
shallowTyCoVarsOfTypes :: [Type] -> TyCoVarSet
shallowTyCoVarsOfTypes :: [Type] -> TyCoVarSet
shallowTyCoVarsOfTypes [Type]
tys = Endo TyCoVarSet -> TyCoVarSet
runTyCoVars ([Type] -> Endo TyCoVarSet
shallow_tys [Type]
tys)
shallowTyCoVarsOfCo :: Coercion -> TyCoVarSet
shallowTyCoVarsOfCo :: Coercion -> TyCoVarSet
shallowTyCoVarsOfCo Coercion
co = Endo TyCoVarSet -> TyCoVarSet
runTyCoVars (Coercion -> Endo TyCoVarSet
shallow_co Coercion
co)
shallowTyCoVarsOfCos :: [Coercion] -> TyCoVarSet
shallowTyCoVarsOfCos :: [Coercion] -> TyCoVarSet
shallowTyCoVarsOfCos [Coercion]
cos = Endo TyCoVarSet -> TyCoVarSet
runTyCoVars ([Coercion] -> Endo TyCoVarSet
shallow_cos [Coercion]
cos)
shallowTyCoVarsOfTyVarEnv :: TyVarEnv Type -> TyCoVarSet
shallowTyCoVarsOfTyVarEnv :: TyVarEnv Type -> TyCoVarSet
shallowTyCoVarsOfTyVarEnv TyVarEnv Type
tys = [Type] -> TyCoVarSet
shallowTyCoVarsOfTypes (TyVarEnv Type -> [Type]
forall key elt. UniqFM key elt -> [elt]
nonDetEltsUFM TyVarEnv Type
tys)
shallowTyCoVarsOfCoVarEnv :: CoVarEnv Coercion -> TyCoVarSet
shallowTyCoVarsOfCoVarEnv :: CoVarEnv Coercion -> TyCoVarSet
shallowTyCoVarsOfCoVarEnv CoVarEnv Coercion
cos = [Coercion] -> TyCoVarSet
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 TyCoVarSet
shallow_ty, [Type] -> Endo TyCoVarSet
shallow_tys, Coercion -> Endo TyCoVarSet
shallow_co, [Coercion] -> Endo TyCoVarSet
shallow_cos) = TyCoFolder TyCoVarSet (Endo TyCoVarSet)
-> TyCoVarSet
-> (Type -> Endo TyCoVarSet, [Type] -> Endo TyCoVarSet,
Coercion -> Endo TyCoVarSet, [Coercion] -> Endo TyCoVarSet)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo TyCoFolder TyCoVarSet (Endo TyCoVarSet)
shallowTcvFolder TyCoVarSet
emptyVarSet
shallowTcvFolder :: TyCoFolder TyCoVarSet (Endo TyCoVarSet)
shallowTcvFolder :: TyCoFolder TyCoVarSet (Endo TyCoVarSet)
shallowTcvFolder = TyCoFolder :: forall env a.
(Type -> Maybe Type)
-> (env -> TyVar -> a)
-> (env -> TyVar -> a)
-> (env -> CoercionHole -> a)
-> (env -> TyVar -> ArgFlag -> env)
-> TyCoFolder env a
TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view = Type -> Maybe Type
noView
, tcf_tyvar :: TyCoVarSet -> TyVar -> Endo TyCoVarSet
tcf_tyvar = TyCoVarSet -> TyVar -> Endo TyCoVarSet
do_tcv, tcf_covar :: TyCoVarSet -> TyVar -> Endo TyCoVarSet
tcf_covar = TyCoVarSet -> TyVar -> Endo TyCoVarSet
do_tcv
, tcf_hole :: TyCoVarSet -> CoercionHole -> Endo TyCoVarSet
tcf_hole = TyCoVarSet -> CoercionHole -> Endo TyCoVarSet
forall a p p. Monoid a => p -> p -> a
do_hole, tcf_tycobinder :: TyCoVarSet -> TyVar -> ArgFlag -> TyCoVarSet
tcf_tycobinder = TyCoVarSet -> TyVar -> ArgFlag -> TyCoVarSet
forall p. TyCoVarSet -> TyVar -> p -> TyCoVarSet
do_bndr }
where
do_tcv :: TyCoVarSet -> TyVar -> Endo TyCoVarSet
do_tcv TyCoVarSet
is TyVar
v = (TyCoVarSet -> TyCoVarSet) -> Endo TyCoVarSet
forall a. (a -> a) -> Endo a
Endo TyCoVarSet -> TyCoVarSet
do_it
where
do_it :: TyCoVarSet -> TyCoVarSet
do_it TyCoVarSet
acc | TyVar
v TyVar -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
is = TyCoVarSet
acc
| TyVar
v TyVar -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
acc = TyCoVarSet
acc
| Bool
otherwise = TyCoVarSet
acc TyCoVarSet -> TyVar -> TyCoVarSet
`extendVarSet` TyVar
v
do_bndr :: TyCoVarSet -> TyVar -> p -> TyCoVarSet
do_bndr TyCoVarSet
is TyVar
tcv p
_ = TyCoVarSet -> TyVar -> TyCoVarSet
extendVarSet TyCoVarSet
is TyVar
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 -> TyCoVarSet
coVarsOfType Type
ty = Endo TyCoVarSet -> TyCoVarSet
runTyCoVars (Type -> Endo TyCoVarSet
deep_cv_ty Type
ty)
coVarsOfTypes :: [Type] -> TyCoVarSet
coVarsOfTypes [Type]
tys = Endo TyCoVarSet -> TyCoVarSet
runTyCoVars ([Type] -> Endo TyCoVarSet
deep_cv_tys [Type]
tys)
coVarsOfCo :: Coercion -> TyCoVarSet
coVarsOfCo Coercion
co = Endo TyCoVarSet -> TyCoVarSet
runTyCoVars (Coercion -> Endo TyCoVarSet
deep_cv_co Coercion
co)
coVarsOfCos :: [Coercion] -> TyCoVarSet
coVarsOfCos [Coercion]
cos = Endo TyCoVarSet -> TyCoVarSet
runTyCoVars ([Coercion] -> Endo TyCoVarSet
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 TyCoVarSet
deep_cv_ty, [Type] -> Endo TyCoVarSet
deep_cv_tys, Coercion -> Endo TyCoVarSet
deep_cv_co, [Coercion] -> Endo TyCoVarSet
deep_cv_cos) = TyCoFolder TyCoVarSet (Endo TyCoVarSet)
-> TyCoVarSet
-> (Type -> Endo TyCoVarSet, [Type] -> Endo TyCoVarSet,
Coercion -> Endo TyCoVarSet, [Coercion] -> Endo TyCoVarSet)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo TyCoFolder TyCoVarSet (Endo TyCoVarSet)
deepCoVarFolder TyCoVarSet
emptyVarSet
deepCoVarFolder :: TyCoFolder TyCoVarSet (Endo CoVarSet)
deepCoVarFolder :: TyCoFolder TyCoVarSet (Endo TyCoVarSet)
deepCoVarFolder = TyCoFolder :: forall env a.
(Type -> Maybe Type)
-> (env -> TyVar -> a)
-> (env -> TyVar -> a)
-> (env -> CoercionHole -> a)
-> (env -> TyVar -> ArgFlag -> env)
-> TyCoFolder env a
TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view = Type -> Maybe Type
noView
, tcf_tyvar :: TyCoVarSet -> TyVar -> Endo TyCoVarSet
tcf_tyvar = TyCoVarSet -> TyVar -> Endo TyCoVarSet
forall a p p. Monoid a => p -> p -> a
do_tyvar, tcf_covar :: TyCoVarSet -> TyVar -> Endo TyCoVarSet
tcf_covar = TyCoVarSet -> TyVar -> Endo TyCoVarSet
do_covar
, tcf_hole :: TyCoVarSet -> CoercionHole -> Endo TyCoVarSet
tcf_hole = TyCoVarSet -> CoercionHole -> Endo TyCoVarSet
do_hole, tcf_tycobinder :: TyCoVarSet -> TyVar -> ArgFlag -> TyCoVarSet
tcf_tycobinder = TyCoVarSet -> TyVar -> ArgFlag -> TyCoVarSet
forall p. TyCoVarSet -> TyVar -> p -> TyCoVarSet
do_bndr }
where
do_tyvar :: p -> p -> a
do_tyvar p
_ p
_ = a
forall a. Monoid a => a
mempty
do_covar :: TyCoVarSet -> TyVar -> Endo TyCoVarSet
do_covar TyCoVarSet
is TyVar
v = (TyCoVarSet -> TyCoVarSet) -> Endo TyCoVarSet
forall a. (a -> a) -> Endo a
Endo TyCoVarSet -> TyCoVarSet
do_it
where
do_it :: TyCoVarSet -> TyCoVarSet
do_it TyCoVarSet
acc | TyVar
v TyVar -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
is = TyCoVarSet
acc
| TyVar
v TyVar -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
acc = TyCoVarSet
acc
| Bool
otherwise = Endo TyCoVarSet -> TyCoVarSet -> TyCoVarSet
forall a. Endo a -> a -> a
appEndo (Type -> Endo TyCoVarSet
deep_cv_ty (TyVar -> Type
varType TyVar
v)) (TyCoVarSet -> TyCoVarSet) -> TyCoVarSet -> TyCoVarSet
forall a b. (a -> b) -> a -> b
$
TyCoVarSet
acc TyCoVarSet -> TyVar -> TyCoVarSet
`extendVarSet` TyVar
v
do_bndr :: TyCoVarSet -> TyVar -> p -> TyCoVarSet
do_bndr TyCoVarSet
is TyVar
tcv p
_ = TyCoVarSet -> TyVar -> TyCoVarSet
extendVarSet TyCoVarSet
is TyVar
tcv
do_hole :: TyCoVarSet -> CoercionHole -> Endo TyCoVarSet
do_hole TyCoVarSet
is CoercionHole
hole = TyCoVarSet -> TyVar -> Endo TyCoVarSet
do_covar TyCoVarSet
is (CoercionHole -> TyVar
coHoleCoVar CoercionHole
hole)
closeOverKinds :: TyCoVarSet -> TyCoVarSet
closeOverKinds :: TyCoVarSet -> TyCoVarSet
closeOverKinds TyCoVarSet
vs = (TyVar -> TyCoVarSet -> TyCoVarSet)
-> TyCoVarSet -> TyCoVarSet -> TyCoVarSet
forall a. (TyVar -> a -> a) -> a -> TyCoVarSet -> a
nonDetStrictFoldVarSet TyVar -> TyCoVarSet -> TyCoVarSet
do_one TyCoVarSet
vs TyCoVarSet
vs
where
do_one :: TyVar -> TyCoVarSet -> TyCoVarSet
do_one TyVar
v TyCoVarSet
acc = Endo TyCoVarSet -> TyCoVarSet -> TyCoVarSet
forall a. Endo a -> a -> a
appEndo (Type -> Endo TyCoVarSet
deep_ty (TyVar -> Type
varType TyVar
v)) TyCoVarSet
acc
closeOverKindsFV :: [TyVar] -> FV
closeOverKindsFV :: [TyVar] -> FV
closeOverKindsFV [TyVar]
tvs =
(TyVar -> FV) -> [TyVar] -> FV
forall a. (a -> FV) -> [a] -> FV
mapUnionFV (Type -> FV
tyCoFVsOfType (Type -> FV) -> (TyVar -> Type) -> TyVar -> FV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> Type
tyVarKind) [TyVar]
tvs FV -> FV -> FV
`unionFV` [TyVar] -> FV
mkFVs [TyVar]
tvs
closeOverKindsList :: [TyVar] -> [TyVar]
closeOverKindsList :: [TyVar] -> [TyVar]
closeOverKindsList [TyVar]
tvs = FV -> [TyVar]
fvVarList (FV -> [TyVar]) -> FV -> [TyVar]
forall a b. (a -> b) -> a -> b
$ [TyVar] -> FV
closeOverKindsFV [TyVar]
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
. [TyVar] -> FV
closeOverKindsFV ([TyVar] -> FV) -> (DTyVarSet -> [TyVar]) -> DTyVarSet -> FV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DTyVarSet -> [TyVar]
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 -> [TyVar]
tyCoVarsOfTypeList Type
ty = FV -> [TyVar]
fvVarList (FV -> [TyVar]) -> FV -> [TyVar]
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] -> [TyVar]
tyCoVarsOfTypesList [Type]
tys = FV -> [TyVar]
fvVarList (FV -> [TyVar]) -> FV -> [TyVar]
forall a b. (a -> b) -> a -> b
$ [Type] -> FV
tyCoFVsOfTypes [Type]
tys
tyCoFVsOfType :: Type -> FV
tyCoFVsOfType :: Type -> FV
tyCoFVsOfType (TyVarTy TyVar
v) InterestingVarFun
f TyCoVarSet
bound_vars ([TyVar]
acc_list, TyCoVarSet
acc_set)
| Bool -> Bool
not (InterestingVarFun
f TyVar
v) = ([TyVar]
acc_list, TyCoVarSet
acc_set)
| TyVar
v TyVar -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
bound_vars = ([TyVar]
acc_list, TyCoVarSet
acc_set)
| TyVar
v TyVar -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
acc_set = ([TyVar]
acc_list, TyCoVarSet
acc_set)
| Bool
otherwise = Type -> FV
tyCoFVsOfType (TyVar -> Type
tyVarKind TyVar
v) InterestingVarFun
f
TyCoVarSet
emptyVarSet
(TyVar
vTyVar -> [TyVar] -> [TyVar]
forall a. a -> [a] -> [a]
:[TyVar]
acc_list, TyCoVarSet -> TyVar -> TyCoVarSet
extendVarSet TyCoVarSet
acc_set TyVar
v)
tyCoFVsOfType (TyConApp TyCon
_ [Type]
tys) InterestingVarFun
f TyCoVarSet
bound_vars ([TyVar], TyCoVarSet)
acc = [Type] -> FV
tyCoFVsOfTypes [Type]
tys InterestingVarFun
f TyCoVarSet
bound_vars ([TyVar], TyCoVarSet)
acc
tyCoFVsOfType (LitTy {}) InterestingVarFun
f TyCoVarSet
bound_vars ([TyVar], TyCoVarSet)
acc = FV
emptyFV InterestingVarFun
f TyCoVarSet
bound_vars ([TyVar], TyCoVarSet)
acc
tyCoFVsOfType (AppTy Type
fun Type
arg) InterestingVarFun
f TyCoVarSet
bound_vars ([TyVar], TyCoVarSet)
acc = (Type -> FV
tyCoFVsOfType Type
fun FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType Type
arg) InterestingVarFun
f TyCoVarSet
bound_vars ([TyVar], TyCoVarSet)
acc
tyCoFVsOfType (FunTy AnonArgFlag
_ Type
w Type
arg Type
res) InterestingVarFun
f TyCoVarSet
bound_vars ([TyVar], TyCoVarSet)
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 TyCoVarSet
bound_vars ([TyVar], TyCoVarSet)
acc
tyCoFVsOfType (ForAllTy TyCoVarBinder
bndr Type
ty) InterestingVarFun
f TyCoVarSet
bound_vars ([TyVar], TyCoVarSet)
acc = TyCoVarBinder -> FV -> FV
tyCoFVsBndr TyCoVarBinder
bndr (Type -> FV
tyCoFVsOfType Type
ty) InterestingVarFun
f TyCoVarSet
bound_vars ([TyVar], TyCoVarSet)
acc
tyCoFVsOfType (CastTy Type
ty Coercion
co) InterestingVarFun
f TyCoVarSet
bound_vars ([TyVar], TyCoVarSet)
acc = (Type -> FV
tyCoFVsOfType Type
ty FV -> FV -> FV
`unionFV` Coercion -> FV
tyCoFVsOfCo Coercion
co) InterestingVarFun
f TyCoVarSet
bound_vars ([TyVar], TyCoVarSet)
acc
tyCoFVsOfType (CoercionTy Coercion
co) InterestingVarFun
f TyCoVarSet
bound_vars ([TyVar], TyCoVarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co InterestingVarFun
f TyCoVarSet
bound_vars ([TyVar], TyCoVarSet)
acc
tyCoFVsBndr :: TyCoVarBinder -> FV -> FV
tyCoFVsBndr :: TyCoVarBinder -> FV -> FV
tyCoFVsBndr (Bndr TyVar
tv ArgFlag
_) FV
fvs = TyVar -> FV -> FV
tyCoFVsVarBndr TyVar
tv FV
fvs
tyCoFVsVarBndrs :: [Var] -> FV -> FV
tyCoFVsVarBndrs :: [TyVar] -> FV -> FV
tyCoFVsVarBndrs [TyVar]
vars FV
fvs = (TyVar -> FV -> FV) -> FV -> [TyVar] -> FV
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TyVar -> FV -> FV
tyCoFVsVarBndr FV
fvs [TyVar]
vars
tyCoFVsVarBndr :: Var -> FV -> FV
tyCoFVsVarBndr :: TyVar -> FV -> FV
tyCoFVsVarBndr TyVar
var FV
fvs
= Type -> FV
tyCoFVsOfType (TyVar -> Type
varType TyVar
var)
FV -> FV -> FV
`unionFV` TyVar -> FV -> FV
delFV TyVar
var FV
fvs
tyCoFVsOfTypes :: [Type] -> FV
tyCoFVsOfTypes :: [Type] -> FV
tyCoFVsOfTypes (Type
ty:[Type]
tys) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc = (Type -> FV
tyCoFVsOfType Type
ty FV -> FV -> FV
`unionFV` [Type] -> FV
tyCoFVsOfTypes [Type]
tys) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
tyCoFVsOfTypes [] InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc = FV
emptyFV InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
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 -> [TyVar]
tyCoVarsOfCoList Coercion
co = FV -> [TyVar]
fvVarList (FV -> [TyVar]) -> FV -> [TyVar]
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 TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
= Type -> FV
tyCoFVsOfType Type
ty InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
tyCoFVsOfCo (GRefl Role
_ Type
ty MCoercion
mco) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
= (Type -> FV
tyCoFVsOfType Type
ty FV -> FV -> FV
`unionFV` MCoercion -> FV
tyCoFVsOfMCo MCoercion
mco) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
tyCoFVsOfCo (TyConAppCo Role
_ TyCon
_ [Coercion]
cos) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc = [Coercion] -> FV
tyCoFVsOfCos [Coercion]
cos InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
tyCoFVsOfCo (AppCo Coercion
co Coercion
arg) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
= (Coercion -> FV
tyCoFVsOfCo Coercion
co FV -> FV -> FV
`unionFV` Coercion -> FV
tyCoFVsOfCo Coercion
arg) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
tyCoFVsOfCo (ForAllCo TyVar
tv Coercion
kind_co Coercion
co) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
= (TyVar -> FV -> FV
tyCoFVsVarBndr TyVar
tv (Coercion -> FV
tyCoFVsOfCo Coercion
co) FV -> FV -> FV
`unionFV` Coercion -> FV
tyCoFVsOfCo Coercion
kind_co) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
tyCoFVsOfCo (FunCo Role
_ Coercion
w Coercion
co1 Coercion
co2) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
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 TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
tyCoFVsOfCo (CoVarCo TyVar
v) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
= TyVar -> FV
tyCoFVsOfCoVar TyVar
v InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
tyCoFVsOfCo (HoleCo CoercionHole
h) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
= TyVar -> FV
tyCoFVsOfCoVar (CoercionHole -> TyVar
coHoleCoVar CoercionHole
h) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
tyCoFVsOfCo (AxiomInstCo CoAxiom Branched
_ BranchIndex
_ [Coercion]
cos) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc = [Coercion] -> FV
tyCoFVsOfCos [Coercion]
cos InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
tyCoFVsOfCo (UnivCo UnivCoProvenance
p Role
_ Type
t1 Type
t2) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], 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 ([TyVar], TyCoVarSet)
acc
tyCoFVsOfCo (SymCo Coercion
co) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
tyCoFVsOfCo (TransCo Coercion
co1 Coercion
co2) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc = (Coercion -> FV
tyCoFVsOfCo Coercion
co1 FV -> FV -> FV
`unionFV` Coercion -> FV
tyCoFVsOfCo Coercion
co2) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
tyCoFVsOfCo (NthCo Role
_ BranchIndex
_ Coercion
co) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
tyCoFVsOfCo (LRCo LeftOrRight
_ Coercion
co) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
tyCoFVsOfCo (InstCo Coercion
co Coercion
arg) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc = (Coercion -> FV
tyCoFVsOfCo Coercion
co FV -> FV -> FV
`unionFV` Coercion -> FV
tyCoFVsOfCo Coercion
arg) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
tyCoFVsOfCo (KindCo Coercion
co) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
tyCoFVsOfCo (SubCo Coercion
co) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
tyCoFVsOfCo (AxiomRuleCo CoAxiomRule
_ [Coercion]
cs) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc = [Coercion] -> FV
tyCoFVsOfCos [Coercion]
cs InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
tyCoFVsOfCoVar :: CoVar -> FV
tyCoFVsOfCoVar :: TyVar -> FV
tyCoFVsOfCoVar TyVar
v InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
= (TyVar -> FV
unitFV TyVar
v FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType (TyVar -> Type
varType TyVar
v)) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
tyCoFVsOfProv :: UnivCoProvenance -> FV
tyCoFVsOfProv :: UnivCoProvenance -> FV
tyCoFVsOfProv (PhantomProv Coercion
co) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
tyCoFVsOfProv (ProofIrrelProv Coercion
co) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
tyCoFVsOfProv (PluginProv String
_) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc = FV
emptyFV InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
tyCoFVsOfCos :: [Coercion] -> FV
tyCoFVsOfCos :: [Coercion] -> FV
tyCoFVsOfCos [] InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc = FV
emptyFV InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
tyCoFVsOfCos (Coercion
co:[Coercion]
cos) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc = (Coercion -> FV
tyCoFVsOfCo Coercion
co FV -> FV -> FV
`unionFV` [Coercion] -> FV
tyCoFVsOfCos [Coercion]
cos) InterestingVarFun
fv_cand TyCoVarSet
in_scope ([TyVar], TyCoVarSet)
acc
almostDevoidCoVarOfCo :: CoVar -> Coercion -> Bool
almostDevoidCoVarOfCo :: TyVar -> Coercion -> Bool
almostDevoidCoVarOfCo TyVar
cv Coercion
co =
Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyVar
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 {}) TyVar
_ = Bool
True
almost_devoid_co_var_of_co (GRefl {}) TyVar
_ = Bool
True
almost_devoid_co_var_of_co (TyConAppCo Role
_ TyCon
_ [Coercion]
cos) TyVar
cv
= [Coercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [Coercion]
cos TyVar
cv
almost_devoid_co_var_of_co (AppCo Coercion
co Coercion
arg) TyVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyVar
cv
Bool -> Bool -> Bool
&& Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
arg TyVar
cv
almost_devoid_co_var_of_co (ForAllCo TyVar
v Coercion
kind_co Coercion
co) TyVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
kind_co TyVar
cv
Bool -> Bool -> Bool
&& (TyVar
v TyVar -> InterestingVarFun
forall a. Eq a => a -> a -> Bool
== TyVar
cv Bool -> Bool -> Bool
|| Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyVar
cv)
almost_devoid_co_var_of_co (FunCo Role
_ Coercion
w Coercion
co1 Coercion
co2) TyVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
w TyVar
cv
Bool -> Bool -> Bool
&& Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co1 TyVar
cv
Bool -> Bool -> Bool
&& Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co2 TyVar
cv
almost_devoid_co_var_of_co (CoVarCo TyVar
v) TyVar
cv = TyVar
v TyVar -> InterestingVarFun
forall a. Eq a => a -> a -> Bool
/= TyVar
cv
almost_devoid_co_var_of_co (HoleCo CoercionHole
h) TyVar
cv = (CoercionHole -> TyVar
coHoleCoVar CoercionHole
h) TyVar -> InterestingVarFun
forall a. Eq a => a -> a -> Bool
/= TyVar
cv
almost_devoid_co_var_of_co (AxiomInstCo CoAxiom Branched
_ BranchIndex
_ [Coercion]
cos) TyVar
cv
= [Coercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [Coercion]
cos TyVar
cv
almost_devoid_co_var_of_co (UnivCo UnivCoProvenance
p Role
_ Type
t1 Type
t2) TyVar
cv
= UnivCoProvenance -> InterestingVarFun
almost_devoid_co_var_of_prov UnivCoProvenance
p TyVar
cv
Bool -> Bool -> Bool
&& Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
t1 TyVar
cv
Bool -> Bool -> Bool
&& Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
t2 TyVar
cv
almost_devoid_co_var_of_co (SymCo Coercion
co) TyVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyVar
cv
almost_devoid_co_var_of_co (TransCo Coercion
co1 Coercion
co2) TyVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co1 TyVar
cv
Bool -> Bool -> Bool
&& Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co2 TyVar
cv
almost_devoid_co_var_of_co (NthCo Role
_ BranchIndex
_ Coercion
co) TyVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyVar
cv
almost_devoid_co_var_of_co (LRCo LeftOrRight
_ Coercion
co) TyVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyVar
cv
almost_devoid_co_var_of_co (InstCo Coercion
co Coercion
arg) TyVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyVar
cv
Bool -> Bool -> Bool
&& Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
arg TyVar
cv
almost_devoid_co_var_of_co (KindCo Coercion
co) TyVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyVar
cv
almost_devoid_co_var_of_co (SubCo Coercion
co) TyVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyVar
cv
almost_devoid_co_var_of_co (AxiomRuleCo CoAxiomRule
_ [Coercion]
cs) TyVar
cv
= [Coercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [Coercion]
cs TyVar
cv
almost_devoid_co_var_of_cos :: [Coercion] -> CoVar -> Bool
almost_devoid_co_var_of_cos :: [Coercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [] TyVar
_ = Bool
True
almost_devoid_co_var_of_cos (Coercion
co:[Coercion]
cos) TyVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyVar
cv
Bool -> Bool -> Bool
&& [Coercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [Coercion]
cos TyVar
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) TyVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyVar
cv
almost_devoid_co_var_of_prov (ProofIrrelProv Coercion
co) TyVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyVar
cv
almost_devoid_co_var_of_prov (PluginProv String
_) TyVar
_ = 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 TyVar
_) TyVar
_ = Bool
True
almost_devoid_co_var_of_type (TyConApp TyCon
_ [Type]
tys) TyVar
cv
= [Type] -> InterestingVarFun
almost_devoid_co_var_of_types [Type]
tys TyVar
cv
almost_devoid_co_var_of_type (LitTy {}) TyVar
_ = Bool
True
almost_devoid_co_var_of_type (AppTy Type
fun Type
arg) TyVar
cv
= Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
fun TyVar
cv
Bool -> Bool -> Bool
&& Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
arg TyVar
cv
almost_devoid_co_var_of_type (FunTy AnonArgFlag
_ Type
w Type
arg Type
res) TyVar
cv
= Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
w TyVar
cv
Bool -> Bool -> Bool
&& Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
arg TyVar
cv
Bool -> Bool -> Bool
&& Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
res TyVar
cv
almost_devoid_co_var_of_type (ForAllTy (Bndr TyVar
v ArgFlag
_) Type
ty) TyVar
cv
= Type -> InterestingVarFun
almost_devoid_co_var_of_type (TyVar -> Type
varType TyVar
v) TyVar
cv
Bool -> Bool -> Bool
&& (TyVar
v TyVar -> InterestingVarFun
forall a. Eq a => a -> a -> Bool
== TyVar
cv Bool -> Bool -> Bool
|| Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
ty TyVar
cv)
almost_devoid_co_var_of_type (CastTy Type
ty Coercion
co) TyVar
cv
= Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
ty TyVar
cv
Bool -> Bool -> Bool
&& Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyVar
cv
almost_devoid_co_var_of_type (CoercionTy Coercion
co) TyVar
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co TyVar
cv
almost_devoid_co_var_of_types :: [Type] -> CoVar -> Bool
almost_devoid_co_var_of_types :: [Type] -> InterestingVarFun
almost_devoid_co_var_of_types [] TyVar
_ = Bool
True
almost_devoid_co_var_of_types (Type
ty:[Type]
tys) TyVar
cv
= Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
ty TyVar
cv
Bool -> Bool -> Bool
&& [Type] -> InterestingVarFun
almost_devoid_co_var_of_types [Type]
tys TyVar
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 TyVar
v) = TyVar -> FV
unitFV TyVar
v FV -> FV -> FV
`unionFV` Type -> FV
go (TyVar -> Type
tyVarKind TyVar
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 TyVar
tv ArgFlag
_) Type
ty) = Type -> FV
go (TyVar -> Type
tyVarKind TyVar
tv) FV -> FV -> FV
`unionFV` TyVar -> FV -> FV
delFV TyVar
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 TyVar
v) = Type -> FV
go (TyVar -> Type
tyVarKind TyVar
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
nfvFolder :: TyCoFolder TyCoVarSet DM.All
nfvFolder :: TyCoFolder TyCoVarSet All
nfvFolder = TyCoFolder :: forall env a.
(Type -> Maybe Type)
-> (env -> TyVar -> a)
-> (env -> TyVar -> a)
-> (env -> CoercionHole -> a)
-> (env -> TyVar -> ArgFlag -> env)
-> TyCoFolder env a
TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view = Type -> Maybe Type
noView
, tcf_tyvar :: TyCoVarSet -> TyVar -> All
tcf_tyvar = TyCoVarSet -> TyVar -> All
do_tcv, tcf_covar :: TyCoVarSet -> TyVar -> All
tcf_covar = TyCoVarSet -> TyVar -> All
do_tcv
, tcf_hole :: TyCoVarSet -> CoercionHole -> All
tcf_hole = TyCoVarSet -> CoercionHole -> All
forall p p. p -> p -> All
do_hole, tcf_tycobinder :: TyCoVarSet -> TyVar -> ArgFlag -> TyCoVarSet
tcf_tycobinder = TyCoVarSet -> TyVar -> ArgFlag -> TyCoVarSet
forall p. TyCoVarSet -> TyVar -> p -> TyCoVarSet
do_bndr }
where
do_tcv :: TyCoVarSet -> TyVar -> All
do_tcv TyCoVarSet
is TyVar
tv = Bool -> All
All (TyVar
tv TyVar -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
is)
do_hole :: p -> p -> All
do_hole p
_ p
_ = Bool -> All
All Bool
True
do_bndr :: TyCoVarSet -> TyVar -> p -> TyCoVarSet
do_bndr TyCoVarSet
is TyVar
tv p
_ = TyCoVarSet
is TyCoVarSet -> TyVar -> TyCoVarSet
`extendVarSet` TyVar
tv
nfv_ty :: Type -> DM.All
nfv_tys :: [Type] -> DM.All
nfv_co :: Coercion -> DM.All
(Type -> All
nfv_ty, [Type] -> All
nfv_tys, Coercion -> All
nfv_co, [Coercion] -> All
_) = TyCoFolder TyCoVarSet All
-> TyCoVarSet
-> (Type -> All, [Type] -> All, Coercion -> All, [Coercion] -> All)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo TyCoFolder TyCoVarSet All
nfvFolder TyCoVarSet
emptyVarSet
noFreeVarsOfType :: Type -> Bool
noFreeVarsOfType :: Type -> Bool
noFreeVarsOfType Type
ty = All -> Bool
DM.getAll (Type -> All
nfv_ty Type
ty)
noFreeVarsOfTypes :: [Type] -> Bool
noFreeVarsOfTypes :: [Type] -> Bool
noFreeVarsOfTypes [Type]
tys = All -> Bool
DM.getAll ([Type] -> All
nfv_tys [Type]
tys)
noFreeVarsOfCo :: Coercion -> Bool
noFreeVarsOfCo :: Coercion -> Bool
noFreeVarsOfCo Coercion
co = All -> Bool
getAll (Coercion -> All
nfv_co Coercion
co)
scopedSort :: [TyCoVar] -> [TyCoVar]
scopedSort :: [TyVar] -> [TyVar]
scopedSort = [TyVar] -> [TyCoVarSet] -> [TyVar] -> [TyVar]
go [] []
where
go :: [TyCoVar]
-> [TyCoVarSet]
-> [TyCoVar]
-> [TyCoVar]
go :: [TyVar] -> [TyCoVarSet] -> [TyVar] -> [TyVar]
go [TyVar]
acc [TyCoVarSet]
_fv_list [] = [TyVar] -> [TyVar]
forall a. [a] -> [a]
reverse [TyVar]
acc
go [TyVar]
acc [TyCoVarSet]
fv_list (TyVar
tv:[TyVar]
tvs)
= [TyVar] -> [TyCoVarSet] -> [TyVar] -> [TyVar]
go [TyVar]
acc' [TyCoVarSet]
fv_list' [TyVar]
tvs
where
([TyVar]
acc', [TyCoVarSet]
fv_list') = TyVar -> [TyVar] -> [TyCoVarSet] -> ([TyVar], [TyCoVarSet])
insert TyVar
tv [TyVar]
acc [TyCoVarSet]
fv_list
insert :: TyCoVar
-> [TyCoVar]
-> [TyCoVarSet]
-> ([TyCoVar], [TyCoVarSet])
insert :: TyVar -> [TyVar] -> [TyCoVarSet] -> ([TyVar], [TyCoVarSet])
insert TyVar
tv [] [] = ([TyVar
tv], [Type -> TyCoVarSet
tyCoVarsOfType (TyVar -> Type
tyVarKind TyVar
tv)])
insert TyVar
tv (TyVar
a:[TyVar]
as) (TyCoVarSet
fvs:[TyCoVarSet]
fvss)
| TyVar
tv TyVar -> TyCoVarSet -> Bool
`elemVarSet` TyCoVarSet
fvs
, ([TyVar]
as', [TyCoVarSet]
fvss') <- TyVar -> [TyVar] -> [TyCoVarSet] -> ([TyVar], [TyCoVarSet])
insert TyVar
tv [TyVar]
as [TyCoVarSet]
fvss
= (TyVar
aTyVar -> [TyVar] -> [TyVar]
forall a. a -> [a] -> [a]
:[TyVar]
as', TyCoVarSet
fvs TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` TyCoVarSet
fv_tv TyCoVarSet -> [TyCoVarSet] -> [TyCoVarSet]
forall a. a -> [a] -> [a]
: [TyCoVarSet]
fvss')
| Bool
otherwise
= (TyVar
tvTyVar -> [TyVar] -> [TyVar]
forall a. a -> [a] -> [a]
:TyVar
aTyVar -> [TyVar] -> [TyVar]
forall a. a -> [a] -> [a]
:[TyVar]
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 (TyVar -> Type
tyVarKind TyVar
tv)
insert TyVar
_ [TyVar]
_ [TyCoVarSet]
_ = String -> ([TyVar], [TyCoVarSet])
forall a. String -> a
panic String
"scopedSort"
tyCoVarsOfTypeWellScoped :: Type -> [TyVar]
tyCoVarsOfTypeWellScoped :: Type -> [TyVar]
tyCoVarsOfTypeWellScoped = [TyVar] -> [TyVar]
scopedSort ([TyVar] -> [TyVar]) -> (Type -> [TyVar]) -> Type -> [TyVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [TyVar]
tyCoVarsOfTypeList
tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
tyCoVarsOfTypesWellScoped = [TyVar] -> [TyVar]
scopedSort ([TyVar] -> [TyVar]) -> ([Type] -> [TyVar]) -> [Type] -> [TyVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Type] -> [TyVar]
tyCoVarsOfTypesList