A Coercion is concrete evidence of the equality/convertibility of two types.

For simplicity, we have just one UnivCo that represents a coercion from some type to some other type, with (in general) no restrictions on the type. The UnivCoProvenance specifies more exactly what the coercion really is and why a program should (or shouldn't!) trust the coercion. It is reasonable to consider each constructor of UnivCoProvenance as a totally independent coercion form; their only commonality is that they don't tell you what types they coercion between. (That info is in the UnivCo constructor of Coercion.

A coercion to be filled in by the type-checker. See Note [Coercion holes]

Variable

Essentially a typed Name, that may also contain some additional information about the Var and it's use sites.

Coercion Variable

Type or Coercion Variable

If it is the case that

c :: (t1 ~ t2)

i.e. the kind of c relates t1 and t2, then coercionKind c = Pair t1 t2.

Apply coercionKind to multiple Coercions

Makes a coercion type from two types: the types whose equality is proven by the relevant Coercion

Retrieve the role from a coercion.

Get a coercion's kind and role. Why both at once? See Note [Computing a coercion kind and role]

Make a representational reflexive coercion

Make a nominal reflexive coercion

Return the left-hand type of the axiom, when the axiom is instantiated at the types given.

Instantiate the left-hand side of an unbranched axiom

Make a forall Coercion, where both types related by the coercion are quantified over the same type variable.

Create a symmetric version of the given Coercion that asserts equality between the same types but in the other "direction", so a kind of t1 ~ t2 becomes the kind t2 ~ t1.

Create a new Coercion by composing the two given Coercions transitively. (co1 ; co2)

Like mkAppCo, but allows the second coercion to be other than nominal. See Note [mkTransAppCo]. Role r3 cannot be more stringent than either r1 or r2.

Instantiates a Coercion.

Apply a Coercion to another Coercion. The second coercion must be Nominal, unless the first is Phantom. If the first is Phantom, then the second can be either Phantom or Nominal.

Applies multiple Coercions to another Coercion, from left to right. See also mkAppCo.

Apply a type constructor to a list of coercions. It is the caller's responsibility to get the roles correct on argument coercions.

Build a function Coercion from two other Coercions. That is, given co1 :: a ~ b and co2 :: x ~ y produce co :: (a -> x) ~ (b -> y).

Make nested function Coercions

Make a Coercion from a tyvar, a kind coercion, and a body coercion. The kind of the tyvar should be the left-hand kind of the kind coercion.

Make nested ForAllCos

Make a Coercion quantified over a type variable; the variable has the same type in both sides of the coercion

Like mkHomoForAllCos, but doesn't check if the inner coercion is reflexive.

Make a phantom coercion between two types. The coercion passed in must be a nominal coercion between the kinds of the types.

Make a phantom coercion between two types of the same kind.

Manufacture an unsafe coercion from thin air. Currently (May 14) this is used only to implement the unsafeCoerce# primitive. Optimise by pushing down through type constructors.

Make a coercion from a coercion hole

Make a universal coercion between two arbitrary types.

Make a "coercion between coercions".

Like downgradeRole_maybe, but panics if the change isn't a downgrade. See Note [Role twiddling functions]

If the EqRel is ReprEq, makes a SubCo; otherwise, does nothing. Note that the input coercion should always be nominal.

A CoherenceCo c1 c2 applies the coercion c2 to the left-hand type in the kind of c1. This function uses sym to get the coercion on the right-hand type of c1. Thus, if c1 :: s ~ t, then mkCoherenceRightCo c1 c2 has the kind (s ~ (t |> c2)) down through type constructors. The second coercion must be representational.

An explicitly directed synonym of mkCoherenceCo. The second coercion must be representational.

Given co :: (a :: k) ~ (b :: k') produce co' :: k ~ k'.

Creates a new coercion with both of its types casted by different casts castCoercionKind g h1 h2, where g :: t1 ~ t2, has type (t1 |> h1) ~ (t2 |> h2) The second and third coercions must be nominal.

If co :: T ts ~ rep_ty then:

instNewTyCon_maybe T ts = Just (rep_ty, co)

Checks for a newtype, and for being saturated

A function to check if we can reduce a type by one step. Used with topNormaliseTypeX.

The result of stepping in a normalisation function. See topNormaliseTypeX.

Try one stepper and then try the next, if the first doesn't make progress. So if it returns NS_Done, it means that both steppers are satisfied

A NormaliseStepper that unwraps newtypes, careful not to fall into a loop. If it would fall into a loop, it produces NS_Abort.

Sometimes we want to look through a newtype and get its associated coercion. This function strips off newtype layers enough to reveal something that isn't a newtype. Specifically, here's the invariant:

topNormaliseNewType_maybe rec_nts ty = Just (co, ty')

then (a) co : ty0 ~ ty'. (b) ty' is not a newtype.

The function returns Nothing for non-newtypes, or unsaturated applications

This function does *not* look through type families, because it has no access to the type family environment. If you do have that at hand, consider to use topNormaliseType_maybe, which should be a drop-in replacement for topNormaliseNewType_maybe If topNormliseNewType_maybe ty = Just (co, ty'), then co : ty ~R ty'

A general function for normalising the top-level of a type. It continues to use the provided NormaliseStepper until that function fails, and then this function returns. The roles of the coercions produced by the NormaliseStepper must all be the same, which is the role returned from the call to topNormaliseTypeX.

Typically ev is Coercion.

If topNormaliseTypeX step plus ty = Just (ev, ty') then ty ~ev1~ t1 ~ev2~ t2 ... ~evn~ ty' and ev = ev1 plus ev2 plus ... plus evn If it returns Nothing then no newtype unwrapping could happen

This breaks a Coercion with type T A B C ~ T D E F into a list of Coercions of kinds A ~ D, B ~ E and E ~ F. Hence:

decomposeCo 3 c = [nth 0 c, nth 1 c, nth 2 c]

Attempts to obtain the type variable underlying a Coercion

Attempts to tease a coercion apart into a type constructor and the application of a number of coercion arguments to that constructor

Attempt to take a coercion application apart.

Converts a coercion to be nominal, if possible. See Note [Role twiddling functions]

Tests if this coercion is obviously reflexive. Guaranteed to work very quickly. Sometimes a coercion can be reflexive, but not obviously so. c.f. isReflexiveCo

Returns the type coerced if this coercion is reflexive. Guaranteed to work very quickly. Sometimes a coercion can be reflexive, but not obviously so. c.f. isReflexiveCo_maybe

Slowly checks if the coercion is reflexive. Don't call this in a loop, as it walks over the entire coercion.

Extracts the coerced type from a reflexive coercion. This potentially walks over the entire coercion, so avoid doing this in a loop.

Extract a covar, if possible. This check is dirty. Be ashamed of yourself. (It's dirty because it cares about the structure of a coercion, which is morally reprehensible.)

Get a deterministic set of the vars free in a coercion

A substitution of Coercions for CoVars

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

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

Coercion substitution, see zipTvSubst

liftCoSubst role lc ty produces a coercion (at role role) that coerces between lc_left(ty) and lc_right(ty), where lc_left is a substitution mapping type variables to the left-hand types of the mapped coercions in lc, and similar for lc_right.

Extend a lifting context with a new type mapping.

Is a var in the domain of a lifting context?

Erase the environments in a lifting context

Like substForAllCoBndr, but works on a lifting context

Extract the underlying substitution from the LiftingContext

Get the InScopeSet from a LiftingContext

Apply "sym" to all coercions in a LiftCoEnv

Syntactic equality of coercions

Compare two Coercions, with respect to an RnEnv2

like mkKindCo, but aggressively & recursively optimizes to avoid using a KindCo constructor. The output role is nominal.