Should instance names inherit macro scopes?

Stream: lean4 dev

[Wojciech Nawrocki]

I ran into an unexpected issue with the RpcEncodable deriving handler and I am wondering as to the appropriate fix. What ends up happening is that two different modules A.lean and B.lean both run something like the following command

#eval (do
  let stx ← `(
    structure Foo where
      field : String
    deriving ToJson)
  elabCommand stx
  : CommandElabM Unit
)

The duplication of the name Foo is fine; macro hygiene turns it into something like `Foo._@.WidgetKit.Component.HtmlDisplay._hyg.7 (by the way, there doesn't seem to be a pp option to show this - is there? I had to resort to using Repr Syntax) so the struct names are not really duplicate. But the automatic instance name ends up being instToJsonFoo in both cases which clashes if we then import both A and B. So I am wondering, is the command itself buggy? I didn't think so as macro hygiene should ensure names don't clash. If it is not, should the automatic instance name pick up macro scopes and become `instToJsonFoo._@.Module._hyg.num ?

[Wojciech Nawrocki]

Making instance names accessible for accessibly-named types makes sense, but for this usecase it seems they should be hygienic.

[Sebastian Ullrich]

Ah, I forgot to answer here. The problematic part when generating a compound name is always how to merge the macro scopes of the different parts, but any solution to that would be preferable to removing all scopes, yeah.

[Wojciech Nawrocki]

@Sebastian Ullrich should I make a GH issue for this?

[Sebastian Ullrich]

Yes, please do!