So I think the bug would actually show up in this situation:
// Send is coinductive: Send(X) :- Foo(X), Bar(X). Foo(X) :- Send(X)
If we were (say) solving
Send(u32), then we would go to solve
Foo(u32) and conclude that -- since
Send(u32) is on the stack --
Foo(u32) is true.
But, in fact, we will later disprove
If we used a delayed literal instead, then the result of
Foo(u32) would be
Send(u32) | (i.e., with a delay), and we would ultimately reject it as false.
So one thing i'm wondering here though -- can we solve this by always selecting "inductive" goals first?
I think I had convinced myself we cannot but now .. I'm wondering why
ah, well, of course
all the predicates could be coinductive