ghc-7.10.1: The GHC API

Safe HaskellNone
LanguageHaskell2010

Coercion

Contents

Description

Module for (a) type kinds and (b) type coercions, as used in System FC. See Expr for more on System FC and how coercions fit into it.

Synopsis

Main data type

data Var Source

Essentially a typed Name, that may also contain some additional information about the Var and it's use sites.

Instances

Eq Var 
Data Var 
Ord Var 
Outputable Var 
Uniquable Var 
NamedThing Var 
type PostRn Id ty = ty 
type PostTc Id ty = ty 

type CoVar = Id Source

pickLR :: LeftOrRight -> (a, a) -> a Source

Functions over coercions

coercionKind :: Coercion -> Pair Type Source

If it is the case that

c :: (t1 ~ t2)

i.e. the kind of c relates t1 and t2, then coercionKind c = Pair t1 t2.

coercionRole :: Coercion -> Role Source

Retrieve the role from a coercion.

coercionKindRole :: Coercion -> (Pair Type, Role) Source

Get a coercion's kind and role. Why both at once? See Note [Computing a coercion kind and role]

mkCoercionType :: Role -> Type -> Type -> Type Source

Makes a coercion type from two types: the types whose equality is proven by the relevant Coercion

Constructing coercions

mkSymCo :: 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.

mkTransCo :: Coercion -> Coercion -> Coercion Source

Create a new Coercion by composing the two given Coercions transitively.

mkInstCo :: Coercion -> Type -> Coercion Source

Instantiates a Coercion with a Type argument.

mkAppCo :: Coercion -> Coercion -> Coercion Source

Apply a Coercion to another Coercion. The second coercion must be Nominal, unless the first is Phantom. If the first is Phantom, then the second can be either Phantom or Nominal.

mkAppCoFlexible :: Coercion -> Role -> Coercion -> Coercion Source

Apply a Coercion to another Coercion. The second Coercions role is given, making this more flexible than mkAppCo.

mkTyConAppCo :: Role -> TyCon -> [Coercion] -> Coercion Source

Apply a type constructor to a list of coercions. It is the caller's responsibility to get the roles correct on argument coercions.

mkFunCo :: Role -> Coercion -> Coercion -> Coercion Source

Make a function Coercion between two other Coercions

mkForAllCo :: Var -> Coercion -> Coercion Source

Make a Coercion which binds a variable within an inner Coercion

mkUnsafeCo :: Type -> Type -> Coercion Source

Manufacture an unsafe coercion from thin air. Currently (May 14) this is used only to implement the unsafeCoerce# primitive. Optimise by pushing down through type constructors.

mkNewTypeCo :: Name -> TyCon -> [TyVar] -> [Role] -> Type -> CoAxiom Unbranched Source

Create a coercion constructor (axiom) suitable for the given newtype TyCon. The Name should be that of a new coercion CoAxiom, 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.

Decomposition

instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion) Source

If co :: T ts ~ rep_ty then:

instNewTyCon_maybe T ts = Just (rep_ty, co)

Checks for a newtype, and for being saturated

type NormaliseStepper = RecTcChecker -> TyCon -> [Type] -> NormaliseStepResult Source

A function to check if we can reduce a type by one step. Used with topNormaliseTypeX_maybe.

data NormaliseStepResult Source

The result of stepping in a normalisation function. See topNormaliseTypeX_maybe.

Constructors

NS_Done

nothing more to do

NS_Abort

utter failure. The outer function should fail too.

NS_Step RecTcChecker Type Coercion

we stepped, yielding new bits; ^ co :: old type ~ new type

composeSteppers :: NormaliseStepper -> NormaliseStepper -> NormaliseStepper Source

Try one stepper and then try the next, if the first doesn't make progress.

unwrapNewTypeStepper :: NormaliseStepper Source

A NormaliseStepper that unwraps newtypes, careful not to fall into a loop. If it would fall into a loop, it produces NS_Abort.

topNormaliseNewType_maybe :: Type -> Maybe (Coercion, Type) Source

Sometimes we want to look through a newtype and get its associated coercion. This function strips off newtype layers enough to reveal something that isn't a newtype, or responds False to ok_tc. Specifically, here's the invariant:

topNormaliseNewType_maybe ty = Just (co, ty')

then (a) co : ty0 ~ ty'. (b) ty' is not a newtype.

The function returns Nothing for non-newtypes, or unsaturated applications

This function does *not* look through type families, because it has no access to the type family environment. If you do have that at hand, consider to use topNormaliseType_maybe, which should be a drop-in replacement for topNormaliseNewType_maybe

topNormaliseTypeX_maybe :: NormaliseStepper -> Type -> Maybe (Coercion, Type) Source

A general function for normalising the top-level of a type. It continues to use the provided NormaliseStepper until that function fails, and then this function returns. The roles of the coercions produced by the NormaliseStepper must all be the same, which is the role returned from the call to topNormaliseTypeX_maybe.

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

This breaks a Coercion with type 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 = [nth 0 c, nth 1 c, nth 2 c]

getCoVar_maybe :: Coercion -> Maybe CoVar Source

Attempts to obtain the type variable underlying a Coercion

splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion) Source

Attempt to take a coercion application apart.

Coercion variables

Free variables

Substitution

type CvSubstEnv = VarEnv Coercion Source

A substitution of Coercions for CoVars (OR TyVars, when doing a "lifting" substitution)

substCo :: CvSubst -> Coercion -> Coercion Source

Substitute within a Coercion

substCos :: CvSubst -> [Coercion] -> [Coercion] Source

Substitute within several Coercions

Lifting

liftCoMatch :: TyVarSet -> Type -> Coercion -> Maybe LiftCoSubst Source

liftCoMatch is sort of inverse to liftCoSubst. In particular, if liftCoMatch vars ty co == Just s, then tyCoSubst s ty == co. That is, it matches a type against a coercion of the same "shape", and returns a lifting substitution which could have been used to produce the given coercion from the given type.

Comparison

coreEqCoercion :: Coercion -> Coercion -> Bool Source

Determines syntactic equality of coercions

Forcing evaluation of coercions

Pretty-printing

Tidying

Other