{-# LANGUAGE MultiWayIf #-}
module GHC.Core.TyCo.FVs
( shallowTyCoVarsOfType, shallowTyCoVarsOfTypes,
tyCoVarsOfType, tyCoVarsOfTypes,
tyCoVarsOfTypeDSet, tyCoVarsOfTypesDSet,
tyCoFVsBndr, tyCoFVsVarBndr, tyCoFVsVarBndrs,
tyCoFVsOfType, tyCoVarsOfTypeList,
tyCoFVsOfTypes, tyCoVarsOfTypesList,
deepTcvFolder,
shallowTyCoVarsOfTyVarEnv, shallowTyCoVarsOfCoVarEnv,
shallowTyCoVarsOfCo, shallowTyCoVarsOfCos,
tyCoVarsOfCo, tyCoVarsOfCos, tyCoVarsOfMCo,
coVarsOfType, coVarsOfTypes,
coVarsOfCo, coVarsOfCos,
tyCoVarsOfCoDSet,
tyCoFVsOfCo, tyCoFVsOfCos,
tyCoVarsOfCoList,
coVarsOfCoDSet, coVarsOfCosDSet,
almostDevoidCoVarOfCo,
injectiveVarsOfType, injectiveVarsOfTypes, isInjectiveInType,
invisibleVarsOfType, invisibleVarsOfTypes,
anyFreeVarsOfType, anyFreeVarsOfTypes, anyFreeVarsOfCo,
noFreeVarsOfType, noFreeVarsOfTypes, noFreeVarsOfCo,
tyConsOfType, tyConsOfTypes,
visVarsOfTypes, visVarsOfType,
occCheckExpand,
scopedSort, tyCoVarsOfTypeWellScoped,
tyCoVarsOfTypesWellScoped,
closeOverKindsDSet, closeOverKindsList,
closeOverKinds,
Endo(..), runTyCoVars
) where
import GHC.Prelude
import {-# SOURCE #-} GHC.Core.Type( partitionInvisibleTypes, coreView, rewriterView )
import {-# SOURCE #-} GHC.Core.Coercion( coercionLKind )
import GHC.Builtin.Types.Prim( funTyFlagTyCon )
import Data.Monoid as DM ( Any(..) )
import GHC.Core.TyCo.Rep
import GHC.Core.TyCon
import GHC.Core.Coercion.Axiom( CoAxiomRule(..), BuiltInFamRewrite(..), coAxiomTyCon )
import GHC.Utils.FV
import GHC.Types.Var
import GHC.Types.Unique.FM
import GHC.Types.Unique.Set
import GHC.Types.Var.Set
import GHC.Types.Var.Env
import GHC.Utils.Misc
import GHC.Utils.Panic
import GHC.Data.Pair
import Data.Semigroup
runTyCoVars :: Endo TyCoVarSet -> TyCoVarSet
{-# INLINE runTyCoVars #-}
runTyCoVars :: Endo VarSet -> VarSet
runTyCoVars Endo VarSet
f = Endo VarSet -> VarSet -> VarSet
forall a. Endo a -> a -> a
appEndo Endo VarSet
f VarSet
emptyVarSet
tyCoVarsOfType :: Type -> TyCoVarSet
tyCoVarsOfType :: Type -> VarSet
tyCoVarsOfType Type
ty = Endo VarSet -> VarSet
runTyCoVars (Type -> Endo VarSet
deep_ty Type
ty)
tyCoVarsOfTypes :: [Type] -> TyCoVarSet
tyCoVarsOfTypes :: [Type] -> VarSet
tyCoVarsOfTypes [Type]
tys = Endo VarSet -> VarSet
runTyCoVars ([Type] -> Endo VarSet
deep_tys [Type]
tys)
tyCoVarsOfCo :: Coercion -> TyCoVarSet
tyCoVarsOfCo :: Coercion -> VarSet
tyCoVarsOfCo Coercion
co = Endo VarSet -> VarSet
runTyCoVars (Coercion -> Endo VarSet
deep_co Coercion
co)
tyCoVarsOfMCo :: MCoercion -> TyCoVarSet
tyCoVarsOfMCo :: MCoercion -> VarSet
tyCoVarsOfMCo MCoercion
MRefl = VarSet
emptyVarSet
tyCoVarsOfMCo (MCo Coercion
co) = Coercion -> VarSet
tyCoVarsOfCo Coercion
co
tyCoVarsOfCos :: [Coercion] -> TyCoVarSet
tyCoVarsOfCos :: [Coercion] -> VarSet
tyCoVarsOfCos [Coercion]
cos = Endo VarSet -> VarSet
runTyCoVars ([Coercion] -> Endo VarSet
deep_cos [Coercion]
cos)
deep_ty :: Type -> Endo TyCoVarSet
deep_tys :: [Type] -> Endo TyCoVarSet
deep_co :: Coercion -> Endo TyCoVarSet
deep_cos :: [Coercion] -> Endo TyCoVarSet
(Type -> Endo VarSet
deep_ty, [Type] -> Endo VarSet
deep_tys, Coercion -> Endo VarSet
deep_co, [Coercion] -> Endo VarSet
deep_cos) = TyCoFolder VarSet (Endo VarSet)
-> VarSet
-> (Type -> Endo VarSet, [Type] -> Endo VarSet,
Coercion -> Endo VarSet, [Coercion] -> Endo VarSet)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo TyCoFolder VarSet (Endo VarSet)
deepTcvFolder VarSet
emptyVarSet
deepTcvFolder :: TyCoFolder TyCoVarSet (Endo TyCoVarSet)
deepTcvFolder :: TyCoFolder VarSet (Endo VarSet)
deepTcvFolder = TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view = Type -> Maybe Type
noView
, tcf_tyvar :: VarSet -> Var -> Endo VarSet
tcf_tyvar = VarSet -> Var -> Endo VarSet
do_tcv, tcf_covar :: VarSet -> Var -> Endo VarSet
tcf_covar = VarSet -> Var -> Endo VarSet
do_tcv
, tcf_hole :: VarSet -> CoercionHole -> Endo VarSet
tcf_hole = VarSet -> CoercionHole -> Endo VarSet
do_hole, tcf_tycobinder :: VarSet -> Var -> ForAllTyFlag -> VarSet
tcf_tycobinder = VarSet -> Var -> ForAllTyFlag -> VarSet
forall {p}. VarSet -> Var -> p -> VarSet
do_bndr }
where
do_tcv :: VarSet -> Var -> Endo VarSet
do_tcv VarSet
is Var
v = (VarSet -> VarSet) -> Endo VarSet
forall a. (a -> a) -> Endo a
Endo VarSet -> VarSet
do_it
where
do_it :: VarSet -> VarSet
do_it VarSet
acc | Var
v Var -> VarSet -> Bool
`elemVarSet` VarSet
is = VarSet
acc
| Var
v Var -> VarSet -> Bool
`elemVarSet` VarSet
acc = VarSet
acc
| Bool
otherwise = Endo VarSet -> VarSet -> VarSet
forall a. Endo a -> a -> a
appEndo (Type -> Endo VarSet
deep_ty (Var -> Type
varType Var
v)) (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$
VarSet
acc VarSet -> Var -> VarSet
`extendVarSet` Var
v
do_bndr :: VarSet -> Var -> p -> VarSet
do_bndr VarSet
is Var
tcv p
_ = VarSet -> Var -> VarSet
extendVarSet VarSet
is Var
tcv
do_hole :: VarSet -> CoercionHole -> Endo VarSet
do_hole VarSet
is CoercionHole
hole = VarSet -> Var -> Endo VarSet
do_tcv VarSet
is (CoercionHole -> Var
coHoleCoVar CoercionHole
hole)
shallowTyCoVarsOfType :: Type -> TyCoVarSet
shallowTyCoVarsOfType :: Type -> VarSet
shallowTyCoVarsOfType Type
ty = Endo VarSet -> VarSet
runTyCoVars (Type -> Endo VarSet
shallow_ty Type
ty)
shallowTyCoVarsOfTypes :: [Type] -> TyCoVarSet
shallowTyCoVarsOfTypes :: [Type] -> VarSet
shallowTyCoVarsOfTypes [Type]
tys = Endo VarSet -> VarSet
runTyCoVars ([Type] -> Endo VarSet
shallow_tys [Type]
tys)
shallowTyCoVarsOfCo :: Coercion -> TyCoVarSet
shallowTyCoVarsOfCo :: Coercion -> VarSet
shallowTyCoVarsOfCo Coercion
co = Endo VarSet -> VarSet
runTyCoVars (Coercion -> Endo VarSet
shallow_co Coercion
co)
shallowTyCoVarsOfCos :: [Coercion] -> TyCoVarSet
shallowTyCoVarsOfCos :: [Coercion] -> VarSet
shallowTyCoVarsOfCos [Coercion]
cos = Endo VarSet -> VarSet
runTyCoVars ([Coercion] -> Endo VarSet
shallow_cos [Coercion]
cos)
shallowTyCoVarsOfTyVarEnv :: TyVarEnv Type -> TyCoVarSet
shallowTyCoVarsOfTyVarEnv :: TyVarEnv Type -> VarSet
shallowTyCoVarsOfTyVarEnv TyVarEnv Type
tys = [Type] -> VarSet
shallowTyCoVarsOfTypes (TyVarEnv Type -> [Type]
forall {k} (key :: k) elt. UniqFM key elt -> [elt]
nonDetEltsUFM TyVarEnv Type
tys)
shallowTyCoVarsOfCoVarEnv :: CoVarEnv Coercion -> TyCoVarSet
shallowTyCoVarsOfCoVarEnv :: CoVarEnv Coercion -> VarSet
shallowTyCoVarsOfCoVarEnv CoVarEnv Coercion
cos = [Coercion] -> VarSet
shallowTyCoVarsOfCos (CoVarEnv Coercion -> [Coercion]
forall {k} (key :: k) elt. UniqFM key elt -> [elt]
nonDetEltsUFM CoVarEnv Coercion
cos)
shallow_ty :: Type -> Endo TyCoVarSet
shallow_tys :: [Type] -> Endo TyCoVarSet
shallow_co :: Coercion -> Endo TyCoVarSet
shallow_cos :: [Coercion] -> Endo TyCoVarSet
(Type -> Endo VarSet
shallow_ty, [Type] -> Endo VarSet
shallow_tys, Coercion -> Endo VarSet
shallow_co, [Coercion] -> Endo VarSet
shallow_cos) = TyCoFolder VarSet (Endo VarSet)
-> VarSet
-> (Type -> Endo VarSet, [Type] -> Endo VarSet,
Coercion -> Endo VarSet, [Coercion] -> Endo VarSet)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo TyCoFolder VarSet (Endo VarSet)
shallowTcvFolder VarSet
emptyVarSet
shallowTcvFolder :: TyCoFolder TyCoVarSet (Endo TyCoVarSet)
shallowTcvFolder :: TyCoFolder VarSet (Endo VarSet)
shallowTcvFolder = TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view = Type -> Maybe Type
noView
, tcf_tyvar :: VarSet -> Var -> Endo VarSet
tcf_tyvar = VarSet -> Var -> Endo VarSet
do_tcv, tcf_covar :: VarSet -> Var -> Endo VarSet
tcf_covar = VarSet -> Var -> Endo VarSet
do_tcv
, tcf_hole :: VarSet -> CoercionHole -> Endo VarSet
tcf_hole = VarSet -> CoercionHole -> Endo VarSet
forall {a} {p} {p}. Monoid a => p -> p -> a
do_hole, tcf_tycobinder :: VarSet -> Var -> ForAllTyFlag -> VarSet
tcf_tycobinder = VarSet -> Var -> ForAllTyFlag -> VarSet
forall {p}. VarSet -> Var -> p -> VarSet
do_bndr }
where
do_tcv :: VarSet -> Var -> Endo VarSet
do_tcv VarSet
is Var
v = (VarSet -> VarSet) -> Endo VarSet
forall a. (a -> a) -> Endo a
Endo VarSet -> VarSet
do_it
where
do_it :: VarSet -> VarSet
do_it VarSet
acc | Var
v Var -> VarSet -> Bool
`elemVarSet` VarSet
is = VarSet
acc
| Var
v Var -> VarSet -> Bool
`elemVarSet` VarSet
acc = VarSet
acc
| Bool
otherwise = VarSet
acc VarSet -> Var -> VarSet
`extendVarSet` Var
v
do_bndr :: VarSet -> Var -> p -> VarSet
do_bndr VarSet
is Var
tcv p
_ = VarSet -> Var -> VarSet
extendVarSet VarSet
is Var
tcv
do_hole :: p -> p -> a
do_hole p
_ p
_ = a
forall a. Monoid a => a
mempty
coVarsOfType :: Type -> CoVarSet
coVarsOfTypes :: [Type] -> CoVarSet
coVarsOfCo :: Coercion -> CoVarSet
coVarsOfCos :: [Coercion] -> CoVarSet
coVarsOfType :: Type -> VarSet
coVarsOfType Type
ty = Endo VarSet -> VarSet
runTyCoVars (Type -> Endo VarSet
deep_cv_ty Type
ty)
coVarsOfTypes :: [Type] -> VarSet
coVarsOfTypes [Type]
tys = Endo VarSet -> VarSet
runTyCoVars ([Type] -> Endo VarSet
deep_cv_tys [Type]
tys)
coVarsOfCo :: Coercion -> VarSet
coVarsOfCo Coercion
co = Endo VarSet -> VarSet
runTyCoVars (Coercion -> Endo VarSet
deep_cv_co Coercion
co)
coVarsOfCos :: [Coercion] -> VarSet
coVarsOfCos [Coercion]
cos = Endo VarSet -> VarSet
runTyCoVars ([Coercion] -> Endo VarSet
deep_cv_cos [Coercion]
cos)
deep_cv_ty :: Type -> Endo CoVarSet
deep_cv_tys :: [Type] -> Endo CoVarSet
deep_cv_co :: Coercion -> Endo CoVarSet
deep_cv_cos :: [Coercion] -> Endo CoVarSet
(Type -> Endo VarSet
deep_cv_ty, [Type] -> Endo VarSet
deep_cv_tys, Coercion -> Endo VarSet
deep_cv_co, [Coercion] -> Endo VarSet
deep_cv_cos) = TyCoFolder VarSet (Endo VarSet)
-> VarSet
-> (Type -> Endo VarSet, [Type] -> Endo VarSet,
Coercion -> Endo VarSet, [Coercion] -> Endo VarSet)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo TyCoFolder VarSet (Endo VarSet)
deepCoVarFolder VarSet
emptyVarSet
deepCoVarFolder :: TyCoFolder TyCoVarSet (Endo CoVarSet)
deepCoVarFolder :: TyCoFolder VarSet (Endo VarSet)
deepCoVarFolder = TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view = Type -> Maybe Type
noView
, tcf_tyvar :: VarSet -> Var -> Endo VarSet
tcf_tyvar = VarSet -> Var -> Endo VarSet
forall {a} {p} {p}. Monoid a => p -> p -> a
do_tyvar, tcf_covar :: VarSet -> Var -> Endo VarSet
tcf_covar = VarSet -> Var -> Endo VarSet
do_covar
, tcf_hole :: VarSet -> CoercionHole -> Endo VarSet
tcf_hole = VarSet -> CoercionHole -> Endo VarSet
do_hole, tcf_tycobinder :: VarSet -> Var -> ForAllTyFlag -> VarSet
tcf_tycobinder = VarSet -> Var -> ForAllTyFlag -> VarSet
forall {p}. VarSet -> Var -> p -> VarSet
do_bndr }
where
do_tyvar :: p -> p -> a
do_tyvar p
_ p
_ = a
forall a. Monoid a => a
mempty
do_covar :: VarSet -> Var -> Endo VarSet
do_covar VarSet
is Var
v = (VarSet -> VarSet) -> Endo VarSet
forall a. (a -> a) -> Endo a
Endo VarSet -> VarSet
do_it
where
do_it :: VarSet -> VarSet
do_it VarSet
acc | Var
v Var -> VarSet -> Bool
`elemVarSet` VarSet
is = VarSet
acc
| Var
v Var -> VarSet -> Bool
`elemVarSet` VarSet
acc = VarSet
acc
| Bool
otherwise = Endo VarSet -> VarSet -> VarSet
forall a. Endo a -> a -> a
appEndo (Type -> Endo VarSet
deep_cv_ty (Var -> Type
varType Var
v)) (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$
VarSet
acc VarSet -> Var -> VarSet
`extendVarSet` Var
v
do_bndr :: VarSet -> Var -> p -> VarSet
do_bndr VarSet
is Var
tcv p
_ = VarSet -> Var -> VarSet
extendVarSet VarSet
is Var
tcv
do_hole :: VarSet -> CoercionHole -> Endo VarSet
do_hole VarSet
is CoercionHole
hole = VarSet -> Var -> Endo VarSet
do_covar VarSet
is (CoercionHole -> Var
coHoleCoVar CoercionHole
hole)
coVarsOfCosDSet :: [Coercion] -> DCoVarSet
coVarsOfCosDSet :: [Coercion] -> DCoVarSet
coVarsOfCosDSet [Coercion]
cos = InterestingVarFun -> FV -> DCoVarSet
fvDVarSetSome InterestingVarFun
isCoVar ([Coercion] -> FV
tyCoFVsOfCos [Coercion]
cos)
coVarsOfCoDSet :: Coercion -> DCoVarSet
coVarsOfCoDSet :: Coercion -> DCoVarSet
coVarsOfCoDSet Coercion
co = InterestingVarFun -> FV -> DCoVarSet
fvDVarSetSome InterestingVarFun
isCoVar (Coercion -> FV
tyCoFVsOfCo Coercion
co)
closeOverKinds :: TyCoVarSet -> TyCoVarSet
closeOverKinds :: VarSet -> VarSet
closeOverKinds VarSet
vs = (Var -> VarSet -> VarSet) -> VarSet -> VarSet -> VarSet
forall a. (Var -> a -> a) -> a -> VarSet -> a
nonDetStrictFoldVarSet Var -> VarSet -> VarSet
do_one VarSet
vs VarSet
vs
where
do_one :: Var -> VarSet -> VarSet
do_one Var
v VarSet
acc = Endo VarSet -> VarSet -> VarSet
forall a. Endo a -> a -> a
appEndo (Type -> Endo VarSet
deep_ty (Var -> Type
varType Var
v)) VarSet
acc
closeOverKindsFV :: [TyVar] -> FV
closeOverKindsFV :: [Var] -> FV
closeOverKindsFV [Var]
tvs =
(Var -> FV) -> [Var] -> FV
forall a. (a -> FV) -> [a] -> FV
mapUnionFV (Type -> FV
tyCoFVsOfType (Type -> FV) -> (Var -> Type) -> Var -> FV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Type
tyVarKind) [Var]
tvs FV -> FV -> FV
`unionFV` [Var] -> FV
mkFVs [Var]
tvs
closeOverKindsList :: [TyVar] -> [TyVar]
closeOverKindsList :: [Var] -> [Var]
closeOverKindsList [Var]
tvs = FV -> [Var]
fvVarList (FV -> [Var]) -> FV -> [Var]
forall a b. (a -> b) -> a -> b
$ [Var] -> FV
closeOverKindsFV [Var]
tvs
closeOverKindsDSet :: DTyVarSet -> DTyVarSet
closeOverKindsDSet :: DCoVarSet -> DCoVarSet
closeOverKindsDSet = FV -> DCoVarSet
fvDVarSet (FV -> DCoVarSet) -> (DCoVarSet -> FV) -> DCoVarSet -> DCoVarSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Var] -> FV
closeOverKindsFV ([Var] -> FV) -> (DCoVarSet -> [Var]) -> DCoVarSet -> FV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DCoVarSet -> [Var]
dVarSetElems
tyCoVarsOfTypeDSet :: Type -> DTyCoVarSet
tyCoVarsOfTypeDSet :: Type -> DCoVarSet
tyCoVarsOfTypeDSet Type
ty = FV -> DCoVarSet
fvDVarSet (FV -> DCoVarSet) -> FV -> DCoVarSet
forall a b. (a -> b) -> a -> b
$ Type -> FV
tyCoFVsOfType Type
ty
tyCoVarsOfTypeList :: Type -> [TyCoVar]
tyCoVarsOfTypeList :: Type -> [Var]
tyCoVarsOfTypeList Type
ty = FV -> [Var]
fvVarList (FV -> [Var]) -> FV -> [Var]
forall a b. (a -> b) -> a -> b
$ Type -> FV
tyCoFVsOfType Type
ty
tyCoVarsOfTypesDSet :: [Type] -> DTyCoVarSet
tyCoVarsOfTypesDSet :: [Type] -> DCoVarSet
tyCoVarsOfTypesDSet [Type]
tys = FV -> DCoVarSet
fvDVarSet (FV -> DCoVarSet) -> FV -> DCoVarSet
forall a b. (a -> b) -> a -> b
$ [Type] -> FV
tyCoFVsOfTypes [Type]
tys
tyCoVarsOfTypesList :: [Type] -> [TyCoVar]
tyCoVarsOfTypesList :: [Type] -> [Var]
tyCoVarsOfTypesList [Type]
tys = FV -> [Var]
fvVarList (FV -> [Var]) -> FV -> [Var]
forall a b. (a -> b) -> a -> b
$ [Type] -> FV
tyCoFVsOfTypes [Type]
tys
tyCoFVsOfType :: Type -> FV
tyCoFVsOfType :: Type -> FV
tyCoFVsOfType (TyVarTy Var
v) InterestingVarFun
f VarSet
bound_vars ([Var]
acc_list, VarSet
acc_set)
| Bool -> Bool
not (InterestingVarFun
f Var
v) = ([Var]
acc_list, VarSet
acc_set)
| Var
v Var -> VarSet -> Bool
`elemVarSet` VarSet
bound_vars = ([Var]
acc_list, VarSet
acc_set)
| Var
v Var -> VarSet -> Bool
`elemVarSet` VarSet
acc_set = ([Var]
acc_list, VarSet
acc_set)
| Bool
otherwise = Type -> FV
tyCoFVsOfType (Var -> Type
tyVarKind Var
v) InterestingVarFun
f
VarSet
emptyVarSet
(Var
vVar -> [Var] -> [Var]
forall a. a -> [a] -> [a]
:[Var]
acc_list, VarSet -> Var -> VarSet
extendVarSet VarSet
acc_set Var
v)
tyCoFVsOfType (TyConApp TyCon
_ [Type]
tys) InterestingVarFun
f VarSet
bound_vars ([Var], VarSet)
acc = [Type] -> FV
tyCoFVsOfTypes [Type]
tys InterestingVarFun
f VarSet
bound_vars ([Var], VarSet)
acc
tyCoFVsOfType (LitTy {}) InterestingVarFun
f VarSet
bound_vars ([Var], VarSet)
acc = FV
emptyFV InterestingVarFun
f VarSet
bound_vars ([Var], VarSet)
acc
tyCoFVsOfType (AppTy Type
fun Type
arg) InterestingVarFun
f VarSet
bound_vars ([Var], VarSet)
acc = (Type -> FV
tyCoFVsOfType Type
fun FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType Type
arg) InterestingVarFun
f VarSet
bound_vars ([Var], VarSet)
acc
tyCoFVsOfType (FunTy FunTyFlag
_ Type
w Type
arg Type
res) InterestingVarFun
f VarSet
bound_vars ([Var], VarSet)
acc = (Type -> FV
tyCoFVsOfType Type
w FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType Type
arg FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType Type
res) InterestingVarFun
f VarSet
bound_vars ([Var], VarSet)
acc
tyCoFVsOfType (ForAllTy ForAllTyBinder
bndr Type
ty) InterestingVarFun
f VarSet
bound_vars ([Var], VarSet)
acc = ForAllTyBinder -> FV -> FV
tyCoFVsBndr ForAllTyBinder
bndr (Type -> FV
tyCoFVsOfType Type
ty) InterestingVarFun
f VarSet
bound_vars ([Var], VarSet)
acc
tyCoFVsOfType (CastTy Type
ty Coercion
co) InterestingVarFun
f VarSet
bound_vars ([Var], VarSet)
acc = (Type -> FV
tyCoFVsOfType Type
ty FV -> FV -> FV
`unionFV` Coercion -> FV
tyCoFVsOfCo Coercion
co) InterestingVarFun
f VarSet
bound_vars ([Var], VarSet)
acc
tyCoFVsOfType (CoercionTy Coercion
co) InterestingVarFun
f VarSet
bound_vars ([Var], VarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co InterestingVarFun
f VarSet
bound_vars ([Var], VarSet)
acc
tyCoFVsBndr :: ForAllTyBinder -> FV -> FV
tyCoFVsBndr :: ForAllTyBinder -> FV -> FV
tyCoFVsBndr (Bndr Var
tv ForAllTyFlag
_) FV
fvs = Var -> FV -> FV
tyCoFVsVarBndr Var
tv FV
fvs
tyCoFVsVarBndrs :: [Var] -> FV -> FV
tyCoFVsVarBndrs :: [Var] -> FV -> FV
tyCoFVsVarBndrs [Var]
vars FV
fvs = (Var -> FV -> FV) -> FV -> [Var] -> FV
forall a b. (a -> b -> b) -> b -> [a] -> b
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 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 (Type
ty:[Type]
tys) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc = (Type -> FV
tyCoFVsOfType Type
ty FV -> FV -> FV
`unionFV` [Type] -> FV
tyCoFVsOfTypes [Type]
tys) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
tyCoFVsOfTypes [] InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc = FV
emptyFV InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
tyCoVarsOfCoDSet :: Coercion -> DTyCoVarSet
tyCoVarsOfCoDSet :: Coercion -> DCoVarSet
tyCoVarsOfCoDSet Coercion
co = FV -> DCoVarSet
fvDVarSet (FV -> DCoVarSet) -> FV -> DCoVarSet
forall a b. (a -> b) -> a -> b
$ Coercion -> FV
tyCoFVsOfCo Coercion
co
tyCoVarsOfCoList :: Coercion -> [TyCoVar]
tyCoVarsOfCoList :: Coercion -> [Var]
tyCoVarsOfCoList Coercion
co = FV -> [Var]
fvVarList (FV -> [Var]) -> FV -> [Var]
forall a b. (a -> b) -> a -> b
$ Coercion -> FV
tyCoFVsOfCo Coercion
co
tyCoFVsOfMCo :: MCoercion -> FV
tyCoFVsOfMCo :: MCoercion -> FV
tyCoFVsOfMCo MCoercion
MRefl = FV
emptyFV
tyCoFVsOfMCo (MCo Coercion
co) = Coercion -> FV
tyCoFVsOfCo Coercion
co
tyCoFVsOfCo :: Coercion -> FV
tyCoFVsOfCo :: Coercion -> FV
tyCoFVsOfCo (Refl Type
ty) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
= Type -> FV
tyCoFVsOfType Type
ty InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
tyCoFVsOfCo (GRefl Role
_ Type
ty MCoercion
mco) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
= (Type -> FV
tyCoFVsOfType Type
ty FV -> FV -> FV
`unionFV` MCoercion -> FV
tyCoFVsOfMCo MCoercion
mco) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
tyCoFVsOfCo (TyConAppCo Role
_ TyCon
_ [Coercion]
cos) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc = [Coercion] -> FV
tyCoFVsOfCos [Coercion]
cos InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
tyCoFVsOfCo (AppCo Coercion
co Coercion
arg) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
= (Coercion -> FV
tyCoFVsOfCo Coercion
co FV -> FV -> FV
`unionFV` Coercion -> FV
tyCoFVsOfCo Coercion
arg) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
tyCoFVsOfCo (ForAllCo { fco_tcv :: Coercion -> Var
fco_tcv = Var
tv, fco_kind :: Coercion -> Coercion
fco_kind = Coercion
kind_co, fco_body :: Coercion -> Coercion
fco_body = Coercion
co }) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
= (Var -> FV -> FV
tyCoFVsVarBndr Var
tv (Coercion -> FV
tyCoFVsOfCo Coercion
co) FV -> FV -> FV
`unionFV` Coercion -> FV
tyCoFVsOfCo Coercion
kind_co) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
tyCoFVsOfCo (FunCo { fco_mult :: Coercion -> Coercion
fco_mult = Coercion
w, fco_arg :: Coercion -> Coercion
fco_arg = Coercion
co1, fco_res :: Coercion -> Coercion
fco_res = Coercion
co2 }) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
= (Coercion -> FV
tyCoFVsOfCo Coercion
co1 FV -> FV -> FV
`unionFV` Coercion -> FV
tyCoFVsOfCo Coercion
co2 FV -> FV -> FV
`unionFV` Coercion -> FV
tyCoFVsOfCo Coercion
w) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
tyCoFVsOfCo (CoVarCo Var
v) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
= Var -> FV
tyCoFVsOfCoVar Var
v InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
tyCoFVsOfCo (HoleCo CoercionHole
h) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
= Var -> FV
tyCoFVsOfCoVar (CoercionHole -> Var
coHoleCoVar CoercionHole
h) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
tyCoFVsOfCo (AxiomCo CoAxiomRule
_ [Coercion]
cs) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc = [Coercion] -> FV
tyCoFVsOfCos [Coercion]
cs InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
tyCoFVsOfCo (UnivCo { uco_lty :: Coercion -> Type
uco_lty = Type
t1, uco_rty :: Coercion -> Type
uco_rty = Type
t2, uco_deps :: Coercion -> [Coercion]
uco_deps = [Coercion]
deps}) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
= ([Coercion] -> FV
tyCoFVsOfCos [Coercion]
deps FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType Type
t1
FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType Type
t2) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
tyCoFVsOfCo (SymCo Coercion
co) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
tyCoFVsOfCo (TransCo Coercion
co1 Coercion
co2) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc = (Coercion -> FV
tyCoFVsOfCo Coercion
co1 FV -> FV -> FV
`unionFV` Coercion -> FV
tyCoFVsOfCo Coercion
co2) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
tyCoFVsOfCo (SelCo CoSel
_ Coercion
co) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
tyCoFVsOfCo (LRCo LeftOrRight
_ Coercion
co) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
tyCoFVsOfCo (InstCo Coercion
co Coercion
arg) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc = (Coercion -> FV
tyCoFVsOfCo Coercion
co FV -> FV -> FV
`unionFV` Coercion -> FV
tyCoFVsOfCo Coercion
arg) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
tyCoFVsOfCo (KindCo Coercion
co) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
tyCoFVsOfCo (SubCo Coercion
co) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc = Coercion -> FV
tyCoFVsOfCo Coercion
co InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
tyCoFVsOfCoVar :: CoVar -> FV
tyCoFVsOfCoVar :: Var -> FV
tyCoFVsOfCoVar Var
v InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
= (Var -> FV
unitFV Var
v FV -> FV -> FV
`unionFV` Type -> FV
tyCoFVsOfType (Var -> Type
varType Var
v)) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
tyCoFVsOfCos :: [Coercion] -> FV
tyCoFVsOfCos :: [Coercion] -> FV
tyCoFVsOfCos [] InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc = FV
emptyFV InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
tyCoFVsOfCos (Coercion
co:[Coercion]
cos) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc = (Coercion -> FV
tyCoFVsOfCo Coercion
co FV -> FV -> FV
`unionFV` [Coercion] -> FV
tyCoFVsOfCos [Coercion]
cos) InterestingVarFun
fv_cand VarSet
in_scope ([Var], VarSet)
acc
almostDevoidCoVarOfCo :: CoVar -> Coercion -> Bool
almostDevoidCoVarOfCo :: Var -> Coercion -> Bool
almostDevoidCoVarOfCo Var
cv Coercion
co =
Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co Var
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 {}) Var
_ = Bool
True
almost_devoid_co_var_of_co (GRefl {}) Var
_ = Bool
True
almost_devoid_co_var_of_co (TyConAppCo Role
_ TyCon
_ [Coercion]
cos) Var
cv
= [Coercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [Coercion]
cos Var
cv
almost_devoid_co_var_of_co (AppCo Coercion
co Coercion
arg) Var
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co Var
cv
Bool -> Bool -> Bool
&& Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
arg Var
cv
almost_devoid_co_var_of_co (ForAllCo { fco_tcv :: Coercion -> Var
fco_tcv = Var
v, fco_kind :: Coercion -> Coercion
fco_kind = Coercion
kind_co, fco_body :: Coercion -> Coercion
fco_body = Coercion
co }) Var
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
kind_co Var
cv
Bool -> Bool -> Bool
&& (Var
v Var -> InterestingVarFun
forall a. Eq a => a -> a -> Bool
== Var
cv Bool -> Bool -> Bool
|| Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co Var
cv)
almost_devoid_co_var_of_co (FunCo { fco_mult :: Coercion -> Coercion
fco_mult = Coercion
w, fco_arg :: Coercion -> Coercion
fco_arg = Coercion
co1, fco_res :: Coercion -> Coercion
fco_res = Coercion
co2 }) Var
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
w Var
cv
Bool -> Bool -> Bool
&& Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co1 Var
cv
Bool -> Bool -> Bool
&& Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co2 Var
cv
almost_devoid_co_var_of_co (CoVarCo Var
v) Var
cv = Var
v Var -> InterestingVarFun
forall a. Eq a => a -> a -> Bool
/= Var
cv
almost_devoid_co_var_of_co (HoleCo CoercionHole
h) Var
cv = (CoercionHole -> Var
coHoleCoVar CoercionHole
h) Var -> InterestingVarFun
forall a. Eq a => a -> a -> Bool
/= Var
cv
almost_devoid_co_var_of_co (AxiomCo CoAxiomRule
_ [Coercion]
cs) Var
cv
= [Coercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [Coercion]
cs Var
cv
almost_devoid_co_var_of_co (UnivCo { uco_lty :: Coercion -> Type
uco_lty = Type
t1, uco_rty :: Coercion -> Type
uco_rty = Type
t2, uco_deps :: Coercion -> [Coercion]
uco_deps = [Coercion]
deps }) Var
cv
= [Coercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [Coercion]
deps 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 Coercion
co) Var
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co Var
cv
almost_devoid_co_var_of_co (TransCo Coercion
co1 Coercion
co2) Var
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co1 Var
cv
Bool -> Bool -> Bool
&& Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co2 Var
cv
almost_devoid_co_var_of_co (SelCo CoSel
_ Coercion
co) Var
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co Var
cv
almost_devoid_co_var_of_co (LRCo LeftOrRight
_ Coercion
co) Var
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co Var
cv
almost_devoid_co_var_of_co (InstCo Coercion
co Coercion
arg) Var
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co Var
cv
Bool -> Bool -> Bool
&& Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
arg Var
cv
almost_devoid_co_var_of_co (KindCo Coercion
co) Var
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co Var
cv
almost_devoid_co_var_of_co (SubCo Coercion
co) Var
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co Var
cv
almost_devoid_co_var_of_cos :: [Coercion] -> CoVar -> Bool
almost_devoid_co_var_of_cos :: [Coercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [] Var
_ = Bool
True
almost_devoid_co_var_of_cos (Coercion
co:[Coercion]
cos) Var
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co Var
cv
Bool -> Bool -> Bool
&& [Coercion] -> InterestingVarFun
almost_devoid_co_var_of_cos [Coercion]
cos Var
cv
almost_devoid_co_var_of_type :: Type -> CoVar -> Bool
almost_devoid_co_var_of_type :: Type -> InterestingVarFun
almost_devoid_co_var_of_type (TyVarTy Var
_) Var
_ = Bool
True
almost_devoid_co_var_of_type (TyConApp TyCon
_ [Type]
tys) Var
cv
= [Type] -> InterestingVarFun
almost_devoid_co_var_of_types [Type]
tys Var
cv
almost_devoid_co_var_of_type (LitTy {}) Var
_ = Bool
True
almost_devoid_co_var_of_type (AppTy Type
fun Type
arg) 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 FunTyFlag
_ Type
w Type
arg Type
res) Var
cv
= Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
w Var
cv
Bool -> Bool -> Bool
&& 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 Var
v ForAllTyFlag
_) Type
ty) 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 Type
ty Coercion
co) Var
cv
= Type -> InterestingVarFun
almost_devoid_co_var_of_type Type
ty Var
cv
Bool -> Bool -> Bool
&& Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
co Var
cv
almost_devoid_co_var_of_type (CoercionTy Coercion
co) Var
cv
= Coercion -> InterestingVarFun
almost_devoid_co_var_of_co Coercion
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 [] Var
_ = Bool
True
almost_devoid_co_var_of_types (Type
ty:[Type]
tys) 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
visVarsOfType :: Type -> Pair TyCoVarSet
visVarsOfType :: Type -> Pair VarSet
visVarsOfType Type
orig_ty = VarSet -> VarSet -> Pair VarSet
forall a. a -> a -> Pair a
Pair VarSet
invis_vars VarSet
vis_vars
where
Pair VarSet
invis_vars1 VarSet
vis_vars = Type -> Pair VarSet
go Type
orig_ty
invis_vars :: VarSet
invis_vars = VarSet
invis_vars1 VarSet -> VarSet -> VarSet
`minusVarSet` VarSet
vis_vars
go :: Type -> Pair VarSet
go (TyVarTy Var
tv) = VarSet -> VarSet -> Pair VarSet
forall a. a -> a -> Pair a
Pair (Type -> VarSet
tyCoVarsOfType (Type -> VarSet) -> Type -> VarSet
forall a b. (a -> b) -> a -> b
$ Var -> Type
tyVarKind Var
tv) (Var -> VarSet
unitVarSet Var
tv)
go (AppTy Type
t1 Type
t2) = Type -> Pair VarSet
go Type
t1 Pair VarSet -> Pair VarSet -> Pair VarSet
forall a. Monoid a => a -> a -> a
`mappend` Type -> Pair VarSet
go Type
t2
go (TyConApp TyCon
tc [Type]
tys) = TyCon -> [Type] -> Pair VarSet
go_tc TyCon
tc [Type]
tys
go (FunTy FunTyFlag
_ Type
w Type
t1 Type
t2) = Type -> Pair VarSet
go Type
w Pair VarSet -> Pair VarSet -> Pair VarSet
forall a. Monoid a => a -> a -> a
`mappend` Type -> Pair VarSet
go Type
t1 Pair VarSet -> Pair VarSet -> Pair VarSet
forall a. Monoid a => a -> a -> a
`mappend` Type -> Pair VarSet
go Type
t2
go (ForAllTy (Bndr Var
tv ForAllTyFlag
_) Type
ty)
= ((VarSet -> Var -> VarSet
`delVarSet` Var
tv) (VarSet -> VarSet) -> Pair VarSet -> Pair VarSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Pair VarSet
go Type
ty) Pair VarSet -> Pair VarSet -> Pair VarSet
forall a. Monoid a => a -> a -> a
`mappend`
(VarSet -> Pair VarSet
invisible (Type -> VarSet
tyCoVarsOfType (Type -> VarSet) -> Type -> VarSet
forall a b. (a -> b) -> a -> b
$ Var -> Type
varType Var
tv))
go (LitTy {}) = Pair VarSet
forall a. Monoid a => a
mempty
go (CastTy Type
ty Coercion
co) = Type -> Pair VarSet
go Type
ty Pair VarSet -> Pair VarSet -> Pair VarSet
forall a. Monoid a => a -> a -> a
`mappend` VarSet -> Pair VarSet
invisible (Coercion -> VarSet
tyCoVarsOfCo Coercion
co)
go (CoercionTy Coercion
co) = VarSet -> Pair VarSet
invisible (VarSet -> Pair VarSet) -> VarSet -> Pair VarSet
forall a b. (a -> b) -> a -> b
$ Coercion -> VarSet
tyCoVarsOfCo Coercion
co
invisible :: VarSet -> Pair VarSet
invisible VarSet
vs = VarSet -> VarSet -> Pair VarSet
forall a. a -> a -> Pair a
Pair VarSet
vs VarSet
emptyVarSet
go_tc :: TyCon -> [Type] -> Pair VarSet
go_tc TyCon
tc [Type]
tys = let ([Type]
invis, [Type]
vis) = TyCon -> [Type] -> ([Type], [Type])
partitionInvisibleTypes TyCon
tc [Type]
tys in
VarSet -> Pair VarSet
invisible ([Type] -> VarSet
tyCoVarsOfTypes [Type]
invis) Pair VarSet -> Pair VarSet -> Pair VarSet
forall a. Monoid a => a -> a -> a
`mappend` (Type -> Pair VarSet) -> [Type] -> Pair VarSet
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Type -> Pair VarSet
go [Type]
vis
visVarsOfTypes :: [Type] -> Pair TyCoVarSet
visVarsOfTypes :: [Type] -> Pair VarSet
visVarsOfTypes = (Type -> Pair VarSet) -> [Type] -> Pair VarSet
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Type -> Pair VarSet
visVarsOfType
isInjectiveInType :: TyVar -> Type -> Bool
isInjectiveInType :: Var -> Type -> Bool
isInjectiveInType Var
tv Type
ty
= Type -> Bool
go Type
ty
where
go :: Type -> Bool
go Type
ty | Just Type
ty' <- Type -> Maybe Type
rewriterView Type
ty = Type -> Bool
go Type
ty'
go (TyVarTy Var
tv') = Var
tv' Var -> InterestingVarFun
forall a. Eq a => a -> a -> Bool
== Var
tv
go (AppTy Type
f Type
a) = Type -> Bool
go Type
f Bool -> Bool -> Bool
|| Type -> Bool
go Type
a
go (FunTy FunTyFlag
_ Type
w Type
ty1 Type
ty2) = Type -> Bool
go Type
w Bool -> Bool -> Bool
|| Type -> Bool
go Type
ty1 Bool -> Bool -> Bool
|| Type -> Bool
go Type
ty2
go (TyConApp TyCon
tc [Type]
tys) = TyCon -> [Type] -> Bool
go_tc TyCon
tc [Type]
tys
go (ForAllTy (Bndr Var
tv' ForAllTyFlag
_) Type
ty) = Type -> Bool
go (Var -> Type
tyVarKind Var
tv')
Bool -> Bool -> Bool
|| (Var
tv Var -> InterestingVarFun
forall a. Eq a => a -> a -> Bool
/= Var
tv' Bool -> Bool -> Bool
&& Type -> Bool
go Type
ty)
go LitTy{} = Bool
False
go (CastTy Type
ty Coercion
_) = Type -> Bool
go Type
ty
go CoercionTy{} = Bool
False
go_tc :: TyCon -> [Type] -> Bool
go_tc TyCon
tc [Type]
tys | TyCon -> Bool
isTypeFamilyTyCon TyCon
tc = Bool
False
| Bool
otherwise = (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Type -> Bool
go [Type]
tys
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
rewriterView Type
ty = Type -> FV
go Type
ty'
go (TyVarTy Var
v) = Var -> FV
unitFV Var
v FV -> FV -> FV
`unionFV` Type -> FV
go (Var -> Type
tyVarKind Var
v)
go (AppTy Type
f Type
a) = Type -> FV
go Type
f FV -> FV -> FV
`unionFV` Type -> FV
go Type
a
go (FunTy FunTyFlag
_ 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) = TyCon -> [Type] -> FV
go_tc TyCon
tc [Type]
tys
go (ForAllTy (Bndr Var
tv ForAllTyFlag
_) 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 Type
ty Coercion
_) = Type -> FV
go Type
ty
go CoercionTy{} = FV
emptyFV
go_tc :: TyCon -> [Type] -> FV
go_tc TyCon
tc [Type]
tys
| TyCon -> Bool
isTypeFamilyTyCon TyCon
tc
= if | Bool
look_under_tfs
, Injective [Bool]
flags <- TyCon -> Injectivity
tyConInjectivityInfo 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]
flags [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ Bool -> [Bool]
forall a. a -> [a]
repeat Bool
True) [Type]
tys
| Bool
otherwise
-> FV
emptyFV
| Bool
otherwise
= (Type -> FV) -> [Type] -> FV
forall a. (a -> FV) -> [a] -> FV
mapUnionFV Type -> FV
go [Type]
tys
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 Var
v) = Type -> FV
go (Var -> Type
tyVarKind Var
v)
go (AppTy Type
f Type
a) = Type -> FV
go Type
f FV -> FV -> FV
`unionFV` Type -> FV
go Type
a
go (FunTy FunTyFlag
_ 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 ForAllTyBinder
tvb Type
ty) = ForAllTyBinder -> FV -> FV
tyCoFVsBndr ForAllTyBinder
tvb (FV -> FV) -> FV -> FV
forall a b. (a -> b) -> a -> b
$ Type -> FV
go Type
ty
go LitTy{} = FV
emptyFV
go (CastTy Type
ty Coercion
co) = Coercion -> FV
tyCoFVsOfCo Coercion
co FV -> FV -> FV
`unionFV` Type -> FV
go Type
ty
go (CoercionTy Coercion
co) = Coercion -> FV
tyCoFVsOfCo Coercion
co
invisibleVarsOfTypes :: [Type] -> FV
invisibleVarsOfTypes :: [Type] -> FV
invisibleVarsOfTypes = (Type -> FV) -> [Type] -> FV
forall a. (a -> FV) -> [a] -> FV
mapUnionFV Type -> FV
invisibleVarsOfType
{-# INLINE afvFolder #-}
afvFolder :: (TyCoVar -> Bool) -> TyCoFolder TyCoVarSet DM.Any
afvFolder :: InterestingVarFun -> TyCoFolder VarSet Any
afvFolder InterestingVarFun
check_fv = TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view = Type -> Maybe Type
noView
, tcf_tyvar :: VarSet -> Var -> Any
tcf_tyvar = VarSet -> Var -> Any
do_tcv, tcf_covar :: VarSet -> Var -> Any
tcf_covar = VarSet -> Var -> Any
do_tcv
, tcf_hole :: VarSet -> CoercionHole -> Any
tcf_hole = VarSet -> CoercionHole -> Any
forall {p} {p}. p -> p -> Any
do_hole, tcf_tycobinder :: VarSet -> Var -> ForAllTyFlag -> VarSet
tcf_tycobinder = VarSet -> Var -> ForAllTyFlag -> VarSet
forall {p}. VarSet -> Var -> p -> VarSet
do_bndr }
where
do_tcv :: VarSet -> Var -> Any
do_tcv VarSet
is Var
tv = Bool -> Any
Any (Bool -> Bool
not (Var
tv Var -> VarSet -> Bool
`elemVarSet` VarSet
is) Bool -> Bool -> Bool
&& InterestingVarFun
check_fv Var
tv)
do_hole :: p -> p -> Any
do_hole p
_ p
_ = Bool -> Any
Any Bool
False
do_bndr :: VarSet -> Var -> p -> VarSet
do_bndr VarSet
is Var
tv p
_ = VarSet
is VarSet -> Var -> VarSet
`extendVarSet` Var
tv
anyFreeVarsOfType :: (TyCoVar -> Bool) -> Type -> Bool
anyFreeVarsOfType :: InterestingVarFun -> Type -> Bool
anyFreeVarsOfType InterestingVarFun
check_fv Type
ty = Any -> Bool
DM.getAny (Type -> Any
f Type
ty)
where (Type -> Any
f, [Type] -> Any
_, Coercion -> Any
_, [Coercion] -> Any
_) = TyCoFolder VarSet Any
-> VarSet
-> (Type -> Any, [Type] -> Any, Coercion -> Any, [Coercion] -> Any)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo (InterestingVarFun -> TyCoFolder VarSet Any
afvFolder InterestingVarFun
check_fv) VarSet
emptyVarSet
anyFreeVarsOfTypes :: (TyCoVar -> Bool) -> [Type] -> Bool
anyFreeVarsOfTypes :: InterestingVarFun -> [Type] -> Bool
anyFreeVarsOfTypes InterestingVarFun
check_fv [Type]
tys = Any -> Bool
DM.getAny ([Type] -> Any
f [Type]
tys)
where (Type -> Any
_, [Type] -> Any
f, Coercion -> Any
_, [Coercion] -> Any
_) = TyCoFolder VarSet Any
-> VarSet
-> (Type -> Any, [Type] -> Any, Coercion -> Any, [Coercion] -> Any)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo (InterestingVarFun -> TyCoFolder VarSet Any
afvFolder InterestingVarFun
check_fv) VarSet
emptyVarSet
anyFreeVarsOfCo :: (TyCoVar -> Bool) -> Coercion -> Bool
anyFreeVarsOfCo :: InterestingVarFun -> Coercion -> Bool
anyFreeVarsOfCo InterestingVarFun
check_fv Coercion
co = Any -> Bool
DM.getAny (Coercion -> Any
f Coercion
co)
where (Type -> Any
_, [Type] -> Any
_, Coercion -> Any
f, [Coercion] -> Any
_) = TyCoFolder VarSet Any
-> VarSet
-> (Type -> Any, [Type] -> Any, Coercion -> Any, [Coercion] -> Any)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo (InterestingVarFun -> TyCoFolder VarSet Any
afvFolder InterestingVarFun
check_fv) VarSet
emptyVarSet
noFreeVarsOfType :: Type -> Bool
noFreeVarsOfType :: Type -> Bool
noFreeVarsOfType Type
ty = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Any -> Bool
DM.getAny (Type -> Any
f Type
ty)
where (Type -> Any
f, [Type] -> Any
_, Coercion -> Any
_, [Coercion] -> Any
_) = TyCoFolder VarSet Any
-> VarSet
-> (Type -> Any, [Type] -> Any, Coercion -> Any, [Coercion] -> Any)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo (InterestingVarFun -> TyCoFolder VarSet Any
afvFolder (Bool -> InterestingVarFun
forall a b. a -> b -> a
const Bool
True)) VarSet
emptyVarSet
noFreeVarsOfTypes :: [Type] -> Bool
noFreeVarsOfTypes :: [Type] -> Bool
noFreeVarsOfTypes [Type]
tys = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Any -> Bool
DM.getAny ([Type] -> Any
f [Type]
tys)
where (Type -> Any
_, [Type] -> Any
f, Coercion -> Any
_, [Coercion] -> Any
_) = TyCoFolder VarSet Any
-> VarSet
-> (Type -> Any, [Type] -> Any, Coercion -> Any, [Coercion] -> Any)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo (InterestingVarFun -> TyCoFolder VarSet Any
afvFolder (Bool -> InterestingVarFun
forall a b. a -> b -> a
const Bool
True)) VarSet
emptyVarSet
noFreeVarsOfCo :: Coercion -> Bool
noFreeVarsOfCo :: Coercion -> Bool
noFreeVarsOfCo Coercion
co = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Any -> Bool
DM.getAny (Coercion -> Any
f Coercion
co)
where (Type -> Any
_, [Type] -> Any
_, Coercion -> Any
f, [Coercion] -> Any
_) = TyCoFolder VarSet Any
-> VarSet
-> (Type -> Any, [Type] -> Any, Coercion -> Any, [Coercion] -> Any)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo (InterestingVarFun -> TyCoFolder VarSet Any
afvFolder (Bool -> InterestingVarFun
forall a b. a -> b -> a
const Bool
True)) VarSet
emptyVarSet
scopedSort :: [TyCoVar] -> [TyCoVar]
scopedSort :: [Var] -> [Var]
scopedSort = [Var] -> [VarSet] -> [Var] -> [Var]
go [] []
where
go :: [TyCoVar]
-> [TyCoVarSet]
-> [TyCoVar]
-> [TyCoVar]
go :: [Var] -> [VarSet] -> [Var] -> [Var]
go [Var]
acc [VarSet]
_fv_list [] = [Var] -> [Var]
forall a. [a] -> [a]
reverse [Var]
acc
go [Var]
acc [VarSet]
fv_list (Var
tv:[Var]
tvs)
= [Var] -> [VarSet] -> [Var] -> [Var]
go [Var]
acc' [VarSet]
fv_list' [Var]
tvs
where
([Var]
acc', [VarSet]
fv_list') = Var -> [Var] -> [VarSet] -> ([Var], [VarSet])
insert Var
tv [Var]
acc [VarSet]
fv_list
insert :: TyCoVar
-> [TyCoVar]
-> [TyCoVarSet]
-> ([TyCoVar], [TyCoVarSet])
insert :: Var -> [Var] -> [VarSet] -> ([Var], [VarSet])
insert Var
tv [] [] = ([Var
tv], [Type -> VarSet
tyCoVarsOfType (Var -> Type
tyVarKind Var
tv)])
insert Var
tv (Var
a:[Var]
as) (VarSet
fvs:[VarSet]
fvss)
| Var
tv Var -> VarSet -> Bool
`elemVarSet` VarSet
fvs
, ([Var]
as', [VarSet]
fvss') <- Var -> [Var] -> [VarSet] -> ([Var], [VarSet])
insert Var
tv [Var]
as [VarSet]
fvss
= (Var
aVar -> [Var] -> [Var]
forall a. a -> [a] -> [a]
:[Var]
as', VarSet
fvs VarSet -> VarSet -> VarSet
`unionVarSet` VarSet
fv_tv VarSet -> [VarSet] -> [VarSet]
forall a. a -> [a] -> [a]
: [VarSet]
fvss')
| Bool
otherwise
= (Var
tvVar -> [Var] -> [Var]
forall a. a -> [a] -> [a]
:Var
aVar -> [Var] -> [Var]
forall a. a -> [a] -> [a]
:[Var]
as, VarSet
fvs VarSet -> VarSet -> VarSet
`unionVarSet` VarSet
fv_tv VarSet -> [VarSet] -> [VarSet]
forall a. a -> [a] -> [a]
: VarSet
fvs VarSet -> [VarSet] -> [VarSet]
forall a. a -> [a] -> [a]
: [VarSet]
fvss)
where
fv_tv :: VarSet
fv_tv = Type -> VarSet
tyCoVarsOfType (Var -> Type
tyVarKind Var
tv)
insert Var
_ [Var]
_ [VarSet]
_ = String -> ([Var], [VarSet])
forall a. HasCallStack => String -> a
panic String
"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
tyConsOfType :: Type -> UniqSet TyCon
tyConsOfType :: Type -> UniqSet TyCon
tyConsOfType Type
ty
= Type -> UniqSet TyCon
go Type
ty
where
go :: Type -> UniqSet TyCon
go :: Type -> UniqSet TyCon
go Type
ty | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = Type -> UniqSet TyCon
go Type
ty'
go (TyVarTy {}) = UniqSet TyCon
forall a. UniqSet a
emptyUniqSet
go (LitTy {}) = UniqSet TyCon
forall a. UniqSet a
emptyUniqSet
go (TyConApp TyCon
tc [Type]
tys) = TyCon -> UniqSet TyCon
forall {a}. Uniquable a => a -> UniqSet a
go_tc TyCon
tc UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` [Type] -> UniqSet TyCon
tyConsOfTypes [Type]
tys
go (AppTy Type
a Type
b) = Type -> UniqSet TyCon
go Type
a UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Type -> UniqSet TyCon
go Type
b
go (FunTy FunTyFlag
af Type
w Type
a Type
b) = Type -> UniqSet TyCon
go Type
w UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets`
Type -> UniqSet TyCon
go Type
a UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Type -> UniqSet TyCon
go Type
b
UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` TyCon -> UniqSet TyCon
forall {a}. Uniquable a => a -> UniqSet a
go_tc (FunTyFlag -> TyCon
funTyFlagTyCon FunTyFlag
af)
go (ForAllTy (Bndr Var
tv ForAllTyFlag
_) Type
ty) = Type -> UniqSet TyCon
go Type
ty UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Type -> UniqSet TyCon
go (Var -> Type
varType Var
tv)
go (CastTy Type
ty Coercion
co) = Type -> UniqSet TyCon
go Type
ty UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Coercion -> UniqSet TyCon
go_co Coercion
co
go (CoercionTy Coercion
co) = Coercion -> UniqSet TyCon
go_co Coercion
co
go_co :: Coercion -> UniqSet TyCon
go_co (Refl Type
ty) = Type -> UniqSet TyCon
go Type
ty
go_co (GRefl Role
_ Type
ty MCoercion
mco) = Type -> UniqSet TyCon
go Type
ty UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` MCoercion -> UniqSet TyCon
go_mco MCoercion
mco
go_co (TyConAppCo Role
_ TyCon
tc [Coercion]
args) = TyCon -> UniqSet TyCon
forall {a}. Uniquable a => a -> UniqSet a
go_tc TyCon
tc UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` [Coercion] -> UniqSet TyCon
go_cos [Coercion]
args
go_co (AppCo Coercion
co Coercion
arg) = Coercion -> UniqSet TyCon
go_co Coercion
co UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Coercion -> UniqSet TyCon
go_co Coercion
arg
go_co (ForAllCo { fco_kind :: Coercion -> Coercion
fco_kind = Coercion
kind_co, fco_body :: Coercion -> Coercion
fco_body = Coercion
co })
= Coercion -> UniqSet TyCon
go_co Coercion
kind_co UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Coercion -> UniqSet TyCon
go_co Coercion
co
go_co (FunCo { fco_mult :: Coercion -> Coercion
fco_mult = Coercion
m, fco_arg :: Coercion -> Coercion
fco_arg = Coercion
a, fco_res :: Coercion -> Coercion
fco_res = Coercion
r })
= Coercion -> UniqSet TyCon
go_co Coercion
m UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Coercion -> UniqSet TyCon
go_co Coercion
a UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Coercion -> UniqSet TyCon
go_co Coercion
r
go_co (AxiomCo CoAxiomRule
ax [Coercion]
args) = CoAxiomRule -> UniqSet TyCon
go_ax CoAxiomRule
ax UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` [Coercion] -> UniqSet TyCon
go_cos [Coercion]
args
go_co (UnivCo { uco_lty :: Coercion -> Type
uco_lty = Type
t1, uco_rty :: Coercion -> Type
uco_rty = Type
t2, uco_deps :: Coercion -> [Coercion]
uco_deps = [Coercion]
cos })
= Type -> UniqSet TyCon
go Type
t1 UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Type -> UniqSet TyCon
go Type
t2 UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` [Coercion] -> UniqSet TyCon
go_cos [Coercion]
cos
go_co (CoVarCo {}) = UniqSet TyCon
forall a. UniqSet a
emptyUniqSet
go_co (HoleCo {}) = UniqSet TyCon
forall a. UniqSet a
emptyUniqSet
go_co (SymCo Coercion
co) = Coercion -> UniqSet TyCon
go_co Coercion
co
go_co (TransCo Coercion
co1 Coercion
co2) = Coercion -> UniqSet TyCon
go_co Coercion
co1 UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Coercion -> UniqSet TyCon
go_co Coercion
co2
go_co (SelCo CoSel
_ Coercion
co) = Coercion -> UniqSet TyCon
go_co Coercion
co
go_co (LRCo LeftOrRight
_ Coercion
co) = Coercion -> UniqSet TyCon
go_co Coercion
co
go_co (InstCo Coercion
co Coercion
arg) = Coercion -> UniqSet TyCon
go_co Coercion
co UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Coercion -> UniqSet TyCon
go_co Coercion
arg
go_co (KindCo Coercion
co) = Coercion -> UniqSet TyCon
go_co Coercion
co
go_co (SubCo Coercion
co) = Coercion -> UniqSet TyCon
go_co Coercion
co
go_mco :: MCoercion -> UniqSet TyCon
go_mco MCoercion
MRefl = UniqSet TyCon
forall a. UniqSet a
emptyUniqSet
go_mco (MCo Coercion
co) = Coercion -> UniqSet TyCon
go_co Coercion
co
go_cos :: [Coercion] -> UniqSet TyCon
go_cos [Coercion]
cos = (Coercion -> UniqSet TyCon -> UniqSet TyCon)
-> UniqSet TyCon -> [Coercion] -> UniqSet TyCon
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
unionUniqSets (UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon)
-> (Coercion -> UniqSet TyCon)
-> Coercion
-> UniqSet TyCon
-> UniqSet TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Coercion -> UniqSet TyCon
go_co) UniqSet TyCon
forall a. UniqSet a
emptyUniqSet [Coercion]
cos
go_tc :: a -> UniqSet a
go_tc a
tc = a -> UniqSet a
forall {a}. Uniquable a => a -> UniqSet a
unitUniqSet a
tc
go_ax :: CoAxiomRule -> UniqSet TyCon
go_ax (UnbranchedAxiom CoAxiom Unbranched
ax) = TyCon -> UniqSet TyCon
forall {a}. Uniquable a => a -> UniqSet a
go_tc (TyCon -> UniqSet TyCon) -> TyCon -> UniqSet TyCon
forall a b. (a -> b) -> a -> b
$ CoAxiom Unbranched -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom Unbranched
ax
go_ax (BranchedAxiom CoAxiom Branched
ax BranchIndex
_) = TyCon -> UniqSet TyCon
forall {a}. Uniquable a => a -> UniqSet a
go_tc (TyCon -> UniqSet TyCon) -> TyCon -> UniqSet TyCon
forall a b. (a -> b) -> a -> b
$ CoAxiom Branched -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom Branched
ax
go_ax (BuiltInFamRew BuiltInFamRewrite
bif) = TyCon -> UniqSet TyCon
forall {a}. Uniquable a => a -> UniqSet a
go_tc (TyCon -> UniqSet TyCon) -> TyCon -> UniqSet TyCon
forall a b. (a -> b) -> a -> b
$ BuiltInFamRewrite -> TyCon
bifrw_fam_tc BuiltInFamRewrite
bif
go_ax (BuiltInFamInj {}) = UniqSet TyCon
forall a. UniqSet a
emptyUniqSet
tyConsOfTypes :: [Type] -> UniqSet TyCon
tyConsOfTypes :: [Type] -> UniqSet TyCon
tyConsOfTypes [Type]
tys = (Type -> UniqSet TyCon -> UniqSet TyCon)
-> UniqSet TyCon -> [Type] -> UniqSet TyCon
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon
forall a. UniqSet a -> UniqSet a -> UniqSet a
unionUniqSets (UniqSet TyCon -> UniqSet TyCon -> UniqSet TyCon)
-> (Type -> UniqSet TyCon)
-> Type
-> UniqSet TyCon
-> UniqSet TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> UniqSet TyCon
tyConsOfType) UniqSet TyCon
forall a. UniqSet a
emptyUniqSet [Type]
tys
occCheckExpand :: [Var] -> Type -> Maybe Type
occCheckExpand :: [Var] -> Type -> Maybe Type
occCheckExpand [Var]
vs_to_avoid Type
ty
| [Var] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
vs_to_avoid
= Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty
| Bool
otherwise
= (VarSet, VarEnv Var) -> Type -> Maybe Type
go ([Var] -> VarSet
mkVarSet [Var]
vs_to_avoid, VarEnv Var
forall a. VarEnv a
emptyVarEnv) Type
ty
where
go :: (VarSet, VarEnv TyCoVar) -> Type -> Maybe Type
go :: (VarSet, VarEnv Var) -> Type -> Maybe Type
go (VarSet
as, VarEnv Var
env) ty :: Type
ty@(TyVarTy Var
tv)
| Just Var
tv' <- VarEnv Var -> Var -> Maybe Var
forall a. VarEnv a -> Var -> Maybe a
lookupVarEnv VarEnv Var
env Var
tv = Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> Type
mkTyVarTy Var
tv')
| VarSet -> InterestingVarFun
bad_var_occ VarSet
as Var
tv = Maybe Type
forall a. Maybe a
Nothing
| Bool
otherwise = Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty
go (VarSet, VarEnv Var)
_ ty :: Type
ty@(LitTy {}) = Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty
go (VarSet, VarEnv Var)
cxt (AppTy Type
ty1 Type
ty2) = do { ty1' <- (VarSet, VarEnv Var) -> Type -> Maybe Type
go (VarSet, VarEnv Var)
cxt Type
ty1
; ty2' <- go cxt ty2
; return (AppTy ty1' ty2') }
go (VarSet, VarEnv Var)
cxt ty :: Type
ty@(FunTy FunTyFlag
_ Type
w Type
ty1 Type
ty2)
= do { w' <- (VarSet, VarEnv Var) -> Type -> Maybe Type
go (VarSet, VarEnv Var)
cxt Type
w
; ty1' <- go cxt ty1
; ty2' <- go cxt ty2
; return (ty { ft_mult = w', ft_arg = ty1', ft_res = ty2' }) }
go cxt :: (VarSet, VarEnv Var)
cxt@(VarSet
as, VarEnv Var
env) (ForAllTy (Bndr Var
tv ForAllTyFlag
vis) Type
body_ty)
= do { ki' <- (VarSet, VarEnv Var) -> Type -> Maybe Type
go (VarSet, VarEnv Var)
cxt (Var -> Type
varType Var
tv)
; let tv' = Var -> Type -> Var
setVarType Var
tv Type
ki'
env' = VarEnv Var -> Var -> Var -> VarEnv Var
forall a. VarEnv a -> Var -> a -> VarEnv a
extendVarEnv VarEnv Var
env Var
tv Var
tv'
as' = VarSet
as VarSet -> Var -> VarSet
`delVarSet` Var
tv
; body' <- go (as', env') body_ty
; return (ForAllTy (Bndr tv' vis) body') }
go (VarSet, VarEnv Var)
cxt ty :: Type
ty@(TyConApp TyCon
tc [Type]
tys)
= case (Type -> Maybe Type) -> [Type] -> Maybe [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((VarSet, VarEnv Var) -> Type -> Maybe Type
go (VarSet, VarEnv Var)
cxt) [Type]
tys of
Just [Type]
tys' -> Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon -> [Type] -> Type
TyConApp TyCon
tc [Type]
tys')
Maybe [Type]
Nothing | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty -> (VarSet, VarEnv Var) -> Type -> Maybe Type
go (VarSet, VarEnv Var)
cxt Type
ty'
| Bool
otherwise -> Maybe Type
forall a. Maybe a
Nothing
go (VarSet, VarEnv Var)
cxt (CastTy Type
ty Coercion
co) = do { ty' <- (VarSet, VarEnv Var) -> Type -> Maybe Type
go (VarSet, VarEnv Var)
cxt Type
ty
; co' <- go_co cxt co
; return (CastTy ty' co') }
go (VarSet, VarEnv Var)
cxt (CoercionTy Coercion
co) = do { co' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv Var)
cxt Coercion
co
; return (CoercionTy co') }
bad_var_occ :: VarSet -> Var -> Bool
bad_var_occ :: VarSet -> InterestingVarFun
bad_var_occ VarSet
vs_to_avoid Var
v
= Var
v Var -> VarSet -> Bool
`elemVarSet` VarSet
vs_to_avoid
Bool -> Bool -> Bool
|| Type -> VarSet
tyCoVarsOfType (Var -> Type
varType Var
v) VarSet -> VarSet -> Bool
`intersectsVarSet` VarSet
vs_to_avoid
go_mco :: (VarSet, VarEnv Var) -> MCoercion -> Maybe MCoercion
go_mco (VarSet, VarEnv Var)
_ MCoercion
MRefl = MCoercion -> Maybe MCoercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return MCoercion
MRefl
go_mco (VarSet, VarEnv Var)
ctx (MCo Coercion
co) = Coercion -> MCoercion
MCo (Coercion -> MCoercion) -> Maybe Coercion -> Maybe MCoercion
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv Var)
ctx Coercion
co
go_co :: (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv Var)
cxt (Refl Type
ty) = do { ty' <- (VarSet, VarEnv Var) -> Type -> Maybe Type
go (VarSet, VarEnv Var)
cxt Type
ty
; return (Refl ty') }
go_co (VarSet, VarEnv Var)
cxt (GRefl Role
r Type
ty MCoercion
mco) = do { mco' <- (VarSet, VarEnv Var) -> MCoercion -> Maybe MCoercion
go_mco (VarSet, VarEnv Var)
cxt MCoercion
mco
; ty' <- go cxt ty
; return (GRefl r ty' mco') }
go_co (VarSet, VarEnv Var)
cxt (TyConAppCo Role
r TyCon
tc [Coercion]
args) = do { args' <- (Coercion -> Maybe Coercion) -> [Coercion] -> Maybe [Coercion]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv Var)
cxt) [Coercion]
args
; return (TyConAppCo r tc args') }
go_co (VarSet, VarEnv Var)
cxt (AppCo Coercion
co Coercion
arg) = do { co' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv Var)
cxt Coercion
co
; arg' <- go_co cxt arg
; return (AppCo co' arg') }
go_co (VarSet, VarEnv Var)
cxt (SymCo Coercion
co) = do { co' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv Var)
cxt Coercion
co
; return (SymCo co') }
go_co (VarSet, VarEnv Var)
cxt (TransCo Coercion
co1 Coercion
co2) = do { co1' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv Var)
cxt Coercion
co1
; co2' <- go_co cxt co2
; return (TransCo co1' co2') }
go_co (VarSet, VarEnv Var)
cxt (SelCo CoSel
n Coercion
co) = do { co' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv Var)
cxt Coercion
co
; return (SelCo n co') }
go_co (VarSet, VarEnv Var)
cxt (LRCo LeftOrRight
lr Coercion
co) = do { co' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv Var)
cxt Coercion
co
; return (LRCo lr co') }
go_co (VarSet, VarEnv Var)
cxt (InstCo Coercion
co Coercion
arg) = do { co' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv Var)
cxt Coercion
co
; arg' <- go_co cxt arg
; return (InstCo co' arg') }
go_co (VarSet, VarEnv Var)
cxt (KindCo Coercion
co) = do { co' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv Var)
cxt Coercion
co
; return (KindCo co') }
go_co (VarSet, VarEnv Var)
cxt (SubCo Coercion
co) = do { co' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv Var)
cxt Coercion
co
; return (SubCo co') }
go_co cxt :: (VarSet, VarEnv Var)
cxt@(VarSet
as, VarEnv Var
env) co :: Coercion
co@(ForAllCo { fco_tcv :: Coercion -> Var
fco_tcv = Var
tv, fco_kind :: Coercion -> Coercion
fco_kind = Coercion
kind_co, fco_body :: Coercion -> Coercion
fco_body = Coercion
body_co })
= do { kind_co' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv Var)
cxt Coercion
kind_co
; let tv' = Var -> Type -> Var
setVarType Var
tv (Type -> Var) -> Type -> Var
forall a b. (a -> b) -> a -> b
$
HasDebugCallStack => Coercion -> Type
Coercion -> Type
coercionLKind Coercion
kind_co'
env' = VarEnv Var -> Var -> Var -> VarEnv Var
forall a. VarEnv a -> Var -> a -> VarEnv a
extendVarEnv VarEnv Var
env Var
tv Var
tv'
as' = VarSet
as VarSet -> Var -> VarSet
`delVarSet` Var
tv
; body' <- go_co (as', env') body_co
; return (co { fco_tcv = tv', fco_kind = kind_co', fco_body = body' }) }
go_co (VarSet, VarEnv Var)
cxt co :: Coercion
co@(FunCo { fco_mult :: Coercion -> Coercion
fco_mult = Coercion
w, fco_arg :: Coercion -> Coercion
fco_arg = Coercion
co1 ,fco_res :: Coercion -> Coercion
fco_res = Coercion
co2 })
= do { co1' <- (VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv Var)
cxt Coercion
co1
; co2' <- go_co cxt co2
; w' <- go_co cxt w
; return (co { fco_mult = w', fco_arg = co1', fco_res = co2' })}
go_co (VarSet
as,VarEnv Var
env) co :: Coercion
co@(CoVarCo Var
c)
| Just Var
c' <- VarEnv Var -> Var -> Maybe Var
forall a. VarEnv a -> Var -> Maybe a
lookupVarEnv VarEnv Var
env Var
c = Coercion -> Maybe Coercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> Coercion
CoVarCo Var
c')
| VarSet -> InterestingVarFun
bad_var_occ VarSet
as Var
c = Maybe Coercion
forall a. Maybe a
Nothing
| Bool
otherwise = Coercion -> Maybe Coercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Coercion
co
go_co (VarSet
as,VarEnv Var
_) co :: Coercion
co@(HoleCo CoercionHole
h)
| VarSet -> InterestingVarFun
bad_var_occ VarSet
as (CoercionHole -> Var
ch_co_var CoercionHole
h) = Maybe Coercion
forall a. Maybe a
Nothing
| Bool
otherwise = Coercion -> Maybe Coercion
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Coercion
co
go_co (VarSet, VarEnv Var)
cxt (AxiomCo CoAxiomRule
ax [Coercion]
cs) = do { cs' <- (Coercion -> Maybe Coercion) -> [Coercion] -> Maybe [Coercion]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((VarSet, VarEnv Var) -> Coercion -> Maybe Coercion
go_co (VarSet, VarEnv Var)
cxt) [Coercion]
cs
; return (AxiomCo ax cs') }
go_co (VarSet, VarEnv Var)
cxt co :: Coercion
co@(UnivCo { uco_lty :: Coercion -> Type
uco_lty = Type
ty1, uco_rty :: Coercion -> Type
uco_rty = Type
ty2, uco_deps :: Coercion -> [Coercion]
uco_deps = [Coercion]
cos })
= do { ty1' <- (VarSet, VarEnv Var) -> Type -> Maybe Type
go (VarSet, VarEnv Var)
cxt Type
ty1
; ty2' <- go cxt ty2
; cos' <- mapM (go_co cxt) cos
; return (co { uco_lty = ty1', uco_rty = ty2', uco_deps = cos' }) }