RFC: have tactic should emit warning on data

fpvandoorn commented 7 months ago

Explanation

The have tactic is an enormous footgun for new users, since if you write have : <some type> := ... (i.e. not a proposition but data), then the value of the data is forgotten. This is especially problematic if the type is a class, since it can then be used without the user realizing.

Typical example:

example (n m : Nat) : True := by
  have h1 : n + m = m + n := Nat.add_comm n m
  have : Add Nat := inferInstance
  -- many other steps
  have : n + m = m + n := h1 -- error

This is treacherous, since the offending have can occur many lines before the error.

Example where a user was confused about this here.

Proposal

The tactic have x? : T := _ will emit a warning if T is a type (anything that is not always a proposition).
A new tactic have! which has the current behavior of have. (Optionally: have! emits a warning when the type is a proposition, and suggests the user to use have instead).
The warning for have suggests the user to switch to either let or have!.
We ensure that have' and haveI (in Std) have the same behavior (and add have'! and haveI!)
Term-mode have and let should probably adopt the same behavior

User Experience: This will decrease the number of mistakes from beginners, and will hardly inconvenience experienced users.
Beneficiaries: Mainly beginners, but everyone
Maintainability: Should have almost no influence on maintainability.

Community Feedback

Overwhelming support on Zulip. Other Zulip threads: 1 2 3

Impact

Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.

nomeata commented 7 months ago

Thanks! Sounds reasonable, but I have a few questions:

If there are clear alternatives (have! and let), why only warn, why not make it an error?
Is this going to make metaprogramming that generates syntax terms with have harder?
The have! syntax doesn't convey much meaning. Is there something better? How useful is it anyways? If the use cases are very rare and obscure and by power users, do we need syntax for it, or could ask them to write out whatever have elaborates to? Or at least use a name like have_data that doesn't squat generic syntax space and explains a bit better what is happening here?

fpvandoorn commented 7 months ago

Good points!

I think warnings are a lot more user-friendly than errors ("Lean knows what I mean, why doesn't it show me the goal state one line below the have?")
That's a fair point, and might be a reason to say that have! (or whatever it will be called) should have exactly the behavior as the current have
That's a good point. I like have! because I think of the ! as "try harder". But I think the use cases are pretty rare, as you said. You might not want a giant term in your proof state. Or you might perform a tactic that fails if your local variable has a body. But it should be pretty rare. Other options: use an even longer name, like have_and_forget_value. Or tell the user that they can use let + clear_value (which is currently a tactic in mathlib). Not sure if I like these two options, though.

nomeata commented 7 months ago

I'd suggest logging an error, but not throwing one. You are right it shouldn't get in the way of showing proof states etc, but it also shouldn't be left in the end if it's considered a footgun.

YaelDillies commented 6 months ago

Should this not be implemented as a syntax linter rather than in have itself so that we can disable the linter locally (and therefore bypass the need for the hypothetical have!)?

fpvandoorn commented 6 months ago

I would also be happy with that, as long as the linter also runs and displays errors when there is a sorry, an elaboration error in a later tactic, or an unsolved goal.

kmill commented 6 months ago

Damiano Testa made a linter for this, and you can see the results here: https://github.com/leanprover-community/mathlib4/pull/12157

Zulip discussion

nomeata commented 1 month ago

How is it going with the mathlib linter? Has it been actively useful to users?

I’m still mildly in favor of this idea, but am not convinced that it’s worth the attention and code complexity. How many beginners or users really stumble due to the lack of this?

leanprover / lean4