Inaccessible name bug

Stream: lean4

[Marcus Rossel]

I think there's a bug when displaying inaccessible names (at least in VS Code on nightly 2022-04-28).
In the following example:

def f : Nat → Option Nat := λ _ => sorry
theorem t : (f m₁ = some n) → (f m₂ = some n) → True := sorry

example : (∃ n₁, f m₁ = some n₁) → (∃ n₂, f m₂ = some n₂) → True := by
  intro ⟨_, h₁⟩ ⟨_, h₂⟩
  exact t h₁ h₂

... the goal state after the intro is:

m₁ m₂ w✝¹ : Nat
h₁ : f m₁ = some w✝¹
w✝ : Nat
h₂ : f m₂ = some w✝
⊢ True

That is, we have inaccessible names w✝ and w✝¹.
When trying to (incorrectly) use theorem t in the next line, Lean complains with:

application type mismatch
  t h₁ h₂
argument
  h₂
has type
  f m₂ = some w✝ : Prop
but is expected to have type
  f m₂ = some w✝ : Prop

... which is very confusing. If we give w✝ and w✝¹ actual names, we can see that the ¹ in w✝¹ simply didn't carry over into the error message:

example : (∃ n₁, f m₁ = some n₁) → (∃ n₂, f m₂ = some n₂) → True := by
  intro ⟨x, h₁⟩ ⟨y, h₂⟩
  exact t h₁ h₂

-- Shows:
-- application type mismatch
--   t h₁ h₂
-- argument
--   h₂
-- has type
--   f m₂ = some y : Prop
-- but is expected to have type
--   f m₂ = some x : Prop

[Leonardo de Moura]

This bug has been fixed
https://github.com/leanprover/lean4/commit/fe00dd8f292ed280684403b4cf6444a83f1b81bd

[Leonardo de Moura]

Relevant thread for more details: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20Problems.20with.20the.20Dependent.20cartesian.20product.20example/near/280857320