From 3796cecc50f46f1068e58aa5937c23f71bd0589b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <emilio@lean-fro.org>
Date: Mon, 23 Feb 2026 01:02:56 +0100
Subject: [PATCH 1/3] feat: Improve role resolution error diagnostics

As seen in #762 , the experience of using a non-registered or incorrect role is far from ideal. In particular, the error message is a syntax error. We can do better if we only consider registered roles for name resolution.

In order to do this we:
remove the role-inline fallback that treated unknown/unregistered roles as plain function applications
- add explicit diagnostics for role resolution failures:
  - function found but not registered as a role
  - function found but likely not a role
  - unknown role with fuzzy suggestion when close, otherwise an available-role list
- display short role names (in-scope style) in diagnostics
- expose `registeredRoleNames` in `Verso.Doc.Elab.Monad` to support role diagnostics
- add `Tests.RoleResolution` and wire it into `src/tests/Tests.lean`

This PR is a RFC. If accepted, I'd suggest implementing the same idea for directives and commands, and implement role/directive/command auto-completion as a follow-up.
---
 src/tests/Tests.lean                          |   1 +
 src/tests/Tests/RoleResolution.lean           | 171 ++++++++++++++++++
 src/verso/Verso/Doc/Elab.lean                 |  87 ++++++++-
 src/verso/Verso/Doc/Elab/Monad.lean           |  13 ++
 .../custom-genre/SimplePage/Demo.lean         |   2 +
 .../PackageManual/DocFeatures.lean            |   2 +
 test-projects/textbook/DemoTextbook.lean      |   4 +
 7 files changed, 275 insertions(+), 5 deletions(-)
 create mode 100644 src/tests/Tests/RoleResolution.lean

diff --git a/src/tests/Tests.lean b/src/tests/Tests.lean
index 704aeeea..67f23762 100644
--- a/src/tests/Tests.lean
+++ b/src/tests/Tests.lean
@@ -23,6 +23,7 @@ import Tests.ParserRegression
 import Tests.Paths
 import Tests.PorterStemmer
 import Tests.Refs
+import Tests.RoleResolution
 import Tests.Serialization
 import Tests.TeX
 import Tests.TexUnit
diff --git a/src/tests/Tests/RoleResolution.lean b/src/tests/Tests/RoleResolution.lean
new file mode 100644
index 00000000..5b7aaf10
--- /dev/null
+++ b/src/tests/Tests/RoleResolution.lean
@@ -0,0 +1,171 @@
+/-
+Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Emilio J. Gallego Arias
+-/
+import Verso
+import VersoManual
+import VersoBlog
+
+namespace Verso.RoleResolutionTest
+set_option guard_msgs.diff true
+
+open Lean
+
+/-
+Role resolution has four relevant outcomes:
+1. role function exists, has type `RoleExpander`, and is registered - good.
+2. role function exists, has a role type, but is not registered - bad.
+3. role function exists, but has the wrong type - bad.
+4. role function does not exist - unresolved role name.
+-/
+
+@[role_expander registered]
+def registered : Verso.Doc.Elab.RoleExpander
+  | _, _ => do
+    pure #[← `(Verso.Doc.Inline.text "registered-role")]
+
+#docs (.none) roleCase1 "Case 1" :=
+:::::::
+{registered}[]
+:::::::
+
+/-- info: #[Verso.Doc.Block.para #[Verso.Doc.Inline.text "registered-role"]] -/
+#guard_msgs in
+#eval roleCase1.toPart.content
+
+def unregistered : Verso.Doc.Elab.RoleExpander
+  | _, _ => do
+    pure #[← `(Verso.Doc.Inline.text "unregistered-role")]
+
+/--
+error: Role function `unregistered` was found but not registered as a role. Register it with `@[role]` or `@[role_expander ...]`.
+-/
+#guard_msgs in
+#docs (.none) roleCase2 "Case 2" :=
+:::::::
+{unregistered}[]
+:::::::
+
+def wrongType : Nat := 7
+
+/--
+error: Function `wrongType` was found but likely not a role.
+-/
+#guard_msgs in
+#docs (.none) roleCase3 "Case 3" :=
+:::::::
+{wrongType}[]
+:::::::
+
+/--
+error: No registered role `registred`. Did you mean role `registered`?
+-/
+#guard_msgs in
+#docs (.none) roleCase4 "Case 4" :=
+:::::::
+{registred}[]
+:::::::
+
+/--
+error: No registered role `nothereatallzzzz`. Available roles (showing 20 of 37): anchor, anchorError, anchorInfo, anchorName, anchorTerm, anchorWarning, blob, citehere, citep, citet, conv, deftech, draft, htmlSpan, inst, label, lean, leanCommand, leanInline, leanKw
+-/
+#guard_msgs in
+#docs (.none) roleCase5 "Case 5" :=
+:::::::
+{nothereatallzzzz}[]
+:::::::
+
+namespace ManualCases
+open Genre Manual
+
+@[role_expander manualRegistered]
+def manualRegistered : Verso.Doc.Elab.RoleExpander
+  | _, _ => do
+    pure #[← `(Verso.Doc.Inline.text "manual-registered-role")]
+
+#docs (Manual) roleCase1 "Manual Case 1" :=
+:::::::
+{manualRegistered}[]
+:::::::
+
+def manualUnregistered : Verso.Doc.Elab.RoleExpander
+  | _, _ => do
+    pure #[← `(Verso.Doc.Inline.text "manual-unregistered-role")]
+
+/--
+error: Role function `manualUnregistered` was found but not registered as a role. Register it with `@[role]` or `@[role_expander ...]`.
+-/
+#guard_msgs in
+#docs (Manual) roleCase2 "Manual Case 2" :=
+:::::::
+{manualUnregistered}[]
+:::::::
+
+/--
+error: No registered role `manualRegistred`. Did you mean role `manualRegistered`?
+-/
+#guard_msgs in
+#docs (Manual) roleCase3 "Manual Case 3" :=
+:::::::
+{manualRegistred}[]
+:::::::
+
+/--
+error: No registered role `manualNowhereNearZzzzz`. Available roles (showing 20 of 38): anchor, anchorError, anchorInfo, anchorName, anchorTerm, anchorWarning, blob, citehere, citep, citet, conv, deftech, draft, htmlSpan, inst, label, lean, leanCommand, leanInline, leanKw
+-/
+#guard_msgs in
+#docs (Manual) roleCase4 "Manual Case 4" :=
+:::::::
+{manualNowhereNearZzzzz}[]
+:::::::
+
+end ManualCases
+
+namespace BlogCases
+open Genre Blog
+
+@[role_expander blogRegistered]
+def blogRegistered : Verso.Doc.Elab.RoleExpander
+  | _, _ => do
+    pure #[← `(Verso.Doc.Inline.text "blog-registered-role")]
+
+#docs (Blog.Post) roleCase1 "Blog Case 1" :=
+:::::::
+{blogRegistered}[]
+:::::::
+
+def blogUnregistered : Verso.Doc.Elab.RoleExpander
+  | _, _ => do
+    pure #[← `(Verso.Doc.Inline.text "blog-unregistered-role")]
+
+/--
+error: Role function `blogUnregistered` was found but not registered as a role. Register it with `@[role]` or `@[role_expander ...]`.
+-/
+#guard_msgs in
+#docs (Blog.Post) roleCase2 "Blog Case 2" :=
+:::::::
+{blogUnregistered}[]
+:::::::
+
+/--
+error: No registered role `blogRegistred`. Did you mean role `blogRegistered`?
+-/
+#guard_msgs in
+#docs (Blog.Post) roleCase3 "Blog Case 3" :=
+:::::::
+{blogRegistred}[]
+:::::::
+
+/--
+error: No registered role `blogNoCloseMatchZzzzz`. Available roles (showing 20 of 39): anchor, anchorError, anchorInfo, anchorName, anchorTerm, anchorWarning, blob, blogRegistered, citehere, citep, citet, conv, deftech, draft, htmlSpan, inst, label, lean, leanCommand, leanInline
+-/
+#guard_msgs in
+#docs (Blog.Post) roleCase4 "Blog Case 4" :=
+:::::::
+{blogNoCloseMatchZzzzz}[]
+:::::::
+
+end BlogCases
+
+end Verso.RoleResolutionTest
diff --git a/src/verso/Verso/Doc/Elab.lean b/src/verso/Verso/Doc/Elab.lean
index a4281c99..4d1c9e01 100644
--- a/src/verso/Verso/Doc/Elab.lean
+++ b/src/verso/Verso/Doc/Elab.lean
@@ -7,6 +7,7 @@ module
 public import Verso.Doc.Elab.Monad
 meta import Verso.Doc.Elab.Monad
 public import Lean.DocString.Syntax
