Safe Haskell	None
Language	Haskell2010

TyCoSubst

Contents

Substitutions

Description

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
mkTyCoInScopeSet :: [Type] -> [Coercion] -> InScopeSet
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
substTyUnchecked :: TCvSubst -> Type -> Type
substTysUnchecked :: TCvSubst -> [Type] -> [Type]
substThetaUnchecked :: TCvSubst -> ThetaType -> ThetaType
substTyWithUnchecked :: [TyVar] -> [Type] -> Type -> Type
substCoUnchecked :: TCvSubst -> Coercion -> Coercion
substCoWithUnchecked :: [TyVar] -> [Type] -> Coercion -> Coercion
substTyWithInScope :: InScopeSet -> [TyVar] -> [Type] -> Type -> Type
substTys :: HasCallStack => TCvSubst -> [Type] -> [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

data TCvSubst Source #

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.

Constructors

TCvSubst InScopeSet TvSubstEnv CvSubstEnv

Instances

Instances details

Outputable TCvSubst #
Instance details Defined in TyCoSubst Methods ppr :: TCvSubst -> SDoc Source # pprPrec :: Rational -> TCvSubst -> SDoc Source #

type TvSubstEnv = TyVarEnv Type Source #

A substitution of Types for TyVars and Kinds for KindVars

type CvSubstEnv = CoVarEnv Coercion Source #

A substitution of Coercions for CoVars

emptyTvSubstEnv :: TvSubstEnv Source #

emptyCvSubstEnv :: CvSubstEnv Source #

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.

emptyTCvSubst :: TCvSubst Source #

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.

isInScope :: Var -> TCvSubst -> Bool Source #

notElemTCvSubst :: Var -> TCvSubst -> Bool Source #

setTvSubstEnv :: TCvSubst -> TvSubstEnv -> TCvSubst Source #

setCvSubstEnv :: TCvSubst -> CvSubstEnv -> TCvSubst Source #

zapTCvSubst :: TCvSubst -> TCvSubst Source #

extendTCvInScope :: TCvSubst -> Var -> TCvSubst Source #

extendTCvInScopeList :: TCvSubst -> [Var] -> TCvSubst Source #

extendTCvInScopeSet :: TCvSubst -> VarSet -> TCvSubst Source #

extendTCvSubst :: TCvSubst -> TyCoVar -> Type -> TCvSubst Source #

extendTCvSubstWithClone :: TCvSubst -> TyCoVar -> TyCoVar -> TCvSubst Source #

extendCvSubst :: TCvSubst -> CoVar -> Coercion -> TCvSubst Source #

extendCvSubstWithClone :: TCvSubst -> CoVar -> CoVar -> TCvSubst Source #

extendTvSubst :: TCvSubst -> TyVar -> Type -> TCvSubst Source #

extendTvSubstBinderAndInScope :: TCvSubst -> TyCoBinder -> Type -> TCvSubst Source #

extendTvSubstWithClone :: TCvSubst -> TyVar -> TyVar -> TCvSubst Source #

extendTvSubstList :: TCvSubst -> [Var] -> [Type] -> TCvSubst Source #

extendTvSubstAndInScope :: TCvSubst -> TyVar -> Type -> TCvSubst Source #

extendTCvSubstList :: TCvSubst -> [Var] -> [Type] -> TCvSubst Source #

unionTCvSubst :: TCvSubst -> TCvSubst -> TCvSubst Source #

zipTyEnv :: HasDebugCallStack => [TyVar] -> [Type] -> TvSubstEnv Source #

zipCoEnv :: HasDebugCallStack => [CoVar] -> [Coercion] -> CvSubstEnv Source #

mkTyCoInScopeSet :: [Type] -> [Coercion] -> InScopeSet Source #

Generates an in-scope set from the free variables in a list of types and a list of coercions

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

substTyWithCoVars :: [CoVar] -> [Coercion] -> Type -> Type Source #

Substitute covars within a type

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].

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 Types 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.

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 Types The substitution has to satisfy the invariants described in Note [The substitution invariant].

substTheta :: HasCallStack => TCvSubst -> ThetaType -> ThetaType Source #

Substitute within a ThetaType The substitution has to satisfy the invariants described in Note [The substitution invariant].

lookupTyVar :: TCvSubst -> TyVar -> Maybe Type Source #

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 Coercions The substitution has to satisfy the invariants described in Note [The substitution invariant].

substCoVar :: TCvSubst -> CoVar -> Coercion Source #

substCoVars :: TCvSubst -> [CoVar] -> [Coercion] Source #

lookupCoVar :: TCvSubst -> Var -> Maybe Coercion Source #

cloneTyVarBndr :: TCvSubst -> TyVar -> Unique -> (TCvSubst, TyVar) Source #

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 #

substTyVar :: TCvSubst -> TyVar -> Type Source #

substTyVars :: TCvSubst -> [TyVar] -> [Type] Source #

substTyCoVars :: TCvSubst -> [TyCoVar] -> [Type] 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].

isValidTCvSubst :: TCvSubst -> Bool Source #

When calling substTy it should be the case that the in-scope set in the substitution is a superset of the free vars of the range of the substitution. See also Note [The substitution invariant].