Safe Haskell	None
Language	Haskell2010

GHC.Core.TyCo.Subst

Contents

Substitutions

Description

Substitution into types and coercions.

Synopsis

data Subst = Subst InScopeSet IdSubstEnv TvSubstEnv CvSubstEnv
type TvSubstEnv = TyVarEnv Type
type CvSubstEnv = CoVarEnv Coercion
type IdSubstEnv = IdEnv CoreExpr
emptyIdSubstEnv :: IdSubstEnv
emptyTvSubstEnv :: TvSubstEnv
emptyCvSubstEnv :: CvSubstEnv
composeTCvSubst :: Subst -> Subst -> Subst
emptySubst :: Subst
mkEmptySubst :: InScopeSet -> Subst
isEmptyTCvSubst :: Subst -> Bool
isEmptySubst :: Subst -> Bool
mkSubst :: InScopeSet -> TvSubstEnv -> CvSubstEnv -> IdSubstEnv -> Subst
mkTvSubst :: InScopeSet -> TvSubstEnv -> Subst
mkCvSubst :: InScopeSet -> CvSubstEnv -> Subst
mkIdSubst :: InScopeSet -> IdSubstEnv -> Subst
getTvSubstEnv :: Subst -> TvSubstEnv
getIdSubstEnv :: Subst -> IdSubstEnv
getCvSubstEnv :: Subst -> CvSubstEnv
getSubstInScope :: Subst -> InScopeSet
setInScope :: Subst -> InScopeSet -> Subst
getSubstRangeTyCoFVs :: Subst -> VarSet
isInScope :: Var -> Subst -> Bool
elemSubst :: Var -> Subst -> Bool
notElemSubst :: Var -> Subst -> Bool
zapSubst :: Subst -> Subst
extendSubstInScope :: Subst -> Var -> Subst
extendSubstInScopeList :: Subst -> [Var] -> Subst
extendSubstInScopeSet :: Subst -> VarSet -> Subst
extendTCvSubst :: Subst -> TyCoVar -> Type -> Subst
extendTCvSubstWithClone :: Subst -> TyCoVar -> TyCoVar -> Subst
extendCvSubst :: Subst -> CoVar -> Coercion -> Subst
extendCvSubstWithClone :: Subst -> CoVar -> CoVar -> Subst
extendTvSubst :: Subst -> TyVar -> Type -> Subst
extendTvSubstBinderAndInScope :: Subst -> PiTyBinder -> Type -> Subst
extendTvSubstWithClone :: Subst -> TyVar -> TyVar -> Subst
extendTvSubstList :: Subst -> [(TyVar, Type)] -> Subst
extendTvSubstAndInScope :: Subst -> TyVar -> Type -> Subst
extendTCvSubstList :: Subst -> [Var] -> [Type] -> Subst
unionSubst :: Subst -> Subst -> Subst
zipTyEnv :: HasDebugCallStack => [TyVar] -> [Type] -> TvSubstEnv
zipCoEnv :: HasDebugCallStack => [CoVar] -> [Coercion] -> CvSubstEnv
zipTvSubst :: HasDebugCallStack => [TyVar] -> [Type] -> Subst
zipCvSubst :: HasDebugCallStack => [CoVar] -> [Coercion] -> Subst
zipTCvSubst :: HasDebugCallStack => [TyCoVar] -> [Type] -> Subst
mkTvSubstPrs :: [(TyVar, Type)] -> Subst
substTyWith :: HasDebugCallStack => [TyVar] -> [Type] -> Type -> Type
substTyWithCoVars :: [CoVar] -> [Coercion] -> Type -> Type
substTysWith :: [TyVar] -> [Type] -> [Type] -> [Type]
substTysWithCoVars :: [CoVar] -> [Coercion] -> [Type] -> [Type]
substCoWith :: HasDebugCallStack => [TyVar] -> [Type] -> Coercion -> Coercion
substTy :: HasDebugCallStack => Subst -> Type -> Type
substTyAddInScope :: Subst -> Type -> Type
substScaledTy :: HasDebugCallStack => Subst -> Scaled Type -> Scaled Type
substTyUnchecked :: Subst -> Type -> Type
substTysUnchecked :: Subst -> [Type] -> [Type]
substScaledTysUnchecked :: Subst -> [Scaled Type] -> [Scaled Type]
substThetaUnchecked :: Subst -> ThetaType -> ThetaType
substTyWithUnchecked :: [TyVar] -> [Type] -> Type -> Type
substScaledTyUnchecked :: HasDebugCallStack => Subst -> Scaled Type -> Scaled Type
substCoUnchecked :: Subst -> Coercion -> Coercion
substCoWithUnchecked :: [TyVar] -> [Type] -> Coercion -> Coercion
substTyWithInScope :: InScopeSet -> [TyVar] -> [Type] -> Type -> Type
substTys :: HasDebugCallStack => Subst -> [Type] -> [Type]
substScaledTys :: HasDebugCallStack => Subst -> [Scaled Type] -> [Scaled Type]
substTheta :: HasDebugCallStack => Subst -> ThetaType -> ThetaType
lookupTyVar :: Subst -> TyVar -> Maybe Type
substCo :: HasDebugCallStack => Subst -> Coercion -> Coercion
substCos :: HasDebugCallStack => Subst -> [Coercion] -> [Coercion]
substCoVar :: Subst -> CoVar -> Coercion
substCoVars :: Subst -> [CoVar] -> [Coercion]
lookupCoVar :: Subst -> Var -> Maybe Coercion
cloneTyVarBndr :: Subst -> TyVar -> Unique -> (Subst, TyVar)
cloneTyVarBndrs :: Subst -> [TyVar] -> UniqSupply -> (Subst, [TyVar])
substVarBndr :: HasDebugCallStack => Subst -> TyCoVar -> (Subst, TyCoVar)
substVarBndrs :: HasDebugCallStack => Subst -> [TyCoVar] -> (Subst, [TyCoVar])
substTyVarBndr :: HasDebugCallStack => Subst -> TyVar -> (Subst, TyVar)
substTyVarBndrs :: HasDebugCallStack => Subst -> [TyVar] -> (Subst, [TyVar])
substCoVarBndr :: HasDebugCallStack => Subst -> CoVar -> (Subst, CoVar)
substTyVar :: Subst -> TyVar -> Type
substTyVars :: Subst -> [TyVar] -> [Type]
substTyVarToTyVar :: HasDebugCallStack => Subst -> TyVar -> TyVar
substTyCoVars :: Subst -> [TyCoVar] -> [Type]
substTyCoBndr :: Subst -> PiTyBinder -> (Subst, PiTyBinder)
substForAllCoBndr :: Subst -> TyCoVar -> KindCoercion -> (Subst, TyCoVar, Coercion)
substVarBndrUsing :: (Subst -> Type -> Type) -> Subst -> TyCoVar -> (Subst, TyCoVar)
substForAllCoBndrUsing :: Bool -> (Coercion -> Coercion) -> Subst -> TyCoVar -> KindCoercion -> (Subst, TyCoVar, KindCoercion)
checkValidSubst :: HasDebugCallStack => Subst -> [Type] -> [Coercion] -> a -> a
isValidTCvSubst :: Subst -> Bool