+public meta import Lean.Data.EditDistance
 import Verso.Doc.Elab.Inline
 public import Verso.Doc.Elab.Inline
 public meta import Verso.Doc.Elab.Inline
@@ -118,6 +119,83 @@ private meta def expanderDocHover (stx : Syntax) (what : String) (name : Name) (
     out := out ++ "\n\n" ++ d
   Hover.addCustomHover stx out
 
+private meta def roleSuggestionThreshold (input _candidate : String) : Nat :=
+  if input.length < 5 then 1 else if input.length < 10 then 2 else 3
+
+private meta def shortRoleName (name : Name) : String :=
+  match name with
+  | .anonymous => toString name
+  | .str _ s => s
+  | .num _ n => toString n
+
+private meta def roleSuggestions (candidates : Array (Name × String)) (input : String) (count : Nat := 10) : Array (Name × String) :=
+  let close := candidates.filterMap fun candidate =>
+    let cand := candidate.2
+    let limit := roleSuggestionThreshold input cand
+    EditDistance.levenshtein cand input limit <&> (candidate, ·)
+  let close := close.qsort (fun x y => x.2 < y.2 || (x.2 == y.2 && x.1.2 < y.1.2))
+  close.take count |>.map (·.1)
+
+private meta def availableRoleNames : DocElabM (Array Name) := do
+  return (← registeredRoleNames).qsort (·.toString < ·.toString)
+
+private meta def availableRoleDisplayNames : DocElabM (Array (Name × String)) := do
+  (← availableRoleNames).mapM fun full =>
+    return (full, shortRoleName full)
+
+private meta def isRoleFunctionType (declName : Name) : DocElabM Bool := do
+  let asCoreRole ← Meta.withNewMCtxDepth do
+    let c ← mkConstWithLevelParams declName
+    let t ← Meta.inferType c
+    Meta.isDefEq t (mkConst ``RoleExpander)
+  if asCoreRole then return true
+
+  Meta.withNewMCtxDepth do
+    try
+      let c ← mkConstWithLevelParams declName
+      discard <| Meta.mkAppM ``toRole #[c]
+      return true
+    catch
+      | _ => return false
+
+private meta def throwRoleNotRegisteredError (name : Ident) (resolvedName : Name) : DocElabM α := do
+  let shownName := shortRoleName resolvedName
+  if ← isRoleFunctionType resolvedName then
+    throwErrorAt name m!"Role function `{shownName}` was found but not registered as a role. Register it with `@[role]` or `@[role_expander ...]`."
+  else
+    throwErrorAt name m!"Function `{shownName}` was found but likely not a role."
+
+private meta def throwUnknownRoleError (name : Ident) : DocElabM α := do
+  let requested := name.getId.toString
+  let available ← availableRoleDisplayNames
+  let suggestions := roleSuggestions available requested
+  match suggestions.toList with
+  | (_, best) :: _ =>
+    throwErrorAt name m!"No registered role `{name.getId}`. Did you mean role `{best}`?"
+  | [] =>
+    if available.isEmpty then
+      throwErrorAt name m!"No registered role `{name.getId}`. No roles are currently registered."
+    else
+      let mut uniqueNames := #[]
+      for (_, n) in available do
+        unless uniqueNames.contains n do
+          uniqueNames := uniqueNames.push n
+      let sortedNames := uniqueNames.qsort (· < ·)
+      let shown := sortedNames.take 20
+      let suffix :=
+        if sortedNames.size > shown.size then
+          s!" (showing {shown.size} of {sortedNames.size})"
+        else ""
+      throwErrorAt name m!"No registered role `{name.getId}`. Available roles{suffix}: {String.intercalate ", " shown.toList}"
+
+private meta def resolveRoleName? (name : Ident) : DocElabM (Option Name) := do
+  match (← observing (realizeGlobalConstWithInfos name)) with
+  | .ok [n] => pure (some n)
+  | .ok [] => pure none
+  | .ok ns =>
+    throwErrorAt name m!"Role name `{name.getId}` is ambiguous. Candidates: {String.intercalate ", " <| ns.map (·.toString)}"
+  | .error _ => pure none
+
 
 open Lean.Parser.Term in
 @[inline_expander Lean.Doc.Syntax.role]
@@ -125,13 +203,12 @@ public meta def _root_.Lean.Doc.Syntax.role.expand : InlineExpander
   | inline@`(inline| role{$name $args*} [$subjects*]) => do
       withRef inline <| withFreshMacroScope <| withIncRecDepth <| do
         let genre := (← readThe DocElabContext).genreSyntax
-        let resolvedName ← realizeGlobalConstNoOverloadWithInfo name
+        let some resolvedName ← resolveRoleName? name
+          | throwUnknownRoleError name
         let exp ← roleExpandersFor resolvedName
-        let argVals ← parseArgs args
         if exp.isEmpty then
-          -- If no expanders are registered, then try elaborating just as a
-          -- function application node
-          return ← appFallback inline name resolvedName argVals subjects
+          throwRoleNotRegisteredError name resolvedName
+        let argVals ← parseArgs args
         for (e, doc?, sig?) in exp do
           try
             let termStxs ← withFreshMacroScope <| e argVals subjects
diff --git a/src/verso/Verso/Doc/Elab/Monad.lean b/src/verso/Verso/Doc/Elab/Monad.lean
index a5c79ee7..b9534646 100644
--- a/src/verso/Verso/Doc/Elab/Monad.lean
+++ b/src/verso/Verso/Doc/Elab/Monad.lean
@@ -627,6 +627,19 @@ private unsafe def roleExpandersForUnsafe (x : Name) : DocElabM (Array (RoleExpa
 @[implemented_by roleExpandersForUnsafe]
 public opaque roleExpandersFor (x : Name) : DocElabM (Array (RoleExpander × Option String × Option SigDoc))
 
+private unsafe def registeredRoleNamesUnsafe : DocElabM (Array Name) := do
+  let env ← getEnv
+  let mut names : NameSet := {}
+  for (n, _) in roleExpanderExt.getState env do
+    names := names.insert n
+  for (n, _) in env.constants do
+    if !(roleExpanderAttr.getEntries env n).isEmpty then
+      names := names.insert n
+  pure names.toList.toArray
+
+@[implemented_by registeredRoleNamesUnsafe]
+public opaque registeredRoleNames : DocElabM (Array Name)
+
 private unsafe def evalIOOptStringUnsafe (x : Name) : MetaM (Option SigDoc) := do
   evalConst (Option SigDoc) x
 
diff --git a/test-projects/custom-genre/SimplePage/Demo.lean b/test-projects/custom-genre/SimplePage/Demo.lean
index b1539884..76cf3993 100644
--- a/test-projects/custom-genre/SimplePage/Demo.lean
+++ b/test-projects/custom-genre/SimplePage/Demo.lean
@@ -9,6 +9,8 @@ open Tutorial
 
 #doc (SimplePage) "An _Astounding_ Document" =>
 
+-- NOTE(rfc-role-resolution): these role calls currently rely on the removed
+-- fallback-to-function-application behavior and now fail during `lake build`.
 Today is {today}[]. This document was created on {date 2024 5 13}[].
 
 # One Section
diff --git a/test-projects/package-manual/PackageManual/DocFeatures.lean b/test-projects/package-manual/PackageManual/DocFeatures.lean
index a23ebea0..07b9c276 100644
--- a/test-projects/package-manual/PackageManual/DocFeatures.lean
+++ b/test-projects/package-manual/PackageManual/DocFeatures.lean
@@ -34,6 +34,8 @@ The example project must depend on the same version of `subverso` that the docum
 Within the example project, examples are drawn from a module.
 Sometimes, the entire module is the example, while other cases use just some part of the module.
 To set a default module, use the option {option}`verso.exampleModule`.
+-- NOTE(rfc-role-resolution): `{index}` below is currently a plain function,
+-- not a registered role expander, and now fails under strict role resolution.
 When there is no default set, or to override it, the example code features all accept a keyword argument `module`.{index (subterm:="keyword argument")}[`module`]
 
 {optionDocs verso.exampleModule}
diff --git a/test-projects/textbook/DemoTextbook.lean b/test-projects/textbook/DemoTextbook.lean
index 7db15ebb..695a15cb 100644
--- a/test-projects/textbook/DemoTextbook.lean
+++ b/test-projects/textbook/DemoTextbook.lean
@@ -30,6 +30,8 @@ set_option pp.rawOnError true
 authors := ["David Thrane Christiansen"]
 %%%
 
+-- NOTE(rfc-role-resolution): `{index}` here is currently a plain function,
+-- not a registered role expander, and now fails under strict role resolution.
 {index}[example]
 Here's an example project showing how to build a certain kind of textbook with Verso.
 It's a good idea to read the document's source together with the rendered output, because it demonstrates how to use various features.
@@ -137,6 +139,8 @@ If incorrect hovers are appearing locally, then try disabling caching in your br
 
 # Using an Index
 
+-- NOTE(rfc-role-resolution): all `{index}` uses in this section fail for the
+-- same reason as above until they are migrated to registered roles.
 {index}[index]
 The index should contain an entry for “lorem ipsum”.
 {index}[lorem ipsum] foo

From 6a6fe491f419f4a0ecf0667b15d5b3b477bed87d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <emilio@lean-fro.org>
Date: Tue, 24 Feb 2026 13:09:30 +0100
Subject: [PATCH 2/3] fix: register legacy roles and update release notes

---
 doc/UsersGuide/Releases.lean                  |  2 +
 doc/UsersGuide/Releases/v4_28_0.lean          |  2 +-
 doc/UsersGuide/Releases/v4_29_0.lean          | 18 ++++++++
 src/tests/Tests/RoleResolution.lean           | 21 +++++++---
 src/verso-manual/VersoManual/Index.lean       | 41 ++++++++++++++++++-
 src/verso/Verso/Doc/Elab.lean                 |  8 +++-
 test-projects/custom-genre/SimplePage.lean    | 39 +++++++++++++++++-
 .../custom-genre/SimplePage/Demo.lean         |  2 -
 .../PackageManual/DocFeatures.lean            |  2 -
 test-projects/textbook/DemoTextbook.lean      |  4 --
 10 files changed, 120 insertions(+), 19 deletions(-)
 create mode 100644 doc/UsersGuide/Releases/v4_29_0.lean

diff --git a/doc/UsersGuide/Releases.lean b/doc/UsersGuide/Releases.lean
index 652b9a9d..0d7ae5f2 100644
--- a/doc/UsersGuide/Releases.lean
+++ b/doc/UsersGuide/Releases.lean
@@ -6,6 +6,7 @@ Author: Emilio J. Gallego Arias
 
 import VersoManual
 
+import UsersGuide.Releases.«v4_29_0»
 import UsersGuide.Releases.«v4_28_0»
 
 open Verso Genre Manual
@@ -26,4 +27,5 @@ Verso versioning follows Lean's.
 This means that we release a new version for each Lean release, usually once per month.
 In particular, note that Verso doesn't follow the [semantic versioning model](https://semver.org/).
 
+{include 0 UsersGuide.Releases.«v4_29_0»}
 {include 0 UsersGuide.Releases.«v4_28_0»}
diff --git a/doc/UsersGuide/Releases/v4_28_0.lean b/doc/UsersGuide/Releases/v4_28_0.lean
index fc9704d7..0a7097af 100644
--- a/doc/UsersGuide/Releases/v4_28_0.lean
+++ b/doc/UsersGuide/Releases/v4_28_0.lean
@@ -11,7 +11,7 @@ open Verso.Genre
 -- To allow ```` below
 set_option linter.verso.markup.codeBlock false
 
-#doc (Manual) "Verso 4.28.0 (unreleased)" =>
+#doc (Manual) "Verso 4.28.0" =>
 %%%
 tag := "release-v4.28.0"
 file := "v4.28.0"
diff --git a/doc/UsersGuide/Releases/v4_29_0.lean b/doc/UsersGuide/Releases/v4_29_0.lean
new file mode 100644
index 00000000..401b3398
--- /dev/null
+++ b/doc/UsersGuide/Releases/v4_29_0.lean
@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Emilio J. Gallego Arias
+-/
+
+import VersoManual
+
+open Verso.Genre
+
+#doc (Manual) "Verso 4.29.0" =>
+%%%
+tag := "release-v4.29.0"
+file := "v4.29.0"
+%%%
+
+* Improve role resolution diagnostics with suggestions and actionable registration errors (@ejgallego, #763)
+* Register legacy inline APIs as roles for compatibility (`today`, `date`, `sectionRef`, `index`, `see`, `seeAlso`) (@ejgallego, #763)
diff --git a/src/tests/Tests/RoleResolution.lean b/src/tests/Tests/RoleResolution.lean
index 5b7aaf10..cd82a71a 100644
--- a/src/tests/Tests/RoleResolution.lean
+++ b/src/tests/Tests/RoleResolution.lean
@@ -59,7 +59,10 @@ error: Function `wrongType` was found but likely not a role.
 :::::::
 
 /--
-error: No registered role `registred`. Did you mean role `registered`?
+error: No registered role `registred`.
+
+Hint: Did you mean role `registered`?
+  registe̲red
 -/
 #guard_msgs in
 #docs (.none) roleCase4 "Case 4" :=
@@ -68,7 +71,7 @@ error: No registered role `registred`. Did you mean role `registered`?
 :::::::
 
 /--
-error: No registered role `nothereatallzzzz`. Available roles (showing 20 of 37): anchor, anchorError, anchorInfo, anchorName, anchorTerm, anchorWarning, blob, citehere, citep, citet, conv, deftech, draft, htmlSpan, inst, label, lean, leanCommand, leanInline, leanKw
+error: No registered role `nothereatallzzzz`. Available roles (showing 20 of 40): anchor, anchorError, anchorInfo, anchorName, anchorTerm, anchorWarning, blob, citehere, citep, citet, conv, deftech, draft, htmlSpan, index, inst, label, lean, leanCommand, leanInline
 -/
 #guard_msgs in
 #docs (.none) roleCase5 "Case 5" :=
@@ -103,7 +106,10 @@ error: Role function `manualUnregistered` was found but not registered as a role
 :::::::
 
 /--
-error: No registered role `manualRegistred`. Did you mean role `manualRegistered`?
+error: No registered role `manualRegistred`.
+
+Hint: Did you mean role `manualRegistered`?
+  manualRegiste̲red
 -/
 #guard_msgs in
 #docs (Manual) roleCase3 "Manual Case 3" :=
@@ -112,7 +118,7 @@ error: No registered role `manualRegistred`. Did you mean role `manualRegistered
 :::::::
 
 /--
-error: No registered role `manualNowhereNearZzzzz`. Available roles (showing 20 of 38): anchor, anchorError, anchorInfo, anchorName, anchorTerm, anchorWarning, blob, citehere, citep, citet, conv, deftech, draft, htmlSpan, inst, label, lean, leanCommand, leanInline, leanKw
+error: No registered role `manualNowhereNearZzzzz`. Available roles (showing 20 of 41): anchor, anchorError, anchorInfo, anchorName, anchorTerm, anchorWarning, blob, citehere, citep, citet, conv, deftech, draft, htmlSpan, index, inst, label, lean, leanCommand, leanInline
 -/
 #guard_msgs in
 #docs (Manual) roleCase4 "Manual Case 4" :=
@@ -149,7 +155,10 @@ error: Role function `blogUnregistered` was found but not registered as a role.
 :::::::
 
 /--
-error: No registered role `blogRegistred`. Did you mean role `blogRegistered`?
+error: No registered role `blogRegistred`.
+
+Hint: Did you mean role `blogRegistered`?
+  blogRegiste̲red
 -/
 #guard_msgs in
 #docs (Blog.Post) roleCase3 "Blog Case 3" :=
@@ -158,7 +167,7 @@ error: No registered role `blogRegistred`. Did you mean role `blogRegistered`?
 :::::::
 
 /--
-error: No registered role `blogNoCloseMatchZzzzz`. Available roles (showing 20 of 39): anchor, anchorError, anchorInfo, anchorName, anchorTerm, anchorWarning, blob, blogRegistered, citehere, citep, citet, conv, deftech, draft, htmlSpan, inst, label, lean, leanCommand, leanInline
+error: No registered role `blogNoCloseMatchZzzzz`. Available roles (showing 20 of 42): anchor, anchorError, anchorInfo, anchorName, anchorTerm, anchorWarning, blob, blogRegistered, citehere, citep, citet, conv, deftech, draft, htmlSpan, index, inst, label, lean, leanCommand
 -/
 #guard_msgs in
 #docs (Blog.Post) roleCase4 "Blog Case 4" :=
diff --git a/src/verso-manual/VersoManual/Index.lean b/src/verso-manual/VersoManual/Index.lean
index 55d87b4e..0850b8ae 100644
--- a/src/verso-manual/VersoManual/Index.lean
+++ b/src/verso-manual/VersoManual/Index.lean
@@ -10,6 +10,8 @@ import Std.Data.HashMap
 import Std.Data.HashSet
 
 import Verso.Doc.Elab
+public import Verso.Doc.Elab.Monad
+meta import Verso.Doc.Elab.Monad
 public import VersoManual.Basic
 import VersoManual.Html.SoftHyphenate
 import MultiVerso
@@ -19,7 +21,8 @@ public import Verso.Doc
 open Verso Genre Manual
 open Verso.Multi
 open Verso.Doc.Elab
-open Lean (ToJson FromJson)
+open Verso.ArgParse
+open Lean (ToJson FromJson quote)
 open Std (HashMap HashSet)
 
 namespace Verso.Genre.Manual.Index
@@ -184,6 +187,42 @@ def seeAlso (args : Array (Doc.Inline Manual)) (target : String) (subterm : Opti
   let data : Index.See := {source := .concat args, target := .text target, subTarget := subterm.map .text, also := true, index}
   Doc.Inline.other {Inline.see with data := ToJson.toJson data} #[]
 
+structure IndexArgs where
+  subterm : Option String
+  index : Option String
+
+structure SeeArgs where
+  target : String
+  subterm : Option String
+  index : Option String
+
+instance : FromArgs IndexArgs DocElabM where
+  fromArgs := IndexArgs.mk <$> .named `subterm .string true <*> .named `index .string true
+
+instance : FromArgs SeeArgs DocElabM where
+  fromArgs := SeeArgs.mk <$>
+    .positional `target .string <*>
+    .named `subterm .string true <*>
+    .named `index .string true
+
+@[role index]
+def indexRole : RoleExpanderOf IndexArgs
+  | {subterm, index}, args => do
+    let args ← args.mapM elabInline
+    ``(index #[$args,*] $(quote subterm) $(quote index))
+
+@[role see]
+def seeRole : RoleExpanderOf SeeArgs
+  | {target, subterm, index}, args => do
+    let args ← args.mapM elabInline
+    ``(see #[$args,*] $(quote target) $(quote subterm) $(quote index))
+
+@[role seeAlso]
+def seeAlsoRole : RoleExpanderOf SeeArgs
+  | {target, subterm, index}, args => do
+    let args ← args.mapM elabInline
+    ``(seeAlso #[$args,*] $(quote target) $(quote subterm) $(quote index))
+
 @[inline_extension see]
 def see.descr : InlineDescr where
   traverse _id data _contents := do
diff --git a/src/verso/Verso/Doc/Elab.lean b/src/verso/Verso/Doc/Elab.lean
index 4d1c9e01..721aa8e9 100644
--- a/src/verso/Verso/Doc/Elab.lean
+++ b/src/verso/Verso/Doc/Elab.lean
@@ -120,7 +120,7 @@ private meta def expanderDocHover (stx : Syntax) (what : String) (name : Name) (
   Hover.addCustomHover stx out
 
 private meta def roleSuggestionThreshold (input _candidate : String) : Nat :=
-  if input.length < 5 then 1 else if input.length < 10 then 2 else 3
+  if input.length < 3 then 1 else if input.length < 7 then 2 else 3
 
 private meta def shortRoleName (name : Name) : String :=
   match name with
@@ -171,7 +171,11 @@ private meta def throwUnknownRoleError (name : Ident) : DocElabM α := do
   let suggestions := roleSuggestions available requested
   match suggestions.toList with
   | (_, best) :: _ =>
-    throwErrorAt name m!"No registered role `{name.getId}`. Did you mean role `{best}`?"
+    let hint ← MessageData.hint
+      m!"Did you mean role `{best}`?"
+      #[{suggestion := .string best}]
+      (ref? := some name)
+    throwErrorAt name m!"No registered role `{name.getId}`.{hint}"
   | [] =>
     if available.isEmpty then
       throwErrorAt name m!"No registered role `{name.getId}`. No roles are currently registered."
diff --git a/test-projects/custom-genre/SimplePage.lean b/test-projects/custom-genre/SimplePage.lean
index f7495a31..adb02e63 100644
--- a/test-projects/custom-genre/SimplePage.lean
+++ b/test-projects/custom-genre/SimplePage.lean
@@ -12,7 +12,9 @@ genre as simply as possible.
 
 -/
 
-open Verso Doc
+open Verso Doc Elab
+open Verso.ArgParse
+open Lean (quote)
 
 namespace Tutorial
 
@@ -293,3 +295,38 @@ def today (_content : Array (Inline SimplePage)) : Inline SimplePage :=
 /-- Insert a particular date here -/
 def date (_content : Array (Inline SimplePage)) (year month day : Nat) : Inline SimplePage :=
   .other (.inl (.specific day month year)) #[]
+
+structure SectionRefArgs where
+  dest : String
+
+structure DateArgs where
+  year : Nat
+  month : Nat
+  day : Nat
+
+instance : FromArgs SectionRefArgs DocElabM where
+  fromArgs := SectionRefArgs.mk <$> .positional `dest .string
+
+instance : FromArgs DateArgs DocElabM where
+  fromArgs := DateArgs.mk <$>
+    .positional `year .nat <*>
+    .positional `month .nat <*>
+    .positional `day .nat
+
+@[role sectionRef]
+def sectionRefRole : RoleExpanderOf SectionRefArgs
+  | {dest}, content => do
+    let content ← content.mapM elabInline
+    ``(sectionRef #[$content,*] $(quote dest))
+
+@[role today]
+def todayRole : RoleExpanderOf Unit
+  | (), content => do
+    let content ← content.mapM elabInline
+    ``(today #[$content,*])
+
+@[role date]
+def dateRole : RoleExpanderOf DateArgs
+  | {year, month, day}, content => do
+    let content ← content.mapM elabInline
+    ``(date #[$content,*] $(quote year) $(quote month) $(quote day))
diff --git a/test-projects/custom-genre/SimplePage/Demo.lean b/test-projects/custom-genre/SimplePage/Demo.lean
index 76cf3993..b1539884 100644
--- a/test-projects/custom-genre/SimplePage/Demo.lean
+++ b/test-projects/custom-genre/SimplePage/Demo.lean
@@ -9,8 +9,6 @@ open Tutorial
 
 #doc (SimplePage) "An _Astounding_ Document" =>
 
--- NOTE(rfc-role-resolution): these role calls currently rely on the removed
--- fallback-to-function-application behavior and now fail during `lake build`.
 Today is {today}[]. This document was created on {date 2024 5 13}[].
 
 # One Section
diff --git a/test-projects/package-manual/PackageManual/DocFeatures.lean b/test-projects/package-manual/PackageManual/DocFeatures.lean
index 07b9c276..a23ebea0 100644
--- a/test-projects/package-manual/PackageManual/DocFeatures.lean
+++ b/test-projects/package-manual/PackageManual/DocFeatures.lean
@@ -34,8 +34,6 @@ The example project must depend on the same version of `subverso` that the docum
 Within the example project, examples are drawn from a module.
 Sometimes, the entire module is the example, while other cases use just some part of the module.
 To set a default module, use the option {option}`verso.exampleModule`.
--- NOTE(rfc-role-resolution): `{index}` below is currently a plain function,
--- not a registered role expander, and now fails under strict role resolution.
 When there is no default set, or to override it, the example code features all accept a keyword argument `module`.{index (subterm:="keyword argument")}[`module`]
 
 {optionDocs verso.exampleModule}
diff --git a/test-projects/textbook/DemoTextbook.lean b/test-projects/textbook/DemoTextbook.lean
index 695a15cb..7db15ebb 100644
--- a/test-projects/textbook/DemoTextbook.lean
+++ b/test-projects/textbook/DemoTextbook.lean
@@ -30,8 +30,6 @@ set_option pp.rawOnError true
 authors := ["David Thrane Christiansen"]
 %%%
 
--- NOTE(rfc-role-resolution): `{index}` here is currently a plain function,
--- not a registered role expander, and now fails under strict role resolution.
 {index}[example]
 Here's an example project showing how to build a certain kind of textbook with Verso.
 It's a good idea to read the document's source together with the rendered output, because it demonstrates how to use various features.
@@ -139,8 +137,6 @@ If incorrect hovers are appearing locally, then try disabling caching in your br
 
 # Using an Index
 
--- NOTE(rfc-role-resolution): all `{index}` uses in this section fail for the
--- same reason as above until they are migrated to registered roles.
 {index}[index]
 The index should contain an entry for “lorem ipsum”.
 {index}[lorem ipsum] foo

From 495f237b79b3163ac6750610fc8b20fadbd98b82 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <emilio@lean-fro.org>
Date: Tue, 24 Feb 2026 13:26:51 +0100
Subject: [PATCH 3/3] refine: cap unknown-role fallback hints to 5 closest
 entries

---
 src/tests/Tests/RoleResolution.lean | 27 +++++++++++++++++++---
 src/verso/Verso/Doc/Elab.lean       | 36 ++++++++++++++++++-----------
 2 files changed, 46 insertions(+), 17 deletions(-)

diff --git a/src/tests/Tests/RoleResolution.lean b/src/tests/Tests/RoleResolution.lean
index cd82a71a..e1d615b1 100644
--- a/src/tests/Tests/RoleResolution.lean
+++ b/src/tests/Tests/RoleResolution.lean
@@ -71,7 +71,14 @@ Hint: Did you mean role `registered`?
 :::::::
 
 /--
-error: No registered role `nothereatallzzzz`. Available roles (showing 20 of 40): anchor, anchorError, anchorInfo, anchorName, anchorTerm, anchorWarning, blob, citehere, citep, citet, conv, deftech, draft, htmlSpan, index, inst, label, lean, leanCommand, leanInline
+error: No registered role `nothereatallzzzz`.
+
+Hint: Closest registered roles:
+  • n̵o̵t̵h̵e̵r̵e̵a̵t̵a̵l̵l̵z̵z̵z̵z̵c̲i̲t̲e̲h̲e̲r̲e̲
+  • n̵o̵t̵h̵e̵r̵e̵a̵t̵a̵l̵l̵z̵z̵z̵z̵a̲n̲c̲h̲o̲r̲N̲a̲m̲e̲
+  • n̵o̵t̵h̵e̵r̵e̵a̵t̵a̵l̵l̵z̵z̵z̵z̵a̲n̲c̲h̲o̲r̲W̲a̲r̲n̲i̲n̲g̲
+  • n̵o̵t̵h̵e̵r̵e̵a̵t̵a̵l̵l̵z̵z̵z̵z̵c̲i̲t̲e̲t̲
+  • n̵o̵t̵h̵e̵r̵e̵a̵t̵a̵l̵l̵z̵z̵z̵z̵h̲t̲m̲l̲S̲p̲a̲n̲
 -/
 #guard_msgs in
 #docs (.none) roleCase5 "Case 5" :=
@@ -118,7 +125,14 @@ Hint: Did you mean role `manualRegistered`?
 :::::::
 
 /--
-error: No registered role `manualNowhereNearZzzzz`. Available roles (showing 20 of 41): anchor, anchorError, anchorInfo, anchorName, anchorTerm, anchorWarning, blob, citehere, citep, citet, conv, deftech, draft, htmlSpan, index, inst, label, lean, leanCommand, leanInline
+error: No registered role `manualNowhereNearZzzzz`.
+
+Hint: Closest registered roles:
+  • m̵a̵n̵u̵a̵l̵N̵o̵w̵h̵e̵r̵e̵N̵e̵a̵r̵Z̵z̵z̵z̵z̵m̲a̲n̲u̲a̲l̲R̲e̲g̲i̲s̲t̲e̲r̲e̲d̲
+  • m̵a̵n̵u̵a̵l̵N̵o̵w̵h̵e̵r̵e̵N̵e̵a̵r̵Z̵z̵z̵z̵z̵a̲n̲c̲h̲o̲r̲N̲a̲m̲e̲
+  • m̵a̵n̵u̵a̵l̵N̵o̵w̵h̵e̵r̵e̵N̵e̵a̵r̵Z̵z̵z̵z̵z̵a̲n̲c̲h̲o̲r̲T̲e̲r̲m̲
+  • m̵a̵n̵u̵a̵l̵N̵o̵w̵h̵e̵r̵e̵N̵e̵a̵r̵Z̵z̵z̵z̵z̵a̲n̲c̲h̲o̲r̲W̲a̲r̲n̲i̲n̲g̲
+  • m̵a̵n̵u̵a̵l̵N̵o̵w̵h̵e̵r̵e̵N̵e̵a̵r̵Z̵z̵z̵z̵z̵m̲o̲d̲u̲l̲e̲N̲a̲m̲e̲
 -/
 #guard_msgs in
 #docs (Manual) roleCase4 "Manual Case 4" :=
@@ -167,7 +181,14 @@ Hint: Did you mean role `blogRegistered`?
 :::::::
 
 /--
-error: No registered role `blogNoCloseMatchZzzzz`. Available roles (showing 20 of 42): anchor, anchorError, anchorInfo, anchorName, anchorTerm, anchorWarning, blob, blogRegistered, citehere, citep, citet, conv, deftech, draft, htmlSpan, index, inst, label, lean, leanCommand
+error: No registered role `blogNoCloseMatchZzzzz`.
+
+Hint: Closest registered roles:
+  • b̵l̵o̵g̵N̵o̵C̵l̵o̵s̵e̵M̵a̵t̵c̵h̵Z̵z̵z̵z̵z̵b̲l̲o̲g̲R̲e̲g̲i̲s̲t̲e̲r̲e̲d̲
+  • b̵l̵o̵g̵N̵o̵C̵l̵o̵s̵e̵M̵a̵t̵c̵h̵Z̵z̵z̵z̵z̵l̲e̲a̲n̲C̲o̲m̲m̲a̲n̲d̲
+  • b̵l̵o̵g̵N̵o̵C̵l̵o̵s̵e̵M̵a̵t̵c̵h̵Z̵z̵z̵z̵z̵m̲o̲d̲u̲l̲e̲N̲a̲m̲e̲
+  • b̵l̵o̵g̵N̵o̵C̵l̵o̵s̵e̵M̵a̵t̵c̵h̵Z̵z̵z̵z̵z̵m̲o̲d̲u̲l̲e̲O̲u̲t̲
+  • b̵l̵o̵g̵N̵o̵C̵l̵o̵s̵e̵M̵a̵t̵c̵h̵Z̵z̵z̵z̵z̵m̲o̲d̲u̲l̲e̲W̲a̲r̲n̲i̲n̲g̲
 -/
 #guard_msgs in
 #docs (Blog.Post) roleCase4 "Blog Case 4" :=
diff --git a/src/verso/Verso/Doc/Elab.lean b/src/verso/Verso/Doc/Elab.lean
index 721aa8e9..218d7db5 100644
--- a/src/verso/Verso/Doc/Elab.lean
+++ b/src/verso/Verso/Doc/Elab.lean
@@ -136,6 +136,14 @@ private meta def roleSuggestions (candidates : Array (Name × String)) (input :
   let close := close.qsort (fun x y => x.2 < y.2 || (x.2 == y.2 && x.1.2 < y.1.2))
   close.take count |>.map (·.1)
 
+private meta def closestRoleNames (candidates : Array (Name × String)) (input : String) (count : Nat := 5) : Array (Name × String) :=
+  let ranked := candidates.filterMap fun candidate =>
+    let cand := candidate.2
+    let limit := max cand.length input.length
+    EditDistance.levenshtein cand input limit <&> (candidate, ·)
+  let ranked := ranked.qsort (fun x y => x.2 < y.2 || (x.2 == y.2 && x.1.2 < y.1.2))
+  ranked.take count |>.map (·.1)
+
 private meta def availableRoleNames : DocElabM (Array Name) := do
   return (← registeredRoleNames).qsort (·.toString < ·.toString)
 
@@ -170,27 +178,27 @@ private meta def throwUnknownRoleError (name : Ident) : DocElabM α := do
   let available ← availableRoleDisplayNames
   let suggestions := roleSuggestions available requested
   match suggestions.toList with
-  | (_, best) :: _ =>
+  | _ :: _ =>
+    let best := suggestions[0]!.2
+    let hintSuggestions := suggestions.map fun (_, roleName) =>
+      ({suggestion := .string roleName} : Lean.Meta.Hint.Suggestion)
     let hint ← MessageData.hint
       m!"Did you mean role `{best}`?"
-      #[{suggestion := .string best}]
-      (ref? := some name)
+      hintSuggestions
+      (ref? := some name) (forceList := suggestions.size > 1)
     throwErrorAt name m!"No registered role `{name.getId}`.{hint}"
   | [] =>
     if available.isEmpty then
       throwErrorAt name m!"No registered role `{name.getId}`. No roles are currently registered."
     else
-      let mut uniqueNames := #[]
-      for (_, n) in available do
-        unless uniqueNames.contains n do
-          uniqueNames := uniqueNames.push n
-      let sortedNames := uniqueNames.qsort (· < ·)
-      let shown := sortedNames.take 20
-      let suffix :=
-        if sortedNames.size > shown.size then
-          s!" (showing {shown.size} of {sortedNames.size})"
-        else ""
-      throwErrorAt name m!"No registered role `{name.getId}`. Available roles{suffix}: {String.intercalate ", " shown.toList}"
+      let shown := closestRoleNames available requested
+      let hintSuggestions := shown.map fun (_, roleName) =>
+        ({suggestion := .string roleName} : Lean.Meta.Hint.Suggestion)
+      let hint ← MessageData.hint
+        m!"Closest registered roles:"
+        hintSuggestions
+        (ref? := some name) (forceList := true)
+      throwErrorAt name m!"No registered role `{name.getId}`.{hint}"
 
 private meta def resolveRoleName? (name : Ident) : DocElabM (Option Name) := do
   match (← observing (realizeGlobalConstWithInfos name)) with