fix(frontends/lean/elaborator): bug when mixing implicit arguments and sections

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

src/frontends/lean/decl_cmds.cpp

@@ -258,7 +258,7 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
         type = Pi_as_is(section_ps, type, p);
         value = Fun_as_is(section_ps, value, p);
         levels section_ls = collect_section_levels(ls, p);
-        expr ref = mk_app(mk_explicit(mk_constant(real_n, section_ls)), section_ps);
+        expr ref = mk_implicit(mk_app(mk_explicit(mk_constant(real_n, section_ls)), section_ps));
         p.add_local_expr(n, ref);
     }
     level_param_names new_ls;

src/frontends/lean/elaborator.cpp

@@ -948,7 +948,13 @@ public:
         } else if (is_explicit(get_app_fn(e))) {
             r    = visit_core(e);
         } else {
-            r    = visit_core(e);
+            if (is_implicit(e)) {
+                r = get_implicit_arg(e);
+                if (is_explicit(r)) r = get_explicit_arg(r);
+                r = visit_core(r);
+            } else {
+                r = visit_core(e);
+            }
             if (!is_lambda(r)) {
                 tag  g      = e.get_tag();
                 expr r_type = whnf(infer_type(r));

src/library/explicit.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 static name g_explicit_name("@");
+static name g_implicit_name("@^-1");
 static name g_as_is_name("as_is");
 [[ noreturn ]] static void throw_ex(name const & n) { throw exception(sstream() << "unexpected occurrence of '" << n << "' expression"); }
 
@@ -26,20 +27,22 @@ public:
     virtual void write(serializer &) const { throw_ex(get_name()); }
 };
 
-class as_is_macro_cell : public explicit_macro_cell {
-public:
-    virtual name get_name() const { return g_as_is_name; }
-};
+struct as_is_macro_cell : public explicit_macro_cell { virtual name get_name() const { return g_as_is_name; } };
+struct implicit_macro_cell : public explicit_macro_cell { virtual name get_name() const { return g_implicit_name; } };
 
 static macro_definition g_explicit(new explicit_macro_cell());
 static macro_definition g_as_is(new as_is_macro_cell());
+static macro_definition g_implicit(new implicit_macro_cell());
 
 expr mk_explicit(expr const & e) { return mk_macro(g_explicit, 1, &e); }
 bool is_explicit(expr const & e) { return is_macro(e) && macro_def(e) == g_explicit; }
 expr mk_as_is(expr const & e) { return mk_macro(g_as_is, 1, &e); }
 bool is_as_is(expr const & e) { return is_macro(e) && macro_def(e) == g_as_is; }
+expr mk_implicit(expr const & e) { return mk_macro(g_implicit, 1, &e); }
+bool is_implicit(expr const & e) { return is_macro(e) && macro_def(e) == g_implicit; }
 expr const & get_explicit_arg(expr const & e) { lean_assert(is_explicit(e)); return macro_arg(e, 0); }
 expr const & get_as_is_arg(expr const & e) { lean_assert(is_as_is(e)); return macro_arg(e, 0); }
+expr const & get_implicit_arg(expr const & e) { lean_assert(is_implicit(e)); return macro_arg(e, 0); }
 
 static int mk_explicit(lua_State * L) { return push_expr(L, mk_explicit(to_expr(L, 1))); }
 static int is_explicit(lua_State * L) { return push_boolean(L, is_explicit(to_expr(L, 1))); }

src/library/explicit.h

@@ -9,29 +9,35 @@ Author: Leonardo de Moura
 #include "kernel/expr.h"
 
 namespace lean {
-/**
-    \brief Create an explicit expression '@ f'.
+/** \brief Create an explicit expression '@ f'.
     This only affects the elaborator behavior.
 */
 expr mk_explicit(expr const & e);
 /** \brief Return true iff \c e is an explicit expression. */
 bool is_explicit(expr const & e);
-/**
-    \brief Create an explicit expression that is accepted as is
+/** \brief Create an explicit expression that is accepted as is
     by the elaborator.
 */
 expr mk_as_is(expr const & e);
 /** \brief Return true iff \c e was created with mk_as_is. */
 bool is_as_is(expr const & e);
-/**
-   \brief Return the argument of an explicit expression.
-   \pre is_explicit(e)
+/** \brief Create an implicit expression '@^-1 f'.
+    This only affects the elaborator behavior. This expression "cancels" the effect of '@'
+*/
+expr mk_implicit(expr const & e);
+/** \brief Return true iff \c e is an implicit expression. */
+bool is_implicit(expr const & e);
+/** \brief Return the argument of an explicit expression.
+    \pre is_explicit(e)
 */
 expr const & get_explicit_arg(expr const & e);
-/**
-   \brief Return the argument of an expression created using mk_as_is.
-   \pre is_as_is(e)
+/** \brief Return the argument of an expression created using mk_as_is.
+    \pre is_as_is(e)
 */
 expr const & get_as_is_arg(expr const & e);
+/** \brief Return the argument of an implicit expression.
+    \pre is_implicit(e)
+*/
+expr const & get_implicit_arg(expr const & e);
 void open_explicit(lua_State * L);
 }

tests/lean/run/bug6.lean

@@ -0,0 +1,20 @@
+import standard
+section
+  parameter {A : Type}
+  theorem T {a b : A} (H : a = b) : b = a
+  := symm H
+  variables x y : A
+  axiom H : x = y
+  check T H
+  check T
+end
+
+section
+  parameter {A : Type}
+  theorem T2 ⦃a b : A⦄ (H : a = b) : b = a
+  := symm H
+  variables x y : A
+  axiom H : x = y
+  check T2 H
+  check T2
+end

tests/lean/run/e11.lean

@@ -35,6 +35,7 @@ section
   definition add_in (a : int) (b : nat) := a + (of_nat b)
   infixl + := add_ni
   infixl + := add_in
+  check add_ni
 
   check i + n
   check n + i