diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt
index debddcc777..a7442c3c43 100644
--- a/src/frontends/lean/CMakeLists.txt
+++ b/src/frontends/lean/CMakeLists.txt
@@ -5,6 +5,6 @@ notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp
 inductive_cmds.cpp dependencies.cpp
 pp.cpp structure_cmd.cpp structure_instance.cpp
 init_module.cpp type_util.cpp local_ref_info.cpp decl_attributes.cpp nested_declaration.cpp
-opt_cmd.cpp prenum.cpp print_cmd.cpp elaborator.cpp
+opt_cmd.cpp prenum.cpp print_cmd.cpp elaborator.cpp elaborator_exception.cpp
 match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp
 brackets.cpp tactic_notation.cpp)
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index f69619dd2c..2c3f76d4d6 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -127,6 +127,11 @@ format elaborator::pp_indent(expr const & e) {
     return pp_indent(mk_pp_ctx(), e);
 }
 
+format elaborator::pp(expr const & e) {
+    auto fn = mk_pp_ctx();
+    return fn(e);
+}
+
 format elaborator::pp_overloads(pp_fn const & pp_fn, buffer<expr> const & fns) {
     format r("overloads:");
     r += space();
@@ -303,8 +308,9 @@ auto elaborator::use_elim_elab_core(name const & fn) -> optional<elim_info> {
     buffer<expr> C_args;
     expr const & C = get_app_args(type, C_args);
     if (!is_local(C) || C_args.empty() || !std::all_of(C_args.begin(), C_args.end(), is_local)) {
-        trace_elab_detail(tout() << "'eliminator' elaboration is not used for '" << fn <<
-                          "' because resulting type is not of the expected form\n";);
+        format msg = format("'eliminator' elaboration is not used for '") + format(fn) +
+            format("' because resulting type is not of the expected form\n");
+        m_elim_failure_info.insert(fn, msg);
         return optional<elim_info>();
     }
 
@@ -359,9 +365,10 @@ auto elaborator::use_elim_elab_core(name const & fn) -> optional<elim_info> {
 
     for (unsigned i = 0; i < found.size(); i++) {
         if (!found[i]) {
-            trace_elab_detail(tout() << "'eliminator' elaboration is not used for '" << fn <<
-                              "' because did not find a (reliable) way to synthesize '" << C_args[i] << "' " <<
-                              "which occurs in the resulting type\n";);
+            format msg = format("'eliminator' elaboration is not used for '") + format(fn) +
+                format("' because a (reliable) way to synthesize '") + pp(C_args[i]) +
+                format("', which occurs in the resulting type, was not found\n");
+            m_elim_failure_info.insert(fn, msg);
             return optional<elim_info>();
         }
     }
@@ -828,29 +835,34 @@ expr elaborator::visit_elim_app(expr const & fn, elim_info const & info, buffer<
         throw elaborator_exception(ref, "\"eliminator\" elaborator failed to compute the motive");
     }
 
-    /* Elaborate postponed arguments */
-    for (unsigned i = 0; i < new_args.size(); i++) {
-        if (optional<expr> arg = postponed_args[i]) {
-            lean_assert(is_metavar(new_args[i]));
-            expr new_arg_type = instantiate_mvars(infer_type(new_args[i]));
-            expr new_arg      = visit(*arg, some_expr(new_arg_type));
-            if (!is_def_eq(new_args[i], new_arg)) {
-                auto pp_fn = mk_pp_ctx();
-                throw elaborator_exception(ref, format("\"eliminator\" elaborator type mismatch, term") +
-                                           pp_indent(pp_fn, new_arg) +
-                                           line() + format("has type") +
-                                           pp_indent(pp_fn, infer_type(new_arg)) +
-                                           line() + format("but is expected to have type") +
-                                           pp_indent(pp_fn, new_arg_type));
-            } else {
-                new_args[i] = new_arg;
+    try {
+        /* Elaborate postponed arguments */
+        for (unsigned i = 0; i < new_args.size(); i++) {
+            if (optional<expr> arg = postponed_args[i]) {
+                lean_assert(is_metavar(new_args[i]));
+                expr new_arg_type = instantiate_mvars(infer_type(new_args[i]));
+                expr new_arg      = visit(*arg, some_expr(new_arg_type));
+                if (!is_def_eq(new_args[i], new_arg)) {
+                    auto pp_fn = mk_pp_ctx();
+                    throw elaborator_exception(ref, format("\"eliminator\" elaborator type mismatch, term") +
+                                               pp_indent(pp_fn, new_arg) +
+                                               line() + format("has type") +
+                                               pp_indent(pp_fn, infer_type(new_arg)) +
+                                               line() + format("but is expected to have type") +
+                                               pp_indent(pp_fn, new_arg_type));
+                } else {
+                    new_args[i] = new_arg;
+                }
             }
         }
-    }
 
-    expr r = instantiate_mvars(mk_app(mk_app(fn, new_args), extra_args));
-    trace_elab_debug(tout() << "elaborated recursor:\n  " << r << "\n";);
-    return r;
+        expr r = instantiate_mvars(mk_app(mk_app(fn, new_args), extra_args));
+        trace_elab_debug(tout() << "elaborated recursor:\n  " << r << "\n";);
+        return r;
+    } catch (elaborator_exception & ex) {
+        throw nested_elaborator_exception(ref, ex, format("the inferred motive for the eliminator-like application is") +
+                                          pp_indent(motive));
+    }
 }
 
 struct elaborator::first_pass_info {
@@ -1320,12 +1332,27 @@ expr elaborator::visit_app_core(expr fn, buffer<expr> const & args, optional<exp
                 if (args.size() >= info->m_nexplicit) {
                     return visit_elim_app(new_fn, *info, args, expected_type, ref);
                 } else {
-                    trace_elab(tout() << pos_string_for(ref) << " 'eliminator' elaboration is not used for '" << fn <<
-                               "' because it is not fully applied, #" << info->m_nexplicit <<
-                               " explicit arguments expected\n";);
+                    try {
+                        return visit_base_app(new_fn, amask, args, expected_type, ref);
+                    } catch (elaborator_exception & ex) {
+                        throw nested_elaborator_exception(ref, ex,
+                                                          format("'eliminator' elaboration was not used for '") +
+                                                          pp(fn) + format("' because it is not fully applied, #") +
+                                                          format(info->m_nexplicit) + format(" explicit arguments expected"));
+                    }
                 }
             } else if (is_no_confusion(m_env, const_name(new_fn))) {
                 return visit_no_confusion_app(new_fn, args, expected_type, ref);
+            } else {
+                try {
+                    return visit_base_app(new_fn, amask, args, expected_type, ref);
+                } catch (elaborator_exception & ex) {
+                    if (auto error_msg = m_elim_failure_info.find(const_name(new_fn))) {
+                        throw nested_elaborator_exception(ref, ex, *error_msg);
+                    } else {
+                        throw;
+                    }
+                }
             }
         }
         return visit_base_app(new_fn, amask, args, expected_type, ref);
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index 179150bdec..f0ff86a37c 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -68,7 +68,9 @@ private:
 
     /** \brief Cache for constants that are handled using "eliminator" elaboration. */
     typedef name_map<optional<elim_info>> elim_cache;
+    typedef name_map<format>              elim_failure_info;
     elim_cache        m_elim_cache;
+    elim_failure_info m_elim_failure_info;
 
     /* The following vector contains sorts that we should check
        whether the computed universe is too specific or not. */
@@ -89,6 +91,7 @@ private:
     pp_fn mk_pp_ctx();
     format pp_indent(pp_fn const & pp_fn, expr const & e);
     format pp_indent(expr const & e);
+    format pp(expr const & e);
     format pp_overloads(pp_fn const & pp_fn, buffer<expr> const & fns);
 
     expr whnf(expr const & e) { return m_ctx.whnf(e); }
diff --git a/src/frontends/lean/elaborator_exception.cpp b/src/frontends/lean/elaborator_exception.cpp
new file mode 100644
index 0000000000..23d45413ab
--- /dev/null
+++ b/src/frontends/lean/elaborator_exception.cpp
@@ -0,0 +1,42 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/scope_pos_info_provider.h"
+#include "frontends/lean/elaborator_exception.h"
+
+namespace lean {
+throwable * elaborator_exception::clone() const {
+    return new elaborator_exception(m_expr, m_fmt);
+}
+
+throwable * nested_elaborator_exception::clone() const {
+    return new nested_elaborator_exception(m_expr, m_fmt, m_exception);
+}
+
+optional<expr> nested_elaborator_exception::get_main_expr() const {
+    if (auto r = m_exception->get_main_expr()) return r;
+    else return m_expr;
+}
+
+format nested_elaborator_exception::pp() const {
+    format r = m_exception->pp();
+    if (dynamic_cast<nested_elaborator_exception*>(m_exception.get()) == nullptr) {
+        r += line() + format("Additional information:");
+    }
+    pos_info_provider * pip = get_pos_info_provider();
+    if (pip && m_expr) {
+        if (auto p = pip->get_pos_info(*m_expr)) {
+            r += line() + format(pip->get_file_name()) +
+                colon() + format(p->first) + colon() + format(p->second) + colon() + space() + format("context: ") + m_fmt;
+        } else {
+            r += line() + format("context: ") + m_fmt;
+        }
+    } else {
+        r += line() + format("context: ") + m_fmt;
+    }
+    return r;
+}
+}
diff --git a/src/frontends/lean/elaborator_exception.h b/src/frontends/lean/elaborator_exception.h
index af81c9fd5e..fbd6040f12 100644
--- a/src/frontends/lean/elaborator_exception.h
+++ b/src/frontends/lean/elaborator_exception.h
@@ -5,16 +5,35 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include "util/sstream.h"
 #include "library/io_state.h"
 
 namespace lean {
 class elaborator_exception : public formatted_exception {
+protected:
     elaborator_exception(optional<expr> const & e, format const & fmt):formatted_exception(e, fmt) {}
 public:
     elaborator_exception(expr const & e, format const & fmt):formatted_exception(e, fmt) {}
     elaborator_exception(expr const & e, sstream const & strm):formatted_exception(e, format(strm.str())) {}
     elaborator_exception(expr const & e, char const * msg):formatted_exception(e, format(msg)) {}
-    virtual throwable * clone() const override { return new elaborator_exception(m_expr, m_fmt); }
+    virtual throwable * clone() const override;
     virtual void rethrow() const override { throw *this; }
 };
+
+class nested_elaborator_exception : public elaborator_exception {
+    std::shared_ptr<elaborator_exception> m_exception;
+    nested_elaborator_exception(optional<expr> const & ref, format const & fmt,
+                                std::shared_ptr<elaborator_exception> const & ex):
+        elaborator_exception(ref, fmt), m_exception(ex) {}
+public:
+    nested_elaborator_exception(optional<expr> const & ref, elaborator_exception const & ex, format const & fmt):
+        elaborator_exception(ref, fmt),
+        m_exception(static_cast<elaborator_exception*>(ex.clone())) {}
+    nested_elaborator_exception(expr const & ref, elaborator_exception const & ex, format const & fmt):
+        nested_elaborator_exception(some_expr(ref), ex, fmt) {}
+    virtual void rethrow() const override { throw *this; }
+    virtual throwable * clone() const override;
+    virtual optional<expr> get_main_expr() const override;
+    virtual format pp() const override;
+};
 }
diff --git a/src/library/io_state.h b/src/library/io_state.h
index 907d6286c6..3b64f42395 100644
--- a/src/library/io_state.h
+++ b/src/library/io_state.h
@@ -67,8 +67,8 @@ public:
     virtual char const * what() const noexcept;
     virtual throwable * clone() const { return new formatted_exception(m_expr, m_fmt); }
     virtual void rethrow() const { throw *this; }
-    optional<expr> get_main_expr() const { return m_expr; }
-    format pp() const { return m_fmt; }
+    virtual optional<expr> get_main_expr() const { return m_expr; }
+    virtual format pp() const { return m_fmt; }
 };
 
 struct scope_global_ios {
diff --git a/tests/lean/def1.lean.expected.out b/tests/lean/def1.lean.expected.out
index 5f44ec03a1..c75daa51dd 100644
--- a/tests/lean/def1.lean.expected.out
+++ b/tests/lean/def1.lean.expected.out
@@ -4,3 +4,8 @@ has type
   ?m_2 = ?m_2
 but is expected to have type
   f b = f c
+Additional information:
+def1.lean:5:16: context: the inferred motive for the eliminator-like application is
+  λ (_x : A), f _x = f c
+def1.lean:5:3: context: the inferred motive for the eliminator-like application is
+  λ (_x : A), f a = f c
diff --git a/tests/lean/elab_error_msgs.lean b/tests/lean/elab_error_msgs.lean
new file mode 100644
index 0000000000..023a0a85aa
--- /dev/null
+++ b/tests/lean/elab_error_msgs.lean
@@ -0,0 +1,14 @@
+lemma ex1 (a b : Prop) : a ∧ b ∧ b → b ∧ a :=
+and.rec (λ ha hb hb, ha)
+
+@[elab_as_eliminator]
+def bogus_elim {A : Type} {C : A → A → Prop} {a b : A} (h : C a a) : C a b :=
+sorry
+
+lemma ex2 (a b : Prop) : a ∧ b :=
+bogus_elim trivial
+
+lemma ex1 (a b : Prop) : a ∧ b ∧ b → b ∧ a :=
+λ h, and.rec
+       (λ ha hb, ha + hb)
+       h
diff --git a/tests/lean/elab_error_msgs.lean.expected.out b/tests/lean/elab_error_msgs.lean.expected.out
new file mode 100644
index 0000000000..e124407afb
--- /dev/null
+++ b/tests/lean/elab_error_msgs.lean.expected.out
@@ -0,0 +1,30 @@
+elab_error_msgs.lean:2:0: error: type mismatch at application
+  and.rec (λ (ha : ?m_1) (hb : delayed[?m_2]) (hb : delayed[?m_4]), ha)
+term
+  λ (ha : ?m_1) (hb : delayed[?m_2]) (hb : delayed[?m_4]), ha
+has type
+  Π (ha : ?m_1) (hb : delayed[?m_2]) (hb_1 : delayed[?m_4]), delayed[?m_1]
+but is expected to have type
+  ?m_1 → ?m_2 → ?m_3
+Additional information:
+elab_error_msgs.lean:2:0: context: 'eliminator' elaboration was not used for 'and.rec' because it is not fully applied, #2 explicit arguments expected
+elab_error_msgs.lean:9:0: error: type mismatch at application
+  bogus_elim trivial
+term
+  trivial
+has type
+  true
+but is expected to have type
+  ?m_2 ?m_3 ?m_3
+Additional information:
+elab_error_msgs.lean:9:0: context: 'eliminator' elaboration is not used for 'bogus_elim' because a (reliable) way to synthesize 'a', which occurs in the resulting type, was not found
+
+elab_error_msgs.lean:13:20: error: failed to synthesize type class instance for
+a b : Prop,
+h : a ∧ b ∧ b,
+ha : a,
+hb : b ∧ b
+⊢ has_add (b ∧ a)
+Additional information:
+elab_error_msgs.lean:12:5: context: the inferred motive for the eliminator-like application is
+  b ∧ a
diff --git a/tests/lean/hole_issue2.lean.expected.out b/tests/lean/hole_issue2.lean.expected.out
index daf2d2fd96..de17bdf257 100644
--- a/tests/lean/hole_issue2.lean.expected.out
+++ b/tests/lean/hole_issue2.lean.expected.out
@@ -9,6 +9,9 @@ h : ⟦l₁⟧ ⊆ ⟦l₂⟧,
 w : A,
 hw : ¬list.count w l₁ ≤ list.count w l₂
 ⊢ false
+Additional information:
+hole_issue2.lean:19:0: context: the inferred motive for the eliminator-like application is
+  λ (_x _x_1 : bag A), decidable (_x ⊆ _x_1)
 hole_issue2.lean:29:65: error: don't know how to synthesize placeholder
 state:
 A : Type,
@@ -18,6 +21,9 @@ _match : Π (b : bool), subcount l₁ l₂ = b → decidable (⟦l₁⟧ ⊆ ⟦
 H : subcount l₁ l₂ = ff,
 h : ⟦l₁⟧ ⊆ ⟦l₂⟧
 ⊢ ∀ (a : A), ¬list.count a l₁ ≤ list.count a l₂ → false
+Additional information:
+hole_issue2.lean:26:0: context: the inferred motive for the eliminator-like application is
+  λ (_x _x_1 : bag A), decidable (_x ⊆ _x_1)
 hole_issue2.lean:36:28: error: don't know how to synthesize placeholder
 state:
 A : Type,
@@ -27,3 +33,6 @@ _match : Π (b : bool), subcount l₁ l₂ = b → decidable (⟦l₁⟧ ⊆ ⟦
 H : subcount l₁ l₂ = ff,
 h : ⟦l₁⟧ ⊆ ⟦l₂⟧
 ⊢ false
+Additional information:
+hole_issue2.lean:33:0: context: the inferred motive for the eliminator-like application is
+  λ (_x _x_1 : bag A), decidable (_x ⊆ _x_1)
diff --git a/tests/lean/red.lean.expected.out b/tests/lean/red.lean.expected.out
index 35fbda2da8..41686ba96b 100644
--- a/tests/lean/red.lean.expected.out
+++ b/tests/lean/red.lean.expected.out
@@ -10,9 +10,15 @@ has type
   ?m_2 = ?m_2
 but is expected to have type
   f a = a
+Additional information:
+red.lean:12:0: context: the inferred motive for the eliminator-like application is
+  λ (_x : ℕ), f a = a
 red.lean:17:0: error: "eliminator" elaborator type mismatch, term
   rfl
 has type
   ?m_2 = ?m_2
 but is expected to have type
   f a = a
+Additional information:
+red.lean:17:0: context: the inferred motive for the eliminator-like application is
+  λ (_x : ℕ), f a = a