unused section variable linter is buggy

Stream: lean4

[Jz Pan]

def Foo (n : Nat) [NeZero n] : Prop := n = 37

section

variable {n : Nat} [NeZero n] (H : Foo n)
include H

-- this should not complain since `[NeZero n]` is used in `H : Foo n`
/-
automatically included section variable(s) unused in theorem 'test1':
  [NeZero n]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [NeZero n] in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`
-/
theorem test1 : n = 37 := H

/- cannot omit referenced section variable 'inst✝' -/
omit [NeZero n] in
theorem test2 : n = 37 := H

end

section

-- works
theorem test3 {n : Nat} [NeZero n] (H : Foo n) : n = 37 := H

-- as expected
/-
failed to synthesize
  NeZero n

Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
theorem test4 {n : Nat} (H : Foo n) : n = 37 := H

end

[Jz Pan]

bump Is it a bug?

[Kevin Buzzard]

What is unexpected about this?

[Aaron Liu]

The linter gets it wrong

[Aaron Liu]

it wants you to omit a variable you can't omit

[Aaron Liu]

because the variable is used in the type of the theorem but not in the body

[Jz Pan]

If I use the following instead:

structure Foo (n : Nat) [NeZero n] : Prop where
  eq_37 : n = 37

then it won't complain on test1 anymore, which is good.

[Aaron Liu]

That's because if you do that the variable will be in the body too