Warn when a variable uses sorry

Stream: lean4

[Alex Keizer]

I just ran into a situation where a declaration was depending on sorry, but I had some trouble figuring out why.
Turns out, I made a typo in a variable many lines earlier. See the following MWE (where Foo doesn't exist)

variable (f : (Foo n × Nat))

def foo (x : Nat) : Nat
  := x + f.snd

In this case, the sorryAx does show up in the signature of foo, but in my original code it did not.

Should there be some lint on the variable line to warn that Foo doesn't exist (and it isn't even being bound as an auto-bound implicit, so there's also no different highlighting)?

[Kevin Buzzard]

Whenever I port a file from mathlib3 to mathlib4 I start by adding the line set_option autoImplicit false and it sounds like this would have saved you here.

[Alex Keizer]

Indeed, with that option it raises an error, I'll keep that in mind, thanks.

Still, it feels weird to me, since Foo is not being auto-bound. If we inline the variable, then it does raise an error even if autoImplicit is turned on.

def foo (f : (Foo n × Nat)) (x : Nat) : Nat
  := x + f.snd

So it seems there is some weird interaction with variable and auto bound functions

[Jannis Limperg]

Foo should be auto-bound in the variable declaration afaiu. If it's not highlighted properly, this might be a bug with the highlighting.

[Alex Keizer]

It seems like Foo isn't being auto-bound, it doesn't show up in the signature at all.
I assume auto-binding breaks because neither Foo nor n are defined, so it cannot figure out what the types should be.