Enforcing exclusion
Some inspiration for a system that works this way can be found in Extensible Records Without Subsumption (pdf) by Bob Harper and Benjamin Pierce. They present extensible records via row polymorphism, which your comments on your question indicate you are already familiar with, but the paper also includes the notion of a lacks constraint. From the introduction:
For example, Cardelli and Mitchell’s record extension operator is only defined on records where the field being added is not already present; to prevent run time type errors, the typing rule for the extension operator must check that this is the case. We found it simpler to express this constraint directly as “$r$ lacks $l$” instead of encoding it as “$r$ is less than some type lacking $l$.”
Their system allows quantified type variables to be constrained by both these negative lacks constraints as well as positive has constraints. Lacks constraints provide some of the basic material necessary to implement the mutual exclusion property you’re looking for, and in fact, they’re already sufficient to guarantee it is maintained. To see how, let’s consider a “label declaration” that binds a name that can be used as a label in a record:
$$
\mathbf{label}\ \mathsf{x} : \mathsf{T}
$$
This declares $\mathsf{x}$ as a record label for a value of type $\mathsf{T}$. We can imagine extending this declaration with support for constraints:
$$\begin{array}{l}
\mathbf{label}\ (\mathsf{x} : \mathsf{T}) ∈ \rho \\
\quad \mathbf{where}\ \mathsf{y} ∉ \rho
\end{array}$$
This can be read as “$\mathsf{x}$ is a label for a value of type $\mathsf{T}$ in some row type $\rho$ such that $\rho$ lacks label $\mathsf{y}$.” When a record is constructed using this label, the $\mathsf{y} \notin \rho$ constraint would be generated, and a constraint solver would need to be able to somehow solve it in order for the program to be accepted.
Exposing exclusion
This is enough to enforce the property, but it is not quite enough to truly leverage it. In your question, you state
You'd know that if you found one of them then the others weren't there, so that for example typecase pattern-matching on them all would be exhaustive and order-independent.
which requires that we gain information by pattern matching. This requires something a bit stronger: local assumptions, which are most commonly associated with generalized algebraic data types (GADTs). GADTs offer precisely the sort of property we’re looking for, namely that matching on a constructor can introduce local constraints (i.e. assumptions) only available within the pattern match’s right hand side. For example, we might write the Haskell datatype
$$\begin{array}{l}
\mathbf{data}\;\mathsf{SomeShowable}\ a\;\mathbf{where} \\
\quad \mathsf{MkSomeShowable} :: \mathsf{Show}\ a \Rightarrow a \rightarrow \mathsf{SomeShowable}\ a
\end{array}$$
which “contains” a $\mathsf{Show}$ constraint, so pattern matching on the $\mathsf{MkSomeShowable}$ constructor brings that constraint into scope.
Although these constrained labels aren’t quite GADTs, they can be typechecked using the same principles. Since the constraint must be satisfied for each record they’re added to, a record containing the label serves as a proof that all the constraints must hold, and a local constraint can be brought into scope. Implementing a typechecker that supports local assumptions can be quite tricky, but Modular type inference with local assumptions (pdf) provides an detailed overview.
Challenges, alternatives, and loose ends
While the above description provides a decent sketch of the idea, it is somewhat simplified in that it associates the lacks constraint with a particular label when in fact the exclusion must be mutual. That is, it does not suffice to check that $\rho$ lacks $\mathsf{y}$ when $\mathsf{x}$ is added to a record, but it is also necessary to check that $\rho$ lacks $\mathsf{x}$ when $\mathsf{y}$ is. If records are not extensible (that is, labels cannot be added to an existing record unless all of its labels are statically known), this is not a problem, as checking exclusion in one direction is sufficient. But if polymorphic extension is permitted, you would need to take care to infer the appropriate constraints on excluded labels.
However, this introduces a new quandary: if a label to be considered mutually exclusive may be defined in a yet-to-be-defined module (that is, we take an “open world” assumption), it is impossible to know at any given record construction site which lacks constraints we must enforce! Therefore, some restriction on where/how this mutual exclusiveness may be defined is probably necessary. An easy approach would be to require that both labels be declared in the same module.
Finally, a different approach altogether would be to associate the constraints with a given row type rather than with the labels. In that case, you might allow constrained types like
$$
(\mathsf{x} ⊕ \mathsf{y} ∈ \rho) \Rightarrow \mathsf{Record}\ \rho
$$
where $⊕$ is read as “XOR”. In this case, your constraint solver would need to have inference rules like the following:
$$\begin{array}{l}
\begin{array}{l}
⊢ \ell_1 ∈ \rho \\
⊢ \ell_2 ∉ \rho \\
\hline
⊢ \ell_1 ⊕ \ell_2 ∈ \rho
\end{array}
\begin{array}{l}\\ [\textsf{XOR-intro}]\end{array}\\
%
\begin{array}{l}
⊢ \ell_1 ⊕ \ell_2 ∈ \rho \\
⊢ \ell_1 ∈ \rho \\
\hline
⊢ \ell_2 ∉ \rho
\end{array} \begin{array}{l}\\ [\textsf{XOR-elim}]\end{array}\\
\end{array}$$
When constructing the record, the $\textsf{XOR-intro}$ rule would be used to satisfy the constraint. When pattern matching on a record, a match would supply the necessary has constraint as a local assumption, so the $\textsf{XOR-elim}$ rule could derive the corresponding lacks constraint, permitting bidirectional flow of information.
But be cautious! This approach also runs into some trouble if you allow adding labels after the record has already been constructed, since the constraint may have already been discharged. So you’d need to do some extra work to ensure the property holds globally, which could quickly make the system difficult to use. Such is the pain of proving a negative.
ais present means you can access it. Knowing thatais absent means you don't need to implement it. But what can you do with an object where you know that exactly one ofaandbis present, that doesn't require discriminating between the two cases (in which case you'd just take a discriminating union of the a and b versions)? $\endgroup${x: number, empty}and{x: number, ρ}whereρis a row parameter. In the notation from Wikipedia, mutually exclusive properties might be written as a union type like{x: number, absent(y), ρ} | {y: string, absent(x), ρ}. I'm not really knowledgeable enough to write more on the subject, but if this is useful enough then I can convert it from a comment to an answer. $\endgroup$