Coercion

Main data type

data Coercion

data Var

type CoVar

data LeftOrRight

pickLR

data Role

ltRole

Functions over coercions

coVarKind

coVarRole

coercionType

coercionKind

coercionKinds

isReflCo

isReflCo_maybe

coercionRole

coercionKindRole

mkCoercionType

Constructing coercions

mkReflCo

mkCoVarCo

mkAxInstCo

mkUnbranchedAxInstCo

mkAxInstLHS

mkAxInstRHS

mkUnbranchedAxInstRHS

mkPiCo

mkPiCos

mkCoCast

mkSymCo

mkTransCo

mkNthCo

mkNthCoRole

mkLRCo

mkInstCo

mkAppCo

mkAppCoFlexible

mkTyConAppCo

mkFunCo

mkForAllCo

mkUnsafeCo

mkUnivCo

mkSubCo

mkPhantomCo

mkNewTypeCo

downgradeRole

mkAxiomRuleCo

Decomposition

instNewTyCon_maybe

type NormaliseStepper

data NormaliseStepResult

composeSteppers

modifyStepResultCo

unwrapNewTypeStepper

topNormaliseNewType_maybe

topNormaliseTypeX_maybe

decomposeCo

getCoVar_maybe

splitAppCo_maybe

splitForAllCo_maybe

nthRole

tyConRolesX

setNominalRole_maybe

Coercion variables

mkCoVar

isCoVar

isCoVarType

coVarName

setCoVarName

setCoVarUnique

Free variables

tyCoVarsOfCo

tyCoVarsOfCos

coVarsOfCo

coercionSize

Substitution

type CvSubstEnv

emptyCvSubstEnv

data CvSubst

emptyCvSubst

lookupTyVar

lookupCoVar

isEmptyCvSubst

zapCvSubstEnv

getCvInScope

substCo

substCos

substCoVar

substCoVars

substCoWithTy

substCoWithTys

cvTvSubst

tvCvSubst

mkCvSubst

zipOpenCvSubst

substTy

extendTvSubst

extendCvSubstAndInScope

extendTvSubstAndInScope

substTyVarBndr

substCoVarBndr

Lifting

liftCoMatch

liftCoSubstTyVar

liftCoSubstWith

Comparison

coreEqCoercion

coreEqCoercion2

Forcing evaluation of coercions

seqCo

Pretty-printing

pprCo

pprParendCo

pprCoAxiom

pprCoAxBranch

pprCoAxBranchHdr

Tidying

tidyCo

tidyCos

Other

applyCo