class diamond: field has already been declared

Stream: lean4

[Alexander Bentkamp]

Hello! I am trying to set up a type class diamond in Lean4:

class Foo (α : Type) where
foo : α

class FooBar1 (α : Type) extends Foo α where
bar1 : α

class FooBar2 (α : Type) extends Foo α where
bar2 : α

class FooBar12 (α : Type) extends FooBar1 α, FooBar2 α
-- field 'toFoo' from 'FooBar2' has already been declared

Shouldn't the two occurrences of foo just be merged into one here?

I am on lean4---nightly-2021-05-21.

[Alexander Bentkamp]

Ok, @Jeremy Avigad just told me what's going on here. Apparently this kind of type class diamond is computationally inefficent and has been disabled by default even in Lean3. It still exists in Lean3 when using set_option old_structure_cmd true.

In Lean4 a diamond can be constructed like this:

class Foo (α : Type) where
foo : α

class FooBar1 (α : Type) extends Foo α where
bar1 : α

class FooBar2 (α : Type) extends Foo α where
bar2 : α

class FooBar12 (α : Type) extends FooBar1 α where
bar2 : α

instance [FooBar12 α] : FooBar2 α := {
  bar2 := FooBar12.bar2
}