Automatically generated instance names in modules

Stream: lean4

[Christian Merten]

It seems that automatically generated instance names behave differently in modules:

module

class Foo where

instance : Foo where

/-- error: private declaration `instFoo` has already been declared -/
#guard_msgs in
instance : Foo where

The error message is gone when module is removed. The second instance is then named instFoo_1. Is this known?

[Sebastian Ullrich]

I don't think this has been logged as an issue yet but note that it is not new

private class Foo where

private instance : Foo where

/-- error: private declaration `instFoo` has already been declared -/
#guard_msgs in
private instance : Foo where