From cd21793b5389e8cf88ca54cb3fc2695092b00a46 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 27 Mar 2019 16:42:59 -0700
Subject: [PATCH] fix(frontends/lean/elaborator): assertion violation
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Prevent assertion violation when processing examples such as:
```
@[pattern] def badPattern (x : Nat) : Nat := 0

def tst (y : Nat) : Nat :=
match y with
| (@badPattern _) := 1
| _               := 2
```

The `x` is not used in `badPattern`. Thus, the elaborator fails to
synthesize the metavariable corresponding to `_` at `@badPattern _`.

The fix detects this kind of instance, but I commented the code the
throws the error because we would prevent us from compiling `term.lean`.
The assertion violation was originally triggered by the pattern definition
```
@[pattern] def «explicitBinderContent» (requireType : optParam.{1} Bool Bool.false) :=
  {SyntaxNodeKind . name := `Lean.Parser.Term.explicitBinderContent}
at

...
  view := fun stx, let (stx, i) := match stx.asNode : _ -> Prod Syntax Nat with
  | some {kind := @«explicitBinderContent» requireType,   -- << HERE
          args := [stx], ..} := ...
```
These definitions were generated by the node choice macro.

cc @kha
---
 src/frontends/lean/elaborator.cpp | 21 +++++++++++++++++++--
 src/frontends/lean/elaborator.h   |  1 +
 2 files changed, 20 insertions(+), 2 deletions(-)

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 181cfd3f4f..b3dbad3035 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -2634,10 +2634,23 @@ expr elaborator::visit_equations(expr const & e) {
         new_e = copy_pos(e, mk_equations(header, new_eqs.size(), new_eqs.data()));
     }
     new_e = instantiate_mvars(new_e);
-    ensure_no_unassigned_metavars(new_e);
+    ensure_no_unassigned_metavars_core(new_e);
     if (has_sorry(new_e))
         // aborting here prevents many additional errors
         throw elaborator_exception(e, "[abort visit_equation]").ignore_if(true);
+    if (!has_synth_sorry(new_e) && has_expr_metavar(e)) {
+        /* We perform this check to be able to reject code such as:
+           ```
+           @[pattern] def badPattern (x : Nat) : Nat := 0
+           def tst (x : Nat) : Nat :=
+           match x with
+           | (@badPattern _) := 1
+           | _               := 2
+           ```
+        */
+        // TODO(Leo, Kha): enable the following check
+        // throw elaborator_exception(new_e, "invalid pattern");
+    }
     metavar_context mctx = m_ctx.mctx();
     expr r = compile_equations(m_env, *this, mctx, m_ctx.lctx(), new_e);
     m_ctx.set_env(m_env);
@@ -3793,7 +3806,7 @@ void elaborator::synthesize() {
     synthesize_type_class_instances();
 }
 
-void elaborator::ensure_no_unassigned_metavars(expr & e) {
+void elaborator::ensure_no_unassigned_metavars_core(expr & e) {
     e = instantiate_mvars(e);
     if (!has_expr_metavar(e))
         return;
@@ -3832,6 +3845,10 @@ void elaborator::ensure_no_unassigned_metavars(expr & e) {
         }
     }
     e = instantiate_mvars(e);
+}
+
+void elaborator::ensure_no_unassigned_metavars(expr & e) {
+    ensure_no_unassigned_metavars_core(e);
     /* If we still have an unassigned mvar, it means the mvar doesn't directly correspond to a user-facing mvar.
      * That's bad (because we can't generate a sensible error message) and shouldn't happen. */
     lean_assert(has_synth_sorry(e) || !has_expr_metavar(e));
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index 30a5943cae..9f83e3b0e1 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -314,6 +314,7 @@ public:
     expr elaborate(expr const & e);
     expr elaborate_type(expr const & e);
     expr_pair elaborate_with_type(expr const & e, expr const & e_type);
+    void ensure_no_unassigned_metavars_core(expr & e);
     void ensure_no_unassigned_metavars(expr & e);
     /**
        \brief Finalize all expressions in \c es.