Misleading error message on type mismatch

Stream: lean4 dev

[Dan Abramov]

Admittedly I'm a new user but I spent a whole half an hour on this.

This proof works:

import Mathlib

example {a b c k : ℕ} (cpos : 0 < c) (h : k ∣ (c * a - c * b)) : k ∣ c * (a - b) := by
  rw [Nat.mul_sub]
  exact h

This proof doesn't:

import Mathlib

example {a b c k : ℕ} (cpos : 0 < c) (h : k ∣ (c * a - c * b)) : k ∣ c * (a - b) := by
  rw [mul_sub]
  exact h

/-
tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ?a * (?b - ?c)

a b c k : ℕ
cpos : 0 < c
h : k ∣ c * a - c * b
⊢ k ∣ c * (a - b)
-/

This specific failure is confusing because "the pattern" is definitely there, it's just the types don't match. (Presumably I was supposed to know that naturals are not, in fact, a NonUnitalNonAssocRing. Or maybe they are? I don't know how to check.)

I wonder if it would be possible to give a better error message in cases like this? Or is it on me for not looking at the "Expected type" pane? What is the mechanism by which I was expected to find the real error cause in this example?

I also have another example, arguably a more severe one.

This proof works:

import Mathlib

example {a b c k : ℕ} (cpos : 0 < c) (h : k ∣ (c * a - c * b)) : k ∣ c * (a - b) := by
  rw [Nat.mul_sub c]
  exact h

This proof doesn't:

import Mathlib

example {a b c k : ℕ} (cpos : 0 < c) (h : k ∣ (c * a - c * b)) : k ∣ c * (a - b) := by
  rw [mul_sub c]
  exact h

/-
tactic 'rewrite' failed, equality or iff proof expected
  ?m.563

a b c k : ℕ
cpos : 0 < c
h : k ∣ c * a - c * b
⊢ k ∣ c * (a - b)
-/

Yeah, I know, same problem, etc. But the error message here led me on a completely false trail. It seemed to imply that the rw tactic is only valid to "apply" to an expression that looks like an equality (=) or an iff (↔). Being an inexperienced user, I took what it was saying at face value, and thought that somehow rw doesn't work for rewriting statements like k ∣ c * (a - b). Which is, of course, completely wrong, so I wasted a bunch of time.

How I'd love to see this solved, in the order of preference:

• An ideal error message would have "Did you mean Nat.mul_sub?" Presumably the compiler is aware of which namespaces have a theorem with the same name whose types match up unlike mine. But maybe this is too idealistic.
• The next best thing would be if tactic 'rewrite' failed, equality or iff proof expected in the second example instead told me something that reflected the real cause of the issue.

Thanks for reading my rant!

[Dan Abramov]

I'm guessing in the second example, the error message means that the thing I'm passing to rw needs to be an equality or an iif. But since that's what it looks like in the definition, it's not obvious that it ended up being something else (presumably it never got properly "synthesized" so it's some broken placeholder, and rw bails on it?)

So maybe there's an opportunity to improve the rw error message when the thing being passed to it is completely borked.

[Kim Morrison]

@Dan Abramov are you perhaps using an older version of Lean?

I get:

import Mathlib

example {a b c k : ℕ} (cpos : 0 < c) (h : k ∣ (c * a - c * b)) : k ∣ c * (a - b) := by
  rw [mul_sub c]
  exact h

producing

failed to synthesize
  NonUnitalNonAssocRing ℕ

[Kim Morrison]

But ideally the first example would manage to do the same thing. Usually in this case of a failed rewrite I would hover over the lemma to manually inspect the type signature, and hopefully realise that the typeclass was the problem.

Pinging @Joseph Rotella, could you track the first example somewhere? It would be great to improve the error message there.

Checking alternative namespaces and suggesting the lemma that the user really wanted would, of course, be wonderful! :-)

[Dan Abramov]

Looks like I have 4.16.0 installed but running 4.13.0 in the project as per my (maybe outdated?) mathematics_in_lean checkout. Sorry I'm not testing against the latest.

[Dan Abramov]

Re: error message, to be clear, I get both:

Screenshot 2025-02-20 at 02.30.11.png

As a user I usually mentally skip the first one because I have completely no idea what it is saying (what does it mean to "fail to synthesize"? this feels like compiler speak leaking into userland so I tend to ignore messages like this).

Whereas the "tactic 'rewrite' failed" below is at least familiar, usually meaningful, and has context. (In this case, it's misleading though.)

[Dan Abramov]

Usually in this case of a failed rewrite I would hover over the lemma to manually inspect the type signature, and hopefully realise that the typeclass was the problem.

How would you know that it is a problem? There is nothing I can see indicating that N doesn't implement it. And I presume it would require hunting through many definitions to find all typeclasses that N implements. So what is a good way to find this out aside from memorizing all the relevant typeclasses?

Tbh I would expect the tooling to say something like "a is ℕ which does not implement NonUnitalNonAssocRing".

Is this what "failed to synthesize NonUnitalNonAssocRing ℕ" was supposed to convey?

[Dan Abramov]

Just to clarify my confusion, I find the wording "failed to synthesize A B" close to being a word salad — if it really means "B is not of type A", IMO it would be a big improvement to rephrase it as such (and even better if it mentioned which variable failed that check).

[Dan Abramov]

So I guess there's three separate things:

• Would be nice to improve "cannot match pattern" when it does match the shape of the syntax but fails due to typeclasses. In this case, it would be better if the error messaged emphasized the issue with typeclasses. This applies to the first example.
  • For bonus points, it would be nice if it suggested namespaced theorems with the same name if any match the typeclasses.
• Would be nice to rephrase "Cannot synthesize A B" into "Expected type A, but got variable x of incompatible type B" or even just "A is not compatible with B" or "A does not implement B" or something like that. This applies to the second example only.
• Would be nice to not show "equality of iff expected" at all, or to change its wording, when the root issue is due to typeclasses. Right now it's shown together with "Cannot synthesize" but it's unclear which one is the root issue. This applies to the second example only.

[Kyle Miller]

"Failed to synthesize" is talking about the instance argument in mul_sub. It couldn't find an instance to use for that argument.

mul_sub.{u} {α : Type u} [NonUnitalNonAssocRing α] (a b c : α) : a * (b - c) = a * b - a * c

The fact that the error is that it could not synthesize a NonUnitalNonAssocRing ℕ instance, that means that ℕ doesn't implement it.

[Kyle Miller]

It could at least say "failed to synthesize instance" to let you know that there was no instance of that type it could find.

[Kyle Miller]

Dan Abramov said:

Just to clarify my confusion, I find the wording "failed to synthesize A B" close to being a word salad — if it really means "B is not of type A", IMO it would be a big improvement to rephrase it as such (and even better if it mentioned which variable failed that check).

Fundamentally, the way typeclasses and instances work in Lean is incompatible with this. They might be called typeclasses, but the class system is a way to synthesize a term of a particular type automatically. We might think about NonUnitalNonAssocRing ℕ as if it's implemented "for" ℕ, but in general, the question is just whether or not there's a NonUnitalNonAssocRing ℕ instance to be found, which is then used for the instance argument.

One of the ways to check from outside a tactic is with the #synth NonUnitalNonAssocRing ℕ command.

I worry that having error messages pretend that classes are attached to types would give incorrect mental models of how Lean works.

[Kyle Miller]

(deleted, nevermind, that was a different error)

[Kyle Miller]

Dan Abramov said:

For bonus points, it would be nice if it suggested namespaced theorems with the same name if any match the typeclasses.

That could potentially be helpful (though at the same time fairly complicated to do).

Another approach is to figure out if there's a more general setting that would include Nat as well. On one hand, that would make mul_sub work, but on another it might be some weird algebraic structure you'd have to learn something about. Having classes like NonUnitalNonAssocRing is a consequence to trying to make theorems generally applicable...

[Dan Abramov]

We might think about NonUnitalNonAssocRing ℕ as if it's implemented "for" ℕ, but in general, the question is just whether or not there's a NonUnitalNonAssocRing ℕ instance to be found, which is then used for the instance argument.

Would "Could not pass a : ℕ as NonUnitalNonAssocRing because no NonUnitalNonAssocRing ℕ instance was found" be accurate? I'm all for presenting an accurate mental model; the issue in this case for me is that the error does nothing to teach me what the mental model is. It just looks like some internal diagnostic. Tbh I didn't even realize this is the error message I'm supposed to care about.

[Dan Abramov]

In particular, I did not even notice ℕ in the error message because it's printed right after NonUnitalNonAssocRing. So I missed that it's a "Thing A doesn't work with thing B" kind of thing.

[Kyle Miller]

NonUnitalNonAssocRing ℕ is the actual Lean expression for the type though. Typeclasses in Lean are nothing more than a way to automatically insert arguments for you. (While doing some backtracking Prolog-like search to piece the instances together, since instances themselves can have instance parameters too.)

[Kyle Miller]

I do think there is some sort of bug in the error reporting. Somewhere in the system it has the match it found, and the failure to synthesize the instances is causing it to throw that away.

[Dan Abramov]

What I don't see is how it connects to my code. Missing ℕ is my bad, sure. But even then, it would help to at least know which argument failed to match, or that indeed it's one of the arguments that was failing. To give a sense of where I'm coming from — something like https://elm-lang.org/news/compiler-errors-for-humans is inspiring, and I'd like to see more Lean errors feel "connected" to the code being written.

[Kyle Miller]

The issue though is that there's no argument that failed to match though, unless by "match" you mean this instance synthesis subproblem failure

[Kyle Miller]

I do agree that this can be better

[Kyle Miller]

I'm just trying to work out which part is the underlying problem

[Dan Abramov]

Looking at this code:

Screenshot 2025-02-20 at 03.30.28.png

I see a few ways to interpret the mistake, as a chain from the root cause to the surface:

• Root cause (user error): The user is using a wrong mul_sub
  • One degree of separation: The user is passing a Nat there. But this mul_sub doesn't take a Nat — it takes a NonUnitalNonAssocRing.
    • Two degrees of separation: Perhaps Nat is a NonUnitalNonAssocRing? But we weren't able to find a way to treat Nat as a NonUnitalNonAssocRing. Alas :(

To me, the issue is that the error message effectively only reports the innermost problem. It's very hard to notice the tiny part that's relevant in the hovered box, and to connect it to my code.

Screenshot 2025-02-20 at 03.30.28.png

I'm not sure what to propose concretely, but I'd like to see more of the "problem chain" reflected in the user-visible diagnostics.

[Kyle Miller]

Let's be sure to disentangle two issues:

1. There's the issue that it reports "no match found" with metavariables. This should not be there. It's a red herring, and it is throwing people off. In fact, I fixed this mul_sub c example in lean4#6891.
2. How to report synthesis errors in terms in general.

[Kyle Miller]

With 2, the synthesis error is the general one. It's exactly the same as if you had done

have h := mul_sub c
rw [h]

You'll get the synthesis error on mul_sub c. It's a function application, and it fails to fill in the instance argument, like in any other instance synthesis failure.

I agree that the failure should have some more information, but there's not a great chain-of-reasoning story here.

[Dan Abramov]

Yea. I'm trying to look at this holistically (we've not "solved" the problem until the entire flow is good, even down to how it's displayed in VS Code) but mostly focusing on (2) now.

Basically, my problem in (2) is that you have to know that if a function takes A and you give it B, Lean will need "synthesize" B A" by searching for instances of that, and then if it doesn't find it, it'll complain about that. But knowledge is not appropriate to expect at the user education level when this error shows up. This error shows up all the time to beginners. I've been learning Lean almost full time for several weeks and I still have no idea how typeclasses work or what instances are or any of that. So it's not appropriate to make understanding this a hard dependency for solving this error message.

[Dan Abramov]

It's a function application, and it fails to fill in the instance argument, like in any other instance synthesis failure.

What is the instance argument in this case? Is it α? Is it c? Which argument does the error refer to?

[Kyle Miller]

I mean [NonUnitalNonAssocRing ℕ] itself. That's the instance argument.

[Kyle Miller]

nat_sub's second argument is a structure that packages up all the data and proofs of a non-unital non-associative ring (whatever those are). It's implicit, and it's synthesized by the typeclass system based on available instances.

[Kyle Miller]

The name of the argument is unspecified. Instance arguments are generally never passed to nor referred to by name.

[Dan Abramov]

I see. So the real chain of what happened was:

• I passed c which is Nat
• This inferred the type (a b c : α) to be (a b c : Nat)
• This means [NonUnitalNonAssocRing α] became [NonUnitalNonAssocRing Nat]
• But there is no such thing, hence the error

?

[Kyle Miller]

You could write [inst : NonUnitalNonAssocRing Nat] as well, to give it a name.

[Kyle Miller]

Yes, correct.

[Dan Abramov]

I get that failing to instantiate some term is a general error but can this error be special-cased in this more specific circumstance (instance arguments)?

[Kyle Miller]

This is the error in that special case. The error is missing the word "instance"

[Kyle Miller]

If you see "could not synthesize placeholder", that's a more general failure. There's also "type mismatch" errors, which come from failed coercions.

[Dan Abramov]

I feel something like this would feel clearer:

Could not pass [NonUnitalNonAssocRing α] for α = ℕ because no
instance of NonUnitalNonAssocRing ℕ has been defined.
Either you're passing incompatible arguments or missing an import.

What do you think?

[Kyle Miller]

Trying to make this "cannot synthesize" error better for new users is a very hard problem:

• Typeclass synthesis is a fundamental feature that is used pervasively by the entire library.
• Everyone sees this error all the time, new users and experienced alike. We can't put an entire manual here. There's room for improvement of course, and at the least a reference manual link.
• There's no system to trace why a particular unification happened, so we can't currently try to explain what chain of reasoning led to the system looking for this instance. There are still some things we could do better here, like show the function application where the failure occurred, to let users see what types were inferred.
• Mathlib is designed to be very general. This leads to unfamiliar algebraic structures like NonUnitalNonAssocRing, and it makes it harder to get into the system. The antipode would be having a mul_sub per type, which is not scalable.

[Dan Abramov]

Yeah I sympathize with this being a hard problem. Curious what you think about the proposal above. I don't want to make it a mouthful if it shows up all the time but the key thing it fails to convey right now, IMO, is where its "two sides" are coming from. It just says "can't do A B" but A is coming from my code and B is coming from a library. It's not obvious how the system "got to" A B. Even if it reads technically, I think making the "we tried to match the inferred A with expected B" somewhere would be very valuable instead of failing at the last moment (A B failed).

[Kyle Miller]

Here's another attempt:

While elaborating the expression
  mul_sub c
the instance implicit argument of type
  NonUnitalNonAssocRing ℕ
could not be synthesized.

This could be because of a missing instance, a missing import,
or incorrect arguments.

[Dan Abramov]

In this case, the decision to "put A and B together" is something that Lean chose to do when matching up expressions. I didn't write A B in my code. So I feel like presenting the error from the perspective of A B failed is wrong. It needs to "backtrack" the explanation to what I'm aware of as a user, if that makes sense. That's the philosophical principle I'm trying to stick to. Of course, if my code said A B, it would be a different story.

[Kyle Miller]

You did (indirectly) write A B in the code though. It's in the type of mul_sub, which you used.

I get what you're saying, but there are many many places in Lean where when you write something somewhere, it gets unified into another position.

[Dan Abramov]

Yea. I guess I'm advocating for the compiler errors to try to track these unification decisions and special-case some of them with better error messages.

[Kyle Miller]

Right now, the best we have would be to print out the type of mul_sub, or to print out the instance argument in that type, and hope the variable name alpha doesn't shadow anything in the local context, making things horribly confusing

[Dan Abramov]

If we can't do that, I wonder if we can keep the [ and ] in the error message. This would serve as a strong hint that it maps 1:1 to the signature, which I think would provide the intution for what the "instance argument" is. I didn't understand the notation until you said it's an argument and it's literally being filled in.

[Kyle Miller]

At least with the error message proposal I suggested:

1. You can hover over mul_sub to see its type.
2. "instance implicit argument" is the key phrase. I'm not sure this error message is the place to learn about [...] being an instance implicit argument, but I'm sure we could make something short to put there, but in any case "instance implicit argument" can be searched for in the manual.

[Dan Abramov]

Is this too long?

While elaborating the expression
  mul_sub c
the instance implicit argument
  [NonUnitalNonAssocRing α]
was inferred to be
  [NonUnitalNonAssocRing ℕ]
but could not be synthesized.

This could be because of a missing instance, a missing import,
or incorrect arguments.

[Kyle Miller]

Do you think it would be confusing if a user had alpha in their local context? This alpha and the local context alpha are different.

[Kyle Miller]

Example:

example (α : Type) [Mul α] [Sub α] (a b c : α) : a * (b - c) = a * b - a * c := by
  rw [mul_sub a]

[Kyle Miller]

(A better example would have alpha here be for a different type not involved in the goal, but I hope that's enough to point toward the general issue)

[Kyle Miller]

It's not great when error messages have elements that are valid in different local contexts.

[Dan Abramov]

Yea that's fair. I suppose just the formatting changes would go a long way — I probably wouldn't have missed ℕ in the message with this formatting.

[Kyle Miller]

How about this?

failed to synthesize the instance implicit argument
  [NonUnitalNonAssocRing ℕ]
while elaborating the application
  mul_sub c

This could be because of a missing instance, a missing import,
or incorrect arguments.

[Dan Abramov]

Yeah this is a significant improvement IMO!

[Dan Abramov]

:shipit:

[Kyle Miller]

I'm not sold on including the square brackets; I worry it might looking like a one-element list.

It's more grammatical writing

failed to synthesize the instance implicit argument of type
  NonUnitalNonAssocRing ℕ
during elaboration of the application
  mul_sub c

[Kyle Miller]

Want to make a Lean 4 issue to track this? This isn't a five minute job (or I might do it right now), and it'll take work getting the right information to the right places to generate this error.

[Dan Abramov]

I'd appreciate if you could do it (a bit late for me so I should really go to sleep)! And thanks for sticking with me here.

[Kyle Miller]

Ok, I'll star the message and get around to it at some point :-)

[Patrick Massot]

Dan Abramov said:

I've been learning Lean almost full time for several weeks and I still have no idea how typeclasses work or what instances are or any of that. So it's not appropriate to make understanding this a hard dependency for solving this error message.

This is suggest there is something very suboptimal with your way of learning Lean, and working on that is probably more immediately useful for you than working on error messages (but improving error messages is always great, even if it requires users to read them). The type class system is a very very core component of Lean. What resource are you using to learn Lean? We can probably help you find a suitable place where you can learn about type classes.

[Kevin Buzzard]

I learnt them from #tpil which has a section on them.

[Patrick Massot]

There are explained in many different places, but not every place will be equally accessible depending on what Dan read before, that’s why I’m asking about his current learning resources.

[Patrick Massot]

Something else that could be useful to point out: Dan, you should be very careful whenever you use subtraction of natural numbers. This is a very weird operation since it has type ℕ → ℕ → ℕ so it’s bound to do something weird to a - b when b is greater than a (namely it returns 0). So you shouldn’t expect any general lemma about subtraction to apply to ℕ. For instance that Nat.mul_sub actually takes some thinking. It’s kind of a miracle that it actually holds, and the proof is completely different from the proof you would do for a ring (say for ℤ).

[Patrick Massot]

So, before seeing any error message, the first survival trick is to look at the statement and think “this statement is cursed, because it has a natural number subtraction, should I reconsider?”

[Dan Abramov]

I mean, I’ll sure get to them — I understand they’re pretty important. I’m going through Mathematics in Lean and I’m on the fourth chapter now. However, I don’t think I can agree with your statement — of course they’re important to learn by the time you’re doing real stuff, but if we just think from the perspective of learning order, learning to apply theorems about numbers comes way before. And if you can run into an error at that point, the error should be comprehensible.

My background is not in academy (it’s web development). And I want to stress that I’m not just raising this because I got stuck and am uniquely averse to learning typeclasses. I’m raising this because I see it as a basic usability issue that impedes learning. Learning about typeclasses will be important, but it shouldn’t “block” you from understanding what amounts to a basic type error in other languages. I don’t propose to fundamentally change something here, but to make the diagnostic slightly more suggestive so that it provides the right intuition (and if anything, can serve as a starting point to learn about typeclasses). And because my background is not in academia but in mainstream software development tools, I’m trying to apply a slightly higher standard to usability because that’s important if we want a broader audience to not get stuck learning Lean. Hope that makes sense as a motivation.

[Patrick Massot]

Improving error messages totally makes sense! It’s a never ending quest, and I certainly hope this thread contributes to it.

[Patrick Massot]

And indeed MIL will tell you about type classes but a bit later since, as you point out, they are not really needed at this stage.

[Patrick Massot]

Is the exercise with natural number subtraction that started this thread in MIL? If yes then I will definitely fix that trap.

[Dan Abramov]

I got into it from this exercise in chapter 4:

example {m n k r : ℕ} (nnz : n ≠ 0) (pow_eq : m ^ k = r * n ^ k) {p : ℕ} :
    k ∣ r.factorization p := by
  rcases r with _ | r
  · simp
  have npow_nz : n ^ k ≠ 0 := fun npowz ↦ nnz (pow_eq_zero npowz)
  have eq1 : (m ^ k).factorization p = k * m.factorization p := by
    rw [factorization_pow']
  have eq2 : ((r + 1) * n ^ k).factorization p =
      k * n.factorization p + (r + 1).factorization p := by
    rw [← factorization_pow', ← factorization_mul', mul_comm]
    · exact npow_nz
    norm_num
  have : r.succ.factorization p = k * m.factorization p - k * n.factorization p := by
    rw [← eq1, pow_eq, eq2, add_comm, Nat.add_sub_cancel]
  rw [this]
  rw [← Nat.mul_sub] -- forgot to put Nat. here
  apply Nat.dvd_mul_right

Adding Nat.* hasn't been a habit for me because earlier chapters mostly used theorems without prefixes and I forgot that.

[Dan Abramov]

Another nit I want to raise is that the Additional diagnostic information may be available using the set_option diagnostics true command. addendum is distracting and should IMO be at least separated by an extra newline from the actual error. It's not helpful here and makes scanning the error message more difficult.

Screenshot 2025-02-20 at 12.37.37.png

[Patrick Massot]

Ok, that’s definitely not the intended solution, as hinted at by

At the very end, you can use Nat.dvd_sub' and Nat.dvd_mul_right to finish it off.

but it’s a natural thing to do anyway.

[Dan Abramov]

Ah yeah fair enough, I kind of enjoy avoiding hints at this point and trying to bruteforce it myself.

[Dan Abramov]

Feeling silly but I just spent another 20 minutes on this exact set of errors.

My code, simplified, was this:

import Mathlib

theorem bla (n : ℕ) : n / 6 * 6 = n := by
  rw [div_mul_cancel]
  ring

I got this useless error:

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ?a / ?b * ?b

n : ℕ
⊢ n / 6 * 6 = n

But it was, of course, literally that pattern!

Then I remembered about this issue and tried

theorem bla (n : ℕ) : n / 6 * 6 = n := by
  have := div_mul_cancel n 6

to see if I might get a more helpful error message and now I was getting

failed to synthesize
  Group ℕ

At this point I spent another 10 minutes because I thought ℕ was a group (but it really wasn't) and I must be doing something else wrong (but ofc it's not a group).

I know this is user error etc, just conveying how it felt to use this.

[Floris van Doorn]

If you import all of Mathlib, and Lean cannot find an instance about a basic type, like ℕ, ℤ, ℚ, ℝ, ℂ (and more), a very good heuristic is that the instance is actually false.

[Patrick Massot]

This is indeed exactly the same issue as this morning: it has not much to do with type-class synthesis but a lot to do with dangerous operation on ℕ. Your statement is simply false. For instance 1 is a counter-example.

[Patrick Massot]

This time the issue is not subtraction but division.

[Patrick Massot]

Again division on ℕ has type ℕ → ℕ → ℕ, so it cannot be what you think it is.

[Dan Abramov]

Right, I understand what the issue is, I just wish the cause was more clearly communicated.

[Patrick Massot]

The FRO is working on that.

[Patrick Massot]

And I’m working on rewriting the MIL example we discussed before to avoid creating that risk.

[Kim Morrison]

Dan Abramov said:

Another nit I want to raise is that the Additional diagnostic information may be available using the set_option diagnostics true command. addendum is distracting and should IMO be at least separated by an extra newline from the actual error. It's not helpful here and makes scanning the error message more difficult.

Screenshot 2025-02-20 at 12.37.37.png

This one at least is easy to implement: lean#7169. I've asked Kyle and @Joseph Rotella to review; I let them merge if they're happy.

[Kim Morrison]

Just chiming in late here, but I agree with Dan that these are amongst the least helpful common messages from Lean!

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ?a / ?b * ?b

when the pattern is obviously there is just frustrating.

So Dan, despite our various pushbacks and explanations that it's complicated to fix --- we are grateful for you taking the time to explain your unhappy encounters with error messages. It is really helpful to hear the new-user-but-knows-UX perspective, as too often we've just got used to these issues.

[Damiano Testa]

When lean throws the did not find instance error, could it also add a line after saying where the appropriate type(s) satisfy `[typeclass assumptions]` ?

[Patrick Massot]

Kim Morrison said:

Just chiming in late here, but I agree with Dan that these are amongst the least helpful common messages from Lean!

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ?a / ?b * ?b

when the pattern is obviously there is just frustrating.

Of course it’s super frustrating, I don’t think anyone denied that! And it stays frustrating after many years of seeing that message. It’s improving (the failed instance synthesis message is already great progress) and I’m very optimistic we will soon see the end of those messages.

[Patrick Massot]

Reading back quickly that thread after seeing Kim’s message mentioning “pushbacks”, I’m sorry that it may sound like that. I think one issue is that knowing that Dan has a strong programming background probably led us too quickly into super technical discussion territory without spending much time on the “yes that error message is frustrating” part.

[Kyle Miller]

@Damiano Testa There's a suggestion here: #lean4 dev > Misleading error message on type mismatch @ 💬 (and a couple messages up). I'm interested in seeing how you'd incorporate your suggestion in a concrete example.

[Kyle Miller]

Kim Morrison said:

Just chiming in late here, but I agree with Dan that these are amongst the least helpful common messages from Lean!

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ?a / ?b * ?b

when the pattern is obviously there is just frustrating.

I hope it didn't seem like I was pushing back on this being a problem! In #lean4 dev > Misleading error message on type mismatch @ 💬 (maybe there's a better message, it's a long thread, and I was slightly confused in this one because there are lots of errors under consideration) I was calling this a bug. It's not too bad to fix. There are two solutions: (1) record the first match that results in an instance failure and using that match in the error message, or (2) trying to rewrite again without doing instance synthesis while matching, and then doing instance synthesis afterwards once a match is committed to, which generates the error.

Edit: Oh, I really misunderstood the issue here. I wasn't thinking about how the failure is that the implicit arguments aren't of the right form (I imagined there were instances that needed solving after the match). My first thought is to retry matching with all the implicits cleared, but I'll have to think about this...

[Damiano Testa]

I like the suggestion above, actually. One thing that I also like about the suggestion is that it no longer uses instance to mean something that is not the "command" instance.

[Yakov Pechersky]

Is it possible to also, for a rw failure of this sort, to track the syntax of the attempted rewrite and the syntax of the location to be rewritten, and notice when they pp the same? And in that case, do a ^^ style indicator with a pp.all to highlight the difference?

[Kyle Miller]

I've got a first approximation of a more helpful error on match failure (lean4#7172).

The way it works is that if there is no match, it tries to diagnose if the failure is because there are instance arguments that are failing to unify. To do this, it takes the pattern, it replaces all the instance arguments it can with metavariables without making the pattern type incorrect, and then looks for a match again. If there is a match, then it uses the match to produce a "has type expecting type" style error:

theorem mul_sub' (α) [NonUnitalNonAssocRing α] (a b c : α) : a * (b - c) = a * b - a * c := sorry

example {a b c k : Nat} : k = c * (a - b) := by
  rw [mul_sub']
  /-
  tactic 'rewrite' failed, did not find an exact match for the pattern
  in the target expression

  Found approximate match
    c * @HSub.hSub Nat Nat Nat (@instHSub Nat instSubNat) a b
  but expecting pattern
    c * @HSub.hSub Nat Nat Nat (@instHSub Nat SubNegMonoid.toSub) a b
  -/

[Kyle Miller]

It's not great to look at, but there are still some improvements that can be made here. For example, given the match, it can try synthesizing the instance arguments for the rw lemma. That can diagnose that the problem is that it doesn't apply because there's no NonUnitalNonAssocRing Nat instance, and report that rather than showing a confusing-looking diff with @'s.

Imagine something like

tactic 'rewrite' failed, did not find an exact match for the pattern
in the target expression

Found approximate match
  c * (a - b)
but instance implicit arguments in the pattern
  c * (a - b)
require the following instance, which cannot be synthesized:
  NonUnitalNonAssocRing Nat

[Jovan Gerbscheid]

Kim Morrison said:

Dan Abramov said:

Another nit I want to raise is that the Additional diagnostic information may be available using the set_option diagnostics true command. addendum is distracting and should IMO be at least separated by an extra newline from the actual error. It's not helpful here and makes scanning the error message more difficult.

Screenshot 2025-02-20 at 12.37.37.png

This one at least is easy to implement: lean#7169. I've asked Kyle and Joseph Rotella to review; I let them merge if they're happy.

I agree with the newline, but I would argue that the message about set_option diagnostics true is not useful at all. I almost never use this command. If I want to investigate a type class synthesis failure, I use set_option trace.Meta.synthInstance true (possibly combined with trace.Meta.isDefEq or trace.profiler). So if anything, I think the error should mention trace.Meta.synthInstance. (though in this example that isn't too useful either)