From a59eec39b8e69902dca071a76fc8d1a217774b18 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 25 Jul 2014 09:44:40 -0700
Subject: [PATCH] feat(frontends/lean): improve 'type mismatch' error position,
 and annotate 'have'-expressions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/builtin_exprs.cpp | 2 +-
 src/frontends/lean/elaborator.cpp    | 2 +-
 tests/lean/crash.lean.expected.out   | 2 +-
 tests/lean/let1.lean.expected.out    | 2 +-
 tests/lean/t10.lean.expected.out     | 2 +-
 5 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 695730bb1..f36dd63a3 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -265,7 +265,7 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> con
     // remark: mk_contextual_info(false) informs the elaborator that prop should not occur inside metavariables.
     body = abstract(body, l);
     expr r = p.save_pos(mk_lambda(id, prop, body, bi), pos);
-    return p.save_pos(mk_app(r, proof), pos);
+    return p.save_pos(mk_have_annotation(p.mk_app(r, proof, pos)), pos);
 }
 
 static expr parse_have(parser & p, unsigned, expr const *, pos_info const & pos) {
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index f6342951c..1201ea13c 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -806,7 +806,7 @@ public:
                         // rely on unification hints to solve this constraint
                         add_cnstr(mk_eq_cnstr(a_type, d_type, j.get()));
                     } else {
-                        throw_kernel_exception(m_env, a, [=](formatter const & fmt) { return pp_app_type_mismatch(fmt, e, d_type, a_type); });
+                        throw_kernel_exception(m_env, r, [=](formatter const & fmt) { return pp_app_type_mismatch(fmt, e, d_type, a_type); });
                     }
                 }
             }
diff --git a/tests/lean/crash.lean.expected.out b/tests/lean/crash.lean.expected.out
index 023223ef5..a1f1fd67b 100644
--- a/tests/lean/crash.lean.expected.out
+++ b/tests/lean/crash.lean.expected.out
@@ -1,4 +1,4 @@
-crash.lean:6:0: error: type mismatch at application
+crash.lean:8:12: error: type mismatch at application
   (λ (H' : not P), _) H
 expected type:
   not P
diff --git a/tests/lean/let1.lean.expected.out b/tests/lean/let1.lean.expected.out
index eb0dbef4c..d08ac4f68 100644
--- a/tests/lean/let1.lean.expected.out
+++ b/tests/lean/let1.lean.expected.out
@@ -13,7 +13,7 @@ let and_intro : ∀ (p q : Prop),
 in and_intro :
   ∀ (p q : Prop),
     p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q
-let1.lean:17:20: error: type mismatch at application
+let1.lean:16:10: error: type mismatch at application
   (λ (and_intro : ∀ (p q : Prop), p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) q p),
      let and_elim_left : ∀ (p q : Prop),
                            (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) p q → p :=
diff --git a/tests/lean/t10.lean.expected.out b/tests/lean/t10.lean.expected.out
index 1904d191c..4220a613d 100644
--- a/tests/lean/t10.lean.expected.out
+++ b/tests/lean/t10.lean.expected.out
@@ -1,5 +1,5 @@
 ite (and p q) (f x) y : N
-t10.lean:14:22: error: type mismatch at application
+t10.lean:14:6: error: type mismatch at application
   ite (and p q) q
 expected type:
   N