Coercion

Main data type

data Coercion

data Var

type CoVar

Functions over coercions

coVarKind

coercionType

coercionKind

coercionKinds

isReflCo

isReflCo_maybe

mkCoercionType

Constructing coercions

mkReflCo

mkCoVarCo

mkAxInstCo

mkPiCo

mkPiCos

mkSymCo

mkTransCo

mkNthCo

mkInstCo

mkAppCo

mkTyConAppCo

mkFunCo

mkForAllCo

mkUnsafeCo

mkNewTypeCo

mkFamInstCo

Decomposition

splitNewTypeRepCo_maybe

instNewTyCon_maybe

decomposeCo

getCoVar_maybe

splitTyConAppCo_maybe

splitAppCo_maybe

splitForAllCo_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

substTyVarBndr

substCoVarBndr

Lifting

liftCoMatch

liftCoSubstTyVar

liftCoSubstWith

Comparison

coreEqCoercion

coreEqCoercion2

Forcing evaluation of coercions

seqCo

Pretty-printing

pprCo

pprParendCo

pprCoAxiom

Other

applyCo