Substitutions

data Subst Source #

Type & coercion & id substitution

The Subst data type defined in this module contains substitution for tyvar, covar and id. However, operations on IdSubstEnv (mapping from Id to CoreExpr) that require the definition of the Expr data type are defined in GHC.Core.Subst to avoid circular module dependency.

Constructors

Subst InScopeSet IdSubstEnv TvSubstEnv CvSubstEnv

Instances

Instances details

Outputable Subst Source #
Instance details Defined in GHC.Core.TyCo.Subst Methods ppr :: Subst -> 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

type IdSubstEnv = IdEnv CoreExpr Source #

A substitution of Exprs for non-coercion Ids

emptyIdSubstEnv :: IdSubstEnv Source #

emptyTvSubstEnv :: TvSubstEnv Source #

emptyCvSubstEnv :: CvSubstEnv Source #

composeTCvSubst :: Subst -> Subst -> Subst Source #

Composes two substitutions, applying the second one provided first, like in function composition. This function leaves IdSubstEnv untouched because IdSubstEnv is not used during substitution for types.

emptySubst :: Subst Source #

mkEmptySubst :: InScopeSet -> Subst Source #

isEmptyTCvSubst :: Subst -> Bool Source #

Checks whether the tyvar and covar environments are empty. This function should be used over isEmptySubst when substituting for types, because types currently do not contain expressions; we can safely disregard the expression environment when deciding whether to skip a substitution. Using isEmptyTCvSubst gives us a non-trivial performance boost (up to 70% less allocation for T18223)

isEmptySubst :: Subst -> Bool Source #

mkSubst :: InScopeSet -> TvSubstEnv -> CvSubstEnv -> IdSubstEnv -> Subst Source #

mkTvSubst :: InScopeSet -> TvSubstEnv -> Subst Source #

Make a TCvSubst with specified tyvar subst and empty covar subst

mkCvSubst :: InScopeSet -> CvSubstEnv -> Subst Source #

Make a TCvSubst with specified covar subst and empty tyvar subst

mkIdSubst :: InScopeSet -> IdSubstEnv -> Subst Source #

getTvSubstEnv :: Subst -> TvSubstEnv Source #

getIdSubstEnv :: Subst -> IdSubstEnv Source #

getCvSubstEnv :: Subst -> CvSubstEnv Source #

getSubstInScope :: Subst -> InScopeSet Source #

Find the in-scope set: see Note [The substitution invariant]

