ghc-6.12.2: The GHC APISource codeContentsIndex
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
isIdentityCoercion :: Coercion -> Bool
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
mkTyConCoercion :: TyCon -> [Coercion] -> Coercion
mkFunCoercion :: Coercion -> Coercion -> Coercion
mkForAllCoercion :: Var -> 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]
unsafeCoercionTyCon :: TyCon
symCoercionTyCon :: TyCon
transCoercionTyCon :: TyCon
leftCoercionTyCon :: TyCon
rightCoercionTyCon :: TyCon
instCoercionTyCon :: TyCon
coreEqCoercion :: Coercion -> Coercion -> Bool
data CoercionI
= IdCo
| ACo Coercion
isIdentityCoI :: 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 = TypeSource
A Coercion represents a Type something should be coerced to.
mkCoKind :: Type -> Type -> CoercionKindSource
Makes a CoercionKind from two types: the types whose equality is proven by the relevant Coercion
mkReflCoKind :: Type -> CoercionKindSource
Create a reflexive CoercionKind that asserts that a type can be coerced to itself
splitCoercionKind_maybe :: Kind -> Maybe (Type, Type)Source
Take a CoercionKind apart into the two types it relates, if possible. See also splitCoercionKind
splitCoercionKind :: CoercionKind -> (Type, Type)Source
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)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). See also coercionKindPredTy

coercionKinds :: [Coercion] -> ([Type], [Type])Source
Apply coercionKind to multiple Coercions
coercionKindPredTy :: Coercion -> CoercionKindSource
Recover the CoercionKind corresponding to a particular Coerceion. See also coercionKind and mkCoKind
isIdentityCoercion :: Coercion -> BoolSource
Equality predicates
isEqPred :: PredType -> BoolSource
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.

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

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 -> 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
mkRightCoercions :: Int -> Coercion -> [Coercion]Source
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 -> 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.
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
:: 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] -> CoercionSource
Applies multiple Coercions to another Coercion, from left to right. See also mkAppCoercion
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]
unsafeCoercionTyCon :: TyConSource
symCoercionTyCon :: TyConSource
transCoercionTyCon :: TyConSource
Coercion type constructors: avoid using these directly and instead use the mk*Coercion and split*Coercion family of functions if possible.
leftCoercionTyCon :: TyConSource
rightCoercionTyCon :: TyConSource
instCoercionTyCon :: TyConSource
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
ACo Coercion
show/hide Instances
isIdentityCoI :: CoercionI -> BoolSource
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 -> [Type] -> [CoercionI] -> CoercionISource
Smart constructor for type constructor application on CoercionI, see also mkAppCoercion
mkAppTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionISource
Smart constructor for honest-to-god Coercion application on CoercionI, see also mkAppCoercion
mkFunTyCoI :: Type -> CoercionI -> Type -> CoercionI -> CoercionISource
Smart constructor for function-Coercions on CoercionI, see also mkFunCoercion
mkForAllTyCoI :: TyVar -> CoercionI -> CoercionISource
Smart constructor for quantified Coercions on CoercionI, see also mkForAllCoercion
fromCoI :: CoercionI -> Type -> TypeSource
Return either the Coercion contained within the CoercionI or the given Type if the CoercionI is the identity Coercion
fromACo :: CoercionI -> CoercionSource
Extract a Coercion from a CoercionI if it represents one. If it is the identity coercion, panic
mkClassPPredCoI :: Class -> [Type] -> [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 :: Type -> CoercionI -> Type -> CoercionI -> CoercionISource
Smart constructor for type equality Coercions on CoercionI. Similar to mkClassPPredCoI
Produced by Haddock version 2.6.1