A Coercion represents a Type something should be coerced to.

The key type representing kinds in the compiler. Invariant: a kind is always in one of these forms:

 FunTy k1 k2
 TyConApp PrimTyCon [...]
 TyVar kv   -- (during inference only)
 ForAll ... -- (for top-level coercions)

Essentially funResultTy on kinds

Find the result Kind of a type synonym, after applying it to its arity number of type variables Actually this function works fine on data types too, but they'd always return *, so we never need to ask

Essentially splitFunTys on kinds

Essentially splitFunTysN on kinds

See Type for details of the distinction between these Kinds

Is this a kind (i.e. a type-of-types)?

Is this a super-kind (i.e. a type-of-kinds)?

Given two kinds k1 and k2, creates the Kind k1 -> k2

Iterated application of mkArrowKind

True of any sub-kind of ArgTypeKind

True of any sub-kind of OpenTypeKind (i.e. anything except arrow)

k1 `isSubKind` k2 checks that k1 <: k2

Used when generalising: default kind ? and ?? to *. See Type for more information on what that means

kc1 `isSubKindCon` kc2 checks that kc1 <: kc2

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

(mkCoPredTy s t r) produces the type: (s~t) => r

If it is the case that

 c :: (t1 ~ t2)

i.e. the kind of c is a CoercionKind relating t1 and t2, then coercionKind c = (t1, t2).

Apply coercionKind to multiple Coercions

Creates a type equality predicate

Splits apart a type equality predicate, if the supplied PredType is one. Panics otherwise

Tests whether a type is just a type equality predicate

Make a coercion from the specified coercion TyCon and the Type arguments to that coercion. Try to use the mk*Coercion family of functions instead of using this function if possible

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 exploiting transitivity on the two given Coercions.

From an application Coercion build a Coercion that asserts the equality of the functions on either side of the type equality. So if c has kind f x ~ g y then:

 mkLeftCoercion c :: f ~ g

From an application Coercion build a Coercion that asserts the equality of the arguments on either side of the type equality. So if c has kind f x ~ g y then:

 mkLeftCoercion c :: x ~ y

Instantiates a Coercion with a Type argument. If possible, it immediately performs the resulting beta-reduction, otherwise it creates a suspended instantiation.

Apply a Coercion to another Coercion, which is presumably a Coercion constructor of some kind

Apply a type constructor to a list of coercions.

Make a function Coercion between two other Coercions

Make a Coercion which binds a variable within an inner Coercion

As mkInstCoercion, but instantiates the coercion with a number of type arguments, left-to-right

Manufacture a coercion from this 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 implement the unsafeCoerce# primitive. Optimise by pushing down through type constructors

Create a coercion suitable for the given TyCon. The Name should be that of a new coercion TyCon, 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.

Create a coercion identifying a data, newtype or type representation type and its family instance. It has the form Co tvs :: F ts ~ R tvs, where Co is the coercion tycon built here, F the family tycon and R the (derived) representation tycon.

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

Coercion type constructors: avoid using these directly and instead use the mk*Coercion and split*Coercion family of functions if possible.

Each coercion TyCon is built with the special CoercionTyCon record and carries its own kinding rule. Such CoercionTyCons must be fully applied by any TyConApp in which they are applied, however they may also be over applied (see example above) and the kinding function must deal with this.

Sometimes we want to look through a newtype and get its associated coercion. This function only strips *one layer* of newtype off, so the caller will usually call itself recursively. Furthermore, this function should only be applied to types of kind *, hence the newtype is always saturated. If co : ty ~ ty' then:

 splitNewTypeRepCo_maybe ty = Just (ty', co)

The function returns Nothing for non-newtypes or fully-transparent newtypes.

If co :: T ts ~ rep_ty then:

 instNewTyCon_maybe T ts = Just (rep_ty, co)

This breaks a Coercion with CoercionKind 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 = [right (left (left c)), right (left c), right c]

Determines syntactic equality of coercions

CoercionI represents a lifted ordinary Coercion, in that it can represent either one of:

1. A proper Coercion
2. The identity coercion

Smart constructor for sym on CoercionI, see also mkSymCoercion

Smart constructor for trans on CoercionI, see also mkTransCoercion

Smart constructor for type constructor application on CoercionI, see also mkAppCoercion

Smart constructor for honest-to-god Coercion application on CoercionI, see also mkAppCoercion

Smart constructor for quantified Coercions on CoercionI, see also mkForAllCoercion

Return either the Coercion contained within the CoercionI or the given Type if the CoercionI is the identity Coercion

Smart constructor for class Coercions on CoercionI. Satisfies:

 mkClassPPredCoI cls tys cois :: PredTy (cls tys) ~ PredTy (cls (tys `cast` cois))

Smart constructor for implicit parameter Coercions on CoercionI. Similar to mkClassPPredCoI

Smart constructor for type equality Coercions on CoercionI. Similar to mkClassPPredCoI