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

[Rob Simmons]

Thanks for creating a place for collecting these. I'm going to put these in thread in a format I think is likely to be most helpful in the future — you're welcome to use this format or not, but it's useful to be able to tell what the error message was so it's easy to figure out if we already changed it.

[Rob Simmons]

The notorious motive is not type correct example in live lean

Existing error message

Tactic `rewrite` failed: motive is not type correct:
  fun _a => SmallNat.add ⟨_a, hm⟩ 5 = n + 5
Error: Application type mismatch: The argument
  hm
has type
  m < 100
but is expected to have type
  _a < 100
in the application
  ⟨_a, hm⟩

Explanation: ... long explanation ...

[Rob Simmons]

@Snir Broshi's "Another rw suggestion", live lean link, error message already in the thread (thanks!)

Here's an even more sad version (live link)

The lean code

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 0 0 w]
  sorry

Produces the error message

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

[Rob Simmons]

Snir Broshi said:

Illustration:

I don't understand what this is an illustration of — is this an error message you want, or something existing? It doesn't seem like an example of @Aaron Liu 's "application type mismatch"

[Snir Broshi]

Rob Simmons said:

I don't understand what this is an illustration of — is this an error message you want, or something existing? It doesn't seem like an example of Aaron Liu 's "application type mismatch"

It's not an existing error message, I manually edited it to show a mock example of my ideal "motive is not type correct" error message that directs the user to the exact problems, as I described above

[Jakub Nowak]

I think the error message in this example should say something along the lines of failed to unify u and v? Or maybe it's some bug?

import Mathlib

open SimpleGraph

variable {V : Type*} {G : SimpleGraph V}

example {h : G.Adj u v} {p : G.Walk v u} : True :=
  match p with
  | .nil => True.intro
  | .cons _ _ => True.intro

/--
error: Type mismatch
  Walk.nil
has type
  Walk ?m.14 ?m.15 ?m.15
but is expected to have type
  G.Walk v u
-/
#guard_msgs in
example {h : G.Adj u v} {p : G.Walk v u} : (Walk.cons h p).IsCycle :=
  match p with
  | .nil => sorry
  | .cons _ _ => sorry

[Snir Broshi]

#new members > variable not working seems like it could use an improvement, I have also been confused by the same problem.

variable (n : Nat) (hn : n ≠ 0)

/-- error: Unknown identifier `hn` -/
#guard_msgs in
theorem foo : 0 < n := by
  exact Nat.zero_lt_of_ne_zero hn

I suggest something like:

Unknown identifier `hn`. If you meant to include the variable `hn` in this theorem,
add `include hn in` before the `theorem`. Only variables used in the statement are
automatically included.

[Snir Broshi]

This error message is weird since obviously x = t is of the form x = t

import Mathlib

/--
error: Tactic `subst` failed: invalid equality proof, it is not of the form (x = t) or (t = x)
  x = t

a b c d : ℕ
t : ℕ := 0
x : ℕ := a * b
h : x = t
⊢ x = c * d
-/
#guard_msgs in
theorem foo (a b c d : Nat) (h : a * b = 0) : a * b = c * d := by
  set t := 0
  set x := a * b
  subst h
  sorry

I think it should suggest rw [h] at *, and say something about x not being a variable.
If there's another way to fix this I'd also love to know, it's weird that subst fails here just because the value of x is "known".

[Jakub Nowak]

That's a funny one. If you didn't notice, it should be with, not where. .-.

/-- error: 'let rec' expressions must be named -/
#guard_msgs in
example (n : Nat) := by
  induction n where
  | zero => sorry
  | succ n => sorry

[Jakub Nowak]

That error message is very cryptic. It should probably just say (kernel) arg #2 of 'Foo.mk' contains a non valid occurrence of the datatypes being declared instead.

import Std

/--
error: (kernel) application type mismatch
  Std.DTreeMap.Internal.Impl.WF inner
argument has type
  _nested.Std.DTreeMap.Internal.Impl_3
but function has type
  (Std.DTreeMap.Internal.Impl Nat fun x => Foo) → Prop
-/
#guard_msgs in
inductive Foo : Type where
| mk : Std.TreeMap Nat Foo → Foo

[Robin Arnez]

@Jakub Nowak see also lean4#8960

[Snir Broshi]

import Mathlib

/--
error: typeclass instance problem is stuck
  Decidable (∃ x, f = 0)

Note: Lean will not try to resolve this typeclass instance problem because the type argument to `Decidable` contains metavariables. This argument must be fully determined before Lean will try to resolve the typeclass.

Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
-/
#guard_msgs in
theorem foo {f : ℕ → ℕ} : True := by
  classical
  by_cases ∃ x, f = 0
  · sorry
  sorry

The issue is I wrote f = 0 instead of f x = 0, a small typo. The hint is close to helping, but I think the error should be "cannot infer type for x". Also weirdly, the error for a forall shows:

