fix: syntax pattern match against multiple identifiers

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

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"

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"