Coercion

Main data type

data Coercion

data Var

type CoVar

Deconstructing Kinds

kindFunResult

kindAppResult

synTyConResKind

splitKindFunTys

splitKindFunTysN

splitKindFunTy_maybe

Predicates on Kinds

isLiftedTypeKind

isUbxTupleKind

isUnliftedTypeKind

isArgTypeKind

isOpenTypeKind

isKind

isTySuperKind

isSuperKind

isCoercionKind

mkArrowKind

mkArrowKinds

isSubArgTypeKind

isSubOpenTypeKind

isSubKind

defaultKind

eqKind

isSubKindCon

mkCoType

coVarKind

coVarKind_maybe

coercionType

coercionKind

coercionKinds

isReflCo

Constructing coercions

mkReflCo

mkCoVarCo

mkAxInstCo

mkPiCo

mkPiCos

mkSymCo

mkTransCo

mkNthCo

mkInstCo

mkAppCo

mkTyConAppCo

mkFunCo

mkForAllCo

mkUnsafeCo

mkNewTypeCo

mkFamInstCo

mkPredCo

Decomposition

splitCoPredTy_maybe

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

zipOpenCvSubst

substTy

extendTvSubst

substTyVarBndr

substCoVarBndr

Lifting

liftCoMatch

liftCoSubst

liftCoSubstTyVar

liftCoSubstWith

Comparison

coreEqCoercion

coreEqCoercion2

Forcing evaluation of coercions

seqCo

Pretty-printing

pprCo

pprParendCo

pprCoAxiom

Other

applyCo

coVarPred