ghc-6.10.1: The GHC APIContentsIndex
Coercion
Contents
Main data type
Equality predicates
Coercion transformations
Comparison
CoercionI
Description

Module for 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 CoercionTyCon{...} [type, type]
Synopsis
type Coercion = Type
mkCoKind :: Type -> Type -> CoercionKind
mkReflCoKind :: Type -> CoercionKind
splitCoercionKind_maybe :: Kind -> Maybe (Type, Type)
splitCoercionKind :: CoercionKind -> (Type, Type)
coercionKind :: Coercion -> (Type, Type)
coercionKinds :: [Coercion] -> ([Type], [Type])
coercionKindPredTy :: Coercion -> CoercionKind
isEqPred :: PredType -> Bool
mkEqPred :: (Type, Type) -> PredType
getEqPredTys :: PredType -> (Type, Type)
isEqPredTy :: Type -> Bool
mkCoercion :: TyCon -> [Type] -> Coercion
mkSymCoercion :: Coercion -> Coercion
mkTransCoercion :: Coercion -> Coercion -> Coercion
mkLeftCoercion :: Coercion -> Coercion
mkRightCoercion :: Coercion -> Coercion
mkRightCoercions :: Int -> Coercion -> [Coercion]
mkInstCoercion :: Coercion -> Type -> Coercion
mkAppCoercion :: Coercion -> Coercion -> Coercion
mkForAllCoercion :: Var -> Coercion -> Coercion
mkFunCoercion :: Coercion -> Coercion -> Coercion
mkInstsCoercion :: Coercion -> [Type] -> Coercion
mkUnsafeCoercion :: Type -> Type -> Coercion
mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
mkFamInstCoercion :: Name -> [TyVar] -> TyCon -> [Type] -> TyCon -> TyCon
mkAppsCoercion :: Coercion -> [Coercion] -> Coercion
splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)
instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI)
decomposeCo :: Arity -> Coercion -> [Coercion]
transCoercionTyCon :: TyCon
coreEqCoercion :: Coercion -> Coercion -> Bool
data CoercionI
= IdCo
| ACo Coercion
isIdentityCoercion :: CoercionI -> Bool
mkSymCoI :: CoercionI -> CoercionI
mkTransCoI :: CoercionI -> CoercionI -> CoercionI
mkTyConAppCoI :: TyCon -> [Type] -> [CoercionI] -> CoercionI
mkAppTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
mkFunTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
fromCoI :: CoercionI -> Type -> Type
fromACo :: CoercionI -> Coercion
mkClassPPredCoI :: Class -> [Type] -> [CoercionI] -> CoercionI
mkIParamPredCoI :: IPName Name -> CoercionI -> CoercionI
mkEqPredCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
Main data type
type Coercion = Type
A Coercion represents a Type something should be coerced to.
mkCoKind :: Type -> Type -> CoercionKind
Makes a CoercionKind from two types: the types whose equality is proven by the relevant Coercion
mkReflCoKind :: Type -> CoercionKind
Create a reflexive CoercionKind that asserts that a type can be coerced to itself
splitCoercionKind_maybe :: Kind -> Maybe (Type, Type)
Take a CoercionKind apart into the two types it relates, if possible. See also splitCoercionKind
splitCoercionKind :: CoercionKind -> (Type, Type)
Take a CoercionKind apart into the two types it relates: see also mkCoKind. Panics if the argument is not a valid CoercionKind
coercionKind :: Coercion -> (Type, Type)

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). See also coercionKindPredTy

coercionKinds :: [Coercion] -> ([Type], [Type])
Apply coercionKind to multiple Coercions
coercionKindPredTy :: Coercion -> CoercionKind
Recover the CoercionKind corresponding to a particular Coerceion. See also coercionKind and mkCoKind
Equality predicates
isEqPred :: PredType -> Bool
mkEqPred :: (Type, Type) -> PredType
Creates a type equality predicate
getEqPredTys :: PredType -> (Type, Type)
Splits apart a type equality predicate, if the supplied PredType is one. Panics otherwise
isEqPredTy :: Type -> Bool
Tests whether a type is just a type equality predicate
Coercion transformations
mkCoercion :: TyCon -> [Type] -> Coercion
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 -> 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.

