ghc-9.4.0.20220721: The GHC API
Safe HaskellSafe-Inferred
LanguageHaskell2010

GHC.Core.TyCo.Subst

Description

Substitution into types and coercions.

Synopsis

Substitutions

data TCvSubst Source #

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.

Instances

Instances details
Outputable TCvSubst Source # 
Instance details

Defined in GHC.Core.TyCo.Subst

Methods

ppr :: 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

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.

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

getTCvSubstRangeFVs :: TCvSubst -> VarSet Source #

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

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!

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

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

substTyWith :: HasDebugCallStack => [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 :: HasDebugCallStack => [TyVar] -> [Type] -> Coercion -> Coercion Source #

Coercion substitution, see zipTvSubst

substTy :: HasDebugCallStack => 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 :: HasDebugCallStack => TCvSubst -> [Type] -> [Type] Source #

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

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

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

substCo :: HasDebugCallStack => TCvSubst -> Coercion -> Coercion Source #

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

substCos :: HasDebugCallStack => TCvSubst -> [Coercion] -> [Coercion] Source #

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

checkValidSubst :: HasDebugCallStack => 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].