ghc-7.7.20130829: The GHC API

Safe HaskellNone




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


Main data type

data Var Source

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

pickLR :: LeftOrRight -> (a, a) -> aSource

Functions over coercions

coercionKind :: Coercion -> Pair TypeSource

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.

mkCoercionType :: Role -> Type -> Type -> TypeSource

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

Constructing coercions

mkSymCo :: 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.

mkTransCo :: Coercion -> Coercion -> CoercionSource

Create a new Coercion by composing the two given Coercions transitively.

mkInstCo :: Coercion -> Type -> CoercionSource

Instantiates a Coercion with a Type argument.

mkAppCo :: Coercion -> Coercion -> CoercionSource

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.

mkTyConAppCo :: Role -> TyCon -> [Coercion] -> CoercionSource

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

mkFunCo :: Role -> Coercion -> Coercion -> CoercionSource

Make a function Coercion between two other Coercions

mkForAllCo :: Var -> Coercion -> CoercionSource

Make a Coercion which binds a variable within an inner Coercion

mkUnsafeCo :: Type -> Type -> CoercionSource

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.

mkNewTypeCo :: Name -> TyCon -> [TyVar] -> [Role] -> Type -> CoAxiom UnbranchedSource

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.


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

 splitNewTypeRepCo_maybe ty = Just (ty', co)

then co : ty ~ ty'. The function returns Nothing for non-newtypes, or unsaturated applications

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

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]

getCoVar_maybe :: Coercion -> Maybe CoVarSource

Attempts to obtain the type variable underlying a Coercion

splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)Source

Attempt to take a coercion application apart.

Coercion variables

Free variables


type CvSubstEnv = VarEnv CoercionSource

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

substCo :: CvSubst -> Coercion -> CoercionSource

Substitute within a Coercion

substCos :: CvSubst -> [Coercion] -> [Coercion]Source

Substitute within several Coercions


liftCoMatch :: TyVarSet -> Type -> Coercion -> Maybe LiftCoSubstSource

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.


coreEqCoercion :: Coercion -> Coercion -> BoolSource

Determines syntactic equality of coercions

Forcing evaluation of coercions