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

[eric-wieser]

Prerequisites

• [x] 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 :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

[PatrickMassot]

It would be nice to have a more precise linter, but honestly I feel the issue in the given example is really wanting to save a couple of characters. You could write

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

and have your named assumption and no linter complain.

[eric-wieser]

Indeed, the error goes away if you write the theorem in that style; but I think this implicit match style is intended to be encouraged. Perhaps I should have given a better example, to make it clear that this isn't just a problem with theorems:

-- linter complains about `msbs` and `lsb`
def concatBit : ∀ (msbs : List Bool) (lsb : Bool), List Bool
  | [], lsb => [lsb]
  --                                       but these names are needed here!
  | msb :: msbs, lsb => [msb] ++ concatBit (msbs := msbs) (lsb := lsb)

Obviously this is a stupid implementation, but here the intent of this contrived example to have a public API with named data arguments, and the linter is encouraging the user to mangle their names and create a worse API.

[Kha]

If we had attributes on parameters, it could be (@[no_lint] h : ...)

[eric-wieser]

That would certainly be a nice feature, but ideally it wouldn't be necessary for this specific case.

[nomeata]

I'd agree with Eric that such a variable binding isn't lint. The parameter names are in some sense part of the type and affect the public API, so at least for exported types they can't really be considered “unused”

[eric-wieser]

Here's a slightly more tricky example: should this x be considered unused? Again, the proof breaks if you only rename the one that is underlined:

theorem foo (h : ∀ (x : Nat), True) : True := h (x := 1)

[eric-wieser]

Here's a half-baked proposal that I think would fix this: the linter should only run on lambda Exprs not on forall Exprs.

[nomeata]

It doesn't seem much different? h : ∀ (x : Nat), True) and h : ∀ (_ : Nat), True) are not interchangeable, and the x name clearly is used somewhere in the code. In my understanding it's a linter for unused names, not for unused parameters (in the sense that the Nat isn't used in True).

[eric-wieser]

The key difference is that in (h : ∀ (x : Nat), True), the name h is part of the public API, but the name x is effectively an implementation detail that only matters within the scope of the current declaration. Perhaps that's a distinction we don't care about.

[digama0]

Unfortunately almost any binder can end up in downstream code, there is not really a clear boundary for what is accessible. For example:

theorem foo (h : ∀ (x : Nat), True) : True := trivial

example : True := by
  suffices _ from
    have _ := foo (h := this)
    this (x := 1)
  exact fun _ => trivial

However I think it is reasonable to treat this as an edge case and use the heuristic that variables that appear as direct arguments to the function (i.e. the names of arguments in the forall telescope of the type of the constant) are considered public and others are not.

[nomeata]

How important is it to lint unused forall'ed parameters in practice? I.e. how bad would it be to simply not lint there, how many bugs would be prevented?

(Even for completely “unused” parameters, the name may be useful for readability.)

[eric-wieser]

On second thoughts, I think that heuristic is wrong; it would make ∀ (x : Nat), True lint-free but not ∃ (x : Nat), True.

Perhaps a better heuristic is "do not apply unusedVariables in either forall, or lambdas whose codomain is a Type".

[nomeata]

Not sure its wrong; for ∃ (x : Nat), True, how can that be used in a way that the x matters?

[eric-wieser]

I guess what I mean is that it feels morally analogous to ∀ (x : Nat), True (to a mathematician), and should therefore be expected to follow the same linting rules; though you're right that the x doesn't actually matter in the same way.

[nomeata]

A pedantic language designer might point out that it’s not very principled to use the same name for “internal” use (the one the linter warns about) and “external” use (named arguments), and if that was separate we wouldn’t have this discussion. But such a language design would probably be quite unwieldy and impractical, and anyways we have what we have, so these rough edges around “what is unused” we will have to deal with :-)

[digama0]

A pedantic language designer might point out that it’s not very principled to use the same name for “internal” use (the one the linter warns about) and “external” use (named arguments), and if that was separate we wouldn’t have this discussion. But such a language design would probably be quite unwieldy and impractical,

This is Swift FYI