RFC: have tactic should emit warning on data

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 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

No files, tests, or entry points are named in the issue, so begin by locating the tactic and term-mode implementations for have, have', and haveI. Define the warning and new syntax behavior across the listed cases, then add coverage showing the warnings and suggested alternatives.