+Variable coreCoercionKind : Kind -> CoreType*CoreType.
+ Extract Inlined Constant coreCoercionKind => "(Coercion.coercionKind . kindToCoreKind)".
+Variable kindOfCoreType : CoreType -> Kind. Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Kind.typeKind)".
+Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "(outputableToString . coreViewDeep)".
+Variable setVarType : CoreVar -> CoreType -> CoreVar. Extract Inlined Constant setVarType => "Var.setVarType".
+
+(* GHC provides decision procedures for equality on its primitive types; we tell Coq to blindly trust them *)
+Variable coreTyCon_eq : EqDecider CoreTyCon. Extract Inlined Constant coreTyCon_eq => "(==)".
+Variable tyCon_eq : EqDecider TyCon. Extract Inlined Constant tyCon_eq => "(==)".
+Variable tyFun_eq : EqDecider TyFun. Extract Inlined Constant tyFun_eq => "(==)".
+Variable dataCon_eq : EqDecider CoreDataCon. Extract Inlined Constant dataCon_eq => "(==)".
+Variable coreName_eq : EqDecider CoreName. Extract Inlined Constant coreName_eq => "(==)".
+Instance CoreTyConEqDecidable : EqDecidable CoreTyCon := { eqd_dec := coreTyCon_eq }.
+Instance TyConEqDecidable : EqDecidable TyCon := { eqd_dec := tyCon_eq }.
+Instance TyFunEqDecidable : EqDecidable TyFun := { eqd_dec := tyFun_eq }.
+Instance DataConEqDecidable : EqDecidable CoreDataCon := { eqd_dec := dataCon_eq }.
+Instance CoreNameEqDecidable : EqDecidable CoreName := { eqd_dec := coreName_eq }.
+Instance CoreTypeToString : ToString CoreType := { toString := coreTypeToString }.
+Instance CoreNameToString : ToString CoreName := { toString := coreNameToString }.
+Instance CoreCoercionToString : ToString CoreCoercion := { toString := coreCoercionToString }.
+Instance CoreDataConToString : ToString CoreDataCon := { toString := coreDataConToString }.
+Instance CoreTyConToString : ToString CoreTyCon := { toString := coreTyConToString }.
+