fix(frontends/lean): auxiliary bind-application in do-notation was not allowing us to obtain type information for the monadic actions.

The new test exposes the problem.

src/frontends/lean/builtin_exprs.cpp

@@ -471,6 +471,10 @@ static std::tuple<optional<expr>, expr, expr, optional<expr>> parse_do_action(pa
     return std::make_tuple(lhs, type, curr, else_case);
 }
 
+static expr mk_bind_fn() {
+    return mk_no_info(mk_constant(get_bind_name()));
+}
+
 static expr parse_do(parser & p, unsigned, expr const *, pos_info const &) {
     parser::local_scope scope(p);
     buffer<expr>               es;
@@ -524,7 +528,7 @@ static expr parse_do(parser & p, unsigned, expr const *, pos_info const &) {
         --i;
         if (auto lhs = lhss[i]) {
             if (is_local(*lhs)) {
-                r = p.rec_save_pos(mk_app(p.save_pos(mk_constant(get_bind_name()), ps[i]), es[i], Fun(*lhs, r, p)), ps[i]);
+                r = p.rec_save_pos(mk_app(p.save_pos(mk_bind_fn(), ps[i]), es[i], Fun(*lhs, r, p)), ps[i]);
             } else {
                 // must introduce a "fake" match
                 auto pos   = ps[i];
@@ -546,13 +550,13 @@ static expr parse_do(parser & p, unsigned, expr const *, pos_info const &) {
                 expr eqns  = p.save_pos(mk_equations(h, eqs.size(), eqs.data()), pos);
                 expr local = mk_local("p", mk_expr_placeholder());
                 expr match = p.mk_app(eqns, local, pos);
-                r = p.rec_save_pos(mk_app(p.save_pos(mk_constant(get_bind_name()), ps[i]),
+                r = p.rec_save_pos(mk_app(p.save_pos(mk_bind_fn(), ps[i]),
                                           es[i],
                                           p.save_pos(Fun(local, match, p), pos)),
                                    pos);
             }
         } else {
-            r = p.rec_save_pos(mk_app(p.save_pos(mk_constant(get_bind_name()), ps[i]),
+            r = p.rec_save_pos(mk_app(p.save_pos(mk_bind_fn(), ps[i]),
                                       es[i],
                                       p.save_pos(mk_lambda("x", mk_expr_placeholder(), r), p.pos_of(r))),
                                ps[i]);

src/frontends/lean/elaborator.cpp

@@ -2380,6 +2380,9 @@ expr elaborator::visit(expr const & e, optional<expr> const & expected_type) {
         return copy_tag(e, visit_have_expr(e, expected_type));
     } else if (is_suffices_annotation(e)) {
         return copy_tag(e, visit_suffices_expr(e, expected_type));
+    } else if (is_no_info(e)) {
+        flet<bool> set(m_no_info, true);
+        return visit(get_annotation_arg(e), expected_type);
     } else {
         switch (e.kind()) {
         case expr_kind::Var:        lean_unreachable();  // LCOV_EXCL_LINE

src/frontends/lean/init_module.cpp

@@ -23,6 +23,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/notation_cmd.h"
 #include "frontends/lean/tactic_notation.h"
 #include "frontends/lean/decl_attributes.h"
+#include "frontends/lean/util.h"
 
 namespace lean {
 void initialize_frontend_lean_module() {
@@ -45,8 +46,10 @@ void initialize_frontend_lean_module() {
     initialize_elaborator();
     initialize_notation_cmd();
     initialize_tactic_notation();
+    initialize_frontend_lean_util();
 }
 void finalize_frontend_lean_module() {
+    finalize_frontend_lean_util();
     finalize_tactic_notation();
     finalize_notation_cmd();
     finalize_elaborator();

src/frontends/lean/util.cpp

@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "kernel/error_msgs.h"
 #include "kernel/for_each_fn.h"
 #include "library/scoped_ext.h"
+#include "library/annotation.h"
 #include "library/locals.h"
 #include "library/explicit.h"
 #include "library/aliases.h"
@@ -348,4 +349,19 @@ expr quote_name(name const & n) {
         lean_unreachable();
     }
 }
+
+static name * g_no_info = nullptr;
+name const & get_no_info() { return *g_no_info; }
+
+expr mk_no_info(expr const & e) { return mk_annotation(get_no_info(), e); }
+bool is_no_info(expr const & e) { return is_annotation(e, get_no_info()); }
+
+void initialize_frontend_lean_util() {
+    g_no_info = new name("no_info");
+    register_annotation(*g_no_info);
+}
+
+void finalize_frontend_lean_util() {
+    delete g_no_info;
+}
 }

src/frontends/lean/util.h

@@ -106,4 +106,10 @@ pair<name, option_kind> parse_option_name(parser & p, char const * error_msg);
 expr mk_tactic_unit();
 
 expr quote_name(name const & n);
+
+expr mk_no_info(expr const & e);
+bool is_no_info(expr const & e);
+
+void initialize_frontend_lean_util();
+void finalize_frontend_lean_util();
 }

tests/lean/interactive/do_info.lean

@@ -0,0 +1,16 @@
+open tactic
+
+example (a b c : nat) : a = b → c = b → a = c :=
+by do
+  h ← intro `h,
+    --^ "command": "info"
+  intros,
+  transitivity,
+--^ "command": "info"
+  trace_state,
+  assumption,
+--^ "command": "info"
+  symmetry,
+--^ "command": "info"
+  assumption
+--^ "command": "info"

tests/lean/interactive/do_info.lean.expected.out

@@ -0,0 +1,7 @@
+{"msg":{"caption":"trace output","file_name":"f","pos_col":3,"pos_line":4,"severity":"information","text":"a b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ a = ?m_1\n\na b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ ?m_1 = c\n"},"response":"additional_message"}
+{"message":"file invalidated","response":"ok","seq_num":0}
+{"record":{"full-id":"tactic.intro","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":422},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"name → tactic expr"},"response":"ok","seq_num":6}
+{"record":{"full-id":"tactic.transitivity","source":{"column":9,"file":"/library/init/meta/relation_tactics.lean","line":30},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":9}
+{"record":{"full-id":"tactic.assumption","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":529},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":12}
+{"record":{"full-id":"tactic.symmetry","source":{"column":9,"file":"/library/init/meta/relation_tactics.lean","line":27},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":14}
+{"record":{"full-id":"tactic.assumption","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":529},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":16}