Handle negative cycles correctly in the recursive solver #526
Conversation
It's not really needed. The idea is to make an assumption about the recursive case and then compute answers based on that assumption -- we can then update the solution with the new one, we don't have to *merge* them.
This implements the scheme described in the book edits from the previous commit. In particular: * refuting a goal on the stack is always ambiguous * we do not cache results that were dependent on a negative cycle
|
To review, I would recommend reading the "document how negative cycles work" commit first. |
|
Wait so we're actually going to handle negative cycles in the recursive solver? Is it worth it? And, if so, should we add it back to the SLG solver? |
|
@jackh726 Good question. It's fairly easy to handle in the recursive solver, in any case, and the old behavior was just wrong. I'm not sure if we really need to be able to handle negative cycles or not, I feel like I had an example of a case where we might need to, probably involving specialization, but I don't remember the details. I left a comment about it somewhere. UPDATE: This comment and the one after it are the cases I was thinking of, I believe. However, I realize now that, at least in the current rustc code base, I think that a test like this would result in a cycle error, because we do not allow you to construct potential specializations unless there is a strict DAG between the traits (and here, the |
| return *minimums; | ||
| } | ||
|
|
||
| let old_answer = &self.context.search_graph[dfn].solution; |
There was a problem hiding this comment.
so was all the priority handling here just not necessary, or is it somehow subsumed by the negative cycle handling? 🤔
There was a problem hiding this comment.
I think this comment is referring to the changes in the first commit, which remove the logic that merges the "previous answer" (from prior iteration rounds) with the "new answer" (from the current iteration round). I don't believe that logic was ever necessary, precisely because of the monotonic nature of solving -- i.e., each round should be producing strictly more answers than the round before, so it should include whatever answers we were getting before. The only exception would be negative cycles, but we are always producing the same result for those ("ambiguous").
There was a problem hiding this comment.
Hmm I do remember adding it for a reason -- though I wonder whether I didn't manage to write a test for it, or whether that just works now. I think it was related to the fact that the priority logic does break this monotonic nature -- you can get a solution involving Trait::AssocType<> in the first round, and then get the properly normalized type in the second round. (The priority logic could maybe be interpreted as having a "not (the normalize rule applies)" in the fallback rule?)
There was a problem hiding this comment.
Hmm, good point! I remember us discussing this a bit. Sigh, things are complex. =) I guess we should see if we can craft an example where this actually causes a problem. I can imagine some cases where it might.
One situation would be around the infamous logic like
trait SomeTrait {
type Item: Eq;
}
fn foo<T, X: SomeTrait<Item=T>>() {
}where we (in rustc) fail to figure out that T: Eq.
There was a problem hiding this comment.
Still, I think it was important to remove that "merge with the old result" logic -- but maybe more for the coinductive case than for this negative cycle handling, actually.
| G2 :- not { G1 }. | ||
| ``` | ||
|
|
||
| Here we have a negative cycle for `G1`, but only through one of the two |
There was a problem hiding this comment.
The other clause will give back a positive result.
I might be missing something by how would that be. Isn't this other clause G3. If so how does it give a positive result if there is no rule for it?
There was a problem hiding this comment.
Sorry, that's confusing. G3 is the "other subgoal". The other clause is the clause G1., which is trivially true.
There was a problem hiding this comment.
I'll try to rework the test to make it clearer at some point.
There was a problem hiding this comment.
I think the 'other clause' here is G1.
|
Hmm so @jackh726's comment about "Do we really want to support neg cycles" is on the money -- since, if we don't, it's going to simplify greatly the salsa integration. It's easy enough to extend the recursive solver to support them, but I think it's harder to "generalize" the concept, at least it's less obvious to me how to do it. i guess it's really worth trying to look carefully at those places we use |
|
I'm going to close this for the time being. |
This also includes a chapter in the chalk book explaining how it works.
This includes that first commit from #399 (and some further cleanups).
cc @flodiebold @zaharidichev