feat(frontends/lean/elaborator): add pattern validator in the elaborator

@johoelzl We now produce a better message for your example:

   inductive R : ℕ → Prop
   | pos : ∀p n, R (p + n)

   lemma R_id : ∀n, R n → R n
   | (.p + .n) (R.pos p n) := R.pos p n

The new error is:

file.lean:5:2: error: invalid function application in pattern, it cannot be reduced to a constructor (possible solution, mark term as inaccessible using '.( )')
  .p + .n

src/frontends/lean/elaborator.cpp

@@ -38,13 +38,16 @@ Author: Leonardo de Moura
 #include "library/protected.h"
 #include "library/message_builder.h"
 #include "library/aliases.h"
+#include "library/inverse.h"
 #include "library/vm/vm_name.h"
 #include "library/vm/vm_expr.h"
 #include "library/tactic/kabstract.h"
+#include "library/tactic/unfold_tactic.h"
 #include "library/tactic/tactic_state.h"
 #include "library/tactic/elaborate.h"
 #include "library/equations_compiler/compiler.h"
 #include "library/equations_compiler/util.h"
+#include "library/inductive_compiler/ginductive.h"
 #include "frontends/lean/builtin_exprs.h"
 #include "frontends/lean/brackets.h"
 #include "frontends/lean/util.h"
@@ -2035,6 +2038,129 @@ void elaborator::check_inaccessible_annotations(expr const & lhs) {
     }
 }
 
