feat: save aditional information for id completion, and suppress implicit prefix when reporting completion types

src/Lean/Elab/InfoTree.lean

@@ -39,7 +39,7 @@ structure CommandInfo where
 
 inductive CompletionInfo where
   | dot (termInfo : TermInfo) (field? : Option Syntax) (expectedType? : Option Expr)
-  | id (stx : Syntax) (expectedType? : Option Expr)
+  | id (stx : Syntax) (lctx : LocalContext) (openDecls : List OpenDecl) (expectedType? : Option Expr)
   | namespaceId (stx : Syntax)
   | option (stx : Syntax)
   | endSection (stx : Syntax) (scopeNames : List String)
@@ -161,7 +161,8 @@ def TermInfo.format (ctx : ContextInfo) (info : TermInfo) : IO Format := do
 def CompletionInfo.format (ctx : ContextInfo) (info : CompletionInfo) : IO Format :=
   match info with
   | CompletionInfo.dot i .. => return f!"[.] {← i.format ctx}"
-  | _                       => return f!"[.] {info.stx}"
+  | CompletionInfo.id stx lctx _ expectedType? => ctx.runMetaM lctx do return f!"[.] {stx} : {expectedType?}"
+  | _ => return f!"[.] {info.stx}"
 
 def CommandInfo.format (ctx : ContextInfo) (info : CommandInfo) : IO Format := do
   return f!"command @ {formatStxRange ctx info.stx}"

src/Lean/Elab/Term.lean

@@ -1350,7 +1350,7 @@ def resolveName (stx : Syntax) (n : Name) (preresolved : List (Name × List Stri
       process preresolved
   catch ex =>
     if preresolved.isEmpty && explicitLevels.isEmpty then
-      addCompletionInfo <| CompletionInfo.id stx expectedType?
+      addCompletionInfo <| CompletionInfo.id stx (← getLCtx) (← getOpenDecls) expectedType?
     throw ex
 where process (candidates : List (Name × List String)) : TermElabM (List (Expr × List String)) := do
   if candidates.isEmpty then

src/Lean/Server/Completion.lean

@@ -9,6 +9,8 @@ import Lean.Server.InfoUtils
 
 namespace Lean.Server.Completion
 open Lsp
+open Elab
+open Meta
 
 builtin_initialize completionBlackListExt : TagDeclarationExtension ← mkTagDeclarationExtension `blackListCompletion
 
@@ -23,26 +25,46 @@ private def isBlackListedForCompletion (declName : Name) : MetaM Bool := do
   let env ← getEnv
   return isAuxRecursor env declName || isNoConfusion env declName || (← isRec declName) || isBlackListed env declName
 
-open Elab in open Meta in
+private partial def consumeImplicitPrefix (e : Expr) : MetaM Expr := do
+  match e with
+  | Expr.forallE n d b c =>
+    -- We do not consume instance implicit arguments because the user probably wants be aware of this dependency
+    if c.binderInfo == BinderInfo.implicit then
+      let arg ← mkFreshExprMVar (userName := n) d
+      consumeImplicitPrefix (b.instantiate1 arg)
+    else
+      return e
+  | _ => return e
+
+private def dotCompletion (ctx : ContextInfo) (info : TermInfo) (expectedType? : Option Expr) : IO (Option CompletionList) :=
+  info.runMetaM ctx do
+    dbg_trace ">> {info.stx}, {info.expr}"
+    let type ← instantiateMVars (← inferType info.expr)
+    match type.getAppFn with
+    | Expr.const name .. =>
+      let candidates := (← getEnv).constants.fold (init := #[]) fun candidates declName declInfo =>
+        if !declName.isInternal && declName.getPrefix == name then candidates.push declInfo else candidates
+      let items : Array CompletionItem ← candidates.filterMapM fun cinfo => do
+        if (← isBlackListedForCompletion cinfo.name) then
+          return none
+        else
+          let detail ← Meta.ppExpr (← consumeImplicitPrefix cinfo.type)
+          return some { label := cinfo.name.getString!, detail? := some (toString detail), documentation? := none }
+      return some { items := items, isIncomplete := true }
+    | _ => return none
+
+private def idCompletion (ctx : ContextInfo) (lctx : LocalContext) (stx : Syntax) (openDecls : List OpenDecl) (expectedType? : Option Expr) : IO (Option CompletionList) :=
+  ctx.runMetaM lctx do
+    let id := stx.getId
+    if id.hasMacroScopes then return none
+
+    return none
+
 partial def find? (fileMap : FileMap) (hoverPos : String.Pos) (infoTree : InfoTree) : IO (Option CompletionList) := do
   let ⟨hoverLine, _⟩ := fileMap.toPosition hoverPos
   match infoTree.foldInfo (init := none) (choose fileMap hoverLine) with
-  | some (ctx, Info.ofCompletionInfo (CompletionInfo.dot info ..)) =>
-    info.runMetaM ctx do
-      dbg_trace ">> {info.stx}, {info.expr}"
-      let type ← instantiateMVars (← inferType info.expr)
-      match type.getAppFn with
-      | Expr.const name .. =>
-        let candidates := (← getEnv).constants.fold (init := #[]) fun candidates declName declInfo =>
-          if !declName.isInternal && declName.getPrefix == name then candidates.push declInfo else candidates
-        let items : Array CompletionItem ← candidates.filterMapM fun cinfo => do
-          if (← isBlackListedForCompletion cinfo.name) then
-            return none
-          else
-            let detail ← Meta.ppExpr cinfo.type
-            return some { label := cinfo.name.getString!, detail? := some (toString detail), documentation? := none }
-        return some { items := items, isIncomplete := true }
-      | _ => return none
+  | some (ctx, Info.ofCompletionInfo (CompletionInfo.dot info (expectedType? := expectedType?) ..)) => dotCompletion ctx info expectedType?
+  | some (ctx, Info.ofCompletionInfo (CompletionInfo.id stx lctx openDecls expectedType?)) => idCompletion ctx lctx stx openDecls expectedType?
   | _ => return none
 where
   choose (fileMap : FileMap) (hoverLine : Nat) (ctx : ContextInfo) (info : Info) (best? : Option (ContextInfo × Info)) : Option (ContextInfo × Info) :=