Crosscut

I said earlier, that different branches could evaluate to different types, and that those types could then be bundled into a variant. Let's take an if expression as an example. If its "then" and "else" branches evaluate to different types (let's say A and B), then the whole if expression could evaluate to variant { A, B }.

What if they evaluate to the same type X though? This would imply that the whole if evaluates to variant { X, X }, instead of just X, like we'd expect. And I think this example motivates another aspect of normalizing variant types: deduplication.

A variant { X, X } makes no sense, since there's no way to distinguish between those cases. So it would normalize to a variant { X }. Which could then be further normalized to just X. (Assuming automatic lifting is going to be a thing, that last step wouldn't make a difference anyway, semantically.)