linter.unusedVariables false positive

[digama0]

example : ∀ (l : List α) n, l.get? n = some a → True
  | _::_, _+1, _ => trivial
  | _::_, 0, rfl => trivial
  --^ unused variable `a` [linter.unusedVariables]

[Kha]

Somehow the match elaborator is introducing this synthetic name using an original source info. I haven't looked more closely than that yet.