Code action PANIC at Lean.Name.getString!

Stream: mathlib4

[Trebor Huang]

MWE:

import MathLib.Tactic

inductive TpVar : Nat → Type where
| zero : TpVar (m+1)
| succ : TpVar m → TpVar (m+1)

inductive Tp : Nat → Type where
| Var : TpVar m → Tp m
| Pi : Tp (m+1) → Tp m
| Fun : Tp m → Tp m → Tp m

theorem test (X : Tp n) : True := by
  induction X

Clicking on "generate explicit pattern matching", VSCode shows an error

PANIC at Lean.Name.getString! Lean.Data.Name:22:15: unreachable code has been reached

while generating the code

  induction X with
  | Var m _ => sorry
  | Pi m _ _ => sorry
  | Fun m _ _ _ _ => sorry

which contains too many underscores. Is it a problem with implicit variables?

[Trebor Huang]

I'm using Lean (version 4.0.0-nightly-2023-08-29, commit 4a41e7eb5368, Release), just updated mathlib, and OS X (M1 chip) if that's relevant.

[Mario Carneiro]

fixed in std4@dd3a248