Why does lean allow undeclared variables in hypotheses?

Stream: new members

[Nir Paz]

What is the usefulness of something like this compiling?

example (_ : n = m) : True := trivial

Is this kind of thing used in mathlib? It has some disadvantages, I just spent a while trying to figure out why in a case similar to this

import Mathlib

example (nonemp : Set.Nonempty s) (s : Set ℝ) (x : ℝ) (h : x < sSup s) : True := by
  have := exists_lt_of_lt_csSup nonemp h
  trivial

lean couldn't synth an instance on ℝ, because I flipped the order of the first 2 hypotheses. I was surprised it didn't just throw an error at the first line once I figured it out.

[Eric Wieser]

You can disable this behavior with set_option autoImplicit false

[Eric Wieser]

In mathlib it's disabled by default, but in your own project you have to disable it yourself

[Martin Dvořák]

I think autoImplicit false should be a default default.

[Arthur Paulino]

This is probably the 3rd or 4th time I see this suggestion come up. Here's an idea: have a global config so users could set their own default settings. I think it's totally understandable that not everybody likes autoImplicit due to the fear of being setting footguns with typos. And temporarily setting that to false on every working file in a project whose default value is true is an annoying solution

[Eric Wieser]

How would that global config be different to the configuration we have in the mathlib lakefile?

[Eric Wieser]

It needs to be per-project, otherwise you won't be able to open someone else's code that uses autoImplicit

[Arthur Paulino]

Yeah, idk... I think the issue here is that autoImplicit feels more like a programming style preference than something that should be defined per project.

This gets ugly, but maybe, just maybe, autoImplicit could be front-end thing. So you'd code as if you didn't care and Lean would warn you that something was interpreted as auto-implicit, offering a button to concretize it

[Eric Wieser]

Ah; so you're suggesting that it should be impossible to turn autoImplicit off, but it should be possible to make it a linter warning/error?

[Arthur Paulino]

That's probably a better solution. I was suggesting something more radical: there would be no such thing as "auto-implicit", concretely speaking. But Lean would still be able to allow (but warn) that it's being used as a front-end trick

[Mario Carneiro]

that sounds like auto-implicit exists

[Mario Carneiro]

lean is the front end

[Mario Carneiro]

so if it accepts code with auto implicits then they exist

[Arthur Paulino]

So this can be the global config: warn me about autoimplicits

But it has to be done in a friendly way so it's not too spammy

[Mario Carneiro]

Sure that can be done

[Mario Carneiro]

it would only be spammy if you turn it on in a project that doesn't care

[Mario Carneiro]

but a linter warning would still be tantamount to banning it, for the most part

[Mario Carneiro]

you might get slightly better (or worse) error messages if you allow it to lint and continue with the interpretation of the variable as an autoImplicit instead of immediately dying with an unresolved name error like it normally does

[Eric Wieser]

Mario Carneiro said:

but a linter warning would still be tantamount to banning it, for the most part

Demoting from an error to a linter warning would at least mean that the setting no longer breaks the build / browsing in vscode

[Jireh Loreaux]

What would be really nice is if it could be a linter warning (akin to unused variables, the core Lean version, not the Mathlib one), and that warning could be set / overridden locally within a project in VS Code. Then we could have autoimplicits in mathlib again.

We would turn them on, and disable the linter. But then users who think autoimplicit is a footgun could have it enabled locally. IMHO, that would be the best of all possible worlds regarding autoimplicits.

[Eric Wieser]

We would turn them on, and disable the linter. But then users who think autoimplicit is a footgun could have it enabled locally. IMHO, that would be the best of all possible worlds regarding autoimplicits.

The downside of this approach is that reviewers cannot tell (from github) if someone has ignored the linter warnings deliberately or accidentally

[Jireh Loreaux]

I don't see how that's a problem.

[Eric Wieser]

One of the job of review is to check if someone has already blown their foot off; sometimes it's hard to tell from the source code alone. Of course, if every PR is reviewed in a live workspace, that's not an issue.

[Martin Dvořák]

Eric Wieser said:

In mathlib it's disabled by default, but in your own project you have to disable it yourself

In every new project I create in Lean 4, I add to lakefile.lean the settings moreServerArgs := #["-DautoImplicit=false"] for the package and moreLeanArgs := #["-DautoImplicit=false"] for the default target. For example:
https://github.com/madvorak/thue/blob/main/lakefile.lean

[Eric Wieser]

I recommend you add pp.proofs.withType false to that list too

[Joachim Breitner]

This is probably the 3rd or 4th time I see this suggestion come up.

I guess I missed the previous instances of that discussion. I can’t write five lines of lean without stumbling confusedly and then turning autoImplicit off.… so I am genuinely curious what the arguments for autoImplicit as a default are.

(Or is this a contentious topic with flaring tempers best to avoid?)

[Mario Carneiro]

Previous discussions:

• https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60autoImplicit.20true.60.20is.20evil
• https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.5BRFC.5D.20Make.20autoImplicit.20default.20to.20false.20on.20non-greek

[Eric Wieser]

• https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mathlib4.3A.20autoImplicit.20false.20by.20default.3F/near/384204178, where a vote happened

[Martin Dvořák]

We should do another voting, about setting autoImplicit false default for Lean.

[Mario Carneiro]

I'm not going to be the one to write the RFC

[Mario Carneiro]

