Recursive Type Class Annotations

Prerequisites

Description

Consider the following artificial example:

class Test (α : Type) where
  foo {β : Type} [Test β] : String

In f Lean complains that Test is not a type class:

invalid binder annotation, type is not a class instance
  Test β

Note: Use the command `set_option checkBinderAnnotations false` to disable the check

While it does provide a way to work around this, I would expect that Lean does generally support a type class occurring in its own body in this fashion.

Context

Steps to Reproduce

Expected behavior: Code type checks

Actual behavior: Lean does not think that Test is a type class while it's still being defined

Versions

Lean 4.35.0-nightly-2026-08-22
Target: x86_64-unknown-linux-gnu Linux

Additional Information

Impact

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

Start with the minimal Test class and f example in the issue, then trace Lean's type-class and binder-annotation checking while the class body is being elaborated. Done means the example type checks without disabling checkBinderAnnotations, with the existing invalid-annotation behavior preserved elsewhere.