diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index cce9a74b2a..4713991f91 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -532,7 +532,11 @@ optional<expr> elaborator::mk_coercion(expr const & e, expr e_type, expr type, e
 
 bool elaborator::is_def_eq(expr const & e1, expr const & e2) {
     type_context::approximate_scope scope(m_ctx);
-    return m_ctx.is_def_eq(e1, e2);
+    try {
+        return m_ctx.is_def_eq(e1, e2);
+    } catch (exception &) {
+        return false;
+    }
 }
 
 bool elaborator::try_is_def_eq(expr const & e1, expr const & e2) {
diff --git a/tests/lean/bad_error4.lean b/tests/lean/bad_error4.lean
new file mode 100644
index 0000000000..5569189f20
--- /dev/null
+++ b/tests/lean/bad_error4.lean
@@ -0,0 +1,5 @@
+structure foo :=
+(f: unit -> unit)
+
+definition bar : foo :=
+{ f := λ a b, _ }
diff --git a/tests/lean/bad_error4.lean.expected.out b/tests/lean/bad_error4.lean.expected.out
new file mode 100644
index 0000000000..b8e455c604
--- /dev/null
+++ b/tests/lean/bad_error4.lean.expected.out
@@ -0,0 +1,8 @@
+bad_error4.lean:5:0: error: type mismatch at application
+  foo.mk (λ (a : unit) (b : delayed[?m_1]), delayed[?m_2])
+term
+  λ (a : unit) (b : delayed[?m_1]), delayed[?m_2]
+has type
+  Π (a : unit) (b : delayed[?m_1]), delayed[?m_3]
+but is expected to have type
+  unit → unit