(decisions in this space aren't made by a vote, they are made by convincing the devs)

[Shreyas Srinivas]

Joachim Breitner said:

This is probably the 3rd or 4th time I see this suggestion come up.

I guess I missed the previous instances of that discussion. I can’t write five lines of lean without stumbling confusedly and then turning autoImplicit off.… so I am genuinely curious what the arguments for autoImplicit as a default are.

(Or is this a contentious topic with flaring tempers best to avoid?)

I thought this issue was settled in favour of relaxed autoImplicit for mathlib (single char variables) and letting everyone have their settings for others.

[Mario Carneiro]

mathlib has no autoImplicits at all

[Mario Carneiro]

it was relaxed for a while but then there was another vote and now it's none

[Shreyas Srinivas]

Does keeping autoImplicit off remove Haskell/ML style type variable introduction?

[Eric Wieser]

Mario Carneiro said:

mathlib has no autoImplicits at all

That's not quite true, it has to ask for them via set_option, but is allowed to do so

[Mario Carneiro]

@Shreyas Srinivas yes

[Eric Wieser]

Still relevant here is lean4#2456, which is needed to fix an annoyance where turning off autoImplicit in mathlib also turns it off for Std when browsing in vscode

[Shreyas Srinivas]

IIRC I asked this once before and you said the same back then and that's why I voted in favour of keeping them

[Mario Carneiro]

The polls are really split on this matter, it's clear no choice of default or default default will settle the problem for good

[Shreyas Srinivas]

Has the following idea been already considered: a new class of warnings called "gentle warnings" in the infoview which that can be configured to be turned on or off in the vscode extension settings/lake settings. If turned on users are told about all the autoimplicit variables in their declaration and other such footguns.

[Mario Carneiro]

those are just regular warnings

[Kyle Miller]

@Arthur Paulino I like the idea of autoImplicit false being a warning rather than an error. (Or maybe another setting, autoImplicit warn?) There's already a hint of whether a variable is auto-implicit in the editor (it's a slighly different color), and having a per-project global option to make it noisier makes sense.

This is more friendly than making it be a strict error, since at least you can still finish some definition/theorem and then deal with the warnings. Mathlib doesn't accept code with warnings, so it's like autoImplicit false.

Unrelated, but I'm wondering, could there be a code action to add the implied implicit variables?

[Kyle Miller]

Mini-RFC: add a autoImplicitWarn option with a Bool value. When set to true, then whenever the auto-implicit feature is activated, it generates a warning message for the introduced variable. (If easy to implement:) The location of the warning is at the location of one of the occurrences of the auto-implicit. (If not:) The location of the warning is at the current syntax ref inside withAutoBoundImplicit (so commands can choose to at least have the warning appear at the variable, theorem, def, etc.)

Hastily-written rationale: many users report finding autoImplicit to lead to confusing situations, and libraries such as mathlib have elected to turn auto-implicits off entirely. However, making auto-implicits be a hard error is stronger than necessary, since auto-implicits can also be viewed as a mechanism to allow elaboration to continue despite potential errors by the user -- similar to automatic sorry insertion. Allowing auto-implicits to function while raising the use of auto-implicits to warnings should give users some of the benefits of auto-implicits minus most of the confusion.

[Mario Carneiro]

suggestion: rename autoImplicitWarn to linter.autoImplicit with default value false

[Mario Carneiro]

it is easy to make this appear at the first occurrence of the autoImplicit, as this is the current ref when processing the autoImplicit

[Mario Carneiro]

otherwise LGTM (but I'm still not volunteering to write the RFC :wink: )

[Patrick Massot]

Joachim Breitner said:

I guess I missed the previous instances of that discussion. I can’t write five lines of lean without stumbling confusedly and then turning autoImplicit off.… so I am genuinely curious what the arguments for autoImplicit as a default are.

Did you try allowing only one-letter long auto-implicits? The should solve 99% of your confusion and still leave you the benefits.

[Kyle Miller]

Mario Carneiro said:

otherwise LGTM (but I'm still not volunteering to write the RFC :wink: )

I'm happy to write the RFC at some point

[Joachim Breitner]

Patrick Massot said:

Did you try allowing only one-letter long auto-implicits? The should solve 99% of your confusion and still leave you the benefits.

No, whenever I hit this issue I'm already briefly frustrated and just slap the shorter set_option to the top of the file. I am aware that this variant exists and if that was the default, I'd probably stumble much less often.

Also when back at the computer I have to verify the claim that implicit parameters have a different color. Maybe the colorscheme isn't great for certain color perceptions. :red_square::green_large_square::see_no_evil:

[Patrick Massot]

Please read https://lean-lang.org/lean4/doc/semantic_highlighting.html about colors.

[Shreyas Srinivas]

I honestly don't see the issue with autoImplicit in your example @Nir Paz . In your example the tactic state is:

α✝: Type ?u.8
s✝: Set α✝
nonemp: Set.Nonempty s✝
s: Set ℝ
x: ℝ
h: x < sSup s
⊢ True

[Shreyas Srinivas]

whereas in the example with the first and second hypothesis flipped ,it is :

s: Set ℝ
nonemp: Set.Nonempty s
x: ℝ
h: x < sSup s
⊢ True

[Shreyas Srinivas]

There is a clear difference between the first and the second example that immediately tells me that lean has inserted another variable s\dagger

[Shreyas Srinivas]

This is why I don't understand the fuss about autoImplicit. On the one hand, it solves the hassle of manually adding type variables in programming defs. In tactic mode, even when it kicks in, lean is very upfront about the fact that it is creating new variables in the infoview

[Nir Paz]

I guess if I'd known about this in the first place it would have been obvious, but as a beginner my eyes tend to skip daggers and I focused on the specific errors I got and went down a rabbit hole. It feels to me that this is one of those thing that end up frustrating new people in this way (there are many such things in lean) so I wanted to hear about the benefits, but I wasn't making a stand against it or anything

[Shreyas Srinivas]

That's fair. What I am saying is that this can be explained in one of the learning materials or documentation. These examples don't make the case that autoimplicit is some extremely evil feature, which is an implication that has come up in these discussions in the past.