`instance` command should reject instances of non-class types

[NicolasRouquette]

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• 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

The instance command (and @[instance] attribute) allows registering instances for types that are not classes. These instances compile without error but are unreachable by type class synthesis, making them useless. This should either produce an error or at least a warning.

Context

Running doc-gen4 on @kbuzzard 's ClassFieldTheory project tripped a panic that I discussed here: #lean4 > doc-gen4 panic with isClass? returning none for a structure @ 💬

Steps to Reproduce

1. Save the following as /tmp/test_instance_struct.lean

-- Test: Can we make an instance of a structure (not a class)?

-- Define a regular structure (not a class)
structure MyPredicate (n : Nat) : Prop where
  isPositive : n > 0

-- This compiles without error!
instance five_positive : MyPredicate 5 where
  isPositive := by decide

#check five_positive
#print five_positive

-- Also works with anonymous instance
instance : MyPredicate 10 where
  isPositive := by decide

-- Let's check if it's registered as an instance
#check (inferInstance : MyPredicate 5)  -- This will fail since MyPredicate is not a class!

2. Run lake env lean /tmp/test_instance_struct.lean

This produces an error:

five_positive : MyPredicate 5
theorem five_positive : MyPredicate 5 :=
{ isPositive := of_decide_eq_true (id (Eq.refl true)) }
/tmp/test_instance_struct.lean:19:8: error: type class instance expected
  MyPredicate 5

3. Even more extreme as observed by @Rob23oba on the chat:

instance : Nat := 0  -- Compiles!

Expected behavior:

The instance command in the examples should yield an exception, similar to the behavior of Lean.Meta.addDefaultInstance

  throwError "invalid default instance `{.ofConstName declName}`, it has type `({className} ...)`, but `{.ofConstName className}` is not a type class"

Actual behavior:

The instance command accepts creating an instance of a non-class type.

Versions

• Tested with Lean4 nightly (on 01/20/2026)
• leanprover/lean4:v4.27.0-rc1

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

This issue was discovered via a doc-gen4 panic [https://github.com/leanprover/doc-gen4/issues/348 In Mathlib4, where Continuous is defined as a structure (not a class): https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Defs/Basic.html#Continuous

When someone writes instance : Continuous f := ..., it compiles but:

• Is never used by type class synthesis
• Causes doc-gen4 to panic (it expects isClass? to return some)

Proposed fix

1. Add an isClass? check to addInstance:

def addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : MetaM Unit := do
  let c ← mkConstWithLevelParams declName
  let keys ← mkInstanceKey c
  let type ← inferType c
  forallTelescopeReducing type fun _ type => do
    match type.getAppFn with
    | .const className _ =>
      unless isClass (← getEnv) className do
        throwError "invalid instance `{.ofConstName declName}`, it has type `({className} ...)`, but `{.ofConstName className}` is not a type class"
    | _ => pure ()
  addGlobalInstance declName attrKind
  let projInfo? ← getProjectionFnInfo? declName
  let synthOrder ← computeSynthOrder c projInfo?
  instanceExtension.add { keys, val := c, priority := prio, globalName? := declName, attrKind, synthOrder } attrKind

2. Update the Lean4 reference documentation, 11.2 Instance Declarations

It should explicitly state that an instance must be of a class.

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