`deprecated` linter triggered by unrelated local variable names

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

The deprecated linter triggers on local variable names that are identical with the name of a deprecated definition when using the let syntax with pattern matching.

Steps to Reproduce

Use the following code to reproduce the issue:

@[deprecated True]
def test := True

#eval Id.run do
  let (test, _) := (0,0) -- `test` has been deprecated, use `True` instead
  test

Note that the variable test in the #eval command does not refer to the definition above at all.

Expected behavior: No linter warning since the global definition test is not used.

Actual behavior: I get a linter warning on the variable test in let (test, _) := (0,0).

Reproduces how often: 100%

Versions

Tested on Lean4 nightly-2023-02-24

Start by running the supplied Lean reproduction using the deprecated attribute, #eval, and a let pattern binding. Trace how the deprecated linter resolves names for local pattern variables; the issue names no source file or test path. Done means the local test binding produces no warning while actual uses of the deprecated definition remain diagnosed.