fix(frontends/lean/tactic_notation): erase position information quoted terms occurring inside `[...]

See new test for understanding the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/parser.cpp

@@ -318,6 +318,11 @@ expr parser::save_pos(expr e, pos_info p) {
     return e;
 }
 
+void parser::erase_pos(expr const & e) {
+    auto t = get_tag(e);
+    m_pos_table.erase(t);
+}
+
 expr parser::update_pos(expr e, pos_info p) {
     auto t = get_tag(e);
     m_pos_table.insert(t, p);

src/frontends/lean/parser.h

@@ -225,6 +225,7 @@ public:
     expr save_pos(expr e, pos_info p);
     expr rec_save_pos(expr const & e, pos_info p);
     expr update_pos(expr e, pos_info p);
+    void erase_pos(expr const & e);
     pos_info pos_of(expr const & e, pos_info default_pos) const;
     pos_info pos_of(expr const & e) const { return pos_of(e, pos()); }
     pos_info cmd_pos() const { return m_last_cmd_pos; }

src/frontends/lean/tactic_notation.cpp

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "kernel/abstract.h"
+#include "kernel/for_each_fn.h"
 #include "library/annotation.h"
 #include "library/constants.h"
 #include "library/quote.h"
@@ -584,14 +585,41 @@ expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) {
     }
 }
 
+/*
+Consider the following example:
+
+  meta def apply_zero_add (a : pexpr) : tactic unit :=
+  `[apply zero_add %%a] -- We don't want the error to be reported here when 'a' does not have the expected type.
+
+  example (a : nat) : 0 + a = a :=
+  begin
+    apply_zero_add `(tt), -- Error should be here
+  end
+
+We address the issue above by erasing position information from quoted terms nested in 'e'.
+*/
+static void erase_quoted_terms_pos_info(parser & p, expr const & e) {
+    for_each(e, [&](expr const & e, unsigned) {
+            if (is_quote(e)) {
+                for_each(get_quote_expr(e), [&](expr const & e, unsigned) {
+                        p.erase_pos(e);
+                        return true;
+                    });
+            }
+            return true;
+        });
+}
+
 expr parse_auto_quote_tactic_block(parser & p, unsigned, expr const *, pos_info const & pos) {
     name const & tac_class = get_tactic_name();
     bool use_rstep    = false;
     bool report_error = false;
     expr r = parse_tactic(p, tac_class, use_rstep, report_error);
+    erase_quoted_terms_pos_info(p, r);
     while (p.curr_is_token(get_comma_tk())) {
         p.next();
         expr next = parse_tactic(p, tac_class, use_rstep, report_error);
+        erase_quoted_terms_pos_info(p, next);
         r = p.mk_app({p.save_pos(mk_constant(get_pre_monad_and_then_name()), pos), r, next}, pos);
     }
     p.check_token_next(get_rbracket_tk(), "invalid auto-quote tactic block, ']' expected");

src/library/tactic/elaborate.cpp

@@ -28,9 +28,11 @@ static bool report_failure(elaborator_exception const & ex, expr const & mvar, c
     if (!ref) return false;
     optional<metavar_decl> d = s.mctx().find_metavar_decl(mvar);
     if (!d) return false;
+    optional<pos_info> pos = pip->get_pos_info(*ref);
+    if (!pos) return false;
     auto tc = std::make_shared<type_context>(s.env(), s.get_options(), s.mctx(), d->get_context());
     message_builder out(pip, tc, s.env(), get_global_ios(), pip->get_file_name(),
-                        pip->get_pos_info_or_some(*ref), ERROR);
+                        *pos, ERROR);
     out.set_exception(ex);
     out << line() + format(header) + line() + s.pp();
     out.report();

tests/lean/quote_error_pos.lean

@@ -8,9 +8,6 @@ begin
   apply_zero_add `(tt), -- Error should be here
 end
 
-/-
--- This test is stil failing, Lean is reporting an error inside of `[apply ...]
--- Possible solution: erase position information from quoted terms inside of `[...]
 meta def apply_zero_add2 (a : pexpr) : tactic unit :=
 `[apply zero_add %%a]
 
@@ -18,5 +15,3 @@ example (a : nat) : 0 + a = a :=
 begin
   apply_zero_add2 `(tt), -- Error should be here
 end
-
--/

tests/lean/quote_error_pos.lean.expected.out

@@ -4,3 +4,9 @@ a : ℕ
 state:
 a : ℕ
 ⊢ 0 + a = a
+quote_error_pos.lean:16:2: error: failed to synthesize type class instance for
+a : ℕ
+⊢ add_monoid bool
+state:
+a : ℕ
+⊢ 0 + a = a