!4#2790 rfl failure

Stream: mathlib4

[Oliver Nash]

In !4#2790 I had to replace a proof term rfl with by dsimp. I commented about this on GitHub here. I'd like to understand this.

[Oliver Nash]

The apparent failure of rfl in this situation is new to me: Lean just pegs a CPU at 100% and nothing happens even after leaving my laptop in this state for several minutes. The replacement by dsimp is essentially instant.

[Oliver Nash]

Has this failure mode been seen before? Any guidance on how to debug this would be very welcome.

[Jireh Loreaux]

Did you try tracing the simp lemmas? Just to see what's being applied.

[Kyle Miller]

@Jireh Loreaux The dsimp is able to prove it because it applies two rfl lemmas, which is probably better than a definition-unfolding rfl proof anyway.

[Oliver Nash]

@Jireh Loreaux Yes I did and so did Kyle (the two lemmas are coe_restrictScalars and Algebra.coe_top). I also added one more comment on GitHub which I will copy here.

[Oliver Nash]

I just let it run even longer and it did eventually timeout after almost 8 minutes with the expected message:

(deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

Even though I agree that by dsimp is a better proof, I'm still very disappointed that rfl fails on something as simple as this, especially given that it works instantly in Lean 3.

[Jireh Loreaux]

I wonder if this is an in-practice example of the subject reduction issue?

[Oliver Nash]

I doubt it, though I'm only basing this opinion on the fact that (as far as I know) we never encountered the SR issue in > 1m lines in Mathlib3.

[Eric Wieser]

It's possible that structure eta makes it more likely to happen

[Eric Wieser]

(combined with the switch to new-style classes such that structure eta is regularly needed in unification)