GHC.Core.Reduction

Reductions

data Reduction

A Reduction is the result of an operation that rewrites a type ty_in. The Reduction includes the rewritten type ty_out and a Coercion co such that co :: ty_in ~ ty_out, where the role of the coercion is determined by the context. That is, the LHS type of the coercion is the original type ty_in, while its RHS type is the rewritten type ty_out.

A Reduction is always homogeneous, unless it is wrapped inside a HetReduction, which separately stores the kind coercion.

See Note [The Reduction type].

Constructors

Reduction

Fields

• reductionCoercion :: Coercion
• reductionReducedType :: !Type

Instances

Outputable Reduction

Defined in GHC.Core.Reduction

Methods

ppr :: Reduction -> SDoc

type ReductionN = Reduction

A Reduction in which the Coercion has Nominal role.

type ReductionR = Reduction

A Reduction in which the Coercion has Representational role.

data HetReduction

Stores a heterogeneous reduction.

The stored kind coercion must relate the kinds of the stored reduction. That is, in HetReduction (Reduction co xi) kco, we must have:

 co :: ty ~ xi
kco :: typeKind ty ~ typeKind xi

Constructors

HetReduction Reduction MCoercionN

data Reductions

A collection of Reductions where the coercions and the types are stored separately.

Use unzipRedns to obtain Reductions from a list of Reductions.

This datatype is used in mkAppRedns, mkClassPredRedns and mkTyConAppRedn, which expect separate types and coercions.

Invariant: the two stored lists are of the same length, and the RHS type of each coercion is the corresponding type.

Constructors

Reductions [Coercion] [Type]

mkReduction :: Coercion -> Type -> Reduction

Create a Reduction from a pair of a Coercion and a 'Type.

Pre-condition: the RHS type of the coercion matches the provided type (perhaps up to zonking).

Use coercionRedn when you only have the coercion.

mkReductions :: [Coercion] -> [Type] -> Reductions

Create Reductions from individual lists of coercions and types.

The lists should be of the same length, and the RHS type of each coercion should match the specified type in the other list.

mkHetReduction

Arguments

:: Reduction

heterogeneous reduction

-> MCoercionN

kind coercion

-> HetReduction

Create a heterogeneous reduction.

Pre-condition: the provided kind coercion (second argument) relates the kinds of the stored reduction. That is, if the coercion stored in the Reduction is of the form

co :: ty ~ xi

Then the kind coercion supplied must be of the form:

kco :: typeKind ty ~ typeKind xi

coercionRedn :: Coercion -> Reduction

Turn a Coercion into a Reduction by inspecting the RHS type of the coercion.

Prefer using mkReduction when you already know the RHS type of the coercion, to avoid computing it anew.

reductionOriginalType :: Reduction -> Type

Get the original, unreduced type corresponding to a Reduction.

This is obtained by computing the LHS kind of the stored coercion, which may be slow.

downgradeRedn

Arguments

:: Role

desired role

-> Role

current role

-> Reduction

-> Reduction

Downgrade the role of the coercion stored in the Reduction.

mkSubRedn :: Reduction -> Reduction

Downgrade the role of the coercion stored in the Reduction, from Nominal to Representational.

mkTransRedn :: Coercion -> Reduction -> Reduction

Compose a reduction with a coercion on the left.

Pre-condition: the provided coercion's RHS type must match the LHS type of the coercion that is stored in the reduction.

mkCoherenceRightRedn :: Role -> Reduction -> CoercionN -> Reduction

Apply a cast to the result of a Reduction.

Given a Reduction ty1 ~co1~> (ty2 :: k2) and a kind coercion kco with LHS kind k2, produce a new Reduction ty1 ~co2~> ( ty2 |> kco ) of the given Role (which must match the role of the coercion stored in the Reduction argument).

mkCoherenceRightMRedn :: Role -> Reduction -> MCoercionN -> Reduction

Apply a cast to the result of a Reduction, using an MCoercionN.

Given a Reduction ty1 ~co1~> (ty2 :: k2) and a kind coercion mco with LHS kind k2, produce a new Reduction ty1 ~co2~> ( ty2 |> mco ) of the given Role (which must match the role of the coercion stored in the Reduction argument).

mkCastRedn1

Arguments

:: Role

-> Type

original type

-> CoercionN

coercion to cast with

-> Reduction

rewritten type, with rewriting coercion

-> Reduction

Apply a cast to a Reduction, casting both the original and the reduced type.

Given cast_co and Reduction ty ~co~> xi, this function returns the Reduction (ty |> cast_co) ~return_co~> (xi |> cast_co) of the given Role (which must match the role of the coercion stored in the Reduction argument).

