Delete key operation?

[dszakallas]

Hi,

I am writing a wasm type checker in Rust, and I am using ena to help with operand unification problems arising during the validation of instruction sequences. Some wasm instructions can bind parametric arguments and I thought it would be much easier to use ena for unifying type parameters than implementing a hand coded solution. This requires me to create a single unification table for the whole instruction sequence, and in a forward chaining manner add a new key for each parameter encountered, possibly unifying some of the existing ones.
Of course the issue is that the UnificationTable just grows and grows while I am munching the sequence, while I only need the keys that are on the operand stack.

So I would need a way to delete keys from the UnificationTable for the symbols that are popped from the stack. This shouldn't affect the merged values, the table should forget about the key, not undo a merge (like reverting snapshots). Of course when the last member of the group is gone, the value should be dropped too.

Is this something that should be worth implementing, or is there a way to do this already and I just overlooked it?

[nikomatsakis]

@dszakallas I don't think we have a way of doing that now. That's kind of a major change to the way the tables work, since the general assumption in the design is that the indices remain valid and are only lazilly updated as needed. In other words, you'd need to do a kind of "global sweep" to ensure that no references remain to those intermediate keys that got created (and of course ena can't know if you have references from outside of its domain). I'm tempted to say that is a feature I would not want to support -- but then I'm also tempted to sort of retire ena or at least try to pull it apart and simplify it.