fix: docstring code suggestions take shadowing into account (#12321)

This PR makes suggestions for builtin docstring roles take shadowing into account and improves the error message when this goes wrong. Closes ##12291
2026-02-05 14:45:35 +01:00 · 2026-02-05 14:45:35 +01:00 · 4046dd1e61
commit 4046dd1e61
parent 398c3622fc
3 changed files with 260 additions and 24 deletions
--- a/src/Lean/Elab/DocString.lean
+++ b/src/Lean/Elab/DocString.lean
@ -552,17 +552,17 @@ private def genWrapper (declName : Name) (argType : Option Expr) (retType : Expr
        else
          argSpec := argSpec.push (.positional name argType)
      if h : args.size < 1 then
-        throwError "Expected at least one parameter"
+        throwError "Expected at least one parameter to `{.ofConstName declName}`"
      else
        if let some expected := argType then
          let final := args[args.size-1]
          let localDecl ← final.fvarId!.getDecl
          unless ← isDefEq localDecl.type expected do
-            throwError "Expected last parameter type to be {expected} but got {localDecl.type}"
+            throwError "Expected type of last parameter to `{.ofConstName declName}` to be `{.ofExpr expected}` but got `{.ofExpr localDecl.type}`"

        let expected ← mkAppM ``DocM #[retType]
        unless ← isDefEq ret expected do
-          throwError "Expected return type to be {expected} but got {ret}"
+          throwError "Expected return type of `{.ofConstName declName}` to be `{.ofExpr expected}` but got `{.ofExpr ret}`"

      pure argSpec
    let inls ← mkAppM ``TSyntaxArray #[← mkListLit (.const ``SyntaxNodeKind []) [toExpr `inline]]
@ -1048,10 +1048,42 @@ private unsafe def codeBlockSuggestionsUnsafe : TermElabM (Array (StrLit → Doc
@[implemented_by codeBlockSuggestionsUnsafe]
 private opaque codeBlockSuggestions : TermElabM (Array (StrLit → DocM (Array CodeBlockSuggestion)))

-private def builtinElabName (n : Name) : Option Name :=
-  if (`Lean.Doc).isPrefixOf n then some n
-  else if n matches (.str .anonymous _) then some <| `Lean.Doc ++ n
-  else none
+/--
+Resolves a name against `NameMap` that contains a list of builtin expanders, taking into account
+open namespaces and the current namespace. This is needed because builtin doc roles/code
+blocks/directives are not present in the environment when `Lean` is not imported, so standard name
+resolution (`realizeGlobalConstNoOverload`) won't find them.
+
+This is called as a fallback when the identifier can't be resolved.
+-/
+private def resolveBuiltinDocName {α : Type} (builtins : NameMap α) (x : Name) : TermElabM (Option α) := do
+  if let some v := builtins.get? x then return some v
+
+  -- Builtins shouldn't require a prefix, as they're part of the language.
+  if let some v := builtins.get? (`Lean.Doc ++ x) then return some v
+
+  -- If this fails, try resolving through open namespaces so that {Doc.lit}`foo` will work when
+  -- `Lean` is opened.
+  let openDecls ← getOpenDecls
+  for decl in openDecls do
+    match decl with
+    | .simple ns exs =>
+      if !exs.any (· == x) then
+        if let some v := builtins.get? (ns ++ x) then return some v
+    | .explicit openedId declName =>
+      if openedId == x then
+        if let some v := builtins.get? declName then return some v
+      else if openedId.isPrefixOf x then
+        let candidate := x.replacePrefix openedId declName
+        if let some v := builtins.get? candidate then return some v
+
+  -- Try resolving through current namespace hierarchy
+  let mut ns ← getCurrNamespace
+  while !ns.isAnonymous do
+    if let some v := builtins.get? (ns ++ x) then return some v
+    ns := ns.getPrefix
+
+  return none

 private unsafe def roleExpandersForUnsafe (roleName : Ident) :
    TermElabM (Array (Name × (TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline)))) := do
@ -1064,8 +1096,7 @@ private unsafe def roleExpandersForUnsafe (roleName : Ident) :
    return (← names.mapM (fun x => do return (x, ← evalConst _ x))) ++ builtins
  else
    let x := roleName.getId
-    let hasBuiltin :=
-      (← builtinDocRoles.get).get? x <|> (← builtinDocRoles.get).get? (`Lean.Doc ++ x)
+    let hasBuiltin ← resolveBuiltinDocName (← builtinDocRoles.get) x
    return hasBuiltin.toArray.flatten


@ -1084,8 +1115,7 @@ private unsafe def codeBlockExpandersForUnsafe (codeBlockName : Ident) :
    return (← names.mapM (fun x => do return (x, ← evalConst _ x))) ++ names'
  else
    let x := codeBlockName.getId
-    let hasBuiltin :=
-      (← builtinDocCodeBlocks.get).get? x <|> (← builtinDocCodeBlocks.get).get? (`Lean.Doc ++ x)
+    let hasBuiltin ← resolveBuiltinDocName (← builtinDocCodeBlocks.get) x
    return hasBuiltin.toArray.flatten


@ -1104,8 +1134,7 @@ private unsafe def directiveExpandersForUnsafe (directiveName : Ident) :
    return (← names.mapM (fun x => do return (x, ← evalConst _ x))) ++ names'
  else
    let x := directiveName.getId
-    let hasBuiltin :=
-      (← builtinDocDirectives.get).get? x <|> (← builtinDocDirectives.get).get? (`Lean.Doc ++ x)
+    let hasBuiltin ← resolveBuiltinDocName (← builtinDocDirectives.get) x
    return hasBuiltin.toArray.flatten

@[implemented_by directiveExpandersForUnsafe]
@ -1178,7 +1207,27 @@ private def suggestionName (name : Name) : TermElabM Name := do
    else if (← builtinDocCodeBlocks.get).contains name then pure (some name)
    else pure none
  match name' with
-    | some (.str _ s) => return .str .anonymous s
+    | some (.str _ s) =>
+      -- Check if the simple name is shadowed locally or globally
+      let simpleName := .str .anonymous s
+      let qualifiedBuiltin := `Lean.Doc ++ simpleName
+      -- Local shadowing check
+      if (← resolveLocalName simpleName).isSome then
+        return qualifiedBuiltin
+      -- Global shadowing check: try to resolve the simple name and see
+      -- if it resolves to something other than the builtin role
+      else
+        let resolved? ← try
+          some <$> resolveGlobalConstNoOverload (mkIdent simpleName)
+        catch _ => pure none
+        match resolved? with
+        | some resolved =>
+          -- If it resolves to the builtin, use simple name; otherwise qualified
+          if resolved == qualifiedBuiltin then return simpleName
+          else return qualifiedBuiltin
+        | none =>
+          -- Nothing to shadow
+          return simpleName
    | some n => return n
    | none =>
      -- If it exists, unresolve it
@ -1203,7 +1252,8 @@ private def mkSuggestion
    DocM MessageData := do
  match (← read).suggestionMode with
  | .interactive =>
-    hintTitle.hint (newStrings.map fun (s, preInfo?, postInfo?) => { suggestion := s, preInfo?, postInfo? }) (ref? := some ref)
+    hintTitle.hint (newStrings.map fun (s, preInfo?, postInfo?) =>
+      { suggestion := s, preInfo?, postInfo? }) (ref? := some ref)
  | .batch =>
    let some ⟨b, e⟩ := ref.getRange?
      | pure m!""
@ -1223,6 +1273,56 @@ def nameOrBuiltinName [Monad m] [MonadEnv m] (x : Name) : m Name := do
  if env.contains x then return x
  else return `Lean.Doc ++ x

+/--
+Finds registered expander names that `x` is a suffix of, for use in error message hints when the
+name is shadowed. Returns display names suitable for `mkSuggestion`.
+-/
+private def findShadowedNames {α : Type}
+    (nonBuiltIns : NameMap (Array Name)) (builtins : NameMap α) (x : Name) :
+    TermElabM (Array Name) := do
+  if x.isAnonymous then return #[]
+  let mut candidates : NameSet := {}
+  for (fullName, _) in nonBuiltIns do
+    if x.isSuffixOf fullName then
+      candidates := candidates.insert fullName
+  for (fullName, _) in builtins do
+    if x.isSuffixOf fullName then
+      candidates := candidates.insert fullName
+  let mut result := #[]
+  for c in candidates do
+    let displayName ← suggestionName c
+    -- Only suggest if the display name differs from what the user wrote
+    if displayName != x then
+      result := result.push displayName
+  return result
+
+/--
+Builds a hint for an "Unknown role/directive/..." error when the name might be shadowed.
+-/
+private def shadowedHint {α : Type}
+    (envEntries : NameMap (Array Name)) (builtins : NameMap α)
+    (name : Ident) (kind : String) : DocM MessageData := do
+  let candidates ← findShadowedNames envEntries builtins name.getId
+  if candidates.isEmpty then return m!""
+  let ss := candidates.map fun c => (c.toString, none, none)
+  mkSuggestion name m!"`{name}` shadows a {kind}. Use the full name of the shadowed {kind}:" ss
+
+/--
+Throws an appropriate error for an unknown doc element (role/directive/code block/command).
+Distinguishes "name resolves but isn't registered" from "name doesn't resolve at all",
+and includes shadowed-name suggestions when applicable.
+-/
+private def throwUnknownDocElem {α β : Type}
+    (envEntries : NameMap (Array Name)) (builtins : NameMap α)
+    (name : Ident) (kind : String) : DocM β := do
+  let hint ← shadowedHint envEntries builtins name kind
+  let resolved? ← try some <$> realizeGlobalConstNoOverload name catch | _ => pure none
+  if let some resolved := resolved? then
+    let info ← getConstInfo resolved
+    throwErrorAt name m!"`{name} : {info.type}` is not registered as a a {kind}{hint}"
+  else
+    throwErrorAt name m!"Unknown {kind} `{name}`{hint}"
+
 /--
 Elaborates the syntax of an inline document element to an actual inline document element.
 -/
@ -1270,8 +1370,9 @@ public partial def elabInline (stx : TSyntax `inline) : DocM (Inline ElabInline)
                snd.snd := moreInfo.map withSpace
              }
          let ss := ss.qsort (fun x y => x.1 < y.1)
+          let litName ← suggestionName `Lean.Doc.lit
          let litSuggestion :=
-            ( "{lit}" ++ str,
+            ( "{" ++ litName.toString ++ "}" ++ str,
              some "Use the `lit` role:\n",
              some "\nto mark the code as literal text and disable suggestions" )
          let ss := ss.push litSuggestion
@ -1300,7 +1401,7 @@ public partial def elabInline (stx : TSyntax `inline) : DocM (Inline ElabInline)
            continue
          else throw e
        | e => throw e
-    throwErrorAt name "Unknown role `{name}`"
+    throwUnknownDocElem (docRoleExt.getState (← getEnv)) (← builtinDocRoles.get) name "role"
  | other =>
    throwErrorAt other "Unsupported syntax {other}"
 where
@ -1366,7 +1467,7 @@ public partial def elabBlock (stx : TSyntax `block) : DocM (Block ElabInline Ela
            continue
          else throw e
        | e => throw e
-    throwErrorAt name "Unknown directive `{name}`"
+    throwUnknownDocElem (docDirectiveExt.getState (← getEnv)) (← builtinDocDirectives.get) name "directive"
  | `(block| ```%$opener | $s ```) =>
    if doc.verso.suggestions.get (← getOptions) then
      if let some ⟨b, e⟩ := opener.getRange? then
@ -1409,7 +1510,7 @@ public partial def elabBlock (stx : TSyntax `block) : DocM (Block ElabInline Ela
            continue
          else throw e
        | e => throw e
-    throwErrorAt name "Unknown code block `{name}`"
+    throwUnknownDocElem (docCodeBlockExt.getState (← getEnv)) (← builtinDocCodeBlocks.get) name "code block"
  | `(block| command{$name $args*}) =>
    let expanders ← commandExpandersFor name
    for (exName, ex) in expanders do
@ -1428,7 +1529,7 @@ public partial def elabBlock (stx : TSyntax `block) : DocM (Block ElabInline Ela
            continue
          else throw e
        | e => throw e
-    throwErrorAt name "Unknown document command `{name}`"
+    throwUnknownDocElem (docCommandExt.getState (← getEnv)) (← builtinDocCommands.get) name "document command"
  | `(block|%%%$_*%%%) =>
    let h ←
      if stx.raw.getRange?.isSome then m!"Remove it".hint #[""] (ref? := stx)
--- a/tests/lean/run/versoDocSuggestionNoImport.lean
+++ b/tests/lean/run/versoDocSuggestionNoImport.lean
@ -0,0 +1,50 @@
+set_option doc.verso true
+
+/-!
+When a builtin role name like {lit}`lit` is shadowed by a user definition, the suggestion should use
+the qualified name {lit}`Lean.Doc.lit`. This test checks that this also works when there are no
+imports.
+-/
+
+namespace ShadowedBuiltin
+def lit := Nat  -- Shadow the builtin 'lit' role
+
+/--
+warning: Code element could be more specific.
+
+Hint: Insert a role to document it:
+  • {̲g̲i̲v̲e̲n̲}̲`test`
+  • Use the `lit` role:
+    {̲L̲e̲a̲n̲.̲D̲o̲c̲.̲l̲i̲t̲}̲`test`
+    to mark the code as literal text and disable suggestions
+-/
+#guard_msgs in
+/--
+`test`
+-/
+def testShadowedLit := 0
+
+-- Verify that {Lean.Doc.lit} works when lit is shadowed
+#guard_msgs in
+/-- {Lean.Doc.lit}`qualified works` -/
+def testQualifiedLit := 1
+
+open Lean
+-- Verify that {Doc.lit} works when lit is shadowed and Lean is not imported
+#guard_msgs in
+/-- {Doc.lit}`qualified works` -/
+def testQualifiedLit2 := 1
+
+
+-- {lit} fails when shadowed
+/--
+error: `lit : Type` is not registered as a a role
+
+Hint: `lit` shadows a role. Use the full name of the shadowed role:
+  L̲e̲a̲n̲.̲D̲o̲c̲.̲lit
+-/
+#guard_msgs in
+/-- {lit}`broken` -/
+def testBrokenLit := 0
+
+end ShadowedBuiltin
--- a/tests/lean/run/versoDocs.lean
+++ b/tests/lean/run/versoDocs.lean
@ -536,8 +536,93 @@ Less than {name}`seven`.
 -/
 add_decl_doc four

-/-
-TODO test:
-* Scope rules for all operators
-
+/-!
+When a builtin role name like {name}`lit` is shadowed by a user definition,
+the suggestion should use the qualified name {name}`Lean.Doc.lit`.
 -/
+namespace ShadowedBuiltin
+def lit := Nat  -- Shadow the builtin 'lit' role
+
+/--
+warning: Code element could be more specific.
+
+Hint: Insert a role to document it:
+  • {̲g̲i̲v̲e̲n̲}̲`test`
+  • Use the `lit` role:
+    {̲L̲e̲a̲n̲.̲D̲o̲c̲.̲l̲i̲t̲}̲`test`
+    to mark the code as literal text and disable suggestions
+-/
+#guard_msgs in
+/--
+`test`
+-/
+def testShadowedLit := 0
+
+/-! Verify that {Lean.Doc.lit}`{Lean.Doc.lit}` works when {name}`lit` is shadowed -/
+#guard_msgs in
+/-- {Lean.Doc.lit}`qualified works` -/
+def testQualifiedLit := 1
+
+-- {lit} fails when shadowed
+/--
+error: `lit : Type` is not registered as a a role
+
+Hint: `lit` shadows a role. Use the full name of the shadowed role:
+  L̲e̲a̲n̲.̲D̲o̲c̲.̲lit
+-/
+#guard_msgs in
+/-- {lit}`broken` -/
+def testBrokenLit := 0
+
+end ShadowedBuiltin
+
+/-! Verify that this also works for non-builtin documentation roles -/
+
+/-- error: Unknown role `r` -/
+#guard_msgs in
+/-! {r}`foo` -/
+
+open Lean in
+@[doc_role]
+def r (_ : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
+  return .empty
+
+/-! {r}`foo` -/
+
+namespace ShadowedNonBuiltin
+def r := 15
+
+/--
+error: `r : Nat` is not registered as a a role
+
+Hint: `r` shadows a role. Use the full name of the shadowed role:
+  _̲ro̲o̲t̲_̲.̲r̲
+-/
+#guard_msgs in
+/-! {r}`foo` -/
+
+end ShadowedNonBuiltin
+
+namespace DoubleShadowed
+
+@[doc_role]
+def lit (_ : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
+  return .empty
+
+namespace Inner
+
+def lit := 5
+
+/--
+error: `lit : Nat` is not registered as a a role
+
+Hint: `lit` shadows a role. Use the full name of the shadowed role:
+  • l̵i̵t̵D̲o̲u̲b̲l̲e̲S̲h̲a̲d̲o̲w̲e̲d̲.̲l̲i̲t̲
+  • L̲e̲a̲n̲.̲D̲o̲c̲.̲lit
+-/
+#guard_msgs in
+/-! {lit}`abc` -/
+
+end Inner
+
+end DoubleShadowed