Class is treated as a mere structure, not a class, in its verso docstring

[datokrat]

Prerequisites

• [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
• [x] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
• [x] Test your test case against the latest nightly release, for example on https://live.lean-lang.org/#project=lean-nightly (You can also use the settings there to switch to “Lean nightly”)

Description

In the docstring of a class declaration, the class cannot be used as a class, only as a mere structure.

For example, functions cannot have instance parameters typed as the class in question, and using the class's instance projections in Lean code fails because it (allegedly in vain) expects a type class instance.

Steps to Reproduce

Run this:

set_option doc.verso true

/--
{name}`X` is a type class and it can be used as follows:

```lean
instance : X := ⟨0⟩

/--
error: invalid binder annotation, type is not a class instance
  X

Note: Use the command `set_option checkBinderAnnotations false` to disable the check
-/
example [X] : Unit := ()

/--
error: type class instance expected
  X
-/
example : Nat := X.x
```
-/
class X where
  x : Nat

Expected behavior:

No error; X should be considered a type class, so that it can be used like any other type class.

Actual behavior:

X is treated as a mere structure, perhaps because it is only registered as a class after verso docstrings are elaborated.

There is a workaround: Set doc.verso to false and write docs_to_verso X at the end of the file.

Versions

Lean 4.27.0-nightly-2025-12-12
Target: x86_64-unknown-linux-gnu

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.