Revert "fix: preserve error locations when expanding match arms"

This reverts commit 92981df.

Author: nomeata

src/Lean/Elab/BindersUtil.lean

@@ -41,23 +41,23 @@ open Lean.Parser.Term
 /-- Helper function for `expandEqnsIntoMatch` -/
 def getMatchAltsNumPatterns (matchAlts : Syntax) : Nat :=
   let alt0 := matchAlts[0][0]
-  let pats := alt0[1][0][0].getSepArgs
+  let pats := alt0[1][0].getSepArgs
   pats.size
 
 /--
   Expand a match alternative such as `| 0 | 1 => rhs` to an array containing `| 0 => rhs` and `| 1 => rhs`.
 -/
 def expandMatchAlt (stx : TSyntax ``matchAlt) : MacroM (Array (TSyntax ``matchAlt)) :=
   match stx with
-  | `(matchAltExpr| | $[$patss:matchAltPats]|* => $rhs) => do
+  | `(matchAltExpr| | $[$patss,*]|* => $rhs) =>
      if patss.size ≤ 1 then
        return #[stx]
      else
-       patss.mapM fun pats => `(matchAltExpr| | $pats => $rhs)
+       patss.mapM fun pats => `(matchAltExpr| | $pats,* => $rhs)
   | _ => return #[stx]
 
 def shouldExpandMatchAlt : TSyntax ``matchAlt → Bool
-  | `(matchAltExpr| | $[$patss:matchAltPats]|* => $_) => patss.size > 1
+  | `(matchAltExpr| | $[$patss,*]|* => $_) => patss.size > 1
   | _ => false
 
 def expandMatchAlts? (stx : Syntax) : MacroM (Option Syntax) := do

src/Lean/Elab/Match.lean

@@ -162,10 +162,10 @@ private def getMatchGeneralizing? : Syntax → Option Bool
 
 /-- Given the `stx` of a single match alternative, return a corresponding `MatchAltView`. -/
 def getMatchAlt : Syntax → Option MatchAltView
-  | alt@`(matchAltExpr| | $patterns:matchAltPats => $rhs) => some {
+  | alt@`(matchAltExpr| | $patterns,* => $rhs) => some {
           ref      := alt,
-          patterns := patterns.raw[0].getSepArgs,
-          lhs      := patterns,
+          patterns := patterns,
+          lhs      := alt[1],
           rhs      := rhs
         }
   | _ => none
@@ -759,13 +759,13 @@ end ToDepElimPattern
 def withDepElimPatterns (patternVarDecls : Array PatternVarDecl) (ps : Array Expr) (matchType : Expr) (k : Array LocalDecl → Array Pattern → Expr → TermElabM α) : TermElabM α := do
   ToDepElimPattern.main patternVarDecls ps matchType k
 
-private def withElaboratedLHS {α} (patternVarDecls : Array PatternVarDecl) (patternStxs : Array Syntax) (lhsStx : Syntax) (numDiscrs : Nat) (matchType : Expr)
+private def withElaboratedLHS {α} (ref : Syntax) (patternVarDecls : Array PatternVarDecl) (patternStxs : Array Syntax) (lhsStx : Syntax) (numDiscrs : Nat) (matchType : Expr)
     (k : AltLHS → Expr → TermElabM α) : ExceptT PatternElabException TermElabM α := do
   let (patterns, matchType) ← withSynthesize <| withRef lhsStx <| elabPatterns patternStxs numDiscrs matchType
   id (α := TermElabM α) do
     trace[Elab.match] "patterns: {patterns}"
     withDepElimPatterns patternVarDecls patterns matchType fun localDecls patterns matchType => do
-      k { ref := lhsStx, fvarDecls := localDecls.toList, patterns := patterns.toList } matchType
+      k { ref := ref, fvarDecls := localDecls.toList, patterns := patterns.toList } matchType
 
 /--
   Try to clear the free variables in `toClear` and auxiliary discriminants, and then execute `k` in the updated local context.
@@ -817,7 +817,7 @@ private def elabMatchAltView (discrs : Array Discr) (alt : MatchAltView) (matchT
     let (patternVars, alt) ← collectPatternVars alt
     trace[Elab.match] "patternVars: {patternVars}"
     withPatternVars patternVars fun patternVarDecls => do
-      withElaboratedLHS patternVarDecls alt.patterns alt.lhs discrs.size matchType fun altLHS matchType =>
+      withElaboratedLHS alt.ref patternVarDecls alt.patterns alt.lhs discrs.size matchType fun altLHS matchType =>
         withEqs discrs altLHS.patterns fun eqs =>
           withLocalInstances altLHS.fvarDecls do
             trace[Elab.match] "elabMatchAltView: {matchType}"

src/Lean/Parser/Term.lean

@@ -259,13 +259,10 @@ def «forall» := leading_parser:leadPrec
   many1 (ppSpace >> (binderIdent <|> bracketedBinder)) >>
   optType >> ", " >> termParser
 
-def matchAltPats : Parser := leading_parser
-  sepBy1 termParser ", "
-
 def matchAlt (rhsParser : Parser := termParser) : Parser :=
   leading_parser (withAnonymousAntiquot := false)
     "| " >> ppIndent (
-      sepBy1 matchAltPats " | " >> darrow >>
+      sepBy1 (sepBy1 termParser ", ") " | " >> darrow >>
       checkColGe "alternative right-hand-side to start in a column greater than or equal to the corresponding '|'" >>
       rhsParser)
 /--