unused variable bug?

Stream: lean4

[Thomas Murrills]

variable (f) [∀ i, Mul (f i)] gives an "unused variable i" linting message—but it's clearly used, right? Is this a bug?

[Thomas Murrills]

Or, wait—I think I get what's happening. We're enforcing an auto-implicit style where possible.

[Thomas Murrills]

Though, as it happens, in the file I'm porting, it isn't possible, as i is declared as a variable earlier! So, I guess that's the bug: saying it's unused when actually it's necessary, since an auto-implicit couldn't be used in that case.

[Thomas Murrills]

Actually, that isn't quite why—it's due to how f is declared as a variable earlier.

[Thomas Murrills]

MWE:

[Thomas Murrills]

variable {I : Type u} (i : I)
variable {f : I → Type v}
variable (f) [∀ i, Mul (f i)] -- unused variable `i` [linter.unusedVariables]
-- replacing i with _ causes the following:
-- invalid parametric local instance, parameter with type ?m.44 does not have forward dependencies, type class resolution cannot use this kind of local instance because it will not be able to infer a value for this parameter.

[Jireh Loreaux]

If you replace i with j in the third line does it work?

[Jireh Loreaux]

Also, it's weird to declare f as implicit and then immediately change it to explicit.

[Thomas Murrills]

No, it doesn't seem to work even then...

In the original file, it doesn't immediately change it; there are many lines of code in between. This is just an mwe.

[Thomas Murrills]

Ok, I worked around this by using [(i : I) → f i] instead. Are these 100% equivalent in this context? I'd expect them to be, but at one point it was mentioned that ∀ gets elaborated slightly differently than →. Can't find the message, though, and it might have just been for the non-dependent case.

[Thomas Murrills]

Still, I'd bet this is a linter bug...[∀ _, Mul (f i)], [∀ _, Mul (f j)] both give actual errors, and [∀ (i : I), Mul (f i)], [∀ (j: I), Mul (f j)], [∀ j, Mul (f j)] all give the same linter error.

[Mario Carneiro]

terms inside variable are a bit weird, because elaboration is delayed until the variable is used:

variable (c : Nat + 1) -- no problem
variable (c : by simp) -- this tactic is never executed [linter.unreachableTactic]

[Mario Carneiro]

I'm thinking this causes the linter warning. Note that f and i are not variable-colored in your example

variable {f : I → Type v}
variable (f) [∀ i, Mul (f i)]
      --  ^     ^ variable-color
                    --  ^ ^ not variable-color

[Mario Carneiro]

you can always suppress the unused variable linter by using a variable name with an initial underscore

[Thomas Murrills]

I see! Interesting!

Not a very important question, but: why is there a difference in the linter between ∀ and → in this case? I would have naively expected them to be treated the same

[Mario Carneiro]

I believe the unused variable linter has a blacklist for variables named in (i : I) → ... dependent functions, because these are often used to give the function's parameter names, which are accessible from user code using the (i := ...) syntax and hence can cause false positives if you really need the name to not have an underscore in it but the function type isn't actually dependent. The blacklist doesn't cover \all probably because it's weird to have a proposition with an unused variable in the statement, and indeed in this case Mul is not a proposition so \all isn't the preferred spelling