error: typeclass instance problem is stuck
  Decidable (∀ (x : ?m.3), f = 0)

which actually shows the metavariable, instantly showing what the problem is (at least for non-beginners).
Strange that exists doesn't show the type of x.

[Jovan Gerbscheid]

It would be nice if ∃ and ∀ printed the same. Currently, only ∀shows the binder types (which can be turned off using pp.piBinderTypes).

[Michael Rothgang]

I had a rather unhelpful error message in #lean4 > Module system error related to `import all` and renaming: I accidentally moved a Lean file outside of MathlibTest (into the mathlib repository root). A more targeted error would have been helpful.

[Notification Bot]

A message was moved from this topic to #lean4 > Printing the binder in Exists by Kyle Miller.

[Bolton Bailey]

I came across this error message which watching someone complete a Lean game on a livestream

import Mathlib

example (x y : ℝ) : (x + y)^2 = x^2 + 2 * x * y + y^2 := by
  have x+y = y+x := by -- invalid pattern
    sorry
  sorry

If you know some functional programming it might be easier to see what is going wrong here, but I think the error message here could be improved to explain this better.

[Floris van Doorn]

The following example shows only the error from the tactic mode, not from the term mode

example : True ∧ True where
  left := _ -- no error shown
  right := by -- only error shown here
    skip

The fact that the first underscore doesn't show an error is confusing, since it looks like Lean is happy with that part of the proof. I would like to see the term-mode error "don't know how to synthesize placeholder" even if there is a tactic-mode error.

A potential downside: the tactic proof could potentially synthesize a term-mode placeholder.

example : Nat :=
  Function.const _ 1 (by skip)

I don't think that it would be bad to show the error in this case.

[Bbbbbbbbba]

Unhelpful error messages for this example:

import Mathlib

example (long_name_a long_name_b long_name_c : ℕ) : long_name_a + long_name_b + long_name_c = long_name_b + long_name_a + long_name_c := by
  calc
    -- long_name_a + long_name_b + long_name_c = long_name_b + long_name_a + long_name_c := by show_term rw[add_comm long_name_a long_name_b]
    long_name_a + long_name_b + long_name_c = long_name_b + long_name_a + long_name_c := by exact
      Eq.mpr
        (id
          (congrArg (fun _a => _a + long_name_c = long_name_b + long_name_a + long_name_c)
            (add_comm long_name_a long_name_b)))
        (Eq.refl (long_name_b + long_name_a + long_name_c))

[Bbbbbbbbba]

(The real fix is to add an opening parenthesis after "exact" on the same line and a closing parenthesis at the end)

[Jakub Nowak]

I'm guessing the unknown constant is inside fun x y, but the error doesn't point that out.

import Mathlib

/-- error: (kernel) unknown constant 'Foo' -/
#guard_msgs in
inductive Foo where
| set (s : List Foo) (h : s.Pairwise (fun x y => True)) : Foo

[Snir Broshi]

Hmm

/--
error: (kernel) application type mismatch
  List.Nodup s
argument has type
  _nested.List_1
but function has type
  List Foo → Prop
-/
#guard_msgs in
inductive Foo where
| set (s : List Foo) (h : s.Nodup) : Foo

[Jakub Nowak]

Snir Broshi said:

Hmm

/--
error: (kernel) application type mismatch
  List.Nodup s
argument has type
  _nested.List_1
but function has type
  List Foo → Prop
-/
#guard_msgs in
inductive Foo where
| set (s : List Foo) (h : s.Nodup) : Foo

Hm, I would say that's an elaboration bug?

[Snir Broshi]

/--
error: (kernel) invalid nested inductive datatype 'Eq', nested inductive datatypes parameters cannot contain local variables.
-/
#guard_msgs in
inductive Foo where
| set (s : List Foo) (h : s = s) : Foo

[Michael Rothgang]

Debugging an erw in differential geometry made me find this very unhelpful rw error message: the left and right hand side shown look identical.

