| ||||||||||||||

| ||||||||||||||

| ||||||||||||||

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

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

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 This function attempts to simplify the generated | ||||||||||||||

mkTransCoercion :: Coercion -> Coercion -> Coercion | ||||||||||||||

Create a new This function attempts to simplify the generated | ||||||||||||||

mkLeftCoercion :: Coercion -> Coercion | ||||||||||||||

From an application mkLeftCoercion c :: f ~ g | ||||||||||||||

mkRightCoercion :: Coercion -> Coercion | ||||||||||||||

From an application 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 | ||||||||||||||

| ||||||||||||||

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 splitNewTypeRepCo_maybe ty = Just (ty', co) The function returns | ||||||||||||||

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

If instNewTyCon_maybe T ts = Just (rep_ty, co) | ||||||||||||||

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

This breaks a decomposeCo 3 c = [right (left (left c)), right (left c), right c] | ||||||||||||||

unsafeCoercionTyCon :: TyCon | ||||||||||||||

symCoercionTyCon :: TyCon | ||||||||||||||

transCoercionTyCon :: TyCon | ||||||||||||||

Coercion type constructors: avoid using these directly and instead use the mk*Coercion and split*Coercion family
of functions if possible.
| ||||||||||||||

leftCoercionTyCon :: TyCon | ||||||||||||||

rightCoercionTyCon :: TyCon | ||||||||||||||

instCoercionTyCon :: TyCon | ||||||||||||||

Comparison | ||||||||||||||

coreEqCoercion :: Coercion -> Coercion -> Bool | ||||||||||||||

Determines syntactic equality of coercions | ||||||||||||||

CoercionI | ||||||||||||||

data CoercionI | ||||||||||||||

| ||||||||||||||

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