RFC regarding adaptions for lean#2793

Stream: nightly-testing

[Kim Morrison]

lean#2793 fixes lean#2736, a bug reported a while back by @Bhavik Mehta.

The change means that rw [f] is now interpreted as rw [@f], and this means makes inference of implicit arguments slightly weaker.

All through the linear algebra library we find errors like "can't synthesize Ring ?R", and we solve this by changing rw [my_lemma] to either rw [my_lemma ..] (which effectively restores the old behaviour) or rw [my_lemma (R := R)] (which is presumably what people encountering this error will do!)

See #8076 for the Mathlib diff.

I would like to feedback about how we think Mathlib users will cope with this change.

Secondarily, I'm happy to hear opinions on whether I should fix these errors as rw [my_lemma ..] or rw [my_lemma (R := R)].

The baseline plan is to merge this as is.

[Eric Wieser]

Changing to rw [(my_lemma)] presumably also fixes this?

[Eric Wieser]

That was the approach we used during the port to fix simp. I think we finally eliminated the last of these ()s in simp /simp_rw after a recent lean bump, so it feels like a bit of a shame for this behavior to reappear elsewhere

[Bhavik Mehta]

Perhaps I'm missing something, but it appears this doesn't fix the root cause as described by @Thomas Murrills in #2736? I'm also curious why the example as I reported it succeeds with this change, but the rw [my_lemma] example fails?

[Patrick Massot]

I think the rw [(my_lemma)] looks really awful and hard to explain to beginners.

[Eric Wieser]

I'm not sure rw [my_lemma ..] is any better, especially in the cases where the number of _s inserted by the .. is zero

[Eric Wieser]

There's already precedent for the (my_lemma) weirdness in #check (my_lemma)

[Thomas Murrills]

(I should probably tweak my comment on lean4#2736: this isn’t necessarily an “issue with” typeclass synthesis in elaboration per se, but is at least an issue arising from how ordinary typeclass synthesis is used in rw.)

I feel like handling of typeclass instance arguments in rw along the lines of “synthesize if we can, but if we can’t, don’t error and instead try to obtain the instance arguments by unification with rewritten subexpressions” might be the best of both worlds. (E.g. some sort of Term.withMaybeSynthesizing combinator, after not insisting on synthesis during initial elaboration.)

But I haven’t looked closely at this again (or the new errors), so I can’t say if this would actually be a viable approach.

[Kim Morrison]

It is too complicated to ask that the spec of rw is "try rw [@lemma], and then try rw[lemma ..], and see which one works better".

[Kim Morrison]

I'd prefer the discussion here be restricted to "can we merge lean#2793?".

[Kim Morrison]

I would like to. Despite the cost of the changes in #8076 (which are not actually that many!), I like the increase in predictability.

[Floris van Doorn]

I agree that there are not that many failures, so I can live with merging it.

Kim Morrison said:

I would like to. Despite the cost of the changes in #8076 (which are not actually that many!), I like the increase in predictability.

In what way is the predictability increased? In what cases would it fail before? In what cases does it fail now? I don't really understand the difference between before and after this fix.

In my proposal I was not asking for "try rw [@foo], and then try rw [foo ..]", but to see if there is a change that is the best of both worlds (something like "try type-class inference/auto-param inference both before and after matching with the goal"). It won't be as simple as that, but I don't actually know in what cases it would fail before/now...

If you want to restrict the discussion to "can we merge this PR" then the answer is clearly "yes, after you fix the CI issues in the mathlib PR". I thought that the question "is this PR desirable" would also be part of the discussion.

[Floris van Doorn]

Btw, I ok with merging that PR as-is. I just expect that very soon we'll get a new issue "rw [foo] fails, but rw [foo ..] works".

[Kim Morrison]

No, no, I want to know "is this desirable".

[Yaël Dillies]

Floris van Doorn said:

In what way is the predictability increased? In what cases would it fail before? In what cases does it fail now? I don't really understand the difference between before and after this fix.

Same here, I failed to parse the relevant discussions

[Floris van Doorn]

I don't think we can answer that without knowing in what situations rw [@foo] fails vs rw [foo ..] fails (and is that the same as rw [(foo)]?).
My guess is that is has to do with the order of operations: things like "will it already fire type-class inference during elaboration, before matching against the goal". But there are probably more subtle issues.