Error messages suggestions

Stream: lean4

[Snir Broshi]

Following this:

Jireh Loreaux said:

Snir Broshi said:

Also unfortunately in my experience Lean doesn't have "helpful error messages". I'm not sure this is a requirement for mass adoption as we've seen beginners successfully learn Lean, but most errors I get are very cryptic, similar to C++ compilers exploding every time you forget a semicolon.

Whenever you see bad error messages, please shout it from the rooftops. We need to be addressing these, and sometimes it's hard for experts to do because it's hard to remember what you didn't know when you were less experienced.

I'll try suggesting things here. I don't currently have metaprogramming skills to fix these or to judge if a fix is even possible, but hopefully someone can help.

[Snir Broshi]

To get the ball rolling, I'll start with the notorious motive is not type correct:

-- `List` + `GetElem.getElem`:
theorem foo (l : List Bool) (i j : Nat) hi hj (h : i = j) : l[i]'hi = l[j]'hj := by
  rw [h]
  rfl

-- `Subtype`:
abbrev SmallNat := {n : Nat // n < 100}
def SmallNat.add (n : SmallNat) (d : Nat) : Nat := n.val + d

theorem bar (m n : Nat) hm (h : m = n) : SmallNat.add ⟨m, hm⟩ 5 = n + 5 := by
  rw [h]

[Snir Broshi]

I'm not sure if rw! will replace rw in core, but until then- after a few of these errors I realized that it usually means that I'm trying to rewrite something that's also part of a proof in the goal. This usually happens with list indices (docs#GetElem.getElem) and Subtype, as shown above.
It seems like a great effort was made to make the error message clear (it tries to explain what a motive is), but I suggest the following:

Highlight exactly which parts of the goal are the problem. For the first example, display the goal with i highlighted in some color and hi highlighted in red (or maybe the square brackets themselves since the pretty-printer hides hi). For the second example, highlight m and hm.

This doesn't help the user solve the problem, but it does communicate the source of the problem.
For list indices I usually try to convert the goal to use GetElem?, do the rewrite, then go back.

It might also be nice to add a clickable Try this that suggests simp [...], simp_rw [...], and rw! [...] if in Mathlib.

[Aaron Liu]

This is a general problem I have encountered, you get "application type mismatch" in a huge expression and usually it's possible to find out the application whose type is mismatched but I don't know of any way to find out where it is in the expression

[Snir Broshi]

Illustration:
image.png

[Snir Broshi]

Another rw suggestion:

In #new members > rw [← add_smul] fails to find pattern in Vector Space World a new member encountered this:

import Mathlib

variable {V K : Type} [Field K] [AddCommGroup V] [Module K V]

theorem zero_smul_v (w : V) : (0 : K) • w = (0 : V) := by
  apply add_right_cancel (b := 0 • w)
  rw [← add_smul]
  sorry

which says

Tactic `rewrite` failed: Did not find an occurrence of the pattern
  ?r • ?x + ?s • ?x
in the target expression
  0 • w + 0 • w = 0 + 0 • w

[Snir Broshi]

It's not trivial to figure out what's wrong, but if you hover over the metavariables you'll see that ?r and ?s have the same type ?m.26, but the two zeros in the expression 0 • w + 0 • w we're trying to rewrite have different types that are hidden by the pretty printer.

Making the experience better requires an algorithm that can find the closest match to an rw, and then explain the differences (similar to the goals that convert generates) either in types or terms.
Like the previous problem it also needs a way to tell the pretty printer to be more explicit just in a few select places, e.g. to render the term 0 • w + 0 • w as (0 : K) • w + (0 : ℕ) • w.

Even without such an algorithm, it'll be amazing to let the user click on the subterm it expected to be rewritten and get the differences pointed out as to why it doesn't match.

[Snir Broshi]

apply/exact can get the same treatment, and maybe it can even highlight when two instances from a diamond are causing the type error