fix: syntax match: do not discard other patterns after splices

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))

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

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"