Spurious linter warning "unused variable"

[PratherConid]

Steps to Reproduce

inductive Foo : (Nat → Nat) × Nat × Nat → Type
  | ctor (n : Nat) : Foo ⟨lctx, n, lctx n⟩

def bar (wft : Foo ⟨lctx, n, s⟩) : True :=
  match wft with
  | .ctor _ => True.intro -- unused variable `n` [linter.unusedVariables]

def bar' (wft : Foo ⟨lctx, n, s⟩) : True :=
  match n, wft with
  | _, .ctor _ => True.intro -- unused variable `s` [linter.unusedVariables]

Versions

Lean (version 4.3.0-rc1, commit baa4b68, Release)
Ubuntu 20.04.6 LTS (WSL)

[marcusrossel]

I think here's the same problem but a simpler example:

example : (x = y) → y = x
  | .refl _ => .refl _
        --^ unused variable 'x'