diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp
index 25f35db1a..820a036af 100644
--- a/src/library/tactic/rewrite_tactic.cpp
+++ b/src/library/tactic/rewrite_tactic.cpp
@@ -1427,28 +1427,43 @@ class rewrite_fn {
         }
     }
 
-    void process_failure(expr const & elem, bool type_error) {
+    void process_failure(expr const & elem, bool type_error, kernel_exception * ex = nullptr) {
+        std::shared_ptr<kernel_exception> saved_ex;
+        if (ex)
+            saved_ex.reset(static_cast<kernel_exception*>(ex->clone()));
         if (m_ps.report_failure()) {
             proof_state curr_ps(m_ps, cons(m_g, tail(m_ps.get_goals())), m_subst, m_ngen);
             if (!m_use_trace || !m_trace_initialized) {
                 throw tactic_exception("rewrite step failed", some_expr(elem), curr_ps,
-                                       [=](formatter const &) {
-                                           if (type_error)
-                                               return format("invalid 'rewrite' tactic, "
+                                       [=](formatter const & fmt) {
+                                           format r;
+                                           if (type_error) {
+                                               r = format("invalid 'rewrite' tactic, "
                                                              "rewrite step produced type incorrect term");
-                                           else
-                                               return format("invalid 'rewrite' tactic, rewrite step failed");
+                                               if (saved_ex) {
+                                                   r += saved_ex->pp(fmt);
+                                                   r += line();
+                                               }
+                                           } else {
+                                               r = format("invalid 'rewrite' tactic, rewrite step failed");
+                                           }
+                                           return r;
                                        });
             } else {
                 trace saved_trace = m_trace;
                 throw tactic_exception("rewrite step failed", some_expr(elem), curr_ps,
                                        [=](formatter const & fmt) {
                                            format r;
-                                           if (type_error)
+                                           if (type_error) {
                                                r += format("invalid 'rewrite' tactic, "
                                                            "step produced type incorrect term, details: ");
-                                           else
+                                               if (saved_ex) {
+                                                   r += saved_ex->pp(fmt);
+                                                   r += line();
+                                               }
+                                           } else {
                                                r += format("invalid 'rewrite' tactic, ");
+                                           }
                                            r += saved_trace.pp(fmt);
                                            return r;
                                        });
@@ -1481,7 +1496,7 @@ public:
                     return proof_state_seq();
                 }
             } catch (kernel_exception & ex) {
-                process_failure(elem, true);
+                process_failure(elem, true, &ex);
                 return proof_state_seq();
             }
         }
diff --git a/tests/lean/550.lean.expected.out b/tests/lean/550.lean.expected.out
index ab3b4e8c5..c07a78000 100644
--- a/tests/lean/550.lean.expected.out
+++ b/tests/lean/550.lean.expected.out
@@ -1,4 +1,12 @@
-550.lean:44:72: error:invalid 'rewrite' tactic, step produced type incorrect term, details: rewrite step failed using pattern
+550.lean:44:72: error:invalid 'rewrite' tactic, step produced type incorrect term, details: type mismatch at application
+  eq.rec (eq.rec (eq.refl function.id) (eq.symm linv))
+term
+  eq.rec (eq.refl function.id) (eq.symm linv)
+has type
+  x = function.id
+but is expected to have type
+  finv ∘ func = function.id
+rewrite step failed using pattern
   finv ∘ func
 proof state:
 A : Type,