From eeab242595253f615769f41cfa0188b19f6e0e24 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 5 Jan 2017 13:37:55 -0800
Subject: [PATCH] feat(frontends/lean/elaborator): catch error early

---
 src/frontends/lean/elaborator.cpp       | 1 +
 tests/lean/bad_error3.lean              | 7 +++++++
 tests/lean/bad_error3.lean.expected.out | 4 ++++
 3 files changed, 12 insertions(+)
 create mode 100644 tests/lean/bad_error3.lean
 create mode 100644 tests/lean/bad_error3.lean.expected.out

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index d58d6e4d59..cce9a74b2a 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -2725,6 +2725,7 @@ expr_pair elaborator::elaborate_with_type(expr const & e, expr const & e_type) {
     {
         expr Type  = visit(copy_tag(e_type, mk_sort(mk_level_placeholder())), none_expr());
         new_e_type = visit(e_type, some_expr(Type));
+        ensure_type(new_e_type, e_type);
         new_e      = visit(e,      some_expr(new_e_type));
         synthesize();
     }
diff --git a/tests/lean/bad_error3.lean b/tests/lean/bad_error3.lean
new file mode 100644
index 0000000000..fe7dc8ee67
--- /dev/null
+++ b/tests/lean/bad_error3.lean
@@ -0,0 +1,7 @@
+example (p : nat → nat → Prop) : p 0 :=
+begin
+end
+
+def ex (p : nat → nat → Prop) : p 0 :=
+begin
+end
diff --git a/tests/lean/bad_error3.lean.expected.out b/tests/lean/bad_error3.lean.expected.out
new file mode 100644
index 0000000000..6e2fb0bdcf
--- /dev/null
+++ b/tests/lean/bad_error3.lean.expected.out
@@ -0,0 +1,4 @@
+bad_error3.lean:1:33: error: type expected at
+  p 0
+bad_error3.lean:5:32: error: type expected at
+  p 0