`linter.unusedVariables` prevents using named arguments with implicit `match`es

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

The unusedVariables linter encourages the user to make changes that break downstream code that uses the named argument syntax ( (name := _) ).

Steps to Reproduce

Run the following:

theorem zero_lt_length_of_ne_nil :
    ∀ (l : List α) (h : l ≠ []), 0 < l.length
  | _ :: _, _ => Nat.zero_lt_succ _

#check zero_lt_length_of_ne_nil (l := [1]) (h := by simp)

Expected behavior: No lint errors are reported, as h is part of the public API of zero_lt_length_of_ne_nil

Actual behavior: unused variable 'h'. The linter error cannot be satisfied without breaking the #check: if you replace h with _h, then the #check breaks.

Versions

"4.5.0-rc1" (web editor)

Impact

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

Start with the minimal Lean reproduction in the issue and inspect the unusedVariables linter's handling of the implicit match. Use the theorem and its named-argument #check as the regression case. Done means the public argument h no longer produces a lint error while the named-argument check continues to work.