Non-class instances don't fail

Stream: lean4

[Arthur Adjedj]

inductive Foo where | mk

instance : Foo := ⟨⟩ --doesn't throw any warning or error, despite `Foo` not being a class

#synth Foo --obviously doesn't work

Is this the expected behaviour ? Since there already is a check to see whether instance arguments (stuff written in [...] brackets) are actually classes, why not also use that check on the type of instances being declared ?

[Kim Morrison]

Seems pretty reasonable. Perhaps this could just be a syntax linter to avoid having to touch instance itself?

[Patrick Massot]

There is already a linter for this.

[Arthur Adjedj]

I am a bit surprised that this isn't an error by default, in the same way that incorrect binders are (an error which can be turned off using set_option checkBinderAnnotations false, but an error nonetheless). I feel like it would make sense for this to also be treated as an error ? The reason why I found this is because some discord user discussing Lean on a functional programming server was defining what should be defs as instances everywhere, and Lean was not complaining in any way.

[Kim Morrison]

I'm afk, but if it is a syntax linter we should move it up to lean (happy to review a PR!). If it's an environment linter it will have to wait for the infrastructure to start moving.

[Patrick Massot]

It is an environment linter.

[Arthur Adjedj]

Perhaps it could be implemented as a check inside the instance's elaborator, and would throw an error instead of a linter warning ? For retro-compatibility purposes, such an error could be turned off with an option similar to checkBinderAnnotations ? If such a PR would be welcome, I could find time to work on this.

[Kim Morrison]

I'm hesitant to greenlight since we're keen to leave everything about typeclass inference alone for a while.

Hence my suggestion that a syntax linter would be a better approach for now.

But I'd happily defer to @Kyle Miller here if they believe an elaboration change could be sufficiently non-invasive.

[Kyle Miller]

I think this should be an error. The actual issue is in the instance attribute, which has no checks. Here's a PR: lean4#4739

[Kyle Miller]

This turns out to cause just one mathlib build failure. In Mathlib.SetTheory.Lists there's a mutually recursive instance, and it looks like some intermediate object is given the instance attribute:

error: ././././Mathlib/SetTheory/Lists.lean:382:2: type class instance expected
  {α : Type u_1} →
    [inst : DecidableEq α] →
      (x : (_ : Lists α) ×' Lists α ⊕' (_ : Lists' α true) ×' Lists' α true ⊕' (_ : Lists α) ×' Lists' α true) →
        PSum.casesOn x (fun _x ↦ Decidable (_x.1 ~ _x.2)) fun _x ↦
          PSum.casesOn _x (fun _x ↦ Decidable (_x.1 ⊆ _x.2)) fun _x ↦ Decidable (_x.1 ∈ _x.2)

I'll try to debug this sometime this week, but if I don't figure it out I might turn these into defs and add the instance attributes immediately after...