type inference: fix bug in union-bound algorithm #289
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
We have logic to output `...` when a type gets too deep and to stop recursing at that point. Most notably this is useful when outputting an occurs-check-failing type. But the max depth is 64, so you can make a type of size 2^64 without hitting this limit, which will still blow out your memory and effectively stall. This can create pretty confusing symptoms when fuzzing for pathological programs -- you will get an apparent stall with no output, and no matter how many debug printlns you add it will appear that they all execute before the stall -- and it turns out that in fact all your code was working correctly up to the point of the final panic where it tries to *display* an occurs-check error. Cut off the display at 10000 nodes. If somebody really needs to output a text representation of such a thing they can write their own logic.
apoelstra
force-pushed
the
2025-04--invalid-encode
branch
from
c61d31f to
0a3fe2a
Compare
In the union-bound algorithm we track our unified type variables as sets, which are represented by trees of pointers, where the roots of the trees are used as set representatives for determining equality etc. When unifying variables, we move one's tree into the tree of the other, and then copy all its bounds to the root of the new unified tree. Most operations within union-bound are given an arbitrary set element and immediately locate its root before doing anything. We obtain better asymptotics by using the "halving" variant of union-bound, wherein on each root lookup, as we follow the path from the element to its root, we update the links to skip every other one. Basically, if node x points to its parent which points to a grandparent, we update x to point to the grandparent directly. *However* our existing code, rather than making x point to the grandparent, would just copy the grandparent over the parent. I'm not sure what I was thinking here -- I think I got tangled up trying to deal with Rust's multiple-aliasing rules without deadlocking and lost track of the actual algorithm, or maybe I misread Russell's C code which I was mostly copying from -- but the result is both weird and incorrect. In particular, if the grandparent is a root, then by copying its data into parent, we duplicate the root, effectively un-unifying the variable at some hard-to-predict point. Once the un-unification happens, then future unifications will appear to only get half-applied, the resulting type inference will be slightly wrong, we will produce programs which fail type-checking or sharing-checking after being encoded, even though they were successfully constructed. The fix, amusingly, actually reduces the amount of locking, which might provide a slight speedup, and will certainly make it easier to convince yourself that this code is deadlock-free. (Probably we should drop all these mutexes and just use raw pointers and unsafe code, which would be easier to follow; the mutexes serve no purpose other than to mollify the Rust typechecker; we assure type-safety by locking the entire slab, and locking individual set elements is neither necessary nor sufficient to get a thread-safe type inference algorithm.) Thanks to Russell O'Connor for identifying this bug, and some thanks to Claude 3.7-sonnet for producing weird not-quite-sensible "fixes" that would change observed behavior on our bad test cases, and pointed us to roughly the correct location.
You can rebase this PR to move the unit tests in front of the fix, and you will see that they both fail.
…code/decode roundtrip This construction algorithm is a bit fragile and will often fail but the fuzzer should be able to make some progress with it. In particular if, during construction, it encounters any type inference errors, it will fail. I used this to generate the unit tests in this PR.
apoelstra
force-pushed
the
2025-04--invalid-encode
branch
from
0a3fe2a to
f821e22
Compare
|
@uncomputable can you ack (or utack) this? |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
We have implemented the "halving" variant of the union-bound algorithm, but my code to do so was wrong in a way that sometimes causes types to "come ununified", i.e. a single type bound is split into two, with different instances in the program more-or-less randomly assigned to each side of the split.
This causes all sorts of weird behavior.
Fixes #286