Unused variable linter false positive

[jthulhu]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The linter "unused variables" has a false positive, which, additionally, is reported at the wrong location.

Context

There is no particular context for this issue, here is the Zulip thread where it was reported.

Steps to Reproduce

inductive Foo {α : Type} : α → Type where
 | bar (x : α) : Foo x

def Foo.baz {α : Type} (y : α) : Foo y → Foo y
 | bar _ => bar _

Expected behavior: Nothing is reported in Foo.baz, the both variables bound α and y are used.

Actual behavior: The linter triggers, are reports unused variable `y` , with the reported location being the catch all pattern in the baz branch.

Versions

This has been checked with Lean nightly on the online version of Lean. On my computer, I'm using Lean 4.10.0-rc1, under NixOS unstable.

Impact

This is a very minor issue.

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[Kha]

duplicate of #2830