feat(frontends/lean/elaborator): hide auxiliary 'match' hypothesis during elaboration

src/frontends/lean/decl_cmds.cpp

@@ -816,6 +816,10 @@ expr parse_local_equations(parser & p, expr const & fn) {
     return p.save_pos(mk_equations(fns.size(), eqns.size(), eqns.data()), pos);
 }
 
+static name * g_match_name = nullptr;
+
+bool is_match_binder_name(name const & n) { return n == *g_match_name; }
+
 /** \brief Use equations compiler infrastructure to implement match-with */
 expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos) {
     buffer<expr> eqns;
@@ -823,7 +827,7 @@ expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos) {
     try {
         t  = p.parse_expr();
         p.check_token_next(get_with_tk(), "invalid 'match' expression, 'with' expected");
-        expr fn = mk_local(p.mk_fresh_name(), "match", mk_expr_placeholder(), binder_info());
+        expr fn = mk_local(p.mk_fresh_name(), *g_match_name, mk_expr_placeholder(), binder_info());
         if (p.curr_is_token(get_end_tk())) {
             p.next();
             // empty match-with
@@ -1466,4 +1470,11 @@ void register_decl_cmds(cmd_table & r) {
     add_cmd(r, cmd_info("abbreviation", "declare a new abbreviation", abbreviation_cmd));
     add_cmd(r, cmd_info("omit",         "undo 'include' command", omit_cmd));
 }
+
+void initialize_decl_cmds() {
+    g_match_name = new name(name::mk_internal_unique_name(), "match");
+}
+void finalize_decl_cmds() {
+    delete g_match_name;
+}
 }

src/frontends/lean/decl_cmds.h

@@ -19,6 +19,9 @@ bool parse_univ_params(parser & p, buffer<name> & ps);
 expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos);
 expr parse_local_equations(parser & p, expr const & fn);
 
+/** \brief Return true iff \c n is the auxiliary name used to elaborate match-expressions. */
+bool is_match_binder_name(name const & n);
+
 /**   \brief Add universe levels from \c found_ls to \c ls_buffer (only the levels that do not already occur in \c ls_buffer are added).
    Then sort \c ls_buffer (using the order in which the universe levels were declared).
 */
@@ -30,4 +33,7 @@ environment local_abbreviation_cmd(parser & p);
 /** \brief Parse a local attribute command */
 environment local_attribute_cmd(parser & p);
 void register_decl_cmds(cmd_table & r);
+
+void initialize_decl_cmds();
+void finalize_decl_cmds();
 }

src/frontends/lean/elaborator.cpp

@@ -52,6 +52,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/begin_end_ext.h"
 #include "frontends/lean/elaborator_exception.h"
 #include "frontends/lean/calc.h"
+#include "frontends/lean/decl_cmds.h"
 
 namespace lean {
 /** \brief Custom converter that does not unfold constants that contains coercions from it.
@@ -828,9 +829,11 @@ expr elaborator::visit_binding(expr e, expr_kind k, constraint_seq & cs) {
 
         ds.push_back(d);
         expr l   = mk_local(binding_name(e), d, binding_info(e));
-        if (binding_info(e).is_contextual())
+        if (!is_match_binder_name(binding_name(e))) {
-            m_context.add_local(l);
+            if (binding_info(e).is_contextual())
-        m_full_context.add_local(l);
+                m_context.add_local(l);
+            m_full_context.add_local(l);
+        }
         ls.push_back(l);
         e = binding_body(e);
     }
@@ -1090,9 +1093,16 @@ static expr assign_equation_lhs_metas(type_checker & tc, expr const & eqns) {
                                 options o = fmt.get_options().update_if_undef(get_pp_implicit_name(), true);
                                 o = o.update_if_undef(get_pp_notation_option_name(), false);
                                 formatter new_fmt = fmt.update_options(o);
-                                format r("invalid recursive equation, left-hand-side contains meta-variable");
+                                expr const & f = get_app_fn(lhs);
-                                r += format(" (possible solution: provide implicit parameters occurring in left-hand-side explicitly)");
+                                format r;
-                                r += pp_indent_expr(new_fmt, lhs);
+                                if (is_local(f) && is_match_binder_name(local_pp_name(f))) {
+                                    r = format("invalid 'match' expression, left-hand-side contains meta-variable");
+                                    r += pp_indent_expr(new_fmt, app_arg(lhs));
+                                } else {
+                                    r = format("invalid recursive equation, left-hand-side contains meta-variable");
+                                    r += format(" (possible solution: provide implicit parameters occurring in left-hand-side explicitly)");
+                                    r += pp_indent_expr(new_fmt, lhs);
+                                }
                                 return r;
                             });
                     }
@@ -1235,7 +1245,10 @@ expr elaborator::visit_equation(expr const & eq, constraint_seq & cs) {
     expr rhs_type = infer_type(new_rhs, cs);
     justification j = mk_justification(eq, [=](formatter const & fmt, substitution const & subst) {
             substitution s(subst);
-            return pp_def_type_mismatch(fmt, local_pp_name(lhs_fn), s.instantiate(lhs_type), s.instantiate(rhs_type));
+            name n = local_pp_name(lhs_fn);
+            if (is_match_binder_name(n))
+                n = "match";
+            return pp_def_type_mismatch(fmt, n, s.instantiate(lhs_type), s.instantiate(rhs_type));
         });
     pair<expr, constraint_seq> new_rhs_cs = ensure_has_type(new_rhs, rhs_type, lhs_type, j);
     new_rhs = new_rhs_cs.first;

src/frontends/lean/init_module.cpp

@@ -30,6 +30,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/server.h"
 #include "frontends/lean/local_ref_info.h"
 #include "frontends/lean/obtain_expr.h"
+#include "frontends/lean/decl_cmds.h"
 
 namespace lean {
 void initialize_frontend_lean_module() {
@@ -59,8 +60,10 @@ void initialize_frontend_lean_module() {
     initialize_find_cmd();
     initialize_local_ref_info();
     initialize_obtain_expr();
+    initialize_decl_cmds();
 }
 void finalize_frontend_lean_module() {
+    finalize_decl_cmds();
     finalize_obtain_expr();
     finalize_local_ref_info();
     finalize_find_cmd();

tests/lean/run/subst_test.lean

@@ -0,0 +1,18 @@
+import data.nat
+open nat
+
+structure less_than (n : nat) := (val : nat) (lt : val < n)
+
+namespace less_than
+open decidable
+
+set_option pp.beta false
+
+definition less_than.has_decidable_eq [instance] (n : nat) : ∀ (i j : less_than n), decidable (i = j)
+| (mk ival ilt) (mk jval jlt) :=
+  match nat.has_decidable_eq ival jval with
+  | inl veq := inl (by subst veq)
+  | inr vne := inr (by intro h; injection h; contradiction)
+  end
+
+end less_than

tests/lean/unzip_error.lean.expected.out

@@ -1,2 +1,2 @@
-unzip_error.lean:9:2: error: invalid recursive equation, left-hand-side contains meta-variable (possible solution: provide implicit parameters occurring in left-hand-side explicitly)
+unzip_error.lean:9:2: error: invalid 'match' expression, left-hand-side contains meta-variable
-  match (@mk (vector A ?M_1) (vector B ?M_1) va vb)
+  @mk (vector A ?M_1) (vector B ?M_1) va vb