Zulip Chat Archive

Stream: mathlib4

Topic: tc synthesis repeatedly tries the last one on the list

Matthew Ballard (Mar 25 2023 at 17:10):

Here is a trace from instance synthesis.

Spoiler

If I ban WithTop.commMonoidWithZero, it does the same with the next entry. What is going on here?

Matthew Ballard (Mar 25 2023 at 17:12):

To clarify, it does not appear to try any of the other instances

Matthew Ballard (Mar 25 2023 at 17:14):

Maybe lean4#2055?

Gabriel Ebner (Mar 25 2023 at 18:58):

tc synthesis repeatedly tries [...]

This is Lean repeatedly trying TC synthesis, not the other way around.

Gabriel Ebner (Mar 25 2023 at 19:03):

During elaboration, we try to synthesize the instance immediately and if that doesn't work it's put on a list of postponed constraints. At the end (or if you call synthesizeSyntheticMVars manually), we try to solve all these constraints. And if we make progress on any one of them, we try all of them again (because now they might succeed after an mvar might have been assigned etc.) in a loop until they've all been solved or we can't make any progress.

Gabriel Ebner (Mar 25 2023 at 19:03):

So this is very much expected.

Matthew Ballard (Mar 25 2023 at 19:11):

Thanks. I am still a little confused. There should or should not be something changing between the repeated apply @WithTop.commMonoidWithZero to CommMonoidWithZero ?m.851292?

Matthew Ballard (Mar 25 2023 at 19:37):

Maybe to spare everyone, what is the best documentation on this? Thanks

Last updated: Dec 20 2023 at 11:08 UTC