motive is not type correct solution

Stream: general

[Mirek Olšák]

It is probably well-known here but after being frustrated enough with the "motive is not type correct" error in rw in examples like

example (l : List ℕ) (a b : ℕ) (h : a + b < l.length) :
    l[a+b] = 0 := by
  rw [Nat.add_comm]

I finally learned that all I need is usually just replace rw with rw!.

I just thought that

1. Could the error message in rw mention this as the first option, rather than listing many other less reliable ideas such as occs, simp, or conv mode? I understand there might be a difficulty that rw is a core tactic, and rw! is Mathlib only, but it would really help.
2. @Jovan Gerbscheid , how hard would be to use DepRewrite in rw??, so that it doesn't fail on such cases, and recommends rw! to the user.

[Kevin Buzzard]

I think I heard from @Kyle Miller that rw was going to be beefed up to solve this problem once and for all?

[Mirek Olšák]

Some time ago, I have heard rumours about a a new promissed rw that could even rewrite under binders but I am not sure about the current status. Deprecating rw! to a strictly better rw in Core would be great of course,

[Jovan Gerbscheid]

I quote from the FRO year 3 roadmap:

"We will unify existing rewriting tactics, such as rw and simp_rw, into a single, more intuitive and powerful rewrite tool."

Which is indeed what Kyle Miller says that he'll be working on.

[Mirek Olšák]

Do not forget to include rw?? :wink: . By the way I tried it as a user quite a lot now, it is great (when it doesn't complain about dependent type hell). It is usually giving more useful ideas than apply? when clicked on the main goal. Of course, having to wait for 15 seconds after a click eventually gets a little annoying, and sometimes I am not sure if it registered my click, so a spinning wheel & speed improvement would be always nice.

[Martin Dvořák]

This week, I was fixing a lot of code generated by Mathport, and this issue was really annoying there.

[Jovan Gerbscheid]

Yes, I am currently working on a new version of rw?? that will be faster, and it will tell you that it is loading when it is loading, and the results are shown as they come in, potentially before all of the results are computed.

[Mirek Olšák]

Sounds great! And in case you are done before rw update, I would also consider using DepRewrite

[Jovan Gerbscheid]

By the way if you want to help, feel free to review my rw?? PRs, which currently are #31609 and #31608.

[Jovan Gerbscheid]

What do you think the right behaviour would be with suggesting rw!? Where in the interaction should there be an explanation of why rw was replaced with rw!? Should there be a warning above the rewrite suggestions?

[Mirek Olšák]

Jovan Gerbscheid said:

By the way if you want to help, feel free to review my rw?? PRs, which currently are #31609 and #31608.

Sounds fair, I can take a look on Tuesday / Wednesday.

[Mirek Olšák]

Jovan Gerbscheid said:

What do you think the right behaviour would be with suggesting rw!? Where in the interaction should there be an explanation of why rw was replaced with rw!? Should there be a warning above the rewrite suggestions?

Explanation is not necessary. Mainly do not fail on the "motive is not type correct". I can imagine two options, and don't have a preference.

1. Always suggest rw!.
2. Suggest rw! only when necessary (so try kabstract first, and replace with dabstract is kabstract fails).