[rbehrends]

> The thing is, the values that satisfy this type are not subtypes of None and a pair. (That would be silly, given None.) Such a value is either None, or a pair.

Unless I'm misreading you, this seems to be a misunderstanding of what sum types are. A sum type `T = A | B` represents the (disjoint) union of all possible values of `A` and of all possible values of `B`, simply put, not the intersection (as you seem to indicate by the phrasing of "not subtypes of None and pair"; correct me if you meant something else).

Recall what subtyping means (I'm going with Wikipedia's definition here for sake of accessibility):

> [S]ubtyping (also subtype polymorphism or inclusion polymorphism) is a form of type polymorphism in which a subtype is a datatype that is related to another datatype (the supertype) by some notion of substitutability, meaning that program elements, typically subroutines or functions, written to operate on elements of the supertype can also operate on elements of the subtype.

This holds in the case of sum types. Operations that work on the sum type will generally also work on the variants that constitute the sum type.

The same goes for inheritance. If an abstract class T has two concrete subclasses `A` and `B`, then a value of type `T` belongs to the union of values of type `A` and of type `B`.