Failed to synthesize [clearly extant]

Stream: lean4

[Adalynn]

axiom Class: Type
axiom Class_mem_Class: Class -> Class -> Prop
instance: Membership Class Class := ⟨Class_mem_Class⟩
def M(x: Class) := ∃W: Class, x ∈ W
def Set := Σ'X: Class, M X
instance: Membership Set Class := ⟨λY: Class => λx: Set => x.1 ∈ Y⟩
axiom Extensionality(X: Class)(Y: Class): (∀z: Class, z∈X ↔ z∈Y)

So, I haven't touched Lean in about a year due to life circumstances, and have come to seem my beloved Lean 3 is deprecated.

Jokes aside, however, I keep seeming to run into errors similar to the one above, which results in an error that it "failed to synthesize Membership Class Class"... while there's clear an instance on the third line. Am I missing something here? IT's very possible, my Lean is rusty.

[Aaron Liu]

Because it finds the Membership Set Class instance and then stops searching

[Aaron Liu]

see docs#outParam

[Aaron Liu]

basically, a type implementing Membership can only hold one kind of thing "inside"

[Adalynn]

Ah crap, THAT'S probably why I remember doing some extremely funky things with notation and overrides I think. Thank you!