ghc-7.0.3: The GHC API

Coercion

Contents

- Main data type
  - Deconstructing Kinds
  - Predicates on Kinds
  - Equality predicates
  - Coercion transformations
  - Decomposition
  - Comparison
- CoercionI

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.

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 CoTyCon{...} [type, type]

Synopsis

- type Coercion = Type
- type Kind = Type
- typeKind :: Type -> Kind
- kindFunResult :: Kind -> Kind
- kindAppResult :: Kind -> [arg] -> Kind
- synTyConResKind :: TyCon -> Kind
- splitKindFunTys :: Kind -> ([Kind], Kind)
- splitKindFunTysN :: Int -> Kind -> ([Kind], Kind)
- splitKindFunTy_maybe :: Kind -> Maybe (Kind, Kind)
- isLiftedTypeKind :: Kind -> Bool
- isUnliftedTypeKind :: Kind -> Bool
- isOpenTypeKind :: Kind -> Bool
- isUbxTupleKind :: Kind -> Bool
- isArgTypeKind :: Kind -> Bool
- isKind :: Kind -> Bool
- isTySuperKind :: SuperKind -> Bool
- isCoSuperKind :: SuperKind -> Bool
- isSuperKind :: Type -> Bool
- isCoercionKind :: Kind -> Bool
- mkArrowKind :: Kind -> Kind -> Kind
- mkArrowKinds :: [Kind] -> Kind -> Kind
- isSubArgTypeKind :: Kind -> Bool
- isSubOpenTypeKind :: Kind -> Bool
- isSubKind :: Kind -> Kind -> Bool
- defaultKind :: Kind -> Kind
- eqKind :: Kind -> Kind -> Bool
- isSubKindCon :: TyCon -> TyCon -> Bool
- mkCoKind :: Type -> Type -> CoercionKind
- mkCoPredTy :: Type -> Type -> Type -> Type
- coVarKind :: CoVar -> (Type, Type)
- coVarKind_maybe :: CoVar -> Maybe (Type, Type)
- coercionKind :: Coercion -> (Type, Type)
- coercionKinds :: [Coercion] -> ([Type], [Type])
- 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
- 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
- mkCsel1Coercion :: Coercion -> Coercion
- mkCsel2Coercion :: Coercion -> Coercion
- mkCselRCoercion :: Coercion -> Coercion
- mkClassPPredCo :: Class -> [Coercion] -> Coercion
- mkIParamPredCo :: IPName Name -> Coercion -> Coercion
- mkEqPredCo :: Coercion -> Coercion -> Coercion
- mkCoVarCoercion :: CoVar -> Coercion
- mkCoPredCo :: Coercion -> Coercion -> Coercion -> Coercion
- unsafeCoercionTyCon :: TyCon
- symCoercionTyCon :: TyCon
- transCoercionTyCon :: TyCon
- leftCoercionTyCon :: TyCon
- rightCoercionTyCon :: TyCon
- instCoercionTyCon :: TyCon
- csel1CoercionTyCon :: TyCon
- csel2CoercionTyCon :: TyCon
- cselRCoercionTyCon :: TyCon
- decompLR_maybe :: (Type, Type) -> Maybe ((Type, Type), (Type, Type))
- decompCsel_maybe :: (Type, Type) -> Maybe ((Type, Type), (Type, Type), (Type, Type))
- decompInst_maybe :: (Type, Type) -> Maybe ((TyVar, TyVar), (Type, Type))
- splitCoPredTy_maybe :: Type -> Maybe (Type, Type, Type)
- splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)
- instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI)
- decomposeCo :: Arity -> Coercion -> [Coercion]
- coreEqCoercion :: Coercion -> Coercion -> Bool
- coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool
- data CoercionI
  - = IdCo Type
  - | ACo Coercion
- isIdentityCoI :: CoercionI -> Bool
- mkSymCoI :: CoercionI -> CoercionI
- mkTransCoI :: CoercionI -> CoercionI -> CoercionI
- mkTyConAppCoI :: TyCon -> [CoercionI] -> CoercionI
- mkAppTyCoI :: CoercionI -> CoercionI -> CoercionI
- mkFunTyCoI :: CoercionI -> CoercionI -> CoercionI
- mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
- fromCoI :: CoercionI -> Type
- mkClassPPredCoI :: Class -> [CoercionI] -> CoercionI
- mkIParamPredCoI :: IPName Name -> CoercionI -> CoercionI
- mkEqPredCoI :: CoercionI -> CoercionI -> CoercionI
- mkCoPredCoI :: CoercionI -> CoercionI -> CoercionI -> CoercionI

