Auto-generated instance names do not inherit macro scopes

[Vtec234]

Description

Suppose that the following metaprogram is executed in two different modules A.lean and B.lean, and that C.lean then imports both modules.

import Lean
open Lean Elab Command

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

The duplication of the name Foo is fine and does not cause a clash thanks to macro hygiene which turns it into something like `[email protected]._hyg.7 and `[email protected]._hyg.7 in the respective module (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, without macro scopes, in both cases. This causes an error on importing both into C.lean.

According to @Kha, this is not the desired behaviour and macro scopes should be preserved in the autogenerated name somehow. See also Zulip.

In practice, this issue arises in the deriving handler for Server.RpcEncodable.

Steps to Reproduce

1. Create three modules as described above.

Expected behavior: Hygiene ensures that no names clash.

Actual behavior: We get a duplicate name error.

Reproduces how often: 100%

Versions

nightly-2023-01-14