diff --git a/src/Lean/Elab/DocString.lean b/src/Lean/Elab/DocString.lean
index 40f3f527b1..8b30dfa3b3 100644
--- 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)
diff --git a/tests/lean/run/versoDocSuggestionNoImport.lean b/tests/lean/run/versoDocSuggestionNoImport.lean
new file mode 100644
index 0000000000..c9acd63b67
--- /dev/null
+++ 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
diff --git a/tests/lean/run/versoDocs.lean b/tests/lean/run/versoDocs.lean
index d59a4ceac9..ab3de67aab 100644
--- 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