[James_K]

> The meaning of `T | null` and the meaning of code you write with such a type does depend on what T is at runtime.

Could you give an example of this? The only case I can imagine is a union null <=: T, T | null. This would cause unexpected behaviour, i.e. a if T = (U | null), the function orElse : T | null → T → T would always return the second argument if the first is null, but this is perfectly consistent with the fact that T itself is a union type. The idea that it should do anything different is presuming that the null assigned to T is different from the null assigned to T | null (that union types are disjoint). But this is an invalid assumption. It's still a validly typed program that obeys a consistent set of rules. It's just that there is no tagging in the union type (you don't know if a member comes from the left or right side). This is only an issue if you write code expecting the union to work like a tagged union.