fix: travelling auto-completion

src/Lean/Elab/App.lean

@@ -1594,10 +1594,13 @@ private def elabAtom : TermElab := fun stx expectedType? => do
 @[builtin_term_elab dotIdent] def elabDotIdent : TermElab := elabAtom
 @[builtin_term_elab explicitUniv] def elabExplicitUniv : TermElab := elabAtom
 @[builtin_term_elab pipeProj] def elabPipeProj : TermElab
-  | `($e |>.$f $args*), expectedType? =>
+  | `($e |>.%$tk$f $args*), expectedType? =>
     universeConstraintsCheckpoint do
       let (namedArgs, args, ellipsis) ← expandArgs args
-      elabAppAux (← `($e |>.$f)) namedArgs args (ellipsis := ellipsis) expectedType?
+      let mut stx ← `($e |>.%$tk$f)
+      if let (some startPos, some stopPos) := (e.raw.getPos?, f.raw.getTailPos?) then
+        stx := ⟨stx.raw.setInfo <| .synthetic (canonical := true) startPos stopPos⟩
+      elabAppAux stx namedArgs args (ellipsis := ellipsis) expectedType?
   | _, _ => throwUnsupportedSyntax
 
 @[builtin_term_elab explicit] def elabExplicit : TermElab := fun stx expectedType? =>

src/Lean/Server/Completion.lean

@@ -235,7 +235,6 @@ private def normPrivateName? (declName : Name) : MetaM (Option Name) := do
   Remark: `danglingDot == true` when the completion point is an identifier followed by `.`.
 -/
 private def matchDecl? (ns : Name) (id : Name) (danglingDot : Bool) (declName : Name) : MetaM (Option (Name × Float)) := do
-  -- dbg_trace "{ns}, {id}, {declName}, {danglingDot}"
   let some declName ← normPrivateName? declName
     | return none
   if !ns.isPrefixOf declName then
@@ -324,16 +323,24 @@ def completeNamespaces (ctx : ContextInfo) (id : Name) (danglingDot : Bool) : M
 
 private def idCompletionCore
     (ctx         : ContextInfo)
+    (stx         : Syntax)
     (id          : Name)
     (hoverInfo   : HoverInfo)
     (danglingDot : Bool)
     : M Unit := do
-  let mut id := id.eraseMacroScopes
+  let mut id := id
+  if id.hasMacroScopes then
+    if stx.getHeadInfo matches .original .. then
+      id := id.eraseMacroScopes
+    else
+      -- Identifier is synthetic and has macro scopes => no completions
+      -- Erasing the macro scopes does not make sense in this case because the identifier name
+      -- is some random synthetic string.
+      return
   let mut danglingDot := danglingDot
   if let HoverInfo.inside delta := hoverInfo then
     id := truncate id delta
     danglingDot := false
-  -- dbg_trace ">> id {id} : {expectedType?}"
   if id.isAtomic then
     -- search for matches in the local context
     for localDecl in (← getLCtx) do
@@ -419,12 +426,13 @@ private def idCompletion
     (params        : CompletionParams)
     (ctx           : ContextInfo)
     (lctx          : LocalContext)
+    (stx           : Syntax)
     (id            : Name)
     (hoverInfo     : HoverInfo)
     (danglingDot   : Bool)
     : IO (Option CompletionList) :=
   runM params ctx lctx do
-    idCompletionCore ctx id hoverInfo danglingDot
+    idCompletionCore ctx stx id hoverInfo danglingDot
 
 private def unfoldeDefinitionGuarded? (e : Expr) : MetaM (Option Expr) :=
   try unfoldDefinition? e catch _ => pure none
@@ -525,10 +533,10 @@ private def dotCompletion
     if nameSet.isEmpty then
       let stx := info.stx
       if stx.isIdent then
-        idCompletionCore ctx stx.getId hoverInfo (danglingDot := false)
+        idCompletionCore ctx stx stx.getId hoverInfo (danglingDot := false)
       else if stx.getKind == ``Lean.Parser.Term.completion && stx[0].isIdent then
         -- TODO: truncation when there is a dangling dot
-        idCompletionCore ctx stx[0].getId HoverInfo.after (danglingDot := true)
+        idCompletionCore ctx stx stx[0].getId HoverInfo.after (danglingDot := true)
       else
         failure
       return
@@ -679,37 +687,48 @@ where
       : Option (HoverInfo × ContextInfo × Info) :=
     if !info.isCompletion then
       best?
-    else if info.occursInside? hoverPos |>.isSome then
-      let headPos          := info.pos?.get!
+    else if info.occursInOrOnBoundary hoverPos then
+      let headPos := info.pos?.get!
+      let tailPos := info.tailPos?.get!
+      let hoverInfo :=
+        if hoverPos < tailPos then
+          HoverInfo.inside (hoverPos - headPos).byteIdx
+        else
+          HoverInfo.after
       let ⟨headPosLine, _⟩ := fileMap.toPosition headPos
       let ⟨tailPosLine, _⟩ := fileMap.toPosition info.tailPos?.get!
       if headPosLine != hoverLine || headPosLine != tailPosLine then
         best?
       else match best? with
-        | none                         => (HoverInfo.inside (hoverPos - headPos).byteIdx, ctx, info)
-        | some (HoverInfo.after, _, _) => (HoverInfo.inside (hoverPos - headPos).byteIdx, ctx, info)
-        | some (_, _, best) =>
-          if info.isSmaller best then
-            (HoverInfo.inside (hoverPos - headPos).byteIdx, ctx, info)
-          else
-            best?
-    else if let some (HoverInfo.inside _, _, _) := best? then
-      -- We assume the "inside matches" have precedence over "before ones".
-      best?
-    else if info.occursDirectlyBefore hoverPos then
-      let pos := info.tailPos?.get!
-      let ⟨line, _⟩ := fileMap.toPosition pos
-      if line != hoverLine then best?
-      else match best? with
-        | none => (HoverInfo.after, ctx, info)
+        | none              => (hoverInfo, ctx, info)
         | some (_, _, best) =>
-          if info.isSmaller best then
-            (HoverInfo.after, ctx, info)
+          if isBetter info best then
+            (hoverInfo, ctx, info)
           else
             best?
     else
       best?
 
+  isBetter : Info → Info → Bool
+    | i₁@(.ofCompletionInfo ci₁), i₂@(.ofCompletionInfo ci₂) =>
+      -- Use the smallest info available and prefer non-id completion over id completions as a
+      -- tie-breaker.
+      -- This is necessary because the elaborator sometimes generates both for the same range.
+      -- If two infos are equivalent, always prefer the first one.
+      if i₁.isSmaller i₂ then
+        true
+      else if i₂.isSmaller i₁ then
+        false
+      else if !(ci₁ matches .id ..) && ci₂ matches .id .. then
+        true
+      else if ci₁ matches .id .. && !(ci₂ matches .id ..) then
+        false
+      else
+        true
+    | .ofCompletionInfo _, _ => true
+    | _, .ofCompletionInfo _ => false
+    | _, _ => true
+
 /--
 Assigns the `CompletionItem.sortText?` for all items in `completions` according to their order
 in `completions`. This is necessary because clients will use their own sort order if the server
@@ -740,8 +759,8 @@ partial def find?
     match info with
     | .dot info .. =>
       dotCompletion params ctx info hoverInfo
-    | .id _ id danglingDot lctx .. =>
-      idCompletion params ctx lctx id hoverInfo danglingDot
+    | .id stx id danglingDot lctx .. =>
+      idCompletion params ctx lctx stx id hoverInfo danglingDot
     | .dotId _ id lctx expectedType? =>
       dotIdCompletion params ctx lctx id expectedType?
     | .fieldId _ id lctx structName =>

src/Lean/Server/InfoUtils.lean

@@ -165,7 +165,7 @@ def Info.size? (i : Info) : Option String.Pos := do
 
 -- `Info` without position information are considered to have "infinite" size
 def Info.isSmaller (i₁ i₂ : Info) : Bool :=
-  match i₁.size?, i₂.pos? with
+  match i₁.size?, i₂.size? with
   | some sz₁, some sz₂ => sz₁ < sz₂
   | some _, none => true
   | _, _ => false
@@ -181,6 +181,13 @@ def Info.occursInside? (i : Info) (hoverPos : String.Pos) : Option String.Pos :=
   guard (headPos ≤ hoverPos && hoverPos < tailPos)
   return hoverPos - headPos
 
+def Info.occursInOrOnBoundary (i : Info) (hoverPos : String.Pos) : Bool := Id.run do
+  let some headPos := i.pos?
+    | return false
+  let some tailPos := i.tailPos?
+    | return false
+  return headPos <= hoverPos && hoverPos <= tailPos
+
 def InfoTree.smallestInfo? (p : Info → Bool) (t : InfoTree) : Option (ContextInfo × Info) :=
   let ts := t.deepestNodes fun ctx i _ => if p i then some (ctx, i) else none
 

tests/lean/interactive/completionBracketedDot.lean

@@ -0,0 +1,10 @@
+inductive Direction where
+  | up
+  | right
+  | down
+  | left
+
+-- It would be nice if this actually provided `up`, `right`, `down` and `left` in the future
+def foo : Direction :=
+  (.)
+  --^ textDocument/completion

tests/lean/interactive/completionBracketedDot.lean.expected.out

@@ -0,0 +1,3 @@
+{"textDocument": {"uri": "file:///completionBracketedDot.lean"},
+ "position": {"line": 8, "character": 4}}
+{"items": [], "isIncomplete": true}

tests/lean/interactive/travellingCompletions.lean

@@ -0,0 +1,44 @@
+import Lean
+
+
+
+-- https://github.com/leanprover/lean4/issues/4455
+def aaaaaaaa := 1
+
+#eval ([1,2,3].map λ c => aaaaaaa).length
+                               --^ textDocument/completion
+
+
+
+-- https://github.com/leanprover/lean4/issues/4705
+structure Bar where
+  foobar : Nat
+
+structure Foo where
+  x : Bar
+
+example (f : Foo) : Nat × Nat :=
+  ⟨f.x.foobar, f.x.f⟩
+                  --^ textDocument/completion
+
+example (b : Bar) : Nat × Nat :=
+  ⟨b.foobar, b.f⟩
+              --^ textDocument/completion
+
+
+
+-- https://github.com/leanprover/lean4/issues/5219
+structure ContinuousSMul (M X : Type) : Prop where
+structure ContinuousAdd (X : Type) : Prop where
+
+theorem Prod.continuousSMul {M X Y : Type} : ContinuousSMul M (X × Y) := ⟨⟩
+
+theorem Prod.continuousAdd {X Y : Type} : ContinuousAdd (X × Y) := ⟨⟩
+
+example : (ContinuousSMul Nat (Nat × Nat)) ∧ (ContinuousAdd (Nat × Nat)) := by
+  exact ⟨Prod.continuousSMul, Prod.continuous⟩
+                                           --^ textDocument/completion
+
+example : True ∧ True := by
+  exact ⟨trivial, True.in⟩
+                       --^ textDocument/completion

tests/lean/interactive/travellingCompletions.lean.expected.out

@@ -0,0 +1,72 @@
+{"textDocument": {"uri": "file:///travellingCompletions.lean"},
+ "position": {"line": 7, "character": 33}}
+{"items":
+ [{"sortText": "0",
+   "label": "aaaaaaaa",
+   "kind": 21,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///travellingCompletions.lean"},
+     "position": {"line": 7, "character": 33}},
+    "id": {"const": {"declName": "aaaaaaaa"}}}}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file:///travellingCompletions.lean"},
+ "position": {"line": 20, "character": 20}}
+{"items":
+ [{"sortText": "0",
+   "label": "foobar",
+   "kind": 5,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///travellingCompletions.lean"},
+     "position": {"line": 20, "character": 20}},
+    "id": {"const": {"declName": "Bar.foobar"}}}}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file:///travellingCompletions.lean"},
+ "position": {"line": 24, "character": 16}}
+{"items":
+ [{"sortText": "0",
+   "label": "foobar",
+   "kind": 5,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///travellingCompletions.lean"},
+     "position": {"line": 24, "character": 16}},
+    "id": {"const": {"declName": "Bar.foobar"}}}}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file:///travellingCompletions.lean"},
+ "position": {"line": 38, "character": 45}}
+{"items":
+ [{"sortText": "0",
+   "label": "continuousAdd",
+   "kind": 3,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///travellingCompletions.lean"},
+     "position": {"line": 38, "character": 45}},
+    "id": {"const": {"declName": "Prod.continuousAdd"}}}},
+  {"sortText": "1",
+   "label": "continuousSMul",
+   "kind": 3,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///travellingCompletions.lean"},
+     "position": {"line": 38, "character": 45}},
+    "id": {"const": {"declName": "Prod.continuousSMul"}}}}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file:///travellingCompletions.lean"},
+ "position": {"line": 42, "character": 25}}
+{"items":
+ [{"sortText": "0",
+   "label": "intro",
+   "kind": 4,
+   "documentation":
+   {"value":
+    "`True` is true, and `True.intro` (or more commonly, `trivial`)\nis the proof. ",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///travellingCompletions.lean"},
+     "position": {"line": 42, "character": 25}},
+    "id": {"const": {"declName": "True.intro"}}}}],
+ "isIncomplete": true}