Prevent false positives in coinductive cycles for recursive solver

[firefighterduck]

This PR is meant to address the issue of false positives in coinductive cycles as described in #399 . It also fixes the two coinduction tests related to that issue (i.e. coinductive_unsound1 and coinductive_multicycle4).

The PR adds a simple mechanisms to delay caching of results inside the coinductive cycle and to store only valid results that can not be false positives. This is done by a simple over-approximation that could potentially increase runtime. The exact mechanism is also described in the corresponding book chapter. In general, it follows the idea from #399 to start with a positive result instead of the negative one but delays its effects on other goals until it is know whether this assumption was correct.

Albeit the mechanism comes with two new tests and was also rather carefully designed, there could be some edge cases that I missed where the delayed caching introduces new problems. Thus the draft status. I'd be thankful for any comments and thoughts on this.

[jackh726]

I still don't know enough about the recursive solver to be able to comment on this in any meaningful way.

Going to cc @nikomatsakis and @flodiebold since they might have better feedback.

[jackh726]

Hmm. So, one consideration here comes with the idea of negative coinduction cycles. Currently, we don't allow them (in SLG; in recursive, they might still be allowed?). But the assumption is here is that an invalid solution is okay because it can never be used to "prove" coinduction. Is this correct?

[firefighterduck]

Yes, that's correct. It might be a false assumption on my side, yet I'm still looking for examples where the approach doesn't work as intended. Regarding negative cycles in general, I did not really think about them as #526 seems to indicate that they are currently not supported/needed in the recursive solver.

[firefighterduck]

While thinking about this rather "hacky" solution, I had a more elaborate idea:
The solver could have another dedicated cache for solutions that depend on the initial assumption of a coinductive cycle. With this it should be simple to delay the actual caching until it is known whether they would hold. The only problem with this approach is that the solver has to somehow track which solution depends on the assumption and forward this information through several layers. This might need some greater restructuring of the recursive solver.
I'll try to sketch this out in an other branch. A sketch for this (with not that much documentation) can be found here: master...firefighterduck:coinductive-recursive-cache

[firefighterduck]

So, I thought a bit more about both approaches:

1. The "hacky" one: this dos not work with negations (simple fix is possible) and does most likely not work if there are other cycles in parallel to the coinductive one. Thus, it improves the soundness a small bit with minimal changes.
2. The two level cache: this does not work for nested coinductive cycles where only the inner fails. This reduces the likelihood of false positives relatively good and thus improves the soundness quite a bit. Unfortunately, it requires a whole lot of changes to the structure of the recursive solver. Adding an own cache for each nested coinductive cycle or tracking which cycle influenced a result would both be possible solutions to improving soundness but would most likely improve complexity even further.

I'm not sure whether either one of these approaches would be acceptable for Chalk but it might help finding an even better solution while improving soundness at least a bit.
I'll probably try implementing the mentioned improvements for the second approach but can't really say whether these are enough to actually solve the whole issue.

[firefighterduck]

Closed in favour of #690 .