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

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

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

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.

Instantiates a Coercion with a Type argument.

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.

Apply a Coercion to another Coercion. The second Coercions role is given, making this more flexible than mkAppCo.

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

Make a function Coercion between two other Coercions

Make a Coercion which binds a variable within an inner Coercion

Manufacture a coercion from thin air. Needless to say, this is not usually safe, but it is used when we know we are dealing with bottom, which is one case in which it is safe. This is also used to implement the unsafeCoerce# primitive. Optimise by pushing down through type constructors.

Create a coercion constructor (axiom) suitable for the given newtype TyCon. The Name should be that of a new coercion CoAxiom, the TyVars the arguments expected by the newtype and the type the appropriate right hand side of the newtype, with the free variables a subset of those TyVars.

If co :: T ts ~ rep_ty then:

instNewTyCon_maybe T ts = Just (rep_ty, co)

Checks for a newtype, and for being saturated

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

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

Attempt to take a coercion application apart.

A substitution of Coercions for CoVars (OR TyVars, when doing a "lifting" substitution)

Substitute within a Coercion

Substitute within several Coercions

liftCoMatch is sort of inverse to liftCoSubst. In particular, if liftCoMatch vars ty co == Just s, then tyCoSubst s ty == co. That is, it matches a type against a coercion of the same "shape", and returns a lifting substitution which could have been used to produce the given coercion from the given type.

Determines syntactic equality of coercions