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:
panagosg7
commented
8 years ago
It turns out it's not safe to even drop the refinements of the union top-level to the parts of the union:
The reason is that
pcould include predicates of the formv = xwhich would cause "sort mismatch" if dropped to thetis. 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