Managing union refinements

[panagosg7]

It turns out it's not safe to even drop the refinements of the union top-level to the parts of the union:

{ t1 + t2 + ... | p } ---> { t1 | p } + { t2 | p } + ...

The reason is that p could include predicates of the form v = x which would cause "sort mismatch" if dropped to the tis. Even dropping a K-var could be dangerous as a seemingly non-existing predicate of that sort could emerge as part of a K-var instantiation and violate a sort check.

Here's an example that throws an exception due to sort mismatch:

https://github.com/UCSD-PL/RefScript/blob/union_preds/tests/pos/unions/noundef-02.ts

[panagosg7]

Added as a "todo" test here:

https://github.com/UCSD-PL/refscript/blob/15ccd4ff8fc4d6447eb842bf6d5f1b283a74decf/tests/todo/pos/unions/or-undef.ts