Safe Haskell | None |
---|---|
Language | Haskell2010 |
Substitution into types and coercions.
Synopsis
- data TCvSubst = TCvSubst InScopeSet TvSubstEnv CvSubstEnv
- type TvSubstEnv = TyVarEnv Type
- type CvSubstEnv = CoVarEnv Coercion
- emptyTvSubstEnv :: TvSubstEnv
- emptyCvSubstEnv :: CvSubstEnv
- composeTCvSubstEnv :: InScopeSet -> (TvSubstEnv, CvSubstEnv) -> (TvSubstEnv, CvSubstEnv) -> (TvSubstEnv, CvSubstEnv)
- composeTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst
- emptyTCvSubst :: TCvSubst
- mkEmptyTCvSubst :: InScopeSet -> TCvSubst
- isEmptyTCvSubst :: TCvSubst -> Bool
- mkTCvSubst :: InScopeSet -> (TvSubstEnv, CvSubstEnv) -> TCvSubst
- mkTvSubst :: InScopeSet -> TvSubstEnv -> TCvSubst
- mkCvSubst :: InScopeSet -> CvSubstEnv -> TCvSubst
- getTvSubstEnv :: TCvSubst -> TvSubstEnv
- getCvSubstEnv :: TCvSubst -> CvSubstEnv
- getTCvInScope :: TCvSubst -> InScopeSet
- getTCvSubstRangeFVs :: TCvSubst -> VarSet
- isInScope :: Var -> TCvSubst -> Bool
- notElemTCvSubst :: Var -> TCvSubst -> Bool
- setTvSubstEnv :: TCvSubst -> TvSubstEnv -> TCvSubst
- setCvSubstEnv :: TCvSubst -> CvSubstEnv -> TCvSubst
- zapTCvSubst :: TCvSubst -> TCvSubst
- extendTCvInScope :: TCvSubst -> Var -> TCvSubst
- extendTCvInScopeList :: TCvSubst -> [Var] -> TCvSubst
- extendTCvInScopeSet :: TCvSubst -> VarSet -> TCvSubst
- extendTCvSubst :: TCvSubst -> TyCoVar -> Type -> TCvSubst
- extendTCvSubstWithClone :: TCvSubst -> TyCoVar -> TyCoVar -> TCvSubst
- extendCvSubst :: TCvSubst -> CoVar -> Coercion -> TCvSubst
- extendCvSubstWithClone :: TCvSubst -> CoVar -> CoVar -> TCvSubst
- extendTvSubst :: TCvSubst -> TyVar -> Type -> TCvSubst
- extendTvSubstBinderAndInScope :: TCvSubst -> TyCoBinder -> Type -> TCvSubst
- extendTvSubstWithClone :: TCvSubst -> TyVar -> TyVar -> TCvSubst
- extendTvSubstList :: TCvSubst -> [Var] -> [Type] -> TCvSubst
- extendTvSubstAndInScope :: TCvSubst -> TyVar -> Type -> TCvSubst
- extendTCvSubstList :: TCvSubst -> [Var] -> [Type] -> TCvSubst
- unionTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst
- zipTyEnv :: HasDebugCallStack => [TyVar] -> [Type] -> TvSubstEnv
- zipCoEnv :: HasDebugCallStack => [CoVar] -> [Coercion] -> CvSubstEnv
- zipTvSubst :: HasDebugCallStack => [TyVar] -> [Type] -> TCvSubst
- zipCvSubst :: HasDebugCallStack => [CoVar] -> [Coercion] -> TCvSubst
- zipTCvSubst :: HasDebugCallStack => [TyCoVar] -> [Type] -> TCvSubst
- mkTvSubstPrs :: [(TyVar, Type)] -> TCvSubst
- substTyWith :: HasCallStack => [TyVar] -> [Type] -> Type -> Type
- substTyWithCoVars :: [CoVar] -> [Coercion] -> Type -> Type
- substTysWith :: [TyVar] -> [Type] -> [Type] -> [Type]
- substTysWithCoVars :: [CoVar] -> [Coercion] -> [Type] -> [Type]
- substCoWith :: HasCallStack => [TyVar] -> [Type] -> Coercion -> Coercion
- substTy :: HasCallStack => TCvSubst -> Type -> Type
- substTyAddInScope :: TCvSubst -> Type -> Type
- substScaledTy :: HasCallStack => TCvSubst -> Scaled Type -> Scaled Type
- substTyUnchecked :: TCvSubst -> Type -> Type
- substTysUnchecked :: TCvSubst -> [Type] -> [Type]
- substScaledTysUnchecked :: TCvSubst -> [Scaled Type] -> [Scaled Type]
- substThetaUnchecked :: TCvSubst -> ThetaType -> ThetaType
- substTyWithUnchecked :: [TyVar] -> [Type] -> Type -> Type
- substScaledTyUnchecked :: HasCallStack => TCvSubst -> Scaled Type -> Scaled Type
- substCoUnchecked :: TCvSubst -> Coercion -> Coercion
- substCoWithUnchecked :: [TyVar] -> [Type] -> Coercion -> Coercion
- substTyWithInScope :: InScopeSet -> [TyVar] -> [Type] -> Type -> Type
- substTys :: HasCallStack => TCvSubst -> [Type] -> [Type]
- substScaledTys :: HasCallStack => TCvSubst -> [Scaled Type] -> [Scaled Type]
- substTheta :: HasCallStack => TCvSubst -> ThetaType -> ThetaType
- lookupTyVar :: TCvSubst -> TyVar -> Maybe Type
- substCo :: HasCallStack => TCvSubst -> Coercion -> Coercion
- substCos :: HasCallStack => TCvSubst -> [Coercion] -> [Coercion]
- substCoVar :: TCvSubst -> CoVar -> Coercion
- substCoVars :: TCvSubst -> [CoVar] -> [Coercion]
- lookupCoVar :: TCvSubst -> Var -> Maybe Coercion
- cloneTyVarBndr :: TCvSubst -> TyVar -> Unique -> (TCvSubst, TyVar)
- cloneTyVarBndrs :: TCvSubst -> [TyVar] -> UniqSupply -> (TCvSubst, [TyVar])
- substVarBndr :: HasCallStack => TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar)
- substVarBndrs :: HasCallStack => TCvSubst -> [TyCoVar] -> (TCvSubst, [TyCoVar])
- substTyVarBndr :: HasCallStack => TCvSubst -> TyVar -> (TCvSubst, TyVar)
- substTyVarBndrs :: HasCallStack => TCvSubst -> [TyVar] -> (TCvSubst, [TyVar])
- substCoVarBndr :: HasCallStack => TCvSubst -> CoVar -> (TCvSubst, CoVar)
- substTyVar :: TCvSubst -> TyVar -> Type
- substTyVars :: TCvSubst -> [TyVar] -> [Type]
- substTyCoVars :: TCvSubst -> [TyCoVar] -> [Type]
- substForAllCoBndr :: TCvSubst -> TyCoVar -> KindCoercion -> (TCvSubst, TyCoVar, Coercion)
- substVarBndrUsing :: (TCvSubst -> Type -> Type) -> TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar)
- substForAllCoBndrUsing :: Bool -> (Coercion -> Coercion) -> TCvSubst -> TyCoVar -> KindCoercion -> (TCvSubst, TyCoVar, KindCoercion)
- checkValidSubst :: HasCallStack => TCvSubst -> [Type] -> [Coercion] -> a -> a
- isValidTCvSubst :: TCvSubst -> Bool
Substitutions
Type & coercion substitution
The following invariants must hold of a TCvSubst
:
- The in-scope set is needed only to guide the generation of fresh uniques
- In particular, the kind of the type variables in the in-scope set is not relevant
- The substitution is only applied ONCE! This is because in general such application will not reach a fixed point.
composeTCvSubstEnv :: InScopeSet -> (TvSubstEnv, CvSubstEnv) -> (TvSubstEnv, CvSubstEnv) -> (TvSubstEnv, CvSubstEnv) Source #
(compose env1 env2)(x)
is env1(env2(x))
; i.e. apply env2
then env1
.
It assumes that both are idempotent.
Typically, env1
is the refinement to a base substitution env2
composeTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst Source #
Composes two substitutions, applying the second one provided first, like in function composition.
mkEmptyTCvSubst :: InScopeSet -> TCvSubst Source #
isEmptyTCvSubst :: TCvSubst -> Bool Source #
mkTCvSubst :: InScopeSet -> (TvSubstEnv, CvSubstEnv) -> TCvSubst Source #
mkTvSubst :: InScopeSet -> TvSubstEnv -> TCvSubst Source #
Make a TCvSubst with specified tyvar subst and empty covar subst
mkCvSubst :: InScopeSet -> CvSubstEnv -> TCvSubst Source #
Make a TCvSubst with specified covar subst and empty tyvar subst
getTvSubstEnv :: TCvSubst -> TvSubstEnv Source #
getCvSubstEnv :: TCvSubst -> CvSubstEnv Source #
getTCvInScope :: TCvSubst -> InScopeSet Source #
getTCvSubstRangeFVs :: TCvSubst -> VarSet Source #
Returns the free variables of the types in the range of a substitution as a non-deterministic set.
setTvSubstEnv :: TCvSubst -> TvSubstEnv -> TCvSubst Source #
setCvSubstEnv :: TCvSubst -> CvSubstEnv -> TCvSubst Source #
zapTCvSubst :: TCvSubst -> TCvSubst Source #
extendTvSubstBinderAndInScope :: TCvSubst -> TyCoBinder -> Type -> TCvSubst Source #
zipTyEnv :: HasDebugCallStack => [TyVar] -> [Type] -> TvSubstEnv Source #
zipCoEnv :: HasDebugCallStack => [CoVar] -> [Coercion] -> CvSubstEnv Source #
zipTvSubst :: HasDebugCallStack => [TyVar] -> [Type] -> TCvSubst Source #
Generates the in-scope set for the TCvSubst
from the types in the incoming
environment. No CoVars, please!
zipCvSubst :: HasDebugCallStack => [CoVar] -> [Coercion] -> TCvSubst Source #
Generates the in-scope set for the TCvSubst
from the types in the incoming
environment. No TyVars, please!
zipTCvSubst :: HasDebugCallStack => [TyCoVar] -> [Type] -> TCvSubst Source #
mkTvSubstPrs :: [(TyVar, Type)] -> TCvSubst Source #
Generates the in-scope set for the TCvSubst
from the types in the
incoming environment. No CoVars, please!
substTyWith :: HasCallStack => [TyVar] -> [Type] -> Type -> Type Source #
Type substitution, see zipTvSubst
substTysWith :: [TyVar] -> [Type] -> [Type] -> [Type] Source #
Type substitution, see zipTvSubst
substTysWithCoVars :: [CoVar] -> [Coercion] -> [Type] -> [Type] Source #
Type substitution, see zipTvSubst
substCoWith :: HasCallStack => [TyVar] -> [Type] -> Coercion -> Coercion Source #
Coercion substitution, see zipTvSubst
substTy :: HasCallStack => TCvSubst -> Type -> Type Source #
Substitute within a Type
The substitution has to satisfy the invariants described in
Note [The substitution invariant].
substTyAddInScope :: TCvSubst -> Type -> Type Source #
Substitute within a Type
after adding the free variables of the type
to the in-scope set. This is useful for the case when the free variables
aren't already in the in-scope set or easily available.
See also Note [The substitution invariant].
substScaledTy :: HasCallStack => TCvSubst -> Scaled Type -> Scaled Type Source #
substTyUnchecked :: TCvSubst -> Type -> Type Source #
Substitute within a Type
disabling the sanity checks.
The problems that the sanity checks in substTy catch are described in
Note [The substitution invariant].
The goal of #11371 is to migrate all the calls of substTyUnchecked to
substTy and remove this function. Please don't use in new code.
substTysUnchecked :: TCvSubst -> [Type] -> [Type] Source #
Substitute within several Type
s disabling the sanity checks.
The problems that the sanity checks in substTys catch are described in
Note [The substitution invariant].
The goal of #11371 is to migrate all the calls of substTysUnchecked to
substTys and remove this function. Please don't use in new code.
substThetaUnchecked :: TCvSubst -> ThetaType -> ThetaType Source #
Substitute within a ThetaType
disabling the sanity checks.
The problems that the sanity checks in substTys catch are described in
Note [The substitution invariant].
The goal of #11371 is to migrate all the calls of substThetaUnchecked to
substTheta and remove this function. Please don't use in new code.
substTyWithUnchecked :: [TyVar] -> [Type] -> Type -> Type Source #
Type substitution, see zipTvSubst
. Disables sanity checks.
The problems that the sanity checks in substTy catch are described in
Note [The substitution invariant].
The goal of #11371 is to migrate all the calls of substTyUnchecked to
substTy and remove this function. Please don't use in new code.
substScaledTyUnchecked :: HasCallStack => TCvSubst -> Scaled Type -> Scaled Type Source #
substCoUnchecked :: TCvSubst -> Coercion -> Coercion Source #
Substitute within a Coercion
disabling sanity checks.
The problems that the sanity checks in substCo catch are described in
Note [The substitution invariant].
The goal of #11371 is to migrate all the calls of substCoUnchecked to
substCo and remove this function. Please don't use in new code.
substCoWithUnchecked :: [TyVar] -> [Type] -> Coercion -> Coercion Source #
Coercion substitution, see zipTvSubst
. Disables sanity checks.
The problems that the sanity checks in substCo catch are described in
Note [The substitution invariant].
The goal of #11371 is to migrate all the calls of substCoUnchecked to
substCo and remove this function. Please don't use in new code.
substTyWithInScope :: InScopeSet -> [TyVar] -> [Type] -> Type -> Type Source #
Substitute tyvars within a type using a known InScopeSet
.
Pre-condition: the in_scope
set should satisfy Note [The substitution
invariant]; specifically it should include the free vars of tys
,
and of ty
minus the domain of the subst.
substTys :: HasCallStack => TCvSubst -> [Type] -> [Type] Source #
Substitute within several Type
s
The substitution has to satisfy the invariants described in
Note [The substitution invariant].
substScaledTys :: HasCallStack => TCvSubst -> [Scaled Type] -> [Scaled Type] Source #
substTheta :: HasCallStack => TCvSubst -> ThetaType -> ThetaType Source #
Substitute within a ThetaType
The substitution has to satisfy the invariants described in
Note [The substitution invariant].
substCo :: HasCallStack => TCvSubst -> Coercion -> Coercion Source #
Substitute within a Coercion
The substitution has to satisfy the invariants described in
Note [The substitution invariant].
substCos :: HasCallStack => TCvSubst -> [Coercion] -> [Coercion] Source #
Substitute within several Coercion
s
The substitution has to satisfy the invariants described in
Note [The substitution invariant].
cloneTyVarBndrs :: TCvSubst -> [TyVar] -> UniqSupply -> (TCvSubst, [TyVar]) Source #
substVarBndr :: HasCallStack => TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar) Source #
substVarBndrs :: HasCallStack => TCvSubst -> [TyCoVar] -> (TCvSubst, [TyCoVar]) Source #
substTyVarBndr :: HasCallStack => TCvSubst -> TyVar -> (TCvSubst, TyVar) Source #
substTyVarBndrs :: HasCallStack => TCvSubst -> [TyVar] -> (TCvSubst, [TyVar]) Source #
substCoVarBndr :: HasCallStack => TCvSubst -> CoVar -> (TCvSubst, CoVar) Source #
substForAllCoBndr :: TCvSubst -> TyCoVar -> KindCoercion -> (TCvSubst, TyCoVar, Coercion) Source #
substVarBndrUsing :: (TCvSubst -> Type -> Type) -> TCvSubst -> TyCoVar -> (TCvSubst, TyCoVar) Source #
substForAllCoBndrUsing :: Bool -> (Coercion -> Coercion) -> TCvSubst -> TyCoVar -> KindCoercion -> (TCvSubst, TyCoVar, KindCoercion) Source #
checkValidSubst :: HasCallStack => TCvSubst -> [Type] -> [Coercion] -> a -> a Source #
This checks if the substitution satisfies the invariant from Note [The substitution invariant].