setInScope :: Subst -> InScopeSet -> Subst Source #

getSubstRangeTyCoFVs :: Subst -> VarSet Source #

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

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

elemSubst :: Var -> Subst -> Bool Source #

notElemSubst :: Var -> Subst -> Bool Source #

zapSubst :: Subst -> Subst Source #

Remove all substitutions that might have been built up while preserving the in-scope set originally called zapSubstEnv

extendSubstInScope :: Subst -> Var -> Subst Source #

Add the Var to the in-scope set

extendSubstInScopeList :: Subst -> [Var] -> Subst Source #

Add the Vars to the in-scope set: see also extendInScope

extendSubstInScopeSet :: Subst -> VarSet -> Subst Source #

Add the Vars to the in-scope set: see also extendInScope

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

extendTCvSubstWithClone :: Subst -> TyCoVar -> TyCoVar -> Subst Source #

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

Add a substitution from a CoVar to a Coercion to the Subst: you must ensure that the in-scope set satisfies Note [The substitution invariant] after extending the substitution like this

extendCvSubstWithClone :: Subst -> CoVar -> CoVar -> Subst Source #

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

Add a substitution for a TyVar to the Subst The TyVar *must* be a real TyVar, and not a CoVar You must ensure that the in-scope set is such that Note [The substitution invariant] holds after extending the substitution like this.

extendTvSubstBinderAndInScope :: Subst -> PiTyBinder -> Type -> Subst Source #

extendTvSubstWithClone :: Subst -> TyVar -> TyVar -> Subst Source #

extendTvSubstList :: Subst -> [(TyVar, Type)] -> Subst Source #

Adds multiple TyVar substitutions to the Subst: see also extendTvSubst

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

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

unionSubst :: Subst -> Subst -> Subst Source #

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

The InScopeSet is just a thunk so with a bit of luck it'll never be evaluated

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

zipTvSubst :: HasDebugCallStack => [TyVar] -> [Type] -> Subst Source #

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

zipCvSubst :: HasDebugCallStack => [CoVar] -> [Coercion] -> Subst Source #

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

zipTCvSubst :: HasDebugCallStack => [TyCoVar] -> [Type] -> Subst Source #

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

Generates the in-scope set for the TCvSubst from the types in the incoming environment. No CoVars, please! The InScopeSet is just a thunk so with a bit of luck it'll never be evaluated

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 => Subst -> Type -> Type Source #

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

substTyAddInScope :: Subst -> 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 :: HasDebugCallStack => Subst -> Scaled Type -> Scaled Type Source #

substTyUnchecked :: Subst -> 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 :: Subst -> [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.

substScaledTysUnchecked :: Subst -> [Scaled Type] -> [Scaled Type] Source #

substThetaUnchecked :: Subst -> 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 :: HasDebugCallStack => Subst -> Scaled Type -> Scaled Type Source #

substCoUnchecked :: Subst -> 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 => Subst -> [Type] -> [Type] Source #

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

substScaledTys :: HasDebugCallStack => Subst -> [Scaled Type] -> [Scaled Type] Source #

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

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

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

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

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

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

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

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

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

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

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

cloneTyVarBndrs :: Subst -> [TyVar] -> UniqSupply -> (Subst, [TyVar]) Source #

substVarBndr :: HasDebugCallStack => Subst -> TyCoVar -> (Subst, TyCoVar) Source #

substVarBndrs :: HasDebugCallStack => Subst -> [TyCoVar] -> (Subst, [TyCoVar]) Source #

substTyVarBndr :: HasDebugCallStack => Subst -> TyVar -> (Subst, TyVar) Source #

substTyVarBndrs :: HasDebugCallStack => Subst -> [TyVar] -> (Subst, [TyVar]) Source #

substCoVarBndr :: HasDebugCallStack => Subst -> CoVar -> (Subst, CoVar) Source #

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

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

substTyVarToTyVar :: HasDebugCallStack => Subst -> TyVar -> TyVar Source #

substTyCoVars :: Subst -> [TyCoVar] -> [Type] Source #

substTyCoBndr :: Subst -> PiTyBinder -> (Subst, PiTyBinder) Source #

substForAllCoBndr :: Subst -> TyCoVar -> KindCoercion -> (Subst, TyCoVar, Coercion) Source #

substVarBndrUsing :: (Subst -> Type -> Type) -> Subst -> TyCoVar -> (Subst, TyCoVar) Source #

substForAllCoBndrUsing :: Bool -> (Coercion -> Coercion) -> Subst -> TyCoVar -> KindCoercion -> (Subst, TyCoVar, KindCoercion) Source #

checkValidSubst :: HasDebugCallStack => Subst -> [Type] -> [Coercion] -> a -> a Source #

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

isValidTCvSubst :: Subst -> 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]. TODO: take into account ids and rename as isValidSubst