a linter bug

Stream: general

[fonqL]

Linter can't properly handle the for syntax with hypothesis.

def f [Monad m]: α -> m Unit
| _ => pure ()

/--
warning: unused variable `xs`
note: this linter can be disabled with `set_option linter.unusedVariables false`
-/
#guard_msgs in
def find (xs : List α) : Option α := do
  for _h: x in xs do
    f x
  none

[Jon Eugster]

quick sanity check, does it also complain when you actually use x in something nontrivial? I'm not sure that f x counts as using as it is just pure ()?

[fonqL]

yes.

/--
warning: unused variable `xs`
note: this linter can be disabled with `set_option linter.unusedVariables false`
-/
#guard_msgs in
def find (xs : List α) (p: (a: α) -> Bool) : Option α := do
  for _h: x in xs do
    if p x then
      return x
  none

But if I use hypothesis, linter will not complain about xs. Perhaps its request is xs must be used in the "body" of for and the type of h is x ∈ xs, so it stops to complain.

def find (xs : List α) (p: (a: α) -> a ∈ xs -> Bool) : Option α := do
  for h: x in xs do
    if p x h then
      return x
  none

[Jon Eugster]

Ah so the key point seems to be about the h : part... :detective:
Below find1 is fine and find2 has the linter warnings on xs and h, and the only difference is the h :

def f [Monad m]: α -> m Unit
| _ => pure ()

def find1 (xs : List α) : Option α := do
  for x in xs do
    f x
  none

-- unused variable xs and h
def find2 (xs : List α) : Option α := do
  for h : x in xs do
    f x
  none