ghc-7.0.3: The GHC API

Coercion

Contents

Description

Module for (a) type kinds and (b) type coercions, as used in System FC. See CoreSyn.Expr for more on System FC and how coercions fit into it.

Coercions are represented as types, and their kinds tell what types the coercion works on. The coercion kind constructor is a special TyCon that must always be saturated, like so:

 typeKind (symCoercion type) :: TyConApp CoTyCon{...} [type, type]

Synopsis

Main data type

type Coercion = TypeSource

A Coercion represents a Type something should be coerced to.

type Kind = TypeSource

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)

Deconstructing Kinds

kindFunResult :: Kind -> KindSource

Essentially funResultTy on kinds

synTyConResKind :: TyCon -> KindSource

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

splitKindFunTys :: Kind -> ([Kind], Kind)Source

Essentially splitFunTys on kinds

splitKindFunTysN :: Int -> Kind -> ([Kind], Kind)Source

Essentially splitFunTysN on kinds

Predicates on Kinds

isOpenTypeKind :: Kind -> BoolSource

See Type for details of the distinction between these Kinds

isKind :: Kind -> BoolSource

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

isTySuperKind :: SuperKind -> BoolSource

isCoSuperKind :: SuperKind -> BoolSource

isSuperKind :: Type -> BoolSource

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

mkArrowKind :: Kind -> Kind -> KindSource

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

mkArrowKinds :: [Kind] -> Kind -> KindSource

Iterated application of mkArrowKind

isSubArgTypeKind :: Kind -> BoolSource

True of any sub-kind of ArgTypeKind

isSubOpenTypeKind :: Kind -> BoolSource

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

isSubKind :: Kind -> Kind -> BoolSource

k1 `isSubKind` k2 checks that k1 <: k2

defaultKind :: Kind -> KindSource

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

isSubKindCon :: TyCon -> TyCon -> BoolSource

kc1 `isSubKindCon` kc2 checks that kc1 <: kc2

mkCoKind :: Type -> Type -> CoercionKindSource

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

mkCoPredTy :: Type -> Type -> Type -> TypeSource

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

coercionKind :: Coercion -> (Type, Type)Source

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).

coercionKinds :: [Coercion] -> ([Type], [Type])Source

Apply coercionKind to multiple Coercions

Equality predicates

mkEqPred :: (Type, Type) -> PredTypeSource

Creates a type equality predicate

getEqPredTys :: PredType -> (Type, Type)Source

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

isEqPredTy :: Type -> BoolSource

Tests whether a type is just a type equality predicate

Coercion transformations

mkCoercion :: TyCon -> [Type] -> CoercionSource

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

mkSymCoercion :: Coercion -> CoercionSource

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.

mkTransCoercion :: Coercion -> Coercion -> CoercionSource

Create a new Coercion by exploiting transitivity on the two given Coercions.

mkLeftCoercion :: Coercion -> CoercionSource

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

mkRightCoercion :: Coercion -> CoercionSource

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

mkInstCoercion :: Coercion -> Type -> CoercionSource

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

mkAppCoercion :: Coercion -> Coercion -> CoercionSource

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

mkTyConCoercion :: TyCon -> [Coercion] -> CoercionSource

Apply a type constructor to a list of coercions.

mkFunCoercion :: Coercion -> Coercion -> CoercionSource

Make a function Coercion between two other Coercions

mkForAllCoercion :: Var -> Coercion -> CoercionSource

Make a Coercion which binds a variable within an inner Coercion

mkInstsCoercion :: Coercion -> [Type] -> CoercionSource

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

mkUnsafeCoercion :: Type -> Type -> CoercionSource

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

mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyConSource

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.

mkFamInstCoercionSource

Arguments

:: Name

Unique name for the coercion tycon

-> [TyVar]

Type parameters of the coercion (tvs)

-> TyCon

Family tycon (F)

-> [Type]

Type instance (ts)

-> TyCon

Representation tycon (R)

-> TyCon

Coercion tycon (Co)

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.

mkAppsCoercion :: Coercion -> [Coercion] -> CoercionSource

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

transCoercionTyCon :: TyConSource

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.

Decomposition

splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)Source

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.

instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI)Source

If co :: T ts ~ rep_ty then:

 instNewTyCon_maybe T ts = Just (rep_ty, co)

decomposeCo :: Arity -> Coercion -> [Coercion]Source

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]

Comparison

coreEqCoercion :: Coercion -> Coercion -> BoolSource

Determines syntactic equality of coercions

CoercionI

data CoercionI Source

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

  1. A proper Coercion
  2. The identity coercion

Constructors

IdCo Type 
ACo Coercion 

mkSymCoI :: CoercionI -> CoercionISource

Smart constructor for sym on CoercionI, see also mkSymCoercion

mkTransCoI :: CoercionI -> CoercionI -> CoercionISource

Smart constructor for trans on CoercionI, see also mkTransCoercion

mkTyConAppCoI :: TyCon -> [CoercionI] -> CoercionISource

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

mkAppTyCoI :: CoercionI -> CoercionI -> CoercionISource

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

mkForAllTyCoI :: TyVar -> CoercionI -> CoercionISource

Smart constructor for quantified Coercions on CoercionI, see also mkForAllCoercion

fromCoI :: CoercionI -> TypeSource

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

mkClassPPredCoI :: Class -> [CoercionI] -> CoercionISource

Smart constructor for class Coercions on CoercionI. Satisfies:

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

mkIParamPredCoI :: IPName Name -> CoercionI -> CoercionISource

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

mkEqPredCoI :: CoercionI -> CoercionI -> CoercionISource

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