Why doesn't defining this instance work?

Stream: new members

[Dan Abramov]

Consider this setup (extracted from Tao's book):

import Mathlib.Tactic

class SetTheory where
  Set : Type u -- Axiom 3.1
  Object : Type v -- Axiom 3.1
  set_to_object : Set ↪ Object -- Axiom 3.1
  singleton : Object → Set -- Axiom 3.4

export SetTheory (Set Object)

variable [SetTheory]

instance sets_are_objects : Coe Set Object where
  coe X := SetTheory.set_to_object X

theorem SetTheory.Set.coe_eq {X Y:Set} (h: (X: Object) = (Y: Object)) : X = Y :=
  SetTheory.set_to_object.inj' h

instance : Singleton Object Set where
  singleton := SetTheory.singleton

example (x: Object) : Set := {x}

My question is about how instances work in Lean.

Suppose I also want to support declaring nested Sets.

I can do it like this:

example (x: Object) : Set := {(({x}: Set): Object)}

But the two levels of conversion are annoying to write.

I was hoping adding a separate Singleton Set Set instance would help.

So I tried adding this to the end of the file:

instance : Singleton Set Set where
  singleton x := {(x: Object)}

example (s: Set) : Set := {s} -- works
example (x: Object) : Set := {({x}: Set)} -- doesn't

but as you can see, I still won't let me do {({x}: Set)}. Why?

overloaded, errors
  failed to synthesize
    Singleton Object SetTheory.Set

  Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

  invalid {...} notation, expected type is not of the form (C ...)

[Dan Abramov]

Full code:

import Mathlib.Tactic

class SetTheory where
  Set : Type u -- Axiom 3.1
  Object : Type v -- Axiom 3.1
  set_to_object : Set ↪ Object -- Axiom 3.1
  singleton : Object → Set -- Axiom 3.4

export SetTheory (Set Object)

variable [SetTheory]

instance sets_are_objects : Coe Set Object where
  coe X := SetTheory.set_to_object X

theorem SetTheory.Set.coe_eq {X Y:Set} (h: (X: Object) = (Y: Object)) : X = Y :=
  SetTheory.set_to_object.inj' h

instance : Singleton Object Set where
  singleton := SetTheory.singleton

example (x: Object) : Set := {x}

example (x: Object) : Set := {(({x}: Set): Object)}


instance : Singleton Set Set where
  singleton x := {(x: Object)}

example (s: Set) : Set := {s} -- works
example (x: Object) : Set := {({x}: Set)} -- doesn't

[Dan Abramov]

For a concrete use case, I was hoping I could make something like this read shorter.

lemma aux2 : ({(({x}: Set): Object)}: Set) = {(({y}: Set): Object), (({y, z}: Set): Object)} ↔ x = y ∧ x = z := by
  sorry

[Eric Wieser]

Lean is getting confused about your universes; [SetTheory.{u,v}] works

[Kenny Lau]

SetTheory is tricky to work with because it takes no arguments but contains universe parameters

[Kenny Lau]

I don't think we have any similar things in mathlib (but I can be wrong)

[Eric Wieser]

#eval Lean.toLevel.toNat

is the canonical example of "typeclass search is bad at universes"

[Eric Wieser]

It should be complaining that it couldn't work out the universe, rather than picking randomly

[Dan Abramov]

Oh wow. That's unexpected! I'm so glad I asked here.

Would it be correct for me to PR the change to the repo I took the code from? I.e. is it the author's fault that Lean wouldn't infer the universe correctly in this case? Or is it a bug that needs to be filed in Lean? Or is this undefined behavior?

[Dan Abramov]

I guess maybe the approach isn't very fruitful anyway because I'd have to declare each instance twice. So it's not just singleton but also membership, "insert", and so on.