once breaks backtracking references

[adamgundry]

I've been looking at guanxi with @np, and we came across an issue with the interaction between once and backtracking references. The essence of the problem is that once discards the failure continuation of its argument, but writeRef relies on the failure continuation being called in order to unwind the write. Thus any writes in the scope of once will not be backtracked. For example:

    it "backtracks a write under once if it succeeds" $ do
        rs <- observeAllT $ do
            x <- newRef (1 :: Int)
            (once (writeRef x 2 >> pure 2)) <|> (readRef x)
        rs `shouldBe` [2,1] `butIs` [2,2]

Prolog has cut (!) which is rather similar to once, in that it discards relevant choice points. However, Prolog implementations maintain separate representations of the choice point stack (like <|>) and the trail (the addresses of references that have been written). Thus even when cut is used to discard choice points, the trail can still be used to correctly revert writes when backtracking to an earlier choice point. Whereas in guanxi, backtracking to a choice point before once can lead to a state where writes are still visible.

This suggests a possible solution strategy: use a variant of LogicT that maintains an additional continuation for unwinding writes when backtracking, distinct from the failure continuation. Then once can discard the failure continuation but retain the backtracking continuation. This makes msplit slightly more complicated, because it has to reify both continuations, but it appears to work in practice.

I'll open PRs with tests demonstrating the problem, and a proposed solution that we came up with. Feedback on the approach we've taken would be very welcome.

[ekmett]

My most recent intention with the code was to go through and replace the current LogicT implementation based on Alexis' work on delimited continuations. Thoughts?