Incorrect unused variable warning in lambda with pattern match and type signature

[mniip]

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

Incorrect "unused variable" warnings are reported around lambdas with pattern matches and explicit type annotations. See example below.

Context

Steps to Reproduce

#check λα (p : α → Prop) (⟨x, _⟩ : {a // p a}) => x
--         ^                             ^ ^
--         1                             2 3

Expected behavior: No unused variable warnings.

Actual behavior: Lean reports 3 unused variable warnings at the indicated locations:

• Lean claims p at location 1 is unused, even though though 2 is its use.
• Lean claims p at location 2 and a at location 3 are unused, even though these are not the variables' binding sites.

Versions

4.13.0

Additional Information

The "2" warning goes away if we use p in the body of the lambda:

#check λα (p : α → Prop) (⟨x, _⟩ : {a // p a}) => (x, p)
--         ^                             ^ ^
--         1                             2 3

as if Lean believes 2 is p's binding site which in turn shadows the p bound at 1.

The problem goes away if matching is moved out of the lambda:

#check λα (p : α → Prop) (x : {a // p a}) => match x with | ⟨x, _⟩ => x

The use of (Subtype.mk _ _) versus ⟨_, _⟩ makes no difference.

Impact

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

[digama0]

• Lean claims p at location 2 and a at location 3 are unused, even though these are not the variables' binding sites.

This behavior is indicative of an auto implicit, which has its definition site set to the first use if the variable.

[Kha]

This is a bug in the match compiler:

lean4/src/Lean/Elab/Match.lean

Lines 648 to 649 in 6e60d13

	/- If `p` is a free variable and we are not inside of an "inaccessible" pattern, this `p` is a binder. -/
	mkTermInfo Name.anonymous stx p (isBinder := p.isFVar && !(← read))