unfreezeI

Stream: general

[Johan Commelin]

I've never understood what unfreezeI was for. But I know that we needed it because of "core". Now that "core" is no longer a reason... can we get rid of unfreezeI?

[Gabriel Ebner]

The "core" reason is deeply buried in type class resolution. IIRC, calling unfreezeI (partly) disables caching for type class resolution. @Anne Baanen tried to remove this caching mechanism, but apparently it's not entirely trivial.

[Sebastian Ullrich]

But the caching was actually broken for the longest time in such a way that unfreezeI etc wasn't necessary, until Leo fixed it. Can't that fix just be reverted? I don't remember anyone noticing any actual benefits such as better performance from the fix.

[Patrick Massot]

I have a more relevant question (I think). Do we know what will be the situation in Lean 4? We don't want to unlearn our instance cache management habits in Lean 3 only to relearn them when we'll switch to Lean 4? I don't expect Leo will change his mind on this question, but maybe the question itself will become irrelevant in Lean 4.

[Sebastian Ullrich]

I believe the plan is that all surface-level binders automatically reset the cache. Only tactics introducing instances internally have to worry about it.

[Patrick Massot]

I'm afraid I don't understand this whole story well enough to parse this answer.

[Patrick Massot]

Does it mean we won't need haveI and letI?

[Sebastian Ullrich]

Yes, unless you're a tactic writer and care about that level of optimization.