feat: suggest qualified names while editing Verso docstrings (#10584)

This PR causes Verso docstrings to search for a name in the environment
that is at least as long as the current name, providing it as a
suggestion.

Author: david-christiansen

src/Lean/Elab/DocString/Builtin.lean

@@ -22,6 +22,7 @@ import Lean.Elab.Tactic.Doc
 import Lean.Data.EditDistance
 public import Lean.Elab.DocString.Builtin.Keywords
 import Lean.Server.InfoUtils
+import Lean.Meta.Hint
 
 
 namespace Lean.Doc
@@ -132,6 +133,15 @@ meta def checkNameExists : PostponedCheckHandler := fun _ info => do
     | throwError "Expected `{.ofConstName ``PostponedName}`, got `{.ofConstName info.typeName}`"
   discard <| realizeGlobalConstNoOverload (mkIdent name)
 
+private def getQualified (x : Name) : DocM (Array Name) := do
+  let names := (← getEnv).constants.toList
+  let names := names.filterMap fun (y, _) => if !isPrivateName y && x.isSuffixOf y then some y else none
+  names.toArray.mapM fun y => do
+    let y ← unresolveNameGlobalAvoidingLocals y
+    pure y
+
+open Lean.Doc
+
 /--
 Displays a name, without attempting to elaborate implicit arguments.
 -/
@@ -168,7 +178,20 @@ def name (full : Option Ident := none) (scope : DocScope := .local)
         addConstInfo n x
         pure x
       else
-        realizeGlobalConstNoOverloadWithInfo n
+        try
+          realizeGlobalConstNoOverloadWithInfo n
+        catch
+          | err => do
+            let ref ← getRef
+            if let `(inline|role{$_x $_args*}%$tok[$_*]) := ref then
+              let ss ← getQualified n.raw.getId
+              let h ←
+                if ss.isEmpty then pure m!""
+                else m!"Insert a fully-qualified name:".hint (ref? := some tok) <|
+                  ss.map fun x => { suggestion := s!" (full := {x})" ++ "}", previewSpan? := ref}
+              logErrorAt s m!"{err.toMessageData}{h}"
+            else logErrorAt s m!"{err.toMessageData}"
+            return .code s!"{n.raw.getId}"
     return .other (.mk ``Data.Const (.mk (Data.Const.mk x))) #[.code s.getString]
   | .import xs =>
     let name :=

tests/lean/run/versoDocs.lean

@@ -199,7 +199,12 @@ def a := "a"
 def b := "b"
 end A
 
-/-- error: Unknown constant `a` -/
+/--
+error: Unknown constant `a`
+
+Hint: Insert a fully-qualified name:
+  {name ̲(̲f̲u̲l̲l̲ ̲:̲=̲ ̲A̲.̲a̲)̲}`a`
+-/
 #guard_msgs in
 /--
 role {name}`a` here
@@ -223,7 +228,13 @@ def testDef' := 15
 -/
 def testDef'' := 15
 
-/-- error: Unknown constant `b` -/
+/--
+error: Unknown constant `b`
+
+Hint: Insert a fully-qualified name:
+  • {name ̲(̲f̲u̲l̲l̲ ̲:̲=̲ ̲A̲.̲b̲)̲}`b`
+  • {name ̲(̲f̲u̲l̲l̲ ̲:̲=̲ ̲M̲e̲t̲a̲.̲G̲r̲i̲n̲d̲.̲A̲r̲i̲t̲h̲.̲C̲u̲t̲s̲a̲t̲.̲D̲v̲d̲S̲o̲l̲u̲t̲i̲o̲n̲.̲b̲)̲}`b`
+-/
 #guard_msgs in
 /--
 {open A only:=a}
@@ -312,6 +323,18 @@ Suggestions are as well.
 -/
 def otherAttr := ()
 
+/--
+error: Unknown constant `Constraint.add`
+
+Hint: Insert a fully-qualified name:
+  {name ̲(̲f̲u̲l̲l̲ ̲:̲=̲ ̲O̲m̲e̲g̲a̲.̲C̲o̲n̲s̲t̲r̲a̲i̲n̲t̲.̲a̲d̲d̲)̲}`Constraint.add`
+-/
+#guard_msgs in
+/--
+{name}`Constraint.add`
+-/
+def nameErrSuggestions := ()
+
 /--
 Options control Lean.
 Examples: