feat(frontends/lean): remove restriction on implict arguments, add new test that demonstrates the new feature

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

src/frontends/lean/builtin_exprs.cpp

@@ -348,8 +348,7 @@ static expr parse_including_expr(parser & p, unsigned, expr const *, pos_info co
     parser::local_scope scope(p);
     buffer<expr> new_locals;
     for (auto old_l : locals) {
-        binder_info bi = local_info(old_l);
-        bi = bi.update_contextual(true);
+        binder_info bi = mk_contextual_info(true);
         expr new_l     = p.save_pos(mk_local(local_pp_name(old_l), mk_as_is(mlocal_type(old_l)), bi), pos);
         p.add_local(new_l);
         new_locals.push_back(new_l);

src/frontends/lean/decl_cmds.cpp

@@ -202,6 +202,11 @@ static void check_end_of_theorem(parser const & p) {
         throw parser_error("':=', '.', command, script, or end-of-file expected", p.pos());
 }
 
+static void erase_local_binder_info(buffer<expr> & ps) {
+    for (expr & p : ps)
+        p = update_local(p, binder_info());
+}
+
 environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
     auto n_pos = p.pos();
     unsigned start_line = n_pos.first;
@@ -260,6 +265,7 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
                 value = p.parse_scoped_expr(ps, *lenv);
             }
             type  = Pi(ps, type, p);
+            erase_local_binder_info(ps);
             value = Fun(ps, value, p);
         }
 
@@ -285,7 +291,10 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
         buffer<expr> section_ps;
         collect_section_locals(type, value, p, section_ps);
         type = Pi_as_is(section_ps, type, p);
-        value = Fun_as_is(section_ps, value, p);
+        buffer<expr> section_value_ps;
+        section_value_ps.append(section_ps);
+        erase_local_binder_info(section_value_ps);
+        value = Fun_as_is(section_value_ps, value, p);
         levels section_ls = collect_section_levels(ls, p);
         for (expr & p : section_ps)
             p = mk_explicit(p);

src/frontends/lean/elaborator.cpp

@@ -1248,16 +1248,14 @@ public:
             } else {
                 r = visit_core(e, cs);
             }
-            if (!is_lambda(r)) {
-                tag  g         = e.get_tag();
-                expr r_type    = whnf(infer_type(r, cs), cs);
-                expr imp_arg;
-                bool is_strict = false;
-                while (is_pi(r_type) && binding_info(r_type).is_implicit()) {
-                    imp_arg = mk_placeholder_meta(some_expr(binding_domain(r_type)), g, is_strict, cs);
-                    r       = mk_app(r, imp_arg, g);
-                    r_type  = whnf(instantiate(binding_body(r_type), imp_arg), cs);
-                }
+            tag  g         = e.get_tag();
+            expr r_type    = whnf(infer_type(r, cs), cs);
+            expr imp_arg;
+            bool is_strict = false;
+            while (is_pi(r_type) && binding_info(r_type).is_implicit()) {
+                imp_arg = mk_placeholder_meta(some_expr(binding_domain(r_type)), g, is_strict, cs);
+                r       = mk_app(r, imp_arg, g);
+                r_type  = whnf(instantiate(binding_body(r_type), imp_arg), cs);
             }
         }
         save_type_data(b, r);

src/kernel/expr.cpp

@@ -553,6 +553,10 @@ expr update_local(expr const & e, expr const & new_type, binder_info const & bi)
         return copy_tag(e, mk_local(mlocal_name(e), local_pp_name(e), new_type, bi));
 }
 
+expr update_local(expr const & e, binder_info const & bi) {
+    return update_local(e, mlocal_type(e), bi);
+}
+
 expr update_sort(expr const & e, level const & new_level) {
     if (!is_eqp(sort_level(e), new_level))
         return copy_tag(e, mk_sort(new_level));

src/kernel/expr.h

@@ -676,6 +676,7 @@ expr update_binding(expr const & e, expr const & new_domain, expr const & new_bo
 expr update_binding(expr const & e, expr const & new_domain, expr const & new_body, binder_info const & bi);
 expr update_mlocal(expr const & e, expr const & new_type);
 expr update_local(expr const & e, expr const & new_type, binder_info const & bi);
+expr update_local(expr const & e, binder_info const & bi);
 expr update_sort(expr const & e, level const & new_level);
 expr update_constant(expr const & e, levels const & new_levels);
 expr update_macro(expr const & e, unsigned num, expr const * args);

tests/lean/pp.lean.expected.out

@@ -1,5 +1,5 @@
-λ {A : Type} (B : Type) (a : A) (b : B), a : Π {A : Type} (B : Type), A → B → A
-λ {A B : Type} (a : A) (b : B), a : Π {A B : Type}, A → B → A
+λ {A : Type} (B : Type) (a : A) (b : B), a : Π (B : Type), ?M_1 → B → ?M_1
+λ {A B : Type} (a : A) (b : B), a : ?M_1 → ?M_2 → ?M_1
 λ (A : Type) {B : Type} (a : A) (b : B), a : Π (A : Type) {B : Type}, A → B → A
 λ (A B : Type) (a : A) (b : B), a : Π (A B : Type), A → B → A
 λ [A : Type] (B : Type) (a : A) (b : B), a : Π [A : Type] (B : Type), A → B → A

tests/lean/run/imp2.lean

@@ -0,0 +1,4 @@
+import data.num
+check (λ {A : Type} (a : A), a) 10
+check (λ {A} a, a) 10
+check (λ a, a) 10

tests/lean/t7.lean.expected.out

@@ -2,5 +2,5 @@ id : ?M_1 → ?M_1
 trans : (?M_1 → ?M_1 → Prop) → Prop
 symm : (?M_1 → ?M_1 → Prop) → Prop
 equivalence : (?M_1 → ?M_1 → Prop) → Prop
-λ {A : Type} (R : A → A → Prop),
+λ (A : Type) (R : A → A → Prop),
   and (and (refl R) (symm R)) (trans R)