fix: hovers on elabFieldName fields

src/Init/Data/Format/Syntax.lean

@@ -15,7 +15,7 @@ open Std.Format
 
 private def formatInfo (showInfo : Bool) (info : SourceInfo) (f : Format) : Format :=
   match showInfo, info with
-  | true, SourceInfo.original lead pos trail endPos => f!"{lead}:{f}:{pos}:{trail}:{endPos}"
+  | true, SourceInfo.original lead pos trail endPos => f!"{lead}:{pos}:{f}:{endPos}:{trail}"
   | true, SourceInfo.synthetic pos endPos           => f!"{pos}:{f}:{endPos}"
   | _,    _                                         => f
 

src/Lean/Elab/App.lean

@@ -673,7 +673,7 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
   | f, []          => elabAppArgs f namedArgs args expectedType? explicit ellipsis
   | f, lval::lvals => do
     if let LVal.fieldName (ref := fieldStx) (targetStx := targetStx) .. := lval then
-      addDotCompletionInfo  targetStx f expectedType? fieldStx
+      addDotCompletionInfo targetStx f expectedType? fieldStx
     let (f, lvalRes) ← resolveLVal f lval
     match lvalRes with
     | LValResolution.projIdx structName idx =>
@@ -785,9 +785,15 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
       f.getArgs.foldlM (fun acc f => elabAppFn f lvals namedArgs args expectedType? explicit ellipsis true acc) acc
   else
     let elabFieldName (e field : Syntax) := do
-      let newLVals := field.getId.eraseMacroScopes.components.map fun n =>
-        -- We use `none` here since `field` can't be part of a composite name
-        LVal.fieldName field (toString n) none e
+      let newLVals := 
+        -- We use `none` in `suffix?` since `field` can't be part of a composite name
+        if field.getId.hasMacroScopes then
+          -- We assume that names with macro scopes have no meaningful syntax associated
+          field.getId.eraseMacroScopes.components.map fun n =>
+            LVal.fieldName Syntax.missing (toString n) none e
+        else
+          field.identComponents.map fun comp =>
+            LVal.fieldName comp (toString comp.getId) none e
       elabAppFn e (newLVals ++ lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
     let elabFieldIdx (e idxStx : Syntax) := do
       let idx := idxStx.isFieldIdx?.get!

src/Lean/Syntax.lean

@@ -172,6 +172,24 @@ partial def getTailWithPos : Syntax → Option Syntax
   | node _ args         => args.findSomeRev? getTailWithPos
   | _                   => none
 
+open SourceInfo in
+/-- Splits an `ident` into its dot-separated components while preserving source info.
+For example, `` `foo.bla.boo `` ↦ `` [`foo, `bla, `boo] ``. -/
+def identComponents : Syntax → List Syntax
+  | ident info rawStr val _ =>
+    rawStr.splitOn "." |>.map fun ss =>
+      let off := ss.startPos - rawStr.startPos
+      let info := match info with
+        | original lead pos trail _ =>
+          let lead := if off == 0 then lead else "".toSubstring
+          let trail := if ss.stopPos == rawStr.stopPos then trail else "".toSubstring
+          original lead (pos + off) trail (pos + off + ss.bsize)
+        | synthetic pos _ =>
+          synthetic (pos + off) (pos + off + ss.bsize)
+        | SourceInfo.none => SourceInfo.none
+      ident info ss (Name.mkSimple ss.toString) []
+  | _ => unreachable!
+
 structure TopDown where
   firstChoiceOnly : Bool
   stx : Syntax

tests/lean/interactive/hoverDot.lean.expected.out

@@ -28,20 +28,22 @@
 {"textDocument": {"uri": "file://hoverDot.lean"},
  "position": {"line": 18, "character": 13}}
 {"range":
- {"start": {"line": 18, "character": 13}, "end": {"line": 18, "character": 20}},
+ {"start": {"line": 18, "character": 13}, "end": {"line": 18, "character": 15}},
  "contents": {"value": "```lean\nf₂ : Foo → Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hoverDot.lean"},
  "position": {"line": 18, "character": 16}}
 {"range":
- {"start": {"line": 18, "character": 13}, "end": {"line": 18, "character": 20}},
- "contents": {"value": "```lean\nf₂ : Foo → Nat\n```", "kind": "markdown"}}
+ {"start": {"line": 18, "character": 16}, "end": {"line": 18, "character": 20}},
+ "contents":
+ {"value": "```lean\nNat.succ : Nat → Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hoverDot.lean"},
  "position": {"line": 21, "character": 14}}
 {"range":
- {"start": {"line": 21, "character": 14}, "end": {"line": 21, "character": 21}},
+ {"start": {"line": 21, "character": 14}, "end": {"line": 21, "character": 16}},
  "contents": {"value": "```lean\nf₂ : Foo → Nat\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hoverDot.lean"},
  "position": {"line": 21, "character": 17}}
 {"range":
- {"start": {"line": 21, "character": 14}, "end": {"line": 21, "character": 21}},
- "contents": {"value": "```lean\nf₂ : Foo → Nat\n```", "kind": "markdown"}}
+ {"start": {"line": 21, "character": 17}, "end": {"line": 21, "character": 21}},
+ "contents":
+ {"value": "```lean\nNat.succ : Nat → Nat\n```", "kind": "markdown"}}