# Main data type

type Coercion = Type Source

A `Coercion` represents a `Type` something should be coerced to.

type Kind = Type Source

The key type representing kinds in the compiler. Invariant: a kind is always in one of these forms:

     FunTy k1 k2
     TyConApp PrimTyCon [...]
     TyVar kv   -- (during inference only)
     ForAll ... -- (for top-level coercions)

typeKind :: Type -> Kind Source

## Deconstructing Kinds

kindFunResult :: Kind -> Kind Source

Essentially `funResultTy` on kinds

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

synTyConResKind :: TyCon -> Kind Source

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

Essentially `splitFunTys` on kinds

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

Essentially `splitFunTysN` on kinds

splitKindFunTy_maybe :: Kind -> Maybe (Kind, Kind)Source

## Predicates on Kinds

isLiftedTypeKind :: Kind -> Bool Source

isUnliftedTypeKind :: Kind -> Bool Source

isOpenTypeKind :: Kind -> Bool Source

See Type for details of the distinction between these `Kind`s

isUbxTupleKind :: Kind -> Bool Source

isArgTypeKind :: Kind -> Bool Source

isKind :: Kind -> Bool Source

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

isTySuperKind :: SuperKind -> Bool Source

isCoSuperKind :: SuperKind -> Bool Source

isSuperKind :: Type -> Bool Source

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

isCoercionKind :: Kind -> Bool Source

mkArrowKind :: Kind -> Kind -> Kind Source

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

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

Iterated application of `mkArrowKind`

isSubArgTypeKind :: Kind -> Bool Source

True of any sub-kind of ArgTypeKind

isSubOpenTypeKind :: Kind -> Bool Source

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

isSubKind :: Kind -> Kind -> Bool Source

`k1 `isSubKind` k2` checks that `k1` <: `k2`

defaultKind :: Kind -> Kind Source

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

eqKind :: Kind -> Kind -> Bool Source

isSubKindCon :: TyCon -> TyCon -> Bool Source

`kc1 `isSubKindCon` kc2` checks that `kc1` <: `kc2`

mkCoKind :: Type -> Type -> CoercionKindSource

Makes a `CoercionKind` from two types: the types whose equality is proven by the relevant `Coercion`

mkCoPredTy :: Type -> Type -> Type -> Type Source

(mkCoPredTy s t r) produces the type: (s~t) => r

coVarKind :: CoVar -> (Type, Type)Source

coVarKind_maybe :: CoVar -> Maybe (Type, Type)Source

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)`.

coercionKinds :: [Coercion] -> ([Type], [Type])Source

Apply `coercionKind` to multiple `Coercion`s

isIdentityCoercion :: Coercion -> Bool Source

## Equality predicates

isEqPred :: PredType -> Bool Source

mkEqPred :: (Type, Type) -> PredType Source

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

Tests whether a type is just a type equality predicate

## Coercion transformations

mkCoercion :: TyCon -> [Type] -> Coercion Source

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 Source

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

mkTransCoercion :: Coercion -> Coercion -> Coercion Source

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

mkLeftCoercion :: Coercion -> Coercion Source

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 Source

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

mkInstCoercion :: Coercion -> Type -> Coercion Source

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 Source

Apply a `Coercion` to another `Coercion`, which is presumably a `Coercion` constructor of some kind

mkTyConCoercion :: TyCon -> [Coercion] -> Coercion Source

Apply a type constructor to a list of coercions.

mkFunCoercion :: Coercion -> Coercion -> Coercion Source

Make a function `Coercion` between two other `Coercion`s

mkForAllCoercion :: Var -> Coercion -> Coercion Source

Make a `Coercion` which binds a variable within an inner `Coercion`

mkInstsCoercion :: Coercion -> [Type] -> Coercion Source

As `mkInstCoercion`, but instantiates the coercion with a number of type arguments, left-to-right

mkUnsafeCoercion :: Type -> Type -> Coercion Source

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. Optimise by pushing down through type constructors

mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon Source

Create a coercion suitable for the given `TyCon`. The `Name` should be that of a new coercion `TyCon`, the `TyVar`s 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 `TyVar`s.

mkFamInstCoercionSource

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`)
-> 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 Source

