Coercion

Main data type

data Coercion

type CoercionN

type CoercionR

type CoercionP

data UnivCoProvenance

data CoercionHole

data LeftOrRight

data Var

type CoVar

type TyCoVar

data Role

ltRole

Functions over coercions

coVarTypes

coVarKind

coVarKindsTypesRole

coVarRole

coercionType

coercionKind

coercionKinds

mkCoercionType

coercionRole

coercionKindRole

Constructing coercions

mkReflCo

mkRepReflCo

mkNomReflCo

mkCoVarCo

mkCoVarCos

mkAxInstCo

mkUnbranchedAxInstCo

mkAxInstRHS

mkUnbranchedAxInstRHS

mkAxInstLHS

mkUnbranchedAxInstLHS

mkPiCo

mkPiCos

mkCoCast

mkSymCo

mkTransCo

mkTransAppCo

mkNthCo

mkNthCoRole

mkLRCo

mkInstCo

mkAppCo

mkAppCos

mkTyConAppCo

mkFunCo

mkFunCos

mkForAllCo

mkForAllCos

mkHomoForAllCos

mkHomoForAllCos_NoRefl

mkPhantomCo

mkHomoPhantomCo

toPhantomCo

mkUnsafeCo

mkHoleCo

mkUnivCo

mkSubCo

mkAxiomInstCo

mkProofIrrelCo

downgradeRole

maybeSubCo

mkAxiomRuleCo

mkCoherenceCo

mkCoherenceRightCo

mkCoherenceLeftCo

mkKindCo

castCoercionKind

mkHeteroCoercionType

Decomposition

instNewTyCon_maybe

type NormaliseStepper ev

data NormaliseStepResult ev

composeSteppers

mapStepResult

unwrapNewTypeStepper

topNormaliseNewType_maybe

topNormaliseTypeX

decomposeCo

getCoVar_maybe

splitTyConAppCo_maybe

splitAppCo_maybe

splitForAllCo_maybe

nthRole

tyConRolesX

tyConRolesRepresentational

setNominalRole_maybe

pickLR

isReflCo

isReflCo_maybe

isReflexiveCo

isReflexiveCo_maybe

Coercion variables

mkCoVar

isCoVar

coVarName

setCoVarName

setCoVarUnique

isCoVar_maybe

Free variables

tyCoVarsOfCo

tyCoVarsOfCos

coVarsOfCo

tyCoFVsOfCo

tyCoFVsOfCos

tyCoVarsOfCoDSet

coercionSize

Substitution

type CvSubstEnv

emptyCvSubstEnv

lookupCoVar

substCo

substCos

substCoVar

substCoVars

substCoWith

substCoVarBndr

extendTvSubstAndInScope

getCvSubstEnv

Lifting

liftCoSubst

liftCoSubstTyVar

liftCoSubstWith

liftCoSubstWithEx

emptyLiftingContext

extendLiftingContext

liftCoSubstVarBndrCallback

isMappedByLC

mkSubstLiftingContext

zapLiftingContext

substForAllCoBndrCallbackLC

lcTCvSubst

lcInScopeSet

type LiftCoEnv

data LiftingContext

liftEnvSubstLeft

liftEnvSubstRight

substRightCo

substLeftCo

swapLiftCoEnv

lcSubstLeft

lcSubstRight

Comparison

eqCoercion

eqCoercionX

Forcing evaluation of coercions

seqCo

Pretty-printing

pprCo

pprParendCo

pprCoBndr

pprCoAxiom

pprCoAxBranch

pprCoAxBranchHdr

Tidying

tidyCo

tidyCos

Other

promoteCoercion