Undefined variables silently accepted

Stream: lean4

[Oliver Nash]

Lean accepts the following code without complaint:

import Mathlib.Order.LiminfLimsup

lemma foo {s : bar → Set baz} :
    Filter.limsup s qux = ⊥ := by
  sorry

I am very surprised by this and would have expected it to complain that:

• bar is undefined
• baz is undefined
• qux is undefined

Is this expected behaviour?

[Patrick Massot]

Those are all auto-implicit, right?

[Yaël Dillies]

Is that not simply autoImplicit? Try set_option autoImplicit false

[Oliver Nash]

FWIW I encountered this because I was writing some code and I absent-mindedly wrote Mathlib3-style at_top instead of Mathlib4-style atTop in the declaration of a lemma and it took some time to understand that the reason various lemmas would not apply etc.

[Oliver Nash]

I thought this autoImplicit madness only applied to lowercase Greek letters or something?

[Yaël Dillies]

Yeah, look for autoImplicit and you will see all the people complaining about this footgun.

[Oliver Nash]

Admittedly I've only recently started writing non-trivial amounts of Lean 4.

[Oliver Nash]

I presume this has been asked before but: how can we nuke this feature from orbit?

[Oliver Nash]

"feature"

[Oliver Nash]

Or at least globally enable set_option autoImplicit false in Mathlib?

[Oliver Nash]

I should add: thank you @Yaël Dillies and @Patrick Massot

[Patrick Massot]

I would vote for doing this only with 1-letter long variables (both greek and latin). It's pretty nice to write [TopologicalSpace X] instead of {X : Type _} [TopologicalSpace X]. But I've never used this feature for variables with more than one letter.

[Oliver Nash]

I will vote for anything that reduces the scope of this "feature".

[Oliver Nash]

Who do I pester about this?

[Patrick Massot]

Nobody since Leo is probably the only one who can decide this. Note that we can set the default to false at the mathlib level though. It may even be rather painless if we do it before the end of the port since I guess mathport does not use it.

[Yaël Dillies]

Patrick Massot said:

I would vote for doing this only with 1-letter long variables (both greek and latin).

This is actually quite nice because we have close to no one-letter definition.

[Oliver Nash]

A lot of people thought this sort of thing was nice in the 1950s.

[Oliver Nash]

It wasn't.

[Marc Huisinga]

Just for the record, some people do like the feature: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Auto-implicits

[Oliver Nash]

Good for them :) I'm happy for the feature to exist but IMHO it should default to false not true.

[Alex J. Best]

Other things (e.g. semantic syntax highlighting) have also changed since the 1950s. Would you still be against it if it was even more obvious from the colour that some things are variables and some are function names?

[Marc Huisinga]

People from the 50s would likely also take great offense with the notion of implicit tactic state that is only made visible with an editor extension :)

[Oliver Nash]

You are of course right to point out that merely appealing to the passage of time is no logical argument. However I believe this is clearly a case of an obviously awful default and the more links I find in Zulip the more wasted time I see.

[Niels Voss]

I think autoImplicit should at least be false for mathbb symbols like ℕ. I can't give an opinion on the feature as a whole but many times I've forgotten to import the basics of Mathlib or didn't want to because it was the web editor, then became surprised that Lean failed to infer basic typeclass instances on ℕ because it was actually an implicit variable.

[Yaël Dillies]

You can't rely on highlighting to show this kind of information because of accessibility issues. I personally am colorblind and I can't find a color that would be both visually different and not too contrasted.

[Oliver Nash]

I need to return to what I was actually working on before I cost myself half an hour by writing at_top. I will canvass for this to be changed when I have more time.

[Marc Huisinga]

Yaël Dillies said:

You can't rely on highlighting to show this kind of information because of accessibility issues. I personally am colorblind and I can't find a color that would be both visually different and not too contrasted.

Inlay hints would help with this, but as Sebastian previously mentioned somewhere, their LSP design is unfortunately not well-suited for incremental file checking

[Reid Barton]

Maybe a different background color (e.g. bright red)?

[Ruben Van de Velde]

Squiggly underlines?

[Alex J. Best]

Yaël Dillies said:

You can't rely on highlighting to show this kind of information because of accessibility issues. I personally am colorblind and I can't find a color that would be both visually different and not too contrasted.

I think this is a good point, but agree that it should be possible to configure other ways to display the information Lean returns (eg underlines, light block backgrounds, italicization, bolding), it would be great to have some settings file bundled in with mathlib that people can use to easily set this up

[Shreyas Srinivas]

Oliver Nash said:

I will vote for anything that reduces the scope of this "feature".

The notion that something that was "evil" in the 1950s remains evil now is absurd. Haskell autoImplicits types all the time. We are not entering programs on tapes or punch cards. We could definitely work to improve editor highlighting for this feature (for example a warning underline) for those who wish to configure it so.

[Shreyas Srinivas]

Another idea would be to do what the rust extension does to show inferred type signatures on top of declarations. In this case, to simply point out that auto implicit was used.

[Kyle Miller]

If that Rust extension uses inlay hints, then it seems like that won't work for Lean

[Shreyas Srinivas]

Fine, then maybe on the infoview?

[Shreyas Srinivas]

Another counterpoint : removing autoimplicits clutters up theorem statements, which will be a debugging nightmare of its own, especially when one does cs stuff. From a usage standpoint, keeping it and adding an editor feature which displays the implicits might be simpler.

[Shreyas Srinivas]

In this case, just the fact that there are two similar looking names in the implicit variables listing should show people that there is a typo

[Eric Wieser]

removing autoimplicits clutters up theorem statements

I think variables makes this largely moot

[Shreyas Srinivas]

I am not sure about that. variables introduces its own problems when writing a function/theorem. EDIT: there was a thread about this. Anything in variables is automatically inserted as an assumption in all theorems in a section/namespace and there is no meaningful way to fix this automatically. One has to manually use prune or clear. Introducing a section for each higher order function would be a pain.

[Scott Morrison]

See the other thread: we have a solution, PR in the works.

[Scott Morrison]

Not sure why we are having this conversation in two threads at once...

[Mario Carneiro]

Shreyas Srinivas said:

Another idea would be to do what the rust extension does to show inferred type signatures on top of declarations. In this case, to simply point out that auto implicit was used.

As I have mentioned elsewhere, you can already see inferred type signatures for declarations by hovering over the declaration name or putting your cursor there and looking at "expected type"

[Shreyas Srinivas]

Mario Carneiro said:

As I have mentioned elsewhere, you can already see inferred type signatures for declarations by hovering over the declaration name or putting your cursor there and looking at "expected type"

I am using this all the time. But it seems it might help others with debugging if the implicits are shown without having to hover the mouse over the declaration.

[Eric Wieser]

Do we need a github bot that adds a comment under every declaration in a PR with its full type? This feels like the type of thing that's hard to catch during review (though admittedly variables had a similar problem), where typically the reviewer is not using an intelligent editor.

[Gabriel Ebner]

Another related and hard to catch bug is Sort _, which can (and sometimes does) default to Prop.

[Eric Wieser]

Even just defaulting to Type _ is usually a problem

[Eric Wieser]

I think @Kyle Miller had a notational solution to that elsewhere

[Kyle Miller]

Here's a Type* notation that gives you types with distinct universe level variables. I think there ought to be a more sophisticated solution out there, where there are special universe level metavariables that are allowed to unify with nontrivial expressions (rather than just 0 or 1 for example), but at least it's something.