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

@@ -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) {

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); });
                     }
                 }
             }

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

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 :=

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