doc-gen4 panic with isClass? returning none for a structure

Stream: lean4

[Nicolas Rouquette]

@Henrik Böving I've encountered an issue with doc-gen4 and filed it at https://github.com/leanprover/doc-gen4/issues/348

The problem: doc-gen4 panics when processing instances that prove structure predicates (like Continuous) rather than class instances. The panic occurs because Meta.isClass? returns none for these declarations, and doc-gen4 currently expects it to always return some.

Example: In @Kevin Buzzard's ClassFieldTheory, there's an instance continuous_algebraMap_of_density : Continuous (algebraMap K L). Since Continuous is a structure (not a class), isClass? correctly returns none, triggering the panic.

I've created an MWE here: https://github.com/NicolasRouquette/ClassFieldTheory/blob/bug/doc-gen4/isClass/MWE_isClass.lean

Questions:

1. Is it expected that instance declarations can provide structure predicates (not just classes)? It seems valid in Lean but doc-gen4 didn't anticipate this case.

2. What would be the preferred fix? Some options:

   • Have ofDefinitionInfo return Option InstanceInfo and skip these cases
   • Generalize the instance handling to support both classes and structures
   • Log a warning instead of panicking

I'm happy to contribute a PR if there's guidance on the preferred approach. For now, this doesn't break my doc-verification-bridge pipeline since I catch the panic and continue, but it would be nice to handle it more gracefully.

Thanks!

[Henrik Böving]

To the best of my understanding it is illegal to have instances for non-class types. So this might be worth an issue in core instead?

[Kevin Buzzard]

Yeah that should definitely not be an instance! Maybe some linter should have caught this?

[Robin Arnez]

There's literally no error what

instance : Nat := 0

Is there any reason why you'd ever want to allow non-class instance declarations?
Also, huh?

attribute [class] Classical.choice

[Nicolas Rouquette]

Thanks everyone for the helpful discussion!

Based on the insights shared here — particularly @Henrik Böving's observation that instances for non-class types should be illegal, @Kevin Buzzard 's confirmation that the Continuous instance shouldn't have been an instance in the first place, and @Robin Arnez's surprising discovery that even instance : Nat := 0 compiles — I've filed a GitHub issue: https://github.com/leanprover/lean4/issues/12075

The root cause is that addInstance doesn't check whether the target type is a class before registering the instance. Interestingly, addDefaultInstance in the same file does have this check.

For now, the doc-gen4 workaround I'm using is to catch the panic and continue, but having Lean reject these instances at definition time would be the proper fix.