From 31a0d7d52002a76516db5157463fb111711932b3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 6 Jan 2017 08:16:16 -0800
Subject: [PATCH] feat(frontends/lean/elaborator): catch exception at is_def_eq

@semorrison this commit improves the bad error message you have
reported at lean-user. It is not perfect since the user has to
remember the position of the structure field in the constructor.
---
 src/frontends/lean/elaborator.cpp       | 6 +++++-
 tests/lean/bad_error4.lean              | 5 +++++
 tests/lean/bad_error4.lean.expected.out | 8 ++++++++
 3 files changed, 18 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/bad_error4.lean
 create mode 100644 tests/lean/bad_error4.lean.expected.out

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