feat: improve range of missing cases: ... error message

@Kha I added the helper combinator `withHeadRefOnly x`. I executes `x`
using the head token of the current `ref` as the new `ref`.

src/Init/Meta.lean

@@ -253,8 +253,21 @@ def copyRangePos (s : Syntax) (source : Syntax) : Syntax :=
       | _, _ => s
     | _ => s
 
+/-- Return the first atom/identifier that has position information -/
+partial def getHead? : Syntax → Option Syntax
+  | stx@(atom { pos := some _, .. } ..)  => some stx
+  | stx@(ident { pos := some _, .. } ..) => some stx
+  | node _ args      => args.findSome? getHead?
+  | _                => none
+
 end Syntax
 
+/-- Use the head atom/identifier of the current `ref` as the `ref` -/
+@[inline] def withHeadRefOnly {m : Type → Type} [Monad m] [MonadRef m] {α} (x : m α) : m α := do
+  match (← getRef).getHead? with
+  | none => x
+  | some ref => withRef ref x
+
 def mkAtom (val : String) : Syntax :=
   Syntax.atom {} val
 

src/Lean/Elab/Match.lean

@@ -696,7 +696,7 @@ def ignoreUnusedAlts (opts : Options) : Bool :=
 
 def reportMatcherResultErrors (altLHSS : List AltLHS) (result : MatcherResult) : TermElabM Unit := do
   unless result.counterExamples.isEmpty do
-    throwError! "missing cases:\n{Meta.Match.counterExamplesToMessageData result.counterExamples}"
+    withHeadRefOnly <| throwError! "missing cases:\n{Meta.Match.counterExamplesToMessageData result.counterExamples}"
   unless ignoreUnusedAlts (← getOptions) || result.unusedAltIdxs.isEmpty do
     let mut i := 0
     for alt in altLHSS do