diff --git a/src/library/coercion.cpp b/src/library/coercion.cpp
index 60753b790..9b7f4c43d 100644
--- a/src/library/coercion.cpp
+++ b/src/library/coercion.cpp
@@ -16,6 +16,8 @@ Author: Leonardo de Moura
 #include "library/module.h"
 #include "library/kernel_serializer.h"
 #include "library/scoped_ext.h"
+#include "library/pp_options.h"
+#include "library/generic_exception.h"
 
 namespace lean {
 static name * g_fun  = nullptr;
@@ -230,11 +232,23 @@ static void check_pi(name const & f, expr const & t) {
 // similar to check_pi, but produces a more informative message
 static void check_valid_coercion(name const & f, expr const & t) {
     if (!is_pi(t)) {
-        throw exception(sstream() << "invalid coercion, type of '" << f
-                        << "' does not match any of the allowed expected types for coercions\n"
-                        << "  Pi (x_1 : A_1) ... (x_n : A_n) (y: C x_1 ... x_n), D t_1 ... t_m\n"
-                        << "  Pi (x_1 : A_1) ... (x_n : A_n) (y: C x_1 ... x_n), Type\n"
-                        << "  Pi (x_1 : A_1) ... (x_n : A_n) (y: C x_1 ... x_n), A -> B");
+        throw_generic_exception(optional<expr>(),[=](formatter const & fmt) {
+                options o = fmt.get_options();
+                bool show_universes = get_pp_universes(o) || get_pp_all(o);
+                std::string ls = show_universes ? ".{ls}" : "";
+                std::string us = show_universes ? ".{us}" : "";
+                std::string u = show_universes ? ".{u}" : "";
+                return format((sstream()
+                               << "invalid coercion, type of '" << f
+                               << "' does not match any of the acceptable forms "
+                               << "for coercions\n"
+                               << "coe" << ls << " : Pi (x_1 : A_1) ... (x_n : A_n) (y: C"
+                               << ls << " x_1 ... x_n), D" << us << " t_1 ... t_m\n"
+                               << "coe" << ls << " : Pi (x_1 : A_1) ... (x_n : A_n) (y: C"
+                               << ls << " x_1 ... x_n), Type" << u << "\n"
+                               << "coe" << ls << " : Pi (x_1 : A_1) ... (x_n : A_n) (y: C"
+                               << ls << " x_1 ... x_n), (Pi x : A, B x)").str());
+            });
     }
 }