import Mathlib.Geometry.Manifold.MFDeriv.Basic
-- Let `M` be a manifold over the pair `(E, H)`, and `F` a normed space.
variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
  {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {H : Type*} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
  {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
  {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
  {s : Set M} {x : M} {z : M} {f g : M → F}
open Manifold
-- mathlib lemma; minimised to remove one hypothesis
theorem const_smul_mfderiv {s : 𝕜} :
    (mfderiv I 𝓘(𝕜, F) (s • f) z : TangentSpace I z →L[𝕜] F) =
      (s • mfderiv I 𝓘(𝕜, F) f z : TangentSpace I z →L[𝕜] F) :=
  sorry
-- This error message is most unhelpful: it should zoom in on the interesting parts.
-- Guessed error cause: the left and right hand side of `const_smul_mfderiv` naturally live in
-- different tangent spaces. Secretly, `TangentSpace I x` is just `E`, so these are defeq, but not
-- reducibly.

/--
error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
  (a • mfderiv I 𝓘(𝕜, F) f x) v
in the target expression
  (a • mfderiv I 𝓘(𝕜, F) f x) v = a • (mfderiv I 𝓘(𝕜, F) f x) v

𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : M → F
x : M
a : 𝕜
v : TangentSpace I x
⊢ (a • mfderiv I 𝓘(𝕜, F) f x) v = a • (mfderiv I 𝓘(𝕜, F) f x) v
-/
#guard_msgs in
lemma mfderiv_const_smul {x : M} (a : 𝕜) (v : TangentSpace I x) :
    mfderiv I 𝓘(𝕜, F) (a • f) x v = a • mfderiv I 𝓘(𝕜, F) f x v := by
  rw [const_smul_mfderiv]
  rw [ContinuousLinearMap.smul_apply a (mfderiv I 𝓘(𝕜, F) f x) v] -- `erw` closes the goal
  sorry

[Michael Rothgang]

Here's a variant of the same error, but for guard_target:

import Mathlib.Geometry.Manifold.MFDeriv.Basic

-- Let `M` be a manifold over the pair `(E, H)`, and `F` a normed space.
variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
  {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {H : Type*} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
  {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
  {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
  {s : Set M} {x : M} {z : M} {f g : M → F}
open Manifold

-- mathlib lemma; minimised to remove one hypothesis
theorem const_smul_mfderiv {s : 𝕜} :
    (mfderiv I 𝓘(𝕜, F) (s • f) z : TangentSpace I z →L[𝕜] F) =
      (s • mfderiv I 𝓘(𝕜, F) f z : TangentSpace I z →L[𝕜] F) :=
  sorry

-- This error message is most unhelpful: it should zoom in on the interesting parts.
-- Guessed error cause: the left and right hand side of `const_smul_mfderiv` naturally live in
-- different tangent spaces. Secretly, `TangentSpace I x` is just `E`, so these are defeq, but not
-- reducibly.

/--
error: The main goal is
  (a • mfderiv I 𝓘(𝕜, F) f x) v = a • (mfderiv I 𝓘(𝕜, F) f x) v
but was expected to be
  (a • mfderiv I 𝓘(𝕜, F) f x) v = a • (mfderiv I 𝓘(𝕜, F) f x) v
-/
#guard_msgs in
lemma mfderiv_const_smul {x : M} (a : 𝕜) (v : TangentSpace I x) :
    mfderiv I 𝓘(𝕜, F) (a • f) x v = a • mfderiv I 𝓘(𝕜, F) f x v := by
  rw [const_smul_mfderiv]
  guard_target = (a • mfderiv I 𝓘(𝕜, F) f x) v = a • (mfderiv I 𝓘(𝕜, F) f x) v
  sorry

[Patrick Massot]

I just discovered a pretty obscure error message. The following is correct code:

example (u : Nat → Nat) (h : ∀ n, u n = u 0)
  : ∀ n, ∀ m, u m = u n := by
  intro n m
  calc
    u m = u 0 := h m
    _   = u n := (h n).symm

Now remove the first m in the calc block so that it starts with u = u 0 := h m. The first line gets a nice error message, but then the second line gets:

invalid 'calc' step, left-hand side is
  true : Bool
but previous right-hand side is
  Function.const Lean.Name ()
    `external:file:///MathlibDemo/MathlibDemo.lean.5.4.5.12.4.12._sorry._@.external:file:///MathlibDemo/MathlibDemo.lean.2021293395._hygCtx._hyg.40 : Unit

(the external file stuff is what you get on live-lean, otherwise you get your file info). I know calc elaboration is tricky. Probably here it should give up after failing to elaborate the first line.

[Floris van Doorn]

Type mismatch errors are doing a very good job displaying differences between the two expressions. However, here is a case where it fails to print the difference:

 structure Foo1

 structure Foo2 extends Foo1

 inductive Foo1.Bar (x : Foo1) : Prop

 inductive Foo2.Bar (x : Foo2) : Prop

 example {x : Foo2} (h : x.toFoo1.Bar) : x.Bar := h
 /-
 Type mismatch
  h
has type
  x.Bar
but is expected to have type
  x.Bar
-/

(this occurs in the wild, e.g. docs#CategoryTheory.Coverage.saturate_iff_saturate_toPrecoverage)

[Snir Broshi]

I found another thread with great error suggestions: #lean4 dev > Can diagnostics be more resilient to unfinished proofs?
Edit: found more
#lean4 > Confusing error message: a scaling problem @ 💬
#lean4 > error puzzle @ 💬
#lean4 > Improved error message for accidentally recursive def
#lean4 > elaboration of `show type from value`
#lean4 > extract_lets cannot extract syntactically identical lets @ 💬