TyCoSubst

Substitution into types and coercions.

Substitutions

data TCvSubst

Type & coercion substitution

The following invariants must hold of a TCvSubst:

1. The in-scope set is needed only to guide the generation of fresh uniques
2. In particular, the kind of the type variables in the in-scope set is not relevant
3. 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

Outputable TCvSubst

Defined in TyCoSubst

Methods

ppr :: TCvSubst -> SDoc

pprPrec :: Rational -> TCvSubst -> SDoc

type TvSubstEnv = TyVarEnv Type

A substitution of Types for TyVars and Kinds for KindVars

type CvSubstEnv = CoVarEnv Coercion

A substitution of Coercions for CoVars

emptyTvSubstEnv :: TvSubstEnv

emptyCvSubstEnv :: CvSubstEnv

composeTCvSubstEnv :: InScopeSet -> (TvSubstEnv, CvSubstEnv) -> (TvSubstEnv, CvSubstEnv) -> (TvSubstEnv, CvSubstEnv)

(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

Composes two substitutions, applying the second one provided first, like in function composition.

emptyTCvSubst :: TCvSubst

mkEmptyTCvSubst :: InScopeSet -> TCvSubst

isEmptyTCvSubst :: TCvSubst -> Bool

mkTCvSubst :: InScopeSet -> (TvSubstEnv, CvSubstEnv) -> TCvSubst

mkTvSubst :: InScopeSet -> TvSubstEnv -> TCvSubst

Make a TCvSubst with specified tyvar subst and empty covar subst

mkCvSubst :: InScopeSet -> CvSubstEnv -> TCvSubst

Make a TCvSubst with specified covar subst and empty tyvar subst

getTvSubstEnv :: TCvSubst -> TvSubstEnv

getCvSubstEnv :: TCvSubst -> CvSubstEnv

getTCvInScope :: TCvSubst -> InScopeSet

getTCvSubstRangeFVs :: TCvSubst -> VarSet

Returns the free variables of the types in the range of a substitution as a non-deterministic set.

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

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

zipTvSubst :: HasDebugCallStack => [TyVar] -> [Type] -> TCvSubst

Generates the in-scope set for the TCvSubst from the types in the incoming environment. No CoVars, please!

zipCvSubst :: HasDebugCallStack => [CoVar] -> [Coercion] -> TCvSubst

Generates the in-scope set for the TCvSubst from the types in the incoming environment. No TyVars, please!

zipTCvSubst :: HasDebugCallStack => [TyCoVar] -> [Type] -> TCvSubst

mkTvSubstPrs :: [(TyVar, Type)] -> TCvSubst

Generates the in-scope set for the TCvSubst from the types in the incoming environment. No CoVars, please!

substTyWith :: HasCallStack => [TyVar] -> [Type] -> Type -> Type

Type substitution, see zipTvSubst

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

Substitute covars within a type

substTysWith :: [TyVar] -> [Type] -> [Type] -> [Type]

Type substitution, see zipTvSubst

substTysWithCoVars :: [CoVar] -> [Coercion] -> [Type] -> [Type]

Type substitution, see zipTvSubst

substCoWith :: HasCallStack => [TyVar] -> [Type] -> Coercion -> Coercion

Coercion substitution, see zipTvSubst

substTy :: HasCallStack => TCvSubst -> Type -> Type

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

substTyAddInScope :: TCvSubst -> Type -> Type

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

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]

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

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

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

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

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

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]

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

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

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

lookupTyVar :: TCvSubst -> TyVar -> Maybe Type

substCo :: HasCallStack => TCvSubst -> Coercion -> Coercion

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

substCos :: HasCallStack => TCvSubst -> [Coercion] -> [Coercion]

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

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

This checks if the substitution satisfies the invariant from Note [The substitution invariant].

isValidTCvSubst :: TCvSubst -> Bool

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