Showing hygienic binder names

Stream: lean4

[Parth Shastri]

In the following example, both x and l are displayed identically in the type of Foo.mk, even with pp.all set to true.

inductive Foo
  | mk : List.length l = nat_lit 3 → Foo

set_option pp.all true in
#print Foo.mk
-- constructor Foo.mk.{u_1} : {x : Type u_1} → {l : List.{u_1} x} → @Eq.{1} Nat (@List.length.{u_1} x l) 3 → Foo.{u_1}

However, x was introduced hygienically and as such cannot be used as an explicit argument name:

#check Foo.mk (l := [1, 2, 3]) rfl
-- Foo.mk (_ : List.length [1, 2, 3] = List.length [1, 2, 3]) : Foo
#check Foo.mk (x := Nat) (l := [1, 2, 3]) rfl
-- error: invalid argument name 'x' for function 'Foo.mk'

Is there any way to display the type of Foo.mk that shows the hygiene information e.g. displaying x as x✝?

[Parth Shastri]

For a less contrived example, this behavior appears when the name of instance arguments is not specified:

set_option pp.all true in
#print Option.get!
-- def Option.get!.{u} : {α : Type u} → [inst : Inhabited.{u + 1} α] → Option.{u} α → α := ...

#check @Option.get! (α := Nat)
-- @Option.get! Nat : [inst : Inhabited Nat] → Option Nat → Nat
#check @Option.get! (α := Nat) (inst := instInhabitedNat)
-- invalid argument name 'inst' for function 'Option.get!'

In other words, from how the type is displayed, it is unclear whether or not the argument name can actually be used.

[Sebastian Ullrich]

I think this is another instance of https://github.com/leanprover/lean4/issues/375