From 088774536e85610b434fd52464c3d31617a430d2 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 7 May 2021 16:08:10 +0200
Subject: [PATCH] fix: syntax match: do not discard other patterns after
 splices

---
 src/Lean/Elab/Quotation.lean         | 15 ++++++++++-----
 tests/lean/StxQuot.lean              |  6 ++++++
 tests/lean/StxQuot.lean.expected.out |  1 +
 3 files changed, 17 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 45c31c00a5..9ece69df32 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -266,6 +266,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
         if k == Name.anonymous then unconditionally rhsFn else pure {
           check   := shape k none,
           onMatch := fun
+            | other _ => undecided
             | taken@(shape k' sz) =>
               if k' == k then
                 covered (adaptRhs rhsFn ∘ noOpMatchAdaptPats taken) (exhaustive := sz.isNone)
@@ -338,6 +339,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
       pure {
         check    := slice idx numSuffix
         onMatch  := fun
+          | other _ => undecided
           | slice p s =>
             if p == idx && s == numSuffix then
               let argPats := quoted.getArgs.mapIdx fun i arg =>
@@ -362,11 +364,14 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
       let argPats := quoted.getArgs.map fun arg => Unhygienic.run `(`($(arg)))
       pure {
         check := shape kind argPats.size,
-        onMatch := fun taken =>
-          if (match taken with | shape k' sz => k' == kind && sz == argPats.size | _ => false : Bool) then
-            covered (fun (pats, rhs) => (argPats.toList ++ pats, rhs)) (exhaustive := true)
-          else
-            uncovered,
+        onMatch := fun
+          | other _ => undecided
+          | shape k' sz =>
+            if k' == kind && sz == argPats.size then
+              covered (fun (pats, rhs) => (argPats.toList ++ pats, rhs)) (exhaustive := true)
+            else
+              uncovered
+          | _ => uncovered,
         doMatch := fun yes no => do
           let cond ← match kind with
           | `null => `(Syntax.matchesNull discr $(quote argPats.size))
diff --git a/tests/lean/StxQuot.lean b/tests/lean/StxQuot.lean
index 7f749fff83..a8aadadcd7 100644
--- a/tests/lean/StxQuot.lean
+++ b/tests/lean/StxQuot.lean
@@ -107,3 +107,9 @@ syntax "foo" term : term
 #eval run ``(fun x => y)
 #eval run ``(fun x y => x y)
 #eval run ``(fun ⟨x, y⟩ => x)
+
+#eval run do
+  match ← `(have x := y; z) with
+  | `(have $[$x :]? $type from $val $[;]? $body)   => pure 0
+  | `(have $pattern:term := $val:term $[;]? $body) => pure 1
+  | _                                              => pure 2
diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
index 96785da538..9fc3dcb4db 100644
--- a/tests/lean/StxQuot.lean.expected.out
+++ b/tests/lean/StxQuot.lean.expected.out
@@ -54,3 +54,4 @@ StxQuot.lean:101:13-101:14: error: unknown identifier 'x' at quotation precheck;
 StxQuot.lean:107:22-107:23: error: unknown identifier 'y' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check.
 "(Term.fun\n \"fun\"\n (Term.basicFun\n  [`x._@.UnhygienicMain._hyg.1 `y._@.UnhygienicMain._hyg.1]\n  \"=>\"\n  (Term.app `x._@.UnhygienicMain._hyg.1 [`y._@.UnhygienicMain._hyg.1])))"
 "(Term.fun\n \"fun\"\n (Term.basicFun\n  [(Term.anonymousCtor \"⟨\" [`x._@.UnhygienicMain._hyg.1 \",\" `y._@.UnhygienicMain._hyg.1] \"⟩\")]\n  \"=>\"\n  `x._@.UnhygienicMain._hyg.1))"
+"1"