Pre-condition: the Type passed in is the same as the LHS type of the coercion stored in the Reduction.

mkCastRedn2

Arguments

:: Role

-> Type

original type

-> CoercionN

coercion to cast with on the left

-> Reduction

rewritten type, with rewriting coercion

-> CoercionN

coercion to cast with on the right

-> Reduction

Apply casts on both sides of a Reduction (of the given Role).

Use mkCastRedn1 when you want to cast both the original and reduced types in a Reduction using the same coercion.

Pre-condition: the Type passed in is the same as the LHS type of the coercion stored in the Reduction.

mkReflRedn :: Role -> Type -> Reduction

The reflexive reduction.

mkGReflRightRedn :: Role -> Type -> CoercionN -> Reduction

Create a Reduction from a kind cast, in which the casted type is the rewritten type.

Given ty :: k1, mco :: k1 ~ k2, produces the Reduction ty ~res_co~> (ty |> mco) at the given Role.

mkGReflRightMRedn :: Role -> Type -> MCoercionN -> Reduction

Create a Reduction from a kind cast, in which the casted type is the rewritten type.

Given ty :: k1, mco :: k1 ~ k2, produces the Reduction ty ~res_co~> (ty |> mco) at the given Role.

mkGReflLeftRedn :: Role -> Type -> CoercionN -> Reduction

Create a Reduction from a kind cast, in which the casted type is the original (non-rewritten) type.

Given ty :: k1, mco :: k1 ~ k2, produces the Reduction (ty |> mco) ~res_co~> ty at the given Role.

mkGReflLeftMRedn :: Role -> Type -> MCoercionN -> Reduction

Create a Reduction from a kind cast, in which the casted type is the original (non-rewritten) type.

Given ty :: k1, mco :: k1 ~ k2, produces the Reduction (ty |> mco) ~res_co~> ty at the given Role.

mkAppRedn :: Reduction -> Reduction -> Reduction

Apply one Reduction to another.

Combines mkAppCo and mkAppTy.

mkAppRedns :: Reduction -> Reductions -> Reduction

Combines mkAppCos and mkAppTys.

mkFunRedn

Arguments

:: Role

-> FunTyFlag

-> ReductionN

multiplicity reduction

-> Reduction

argument reduction

-> Reduction

result reduction

-> Reduction

Create a function Reduction.

Combines mkFunCo and mkFunTy.

mkForAllRedn

Arguments

:: ForAllTyFlag

-> TyVar

-> ReductionN

kind reduction

-> Reduction

body reduction

-> Reduction

Create a Reduction associated to a Π type, from a kind Reduction and a body Reduction.

Combines mkForAllCo and mkForAllTy.

mkHomoForAllRedn :: [TyVarBinder] -> Reduction -> Reduction

Create a Reduction of a quantified type from a Reduction of the body.

Combines mkHomoForAllCos and mkForAllTys.

mkTyConAppRedn :: Role -> TyCon -> Reductions -> Reduction

TyConAppCo for Reductions: combines mkTyConAppCo and mkTyConApp.

mkClassPredRedn :: Class -> Reductions -> Reduction

Reduce the arguments of a Class TyCon.

mkProofIrrelRedn

Arguments

:: Role

role of the created coercion, "r"

-> CoercionN

co :: phi1 ~N phi2

-> Coercion

g1 :: phi1

-> Coercion

g2 :: phi2

-> Reduction

res_co :: g1 ~r g2

Create a Reduction from a coercion between coercions.

Combines mkProofIrrelCo and mkCoercionTy.

mkReflCoRedn :: Role -> Coercion -> Reduction

Create a reflexive Reduction whose RHS is the given Coercion, with the specified Role.

homogeniseHetRedn :: Role -> HetReduction -> Reduction

Homogenise a heterogeneous reduction.

Given HetReduction (Reduction co xi) kco, with

 co :: ty ~ xi
kco :: typeKind(ty) ~ typeKind(xi)

this returns the homogeneous reduction:

hco :: ty ~ ( xi |> sym kco )

unzipRedns :: [Reduction] -> Reductions

Obtain Reductions from a list of Reductions by unzipping.

Rewriting type arguments

data ArgsReductions

Stores Reductions as well as a kind coercion.

Used when rewriting arguments to a type function f.

Invariant: when the stored reductions are of the form co_i :: ty_i ~ xi_i, the kind coercion is of the form kco :: typeKind (f ty_1 ... ty_n) ~ typeKind (f xi_1 ... xi_n)

The type function f depends on context.

Constructors

ArgsReductions !Reductions !MCoercionN

simplifyArgsWorker :: HasDebugCallStack => [PiTyBinder] -> Kind -> TyCoVarSet -> Infinite Role -> [Reduction] -> ArgsReductions