From e4bf5977d94a78a8ddf9369674abf5227e6c7e36 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 10 Jun 2021 18:15:40 +0200
Subject: [PATCH] fix: syntax pattern match against multiple identifiers

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

diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 5678806277..9b6c6431f8 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -386,11 +386,19 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
       let kind := quoted.getKind
       let argPats := quoted.getArgs.map fun arg => Unhygienic.run `(`($(arg)))
       pure {
-        check := shape kind argPats.size,
+        check :=
+          if quoted.isIdent then
+            other quoted
+          else
+            shape kind argPats.size,
         onMatch := fun
-          | other _ => undecided
+          | other stx' =>
+            if quoted.isIdent && quoted == stx' then
+              covered pure (exhaustive := true)
+            else
+              uncovered
           | shape k' sz =>
-            if k' == kind && sz == argPats.size then
+            if k' == kind && sz == argPats.size && kind != `ident then
               covered (fun (pats, rhs) => (argPats.toList ++ pats, rhs)) (exhaustive := true)
             else
               uncovered
diff --git a/tests/lean/StxQuot.lean b/tests/lean/StxQuot.lean
index 7f749fff83..0af82cda0d 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 mkIdent `b with
+  | `(a) => "0"
+  | `(b) => "1"
+  | _    => "2"
diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
index 16ede81946..a303f4dbcc 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"