Applies multiple `Coercion`s to another `Coercion`, from left to right. See also `mkAppCoercion`

mkCsel1Coercion :: Coercion -> Coercion Source

mkCsel2Coercion :: Coercion -> Coercion Source

mkCselRCoercion :: Coercion -> Coercion Source

mkClassPPredCo :: Class -> [Coercion] -> Coercion Source

mkIParamPredCo :: IPName Name -> Coercion -> Coercion Source

mkEqPredCo :: Coercion -> Coercion -> Coercion Source

mkCoVarCoercion :: CoVar -> Coercion Source

mkCoPredCo :: Coercion -> Coercion -> Coercion -> Coercion Source

unsafeCoercionTyCon :: TyCon Source

symCoercionTyCon :: TyCon Source

transCoercionTyCon :: TyCon Source

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

Each coercion TyCon is built with the special CoercionTyCon record and carries its own kinding rule. Such CoercionTyCons must be fully applied by any TyConApp in which they are applied, however they may also be over applied (see example above) and the kinding function must deal with this.

leftCoercionTyCon :: TyCon Source

rightCoercionTyCon :: TyCon Source

instCoercionTyCon :: TyCon Source

csel1CoercionTyCon :: TyCon Source

csel2CoercionTyCon :: TyCon Source

cselRCoercionTyCon :: TyCon Source

## Decomposition

decompLR_maybe :: (Type, Type) -> Maybe ((Type, Type), (Type, Type))Source

decompCsel_maybe :: (Type, Type) -> Maybe ((Type, Type), (Type, Type), (Type, Type))Source

decompInst_maybe :: (Type, Type) -> Maybe ((TyVar, TyVar), (Type, Type))Source

splitCoPredTy_maybe :: Type -> Maybe (Type, Type, Type)Source

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 `newtype`s.

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 `Coercion`s of kinds `A ~ D`, `B ~ E` and `E ~ F`. Hence:

     decomposeCo 3 c = [right (left (left c)), right (left c), right c]

## Comparison

coreEqCoercion :: Coercion -> Coercion -> Bool Source

Determines syntactic equality of coercions

coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool Source

# 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 Type |
ACo Coercion |

Instances

Outputable CoercionI |

isIdentityCoI :: CoercionI -> Bool Source

mkSymCoI :: CoercionI -> CoercionI Source

Smart constructor for `sym` on `CoercionI`, see also `mkSymCoercion`

mkTransCoI :: CoercionI -> CoercionI -> CoercionI Source

Smart constructor for `trans` on `CoercionI`, see also `mkTransCoercion`

mkTyConAppCoI :: TyCon -> [CoercionI] -> CoercionI Source

Smart constructor for type constructor application on `CoercionI`, see also `mkAppCoercion`

mkAppTyCoI :: CoercionI -> CoercionI -> CoercionI Source

Smart constructor for honest-to-god `Coercion` application on `CoercionI`, see also `mkAppCoercion`

mkFunTyCoI :: CoercionI -> CoercionI -> CoercionI Source

mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI Source

Smart constructor for quantified `Coercion`s on `CoercionI`, see also `mkForAllCoercion`

fromCoI :: CoercionI -> Type Source

Return either the `Coercion` contained within the `CoercionI` or the given `Type` if the `CoercionI` is the identity `Coercion`

mkClassPPredCoI :: Class -> [CoercionI] -> CoercionI Source

Smart constructor for class `Coercion`s on `CoercionI`. Satisfies:

     mkClassPPredCoI cls tys cois :: PredTy (cls tys) ~ PredTy (cls (tys `cast` cois))

mkIParamPredCoI :: IPName Name -> CoercionI -> CoercionI Source

Smart constructor for implicit parameter `Coercion`s on `CoercionI`. Similar to `mkClassPPredCoI`

mkEqPredCoI :: CoercionI -> CoercionI -> CoercionI Source

Smart constructor for type equality `Coercion`s on `CoercionI`. Similar to `mkClassPPredCoI`

mkCoPredCoI :: CoercionI -> CoercionI -> CoercionI -> CoercionI Source