extends and namespaces

Stream: lean4

[Michael Jam]

This fails:

namespace A
class Z (α : Type)
namespace SpecificA
class Z (α : Type) extends A.Z α
namespace VerySpecificA
class Z (α : Type) extends SpecificA.Z α
end VerySpecificA
end SpecificA
end A

The reason is that the first extends creates a field called "toZ" to convert to its parent class, and the second extends wants to create a similar field with the exact same name "toZ".

To fix that I can rename the classes with specific names. But that kinds of defeats the idea of using a namespace to recycle names ...

Another idea would be for lean to generate the "to" fields with the full path explicit in their names for example: the first one "toA_Z" and the second one "toA_SpecificA_Z"
Is that a good or bad idea?

[Michael Jam]

A more compact version:

class Z (α : Type)
class Specific.Z (α : Type) extends Z α
class Specific.EvenMore.Z (α : Type) extends Specific.Z α

[Leonardo de Moura]

This issue has been fixed a few days ago. Could you please try the current nightly build?
https://github.com/leanprover/lean4/commit/74bd537465b650eb5796beda971619dcba4824e9