Renaming base classes doesn't help with overlaps

Stream: lean4

[Eric Wieser]

I was hoping the new support for naming base classes would allow this, but it doesn't seem to:

class Foo (α β) where foo : α → β → β

--                                     duplicate parent structure 'Foo', skipping
--                                     VVVVVVVVVVVVVVVVVVV
class DoubleFoo (α β) extends Foo α β, toSymmFoo : Foo β α where
  foo_eq (a : α) (b : β) : Foo.foo (Foo.foo b a) b = b
--                                  ^^^^^^^^^^^
--                                  Failed to synthesize Foo β α

[Eric Wieser]

Is this a case of "this feature isn't implemented yet but may be in future" or closer to "this would be very hard to even specify, so is not planned"?

[Robin Arnez]

The problem is that field names are expected to be unique. This is a class of course but still, if you have inst : DoubleFoo α β, what should inst.foo be?

[Aaron Liu]

Well it should be inst.toFoo : Foo α β and inst.toSymmFoo : Foo β α

[Robin Arnez]

Well I'm referring to this (I mean classes are basically structures):

structure Foo (α β) where
  foo : α → β → β

structure DoubleFoo (α β) extends Foo α β, toSymmFoo : Foo β α

variable (x : DoubleFoo α β)
#check x.foo

What should that be then? The first occurrence?
Also, extends usually merges parent projections of the same name, so not even this works (and is not expected to):

structure Foo (α β) where
  foo : α → β → β

structure SymmFoo (α β) where
  foo : α → β → β

/--
error: field type mismatch, field 'foo' from parent 'SymmFoo' has type
  β → α → α : Sort (imax ?u.700 ?u.701)
but is expected to have type
  α → β → β : Sort (imax ?u.701 ?u.700)
-/
#guard_msgs in
structure DoubleFoo (α β) extends Foo α β, SymmFoo β α

[Robin Arnez]

Really, extends is mostly for being able to write projections and merging projections of the same name so if you don't want these why not:

class Foo (α β) where
  foo : α → β → β

class DoubleFoo (α β) extends Foo α β where
  [toSymmFoo : Foo β α]
  foo_eq (a : α) (b : β) : Foo.foo (Foo.foo b a) b = b

attribute [instance] DoubleFoo.toSymmFoo

[Kenny Lau]

Aaron Liu said:

Well it should be inst.toFoo : Foo α β and inst.toSymmFoo : Foo β α

I initially thought the same, indeed I think what tripped me up is that I forgot the name you provide in extends is just the name of the projection function, e.g.

variable (α : Type)

class Foo : Type where
  fst : α
  snd : α

class Bar : Type where
  thd : α
  frt : α

class FooBar extends toFoo : Foo α, toBar : Bar α

variable [FooBar α]
#check (Foo.fst : α)
#check (FooBar.toFoo : Foo α)