fix: auto-completion bugs and performance

src/Lean/Data/Lsp/LanguageFeatures.lean

@@ -47,19 +47,19 @@ structure CompletionItem where
   documentation? : Option MarkupContent := none
   kind?          : Option CompletionItemKind := none
   textEdit?      : Option InsertReplaceEdit := none
+  sortText?      : Option String := none
+  data?          : Option Json := none
   /-
   tags? : CompletionItemTag[]
   deprecated? : boolean
   preselect? : boolean
-  sortText? : string
   filterText? : string
   insertText? : string
   insertTextFormat? : InsertTextFormat
   insertTextMode? : InsertTextMode
   additionalTextEdits? : TextEdit[]
   commitCharacters? : string[]
-  command? : Command
-  data? : any -/
+  command? : Command -/
   deriving FromJson, ToJson, Inhabited
 
 structure CompletionList where

src/Lean/Elab/BuiltinCommand.lean

@@ -534,10 +534,10 @@ open Meta
 def elabCheckCore (ignoreStuckTC : Bool) : CommandElab
   | `(#check%$tk $term) => withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_check do
     -- show signature for `#check id`/`#check @id`
-    if let `($_:ident) := term then
+    if let `($id:ident) := term then
       try
         for c in (← resolveGlobalConstWithInfos term) do
-          addCompletionInfo <| .id term c (danglingDot := false) {} none
+          addCompletionInfo <| .id term id.getId (danglingDot := false) {} none
           logInfoAt tk <| .ofPPFormat { pp := fun
             | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature c
             | none     => return f!"{c}"  -- should never happen

src/Lean/Elab/BuiltinTerm.lean

@@ -158,7 +158,10 @@ private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr :=
 @[builtin_term_elab noImplicitLambda] def elabNoImplicitLambda : TermElab := fun stx expectedType? =>
   elabTerm stx[1] (mkNoImplicitLambdaAnnotation <$> expectedType?)
 
-@[builtin_term_elab Lean.Parser.Term.cdot] def elabBadCDot : TermElab := fun _ _ =>
+@[builtin_term_elab Lean.Parser.Term.cdot] def elabBadCDot : TermElab := fun stx expectedType? => do
+  if stx[0].getAtomVal == "." then
+    -- Users may input bad cdots because they are trying to auto-complete them using the expected type
+    addCompletionInfo <| CompletionInfo.dotId stx .anonymous (← getLCtx) expectedType?
   throwError "invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`)"
 
 @[builtin_term_elab str] def elabStrLit : TermElab := fun stx _ => do

src/Lean/Elab/InfoTree/Main.lean

@@ -49,14 +49,25 @@ def PartialContextInfo.mergeIntoOuter?
     some { outer with parentDecl? := innerParentDecl }
 
 def CompletionInfo.stx : CompletionInfo → Syntax
-  | dot i .. => i.stx
-  | id stx .. => stx
-  | dotId stx .. => stx
-  | fieldId stx .. => stx
-  | namespaceId stx => stx
-  | option stx => stx
+  | dot i ..          => i.stx
+  | id stx ..         => stx
+  | dotId stx ..      => stx
+  | fieldId stx ..    => stx
+  | namespaceId stx   => stx
+  | option stx        => stx
   | endSection stx .. => stx
-  | tactic stx .. => stx
+  | tactic stx ..     => stx
+
+/--
+Obtains the `LocalContext` from this `CompletionInfo` if available and yields an empty context
+otherwise.
+-/
+def CompletionInfo.lctx : CompletionInfo → LocalContext
+  | dot i ..            => i.lctx
+  | id _ _ _ lctx ..    => lctx
+  | dotId _ _ lctx ..   => lctx
+  | fieldId _ _ lctx .. => lctx
+  | _                   => .empty
 
 def CustomInfo.format : CustomInfo → Format
   | i => f!"CustomInfo({i.value.typeName})"

src/Lean/Meta/CompletionName.lean

@@ -29,11 +29,21 @@ builtin_initialize completionBlackListExt : TagDeclarationExtension ← mkTagDec
 def addToCompletionBlackList (env : Environment) (declName : Name) : Environment :=
   completionBlackListExt.tag env declName
 
+/--
+Checks whether a given name is internal due to something other than `_private`.
+Correctly deals with names like `_private.<SomeNamespace>.0.<SomeType>._sizeOf_1` in a private type
+`SomeType`, which `n.isInternal && !isPrivateName n` does not.
+-/
+private def isInternalNameModuloPrivate : Name → Bool
+  | n@(.str p s) => s.get 0 == '_' && n != privateHeader || isInternalNameModuloPrivate p
+  | .num p _ => isInternalNameModuloPrivate p
+  | _       => false
+
 /--
 Return true if name is blacklisted for completion purposes.
 -/
 private def isBlacklisted (env : Environment) (declName : Name) : Bool :=
-  declName.isInternal && !isPrivateName declName
+  isInternalNameModuloPrivate declName
   || isAuxRecursor env declName
   || isNoConfusion env declName
   || isRecCore env declName

src/Lean/Modifiers.lean

@@ -47,7 +47,7 @@ def isPrivateNameExport (n : Name) : Bool :=
 Return `true` if `n` is of the form `_private.<module_name>.0`
 See comment above.
 -/
-private def isPrivatePrefix (n : Name) : Bool :=
+def isPrivatePrefix (n : Name) : Bool :=
   match n with
   | .num p 0 => go p
   | _ => false