fix: match or-pattern

This issue has been reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Probably.20a.20bug/near/283779934

src/Lean/Elab/BindersUtil.lean

@@ -30,25 +30,25 @@ def getMatchAltsNumPatterns (matchAlts : Syntax) : Nat :=
 /--
   Expand a match alternative such as `| 0 | 1 => rhs` to an array containing `| 0 => rhs` and `| 1 => rhs`.
 -/
-def expandMatchAlt (stx : Syntax) : MacroM (Array Syntax) :=
-  match stx with
-  | `(matchAltExpr| | $[$patss]|* => $rhs) =>
-     if patss.size ≤ 1 then
-       return #[stx]
-     else
-       patss.mapM fun pats => let pats := #[pats]; `(matchAltExpr| | $[$pats]|* => $rhs)
-  | _ => return #[stx]
+def expandMatchAlt (matchAlt : Syntax) : Array Syntax :=
+  let patss := matchAlt[1]
+  let rhs   := matchAlt[3]
+  if patss.getArgs.size ≤ 1 then
+    #[matchAlt]
+  else
+    patss.getSepArgs.map fun pats =>
+      let patss := mkNullNode #[pats]
+      matchAlt.setArg 1 patss
 
 def shouldExpandMatchAlt (matchAlt : Syntax) : Bool :=
-  match matchAlt with
-  | `(matchAltExpr| | $[$patss]|* => $rhs) => patss.size > 1
-  | _ => false
+  let patss := matchAlt[1]
+  patss.getArgs.size > 1
 
 def expandMatchAlts? (stx : Syntax) : MacroM (Option Syntax) := do
   match stx with
   | `(match $[$gen]? $[$motive]? $discrs,* with $alts:matchAlt*) =>
     if alts.any shouldExpandMatchAlt then
-      let alts ← alts.foldlM (init := #[]) fun alts alt => return alts ++ (← expandMatchAlt alt)
+      let alts := alts.foldl (init := #[]) fun alts alt => alts ++ expandMatchAlt alt
       `(match $[$gen]? $[$motive]? $discrs,* with $alts:matchAlt*)
     else
       return none

src/Lean/Elab/Do.lean

@@ -1460,7 +1460,7 @@ mutual
     let optMotive := doMatch[2]
     let discrs    := doMatch[3]
     let matchAlts := doMatch[5][0].getArgs -- Array of `doMatchAlt`
-    let matchAlts ← matchAlts.foldlM (init := #[]) fun result matchAlt => return result ++ (← liftMacroM <| expandMatchAlt matchAlt)
+    let matchAlts := matchAlts.foldl (init := #[]) fun result matchAlt => result ++ expandMatchAlt matchAlt
     let alts ←  matchAlts.mapM fun matchAlt => do
       let patterns := matchAlt[1][0]
       let vars ← getPatternsVarsEx patterns.getSepArgs

src/Lean/Elab/Match.lean

@@ -1256,7 +1256,7 @@ enforce this. -/
 where
   elabMatchDefault (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
     match (← liftMacroM <| expandMatchAlts? stx) with
-    | some stxNew => withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
+    | some stxNew => trace[Meta.debug] "expanded  alts"; withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
     | none =>
     match (← expandNonAtomicDiscrs? stx) with
     | some stxNew => withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?

tests/lean/matchOrIssue.lean

@@ -0,0 +1,18 @@
+inductive A : Type
+| ctor : A → A
+| inh
+
+-- set_option trace.Elab true in
+def f : A → A → Bool
+| banana, a b | _, lol how => 1 + "test" + f1 -- Error
+| _, _ => false
+
+
+def g : A → A → Bool
+| A.inh, _ | _, A.inh => true
+| _, _ => false
+
+example : g .inh (.ctor a) = true := rfl
+example : g .inh .inh = true := rfl
+example : g (.ctor a) .inh = true := rfl
+example : g (.ctor a) (.ctor b) = false := rfl

tests/lean/matchOrIssue.lean.expected.out

@@ -0,0 +1 @@
+matchOrIssue.lean:7:10-7:13: error: invalid pattern, constructor or constant marked with '[matchPattern]' expected