resuming synthesis

Stream: lean4 dev

[Reid Barton]

Johan and I looked into one instance-related performance issue a while back, where specifying an "obvious" type explicitly was the difference between succeeding instantly and a timeout.

Say that trying to apply a lemma causes the creation of two new metavariables ?t : Type and ?i : Ring ?t. In the example we were looking at Lean decided to try to synthesize ?i first, which wouldn't have occured to a human as the thing to do, but needn't have been fatal. As soon as it tried to use any specific Ring instance it determined it needed more information about ?t.

At this point it switched to unification, quickly learning that ?t had to be in this case Real. But then it kept doing unification, which turned out to be a really bad idea for various reasons, related in part to eta for structures and the issues related to lean4#2003, meaning that by the time we give up and synthesize the instance instead, we've created a hugely expanded set of unification problems.

If, instead, we provided the type ?t := Real explicitly, then instance synthesis was fast and the defeq test was also fast (it involved just a couple layers of unfolding).

Has there been consideration of a mechanism whereby, if instance synthesis blocks because we don't yet have enough information about a metavariable, we eagerly resume it when that metavariable gets assigned?

[Reid Barton]

This seems not only likely better for performance but also truer to the original intent (we wanted to determine ?i by instance synthesis in the first place).