Separately, it is also OK to talk about A | B when you don’t require that they be disjoint, but only if any treatment that you apply to an A is also valid if you apply on a B, and conversely. So there are cases where a non-disjoint union can be correct—which means the compiler can’t outright reject non-disjoint union even if it were smart enough to prove them—, although some extra care is also required in that situation.
1 Like