|
|
|
|
|
| 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 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 |
| :: 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)
| | -> TyCon | Coercion 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 | |
|
|
| 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 |
