+make_co :: Coercion -> C.Ty
+make_co (Refl ty) = make_ty ty
+make_co (TyConAppCo tc cos) = make_conAppCo (qtc tc) cos
+make_co (AppCo c1 c2) = C.Tapp (make_co c1) (make_co c2)
+make_co (ForAllCo tv co) = C.Tforall (make_tbind tv) (make_co co)
+make_co (CoVarCo cv) = C.Tvar (make_var_id (coVarName cv))
+make_co (AxiomInstCo cc cos) = make_conAppCo (qcc cc) cos
+make_co (UnsafeCo t1 t2) = C.UnsafeCoercion (make_ty t1) (make_ty t2)
+make_co (SymCo co) = C.SymCoercion (make_co co)
+make_co (TransCo c1 c2) = C.TransCoercion (make_co c1) (make_co c2)
+make_co (NthCo d co) = C.NthCoercion d (make_co co)
+make_co (InstCo co ty) = C.InstCoercion (make_co co) (make_ty ty)
+
+-- Used for both tycon app coercions and axiom instantiations.
+make_conAppCo :: C.Qual C.Tcon -> [Coercion] -> C.Ty
+make_conAppCo con cos =
+ foldl C.Tapp (C.Tcon con)
+ (map make_co cos)
+