The fake GADT we now use for maps and unordered traversals and folds is a little bit unsafe. I thought that we were well protected by the fact that the queue would have to reach O(2^WORDSIZE) elements to cause a problem, but it's actually possible to do this in a reasonable amount of time on systems with 32-bit Word but addressable memory considerably exceeding $2^32$ words, if there are any such around. In particular, an adversary could calculate something like stimes (2^(2^32)) (singleton () ()). This will take quite a long time, and something in excess of 64 gigabytes of memory, but I think it's possible in principle.

Suppose someone uses traverseU on this monstrosity, with a Backwards applicative. I suspect they will be able to actually reach the point where underflow occurs, leading to an unsafe coercion and memory fault.

The easiest solution is to use Word64 instead of Word. I don't think it's realistic to produce a queue whose size exceeds $2^{2^{64}}$ by any means whatsoever. The downside is that this will hurt performance on 32-bit systems. I don't know how much we care.

The other obvious solution is to make sure we never underflow. The best way to do that is probably to perform a size check on insert and on union. This has the side benefit of ensuring that size always produces a correct value. The downside of course is that insertion becomes ever so slightly slower.