Instances of Non-classes?

Stream: lean4

[Mac]

Consider the following:

def addComm {T : Type _} [Add T] (a b : T)
  := a + b = b + a

def inferAddComm {T : Type _} [Add T] {a b : T}
  [i : addComm a b] := i

instance iAddNatComm {a b : Nat} : addComm a b
  := Nat.add_comm (n := a) (m := b)

-- This errors
theorem addNatCommZero (a : Nat) : a + 0 = 0 + a
  := inferAddComm
/-
type class instance expected
  addComm a 0
-/

Why does Lean allow you to define instances and specify synthesis binders for things other than type classes if they don't work? I would have expected Lean to error out on [i : addComm a b] and instance ... : addComm a b and inform me that they are invalid because addComm is not a type class. Or is there something I am missing?

[Kevin Buzzard]

In Lean 3 class and instance are just attributes that you can tag any definition with, and you can remove those tags too, so I guess it would be quite complicated to do what you're suggesting

[Mac]

I know that was true in Lean 3, but I'm pretty sure that's not true any more in Lean 4. If I remember correctly from the mathlib porting discussion, you can't tag defs with class anymore. A structure and def are entirely different things now I believe.

[Yakov Pechersky]

But can you still tag def with instance?

[Yakov Pechersky]

like an local attribute [instance] ...