This function attempts to simplify the generated Coercion by removing redundant applications of sym. This is done by pushing this new sym down into the Coercion and exploiting the fact that sym (sym co) = co.

mkTransCoercion :: Coercion -> Coercion -> Coercion

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

This function attempts to simplify the generated Coercion by exploiting the fact that sym g trans g = id.

mkLeftCoercion :: Coercion -> Coercion

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

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
mkRightCoercions :: Int -> Coercion -> [Coercion]
As mkRightCoercion, but finds the Coercions available on the right side of n nested application Coercions, manufacturing new left or right cooercions as necessary if suffficiently many are not directly available.
mkInstCoercion :: Coercion -> Type -> Coercion
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 -> Coercion
Apply a Coercion to another Coercion, which is presumably a Coercion constructor of some kind
mkForAllCoercion :: Var -> Coercion -> Coercion
Make a Coercion which binds a variable within an inner Coercion
mkFunCoercion :: Coercion -> Coercion -> Coercion
Make a function Coercion between two other Coercions
mkInstsCoercion :: Coercion -> [Type] -> Coercion
As mkInstCoercion, but instantiates the coercion with a number of type arguments, left-to-right
mkUnsafeCoercion :: Type -> Type -> Coercion
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.
mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
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.
mkFamInstCoercion
:: NameUnique name for the coercion tycon
-> [TyVar]Type parameters of the coercion (tvs)
-> TyConFamily tycon (F)
-> [Type]Type instance (ts)
-> TyConRepresentation tycon (R)
-> TyConCoercion 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] -> Coercion
Applies multiple Coercions to another Coercion, from left to right. See also mkAppCoercion
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, CoercionI)

If co :: T ts ~ rep_ty then:

 instNewTyCon_maybe T ts = Just (rep_ty, co)
decomposeCo :: Arity -> Coercion -> [Coercion]

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]
transCoercionTyCon :: TyCon
Coercion type constructors: avoid using these directly and instead use the mk*Coercion and split*Coercion family of functions if possible.
Comparison
coreEqCoercion :: Coercion -> Coercion -> Bool
Determines syntactic equality of coercions
CoercionI
data CoercionI

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

1. A proper Coercion

2. The identity coercion

Constructors
IdCo
ACo Coercion
isIdentityCoercion :: CoercionI -> Bool
mkSymCoI :: CoercionI -> CoercionI
Smart constructor for sym on CoercionI, see also mkSymCoercion
mkTransCoI :: CoercionI -> CoercionI -> CoercionI
Smart constructor for trans on CoercionI, see also mkTransCoercion
mkTyConAppCoI :: TyCon -> [Type] -> [CoercionI] -> CoercionI
Smart constructor for type constructor application on CoercionI, see also mkAppCoercion
mkAppTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
Smart constructor for honest-to-god Coercion application on CoercionI, see also mkAppCoercion
mkFunTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
Smart constructor for function-Coercions on CoercionI, see also mkFunCoercion
mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
Smart constructor for quantified Coercions on CoercionI, see also mkForAllCoercion
fromCoI :: CoercionI -> Type -> Type
Return either the Coercion contained within the CoercionI or the given Type if the CoercionI is the identity Coercion
fromACo :: CoercionI -> Coercion
Extract a Coercion from a CoercionI if it represents one. If it is the identity coercion, panic
mkClassPPredCoI :: Class -> [Type] -> [CoercionI] -> CoercionI

Smart constructor for class Coercions on CoercionI. Satisfies:

 mkClassPPredCoI cls tys cois :: PredTy (cls tys) ~ PredTy (cls (tys `cast` cois))
mkIParamPredCoI :: IPName Name -> CoercionI -> CoercionI
Smart constructor for implicit parameter Coercions on CoercionI. Similar to mkClassPPredCoI
mkEqPredCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionI
Smart constructor for type equality Coercions on CoercionI. Similar to mkClassPPredCoI
Produced by Haddock version 2.3.0