This at least works, though probably not the way to do it

Author: nomeata

src/Lean/Elab/Match.lean

@@ -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 {α} (ref : Syntax) (patternVarDecls : Array PatternVarDecl) (patternStxs : Array Syntax) (lhsStx : Syntax) (numDiscrs : Nat) (matchType : Expr)
+private def withElaboratedLHS {α} (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 := ref, fvarDecls := localDecls.toList, patterns := patterns.toList } matchType
+      k { ref := lhsStx, 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 alt.ref patternVarDecls alt.patterns alt.lhs discrs.size matchType fun altLHS matchType =>
+      withElaboratedLHS 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}"

tests/lean/1057.lean.expected.out

@@ -1,4 +1,4 @@
-1057.lean:9:2-9:28: error: Dependent elimination failed: Type mismatch when solving this alternative: it has type
+1057.lean:9:4-9:15: error: Dependent elimination failed: Type mismatch when solving this alternative: it has type
   motive t Int
 but is expected to have type
   motive t x✝

tests/lean/match1.lean.expected.out

@@ -10,12 +10,12 @@
 4
 ---- inv
 10
-match1.lean:82:0-82:73: error: Dependent elimination failed: Type mismatch when solving this alternative: it has type
+match1.lean:82:2-82:60: error: Dependent elimination failed: Type mismatch when solving this alternative: it has type
   motive 0 (Vec.cons head✝ Vec.nil) ⋯
 but is expected to have type
   motive x✝ (Vec.cons head✝ tail✝) ⋯
 [false, true, true]
-match1.lean:119:0-119:41: error: Dependent match elimination failed: Expected a constructor, but found the inaccessible pattern
+match1.lean:119:2-119:18: error: Dependent match elimination failed: Expected a constructor, but found the inaccessible pattern
   .(j + j)
 [false, true, true]
 match1.lean:136:7-136:22: error: Invalid match expression: The type of pattern variable 'a' contains metavariables:

tests/lean/redundantAlt.lean.expected.out

@@ -1,6 +1,6 @@
-redundantAlt.lean:5:1-5:9: error(lean.redundantMatchAlt): Redundant alternative: Any expression matching
+redundantAlt.lean:5:3-5:4: error(lean.redundantMatchAlt): Redundant alternative: Any expression matching
   2
 will match one of the preceding alternatives
-redundantAlt.lean:7:1-7:9: error(lean.redundantMatchAlt): Redundant alternative: Any expression matching
+redundantAlt.lean:7:3-7:4: error(lean.redundantMatchAlt): Redundant alternative: Any expression matching
   3
 will match one of the preceding alternatives

tests/lean/run/issue10781.lean

@@ -0,0 +1,36 @@
+/--
+@ +4:4...8
+error: Redundant alternative: Any expression matching
+  0, x✝
+will match one of the preceding alternatives
+-/
+#guard_msgs (positions := true) in
+example : Nat → Nat → Nat
+  | _ + 1, _ => 2  -- error was here (bad)
+  | 0, _
+  | 0, _ => 1 -- now error is here (good)
+
+/--
+@ +4:4...8
+error: Redundant alternative: Any expression matching
+  0, x✝
+will match one of the preceding alternatives
+-/
+#guard_msgs (positions := true) in
+example : Nat → Nat → Nat
+  | _ + 1, _ => 2
+  | 0, _ => 1
+  | 0, _ => 1 -- error here (good)
+
+/--
+@ +3:4...12
+error: Redundant alternative: Any expression matching
+  n✝.succ.succ, x✝
+will match one of the preceding alternatives
+-/
+#guard_msgs (positions := true) in
+example : Nat → Nat → Nat
+  | _ + 2, _ => 2
+  | _ + 2, _ => 2 -- error here (good)
+  | 0, _
+  | 1, _ => 1

tests/lean/typeIncorrectPat.lean.expected.out

@@ -1,4 +1,4 @@
-typeIncorrectPat.lean:2:1-2:17: error: Type mismatch in pattern: Pattern
+typeIncorrectPat.lean:2:3-2:12: error: Type mismatch in pattern: Pattern
   true
 has type
   Bool