appUnexpander pitfall

Stream: lean4

[pcpthm]

When I declare an appUnexpander involving an identifier that is not in the root namespace,
and then I change the namespace, the unexpander is not applied anymore.

namespace Test

def Special (α : Type u) := α
def special : Special Nat := (1 : Nat)

@[appUnexpander Test.Special] private def unexpander : Lean.PrettyPrinter.Unexpander
| `(Special $x) => `($x)
| _ => throw ()

-- The unexpander is applied.
-- `special : Nat`
#check special

end Test

-- The unexpander is not applied.
-- Test.special : Test.Special Nat
#check Test.special

-- Workaround: don't match against the identifier
@[appUnexpander Test.Special] private def unexpander : Lean.PrettyPrinter.Unexpander
| `($_Special $x) => `($x)
| _ => throw ()

I think this is because the quotation matching inside my unexpander definition is failing.
I could work around this issue by not matching against the identifier like the workaround above,
but I think this is confusing for users.
Could this situation be improved somehow?

[Sebastian Ullrich]

I'm afraid not. A purely syntactic match can only compare identifiers syntactically, or not at all. There is no magic bullet.

[Mac]

Sebastian Ullrich said:

I'm afraid not. A purely syntactic match can only compare identifiers syntactically, or not at all. There is no magic bullet.

Why not fully qualify names before running unexpanders? That way unexpanders could always target the fully qualified names to work. To make name output still pretty, you could then unqualify the names (as possible) after running the unexpanders.