fix: auto completion when autoBoundImplicit is active

src/Lean/Elab/Term.lean

@@ -1491,6 +1491,15 @@ private def mkConsts (candidates : List (Name × List String)) (explicitLevels :
 def resolveName (stx : Syntax) (n : Name) (preresolved : List (Name × List String)) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × List String)) := do
   try
     if let some (e, projs) ← resolveLocalName n then
+      if (← read).autoBoundImplicit then
+        /- We used to generate completion info nodes only for names that could not be resolved.
+           However, this is very unsatisfactory for when elaborating headers when `autoBoundImplicit` is turned on.
+           The problem is that new local declarations are introduced by `autoBoundImplicit` and we eventually can always resolve the name.
+           Thus, we add the completion info in this case.
+           TODO: revisit this design decision. Alternative design: always create a completion info node.
+           Note that in the current design if a constant name is a prefix of another one, we will not have a completion info node.
+        -/
+        addCompletionInfo <| CompletionInfo.id stx stx.getId (danglingDot := false) (← getLCtx) expectedType?
       unless explicitLevels.isEmpty do
         throwError "invalid use of explicit universe parameters, '{e}' is a local"
       return [(e, projs)]

tests/lean/1018unknowMVarIssue.lean.expected.out

@@ -7,20 +7,25 @@ a : α
 ⊢ α
 [Elab.info] command @ ⟨7, 0⟩-⟨10, 19⟩ @ Lean.Elab.Command.elabDeclaration
   α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent
+    [.] `α : some Sort.{?_uniq.313} @ ⟨7, 13⟩-⟨7, 14⟩
     α : Type @ ⟨7, 13⟩-⟨7, 14⟩
   a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
   α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent
+    [.] `α : some Sort.{?_uniq.319} @ ⟨7, 13⟩-⟨7, 14⟩
     α : Type @ ⟨7, 13⟩-⟨7, 14⟩
   a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
   Fam2 α β : Type 1 @ ⟨7, 21⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabApp
     [.] `Fam2 : some Sort.{?_uniq.321} @ ⟨7, 21⟩-⟨7, 25⟩
     Fam2 : Type → Type → Type 1 @ ⟨7, 21⟩-⟨7, 25⟩
     α : Type @ ⟨7, 26⟩-⟨7, 27⟩ @ Lean.Elab.Term.elabIdent
+      [.] `α : some Type @ ⟨7, 26⟩-⟨7, 27⟩
       α : Type @ ⟨7, 26⟩-⟨7, 27⟩
     β : Type @ ⟨7, 28⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabIdent
+      [.] `β : some Type @ ⟨7, 28⟩-⟨7, 29⟩
       β : Type @ ⟨7, 28⟩-⟨7, 29⟩
   x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
   β : Type @ ⟨7, 33⟩-⟨7, 34⟩ @ Lean.Elab.Term.elabIdent
+    [.] `β : some Sort.{?_uniq.323} @ ⟨7, 33⟩-⟨7, 34⟩
     β : Type @ ⟨7, 33⟩-⟨7, 34⟩
   _example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩†-⟨10, 19⟩†
   a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩

tests/lean/infoTree.lean.expected.out

@@ -67,9 +67,11 @@
               binop% HAdd.hAdd✝ x 0
                 x + 0 : Nat @ ⟨17, 35⟩†-⟨17, 40⟩ @ Lean.Elab.Term.BinOp.elabBinOp
                   x : Nat @ ⟨17, 35⟩-⟨17, 36⟩ @ Lean.Elab.Term.elabIdent
+                    [.] `x : none @ ⟨17, 35⟩-⟨17, 36⟩
                     x : Nat @ ⟨17, 35⟩-⟨17, 36⟩
                   0 : Nat @ ⟨17, 39⟩-⟨17, 40⟩ @ Lean.Elab.Term.elabNumLit
             x : Nat @ ⟨17, 43⟩-⟨17, 44⟩ @ Lean.Elab.Term.elabIdent
+              [.] `x : none @ ⟨17, 43⟩-⟨17, 44⟩
               x : Nat @ ⟨17, 43⟩-⟨17, 44⟩
   h (isBinder := true) : ∀ (x y : Nat), Bool → x + 0 = x @ ⟨17, 4⟩-⟨17, 5⟩
   fun x y b =>
@@ -368,8 +370,10 @@ infoTree.lean:44:0: error: expected stx
     (Term.binrel "binrel%" `Eq._@.infoTree._hyg.179 `x `x)
       Eq.{1} Nat _uniq.892 _uniq.892 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.elabBinRel
         _uniq.892 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent
+          [.] `x : none @ ⟨45, 21⟩-⟨45, 22⟩
           _uniq.892 : Nat @ ⟨45, 21⟩-⟨45, 22⟩
         _uniq.892 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent
+          [.] `x : none @ ⟨45, 25⟩-⟨45, 26⟩
           _uniq.892 : Nat @ ⟨45, 25⟩-⟨45, 26⟩
   _uniq.898 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨45, 4⟩-⟨45, 6⟩
   _uniq.901 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩

tests/lean/interactive/compHeader.lean

@@ -0,0 +1,3 @@
+def veryLongNameForCompletion := Nat
+                    --v textDocument/completion
+def f (x : veryLongNam) := x

tests/lean/interactive/compHeader.lean.expected.out

@@ -0,0 +1,6 @@
+{"textDocument": {"uri": "file://compHeader.lean"},
+ "position": {"line": 2, "character": 22}}
+{"items":
+ [{"label": "veryLongNam", "kind": 6, "detail": "Sort u_1"},
+  {"label": "veryLongNameForCompletion", "kind": 21, "detail": "Type"}],
+ "isIncomplete": true}