+/* Recursive equation pattern validation.*/
+class validate_equation_lhs_fn : public replace_visitor {
+    elaborator &   m_elab;
+    expr           m_ref;
+
+    type_context & ctx() { return m_elab.m_ctx; }
+    environment const & env() { return m_elab.env(); }
+
+    optional<expr> expand(expr const & e) {
+        /* We don't simply use whnf because we want to avoid exposing the internal implementation
+           of definitions compiled using the equation compiler */
+        {
+            /* Try without use delta reduction */
+            type_context::transparency_scope scope(ctx(), transparency_mode::None);
+            expr new_e = ctx().whnf(e);
+            if (new_e != e) return some_expr(new_e);
+        }
+        if (auto new_e = ctx().reduce_projection(e))
+            return new_e;
+        /* Try to unfold using refl equations */
+        if (auto new_e = dunfold(ctx(), e))
+            return new_e;
+        /* Last resort, whnf using current setting */
+        expr new_e = ctx().whnf(e);
+        if (new_e != e) return some_expr(new_e);
+        return none_expr();
+    }
+
+    [[ noreturn ]] void throw_invalid_pattern(char const * msg, expr const & e) {
+        throw elaborator_exception(m_ref, format(msg)
+                                   + format(" (possible solution, mark term as inaccessible using '.( )')")
+                                   + m_elab.pp_indent(e));
+    }
+
+    virtual expr visit_local(expr const & e) override {
+        return e;
+    }
+
+    virtual expr visit_lambda(expr const & e) override {
+        throw_invalid_pattern("invalid occurrence of lambda expression in pattern", e);
+    }
+
+    virtual expr visit_pi(expr const & e) override {
+        throw_invalid_pattern("invalid occurrence of pi/forall expression in pattern", e);
+    }
+
+    virtual expr visit_let(expr const & e) override {
+        return visit(instantiate(let_body(e), let_value(e)));
+    }
+
+    virtual expr visit_sort(expr const & e) override {
+        throw_invalid_pattern("invalid occurrence of sort in pattern", e);
+    }
+
+    virtual expr visit_meta(expr const & e) override {
+        throw_invalid_pattern("invalid occurrence of metavariable in pattern", e);
+    }
+
+    [[ noreturn ]] void throw_invalid_app(expr const & e) {
+        if (is_constant(e))
+            throw_invalid_pattern("invalid constant in pattern, it cannot be reduced to a constructor", e);
+        else
+            throw_invalid_pattern("invalid function application in pattern, it cannot be reduced to a constructor", e);
+    }
+
+    virtual expr visit_app(expr const & e) override {
+        expr it = e;
+        while (true) {
+            if (is_nat_int_char_string_value(ctx(), it))
+                return e;
+            if (!is_app(it) && !is_constant(it))
+                return visit(it);
+            buffer<expr> args;
+            expr const & fn = get_app_args(it, args);
+            if (!is_constant(fn))
+                throw_invalid_app(e);
+
+            if (optional<name> I = is_ginductive_intro_rule(env(), const_name(fn))) {
+                unsigned num_params = get_ginductive_num_params(env(), *I);
+                for (unsigned i = num_params; i < args.size(); i++) {
+                    visit(args[i]);
+                }
+                return e;
+            } else if (optional<inverse_info> info = has_inverse(env(), const_name(fn))) {
+                visit(args.back());
+                return e;
+            } else {
+                if (auto r = expand(it)) {
+                    it = *r;
+                } else {
+                    throw_invalid_app(e);
+                }
+            }
+        }
+    }
+
+    virtual expr visit_constant(expr const & e) override {
+        return visit_app(e);
+    }
+
+    virtual expr visit_macro(expr const & e) override {
+        if (is_inaccessible(e)) {
+            return e;
+        } else if (auto r = ctx().expand_macro(e)) {
+            return visit(*r);
+        } else {
+            throw_invalid_pattern("invalid occurrence of macro expression in pattern", e);
+        }
+    }
+
+public:
+    validate_equation_lhs_fn(elaborator & elab, expr const & ref):
+        m_elab(elab), m_ref(ref) {
+    }
+
+    void validate(expr const & lhs) {
+        buffer<expr> args;
+        get_app_args(lhs, args);
+        for (expr & arg : args)
+            visit(arg);
+    }
+};
+
 expr elaborator::visit_equation(expr const & eq) {
     expr const & lhs = equation_lhs(eq);
     expr const & rhs = equation_rhs(eq);
@@ -2053,6 +2179,7 @@ expr elaborator::visit_equation(expr const & eq) {
     expr new_lhs_type = instantiate_mvars(infer_type(new_lhs));
     expr new_rhs      = visit(rhs, some_expr(new_lhs_type));
     new_rhs = enforce_type(new_rhs, new_lhs_type, "equation type mismatch", eq);
+    validate_equation_lhs_fn(*this, lhs).validate(instantiate_mvars(new_lhs));
     return copy_tag(eq, mk_equation(new_lhs, new_rhs));
 }
 

src/frontends/lean/elaborator.h

@@ -27,6 +27,7 @@ class elaborator {
 public:
     class checkpoint;
 private:
+    friend class validate_equation_lhs_fn;
     typedef std::vector<pair<expr, expr>> to_check_sorts;
     enum class arg_mask {
         AllExplicit /* @ annotation */,

src/library/equations_compiler/elim_match.cpp

@@ -286,12 +286,7 @@ struct elim_match_fn {
     bool is_value(type_context & ctx, expr const & e) {
         try {
         if (!m_use_ite) return false;
-        if (to_char(ctx, e) || to_string(e)) return true;
-        if (is_signed_num(e)) {
-            expr type = ctx.infer(e);
-            if (ctx.is_def_eq(type, mk_nat_type()) || ctx.is_def_eq(type, mk_int_type()))
-                return true;
-        }
+        if (is_nat_int_char_string_value(ctx, e)) return true;
         if (optional<name> I_name = is_constructor(e)) return is_nontrivial_enum(*I_name);
         return false;
         } catch (exception &) {

src/library/equations_compiler/util.cpp

@@ -575,6 +575,16 @@ environment mk_simple_equation_lemma_for(environment const & env, options const
     return add_equation_lemma(env, opts, metavar_context(), ctx.lctx(), is_private, eqn_name, eqn_type, eqn_proof);
 }
 
+bool is_nat_int_char_string_value(type_context & ctx, expr const & e) {
+    if (to_char(ctx, e) || to_string(e)) return true;
+    if (is_signed_num(e)) {
+        expr type = ctx.infer(e);
+        if (ctx.is_def_eq(type, mk_nat_type()) || ctx.is_def_eq(type, mk_int_type()))
+            return true;
+    }
+    return false;
+}
+
 void initialize_eqn_compiler_util() {
     register_trace_class("eqn_compiler");
     register_trace_class(name{"debug", "eqn_compiler"});

src/library/equations_compiler/util.h

@@ -99,6 +99,9 @@ environment mk_simple_equation_lemma_for(environment const & env, options const
 
 name mk_equation_name(name const & f_name, unsigned eqn_idx);
 
+/* Return true iff e is a nat, int, char or string value. */
+bool is_nat_int_char_string_value(type_context & ctx, expr const & e);
+
 void initialize_eqn_compiler_util();
 void finalize_eqn_compiler_util();
 }

tests/lean/eqn_compiler_error_msg.lean

@@ -0,0 +1,5 @@
+inductive R : ℕ → Prop
+| pos : ∀p n, R (p + n)
+
+lemma R_id : ∀n, R n → R n
+| (.p + .n) (R.pos p n) := R.pos p n

tests/lean/eqn_compiler_error_msg.lean.expected.out

@@ -0,0 +1,2 @@
+eqn_compiler_error_msg.lean:5:2: error: invalid function application in pattern, it cannot be reduced to a constructor (possible solution, mark term as inaccessible using '.( )')
+  .p + .n