+toIfaceContext cs = map (toIfacePred toIfaceType) cs
+
+----------------
+coToIfaceType :: Coercion -> IfaceType
+coToIfaceType (Refl ty) = IfaceCoConApp IfaceReflCo [toIfaceType ty]
+coToIfaceType (TyConAppCo tc cos) = IfaceTyConApp (toIfaceTyCon tc)
+ (map coToIfaceType cos)
+coToIfaceType (AppCo co1 co2) = IfaceAppTy (coToIfaceType co1)
+ (coToIfaceType co2)
+coToIfaceType (ForAllCo v co) = IfaceForAllTy (toIfaceTvBndr v)
+ (coToIfaceType co)
+coToIfaceType (CoVarCo cv) = IfaceTyVar (toIfaceTyCoVar cv)
+coToIfaceType (AxiomInstCo con cos) = IfaceCoConApp (IfaceCoAx (coAxiomName con))
+ (map coToIfaceType cos)
+coToIfaceType (UnsafeCo ty1 ty2) = IfaceCoConApp IfaceUnsafeCo
+ [ toIfaceType ty1
+ , toIfaceType ty2 ]
+coToIfaceType (SymCo co) = IfaceCoConApp IfaceSymCo
+ [ coToIfaceType co ]
+coToIfaceType (TransCo co1 co2) = IfaceCoConApp IfaceTransCo
+ [ coToIfaceType co1
+ , coToIfaceType co2 ]
+coToIfaceType (NthCo d co) = IfaceCoConApp (IfaceNthCo d)
+ [ coToIfaceType co ]
+coToIfaceType (InstCo co ty) = IfaceCoConApp IfaceInstCo
+ [ coToIfaceType co
+ , toIfaceType ty ]