Confusion about classes

Stream: lean4

[Kenny Lau]

class Foo (M : Type)

class Bar (M : Type)

/-
cannot find synthesization order for instance @Qux.toBar with type
  {M : Type} → (extra : (M → Prop) → Prop) → [self : Qux M extra] → Bar M
all remaining arguments have metavariables:
  Qux M ?extra
-/
class Qux (M : Type) (extra : (M → Prop) → Prop) extends Foo M, Bar M

-- These succeed!
class Qux' (M : Type) (extra : (M → Prop) → Prop) extends Foo M
class Qux'' (M : Type) (extra : (M → Prop) → Prop) extends Bar M
class Qux''' (M : Type) (extra : (M → Prop) → Prop) extends Qux' M extra, Qux'' M extra

Why does Lean complain about Qux, but not the following two (which seemingly do the same thing when combined); and especially the last one which does exactly the same?

[Eric Wieser]

Relatedly:

structure Foo (M : Type)
structure Bar (M : Type)
structure Qux (M : Type) (extra : (M → Prop) → Prop) extends Foo M, Bar M

#check Qux.mk -- why does this take foo but not bar?

[Aaron Liu]

Eric Wieser said:

Relatedly:

structure Foo (M : Type)
structure Bar (M : Type)
structure Qux (M : Type) (extra : (M → Prop) → Prop) extends Foo M, Bar M

#check Qux.mk -- why does this take foo but not bar?

Because you put Foo M first on you extends list

[Aaron Liu]

Same reason why with class AddCommMonoid (M : Type u) extends AddMonoid M, AddCommSemigroup M you have that AddCommMonoid.mk takes AddMonoid but not AddCommSemigroup

[Kyle Miller]

I think none of the examples should succeed @Kenny Lau. This is a known issue.

The differences in behavior is from which parent projections are represented as true projections.