Description
The new fulfillment context introduced in #30533 could be more efficient in a number of ways in terms of pruning the work it has to do. First, it currently considers obligations to be formed in a tree, but really it ought to detect arbitrary DAGs and avoiding adding needless work. In particular, if a given obligation O is also found elsewhere in the tree -- but NOT as an ancestor! -- then we can drop it. We have some limited support for this where we drop duplicate siblings. This may be good enough, but we can do better.
It seems like we could integrate this with cycle detection. Currently, we wait until the overflow counter trips and then walk back up and look for a cycle. This is perfectly fine. But I could also imagine that we might have some kind of per-tree hashtable (the current ObligationForest doesn't support "per-tree" data, but it seems like an easy enough extension) that tracks obligations currently in the tree. If we find when adding a new obligation O that it is already present, then we could go look for a cycle and otherwise consider it a duplicate. This seems nice, but there is a wrinkle.
In particular, I am wary of getting things wrong around inference variables! We can always add things to the set in their current state, and if unifications occur then the obligation is just kind of out-of-date, but I want to be sure we don't accidentally fail to notice that something is our ancestor. I decided this was subtle enough to merit its own PR.
Another related issue is that it's not clear when is the best time to refresh inference variables. We might be able to find a perfect time, or maybe we should just make it very cheap to do and then do it all over the place.