ghc-7.2.1: 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.

Synopsis

Main data type

data Var

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

type CoVar = Id

Deconstructing Kinds

kindFunResult :: Kind -> Kind

Essentially funResultTy on kinds

kindAppResult :: Kind -> [arg] -> Kind

synTyConResKind :: TyCon -> Kind

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)

Essentially splitFunTys on kinds

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

Essentially splitFunTysN on kinds

Predicates on Kinds

isUbxTupleKind, isUnliftedTypeKind, isArgTypeKind, isOpenTypeKind :: Kind -> Bool

See Type for details of the distinction between these Kinds

isKind :: Kind -> Bool

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

isTySuperKind :: SuperKind -> Bool

isSuperKind :: Type -> Bool

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

mkArrowKind :: Kind -> Kind -> Kind

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

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

Iterated application of mkArrowKind

isSubArgTypeKind :: Kind -> Bool

True of any sub-kind of ArgTypeKind

isSubOpenTypeKind :: Kind -> Bool

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

isSubKind :: Kind -> Kind -> Bool

k1 `isSubKind` k2 checks that k1 <: k2

defaultKind :: Kind -> Kind

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

eqKind :: Kind -> Kind -> Bool

isSubKindCon :: TyCon -> TyCon -> Bool

kc1 `isSubKindCon` kc2 checks that kc1 <: kc2

mkCoType :: Type -> Type -> Type

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

coercionKind :: Coercion -> Pair Type

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.

coercionKinds :: [Coercion] -> Pair [Type]

Apply coercionKind to multiple Coercions

Constructing coercions

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

mkTransCo :: Coercion -> Coercion -> Coercion

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

mkInstCo :: Coercion -> Type -> Coercion

Instantiates a Coercion with a Type argument.

mkAppCo :: Coercion -> Coercion -> Coercion

Apply a Coercion to another Coercion.

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

Apply a type constructor to a list of coercions.

mkFunCo :: Coercion -> Coercion -> Coercion

Make a function Coercion between two other Coercions

mkForAllCo :: Var -> Coercion -> Coercion

Make a Coercion which binds a variable within an inner Coercion

mkUnsafeCo :: Type -> Type -> 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.

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

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.

mkFamInstCo

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)

-> CoAxiom

Coercion constructor (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 constructor built here, F the family tycon and R the (derived) representation tycon.

Decomposition

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

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, Coercion)

If co :: T ts ~ rep_ty then:

 instNewTyCon_maybe T ts = Just (rep_ty, co)

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

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 CoVar

Attempts to obtain the type variable underlying a Coercion

splitTyConAppCo_maybe :: Coercion -> Maybe (TyCon, [Coercion])

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

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

Attempt to take a coercion application apart.

Coercion variables

Free variables

Substitution

type CvSubstEnv = VarEnv Coercion

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

substCo :: CvSubst -> Coercion -> Coercion

Substitute within a Coercion

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

Substitute within several Coercions

Lifting

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

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.

liftCoSubst :: CvSubst -> Type -> Coercion

The "lifting" operation which substitutes coercions for type variables in a type to produce a coercion.

For the inverse operation, see liftCoMatch

Comparison

coreEqCoercion :: Coercion -> Coercion -> Bool

Determines syntactic equality of coercions

Forcing evaluation of coercions

seqCo :: Coercion -> ()

Pretty-printing

Other