Problem

In Clojure we are free to extend datatypes with any combination of protocols and interfaces. To make our type predicates useful, there are sets of protocols/interfaces that should never be extended simultaneously by the same type.

For example, IMap and IVector should probably never be extended by the same type. To see why core.typed needs to know this information, we define a function that takes an argument that can be an IMap or IVector, then we pick a branch based on whether it implements IVector.

(ann foo [(U (IMap Any String) (IVector String)) -> (U nil String)])
(defn foo [a]
  (if (vector? a)
    (nth a 0 nil)
    (get a :key))) 

Let's assume core.typed knows about which protocols are "compatible". Occurrence typing updates the type for each branch as follows:

What happens if core.typed does not know about compatible protocols? The case in red then becomes:

Unfortunately, we now have inferred type (Extends [(IMap Any String) (IVector String)]) on the first branch.

We can fix this locally by using the Extends constructor's :without argument, which specifies protocols which are explicitly not extended.

(ann foo [(U (Extends [(IMap Any String)] :without [(IVector Any)])
             (IVector String)) 
          -> (U nil String)])
(defn foo [a]
 (if (vector? a)
   (nth a 0 nil)
   (get a :key))) 

We regain our accurate type, at the cost of more verbose types. The case becomes:

Interestingly, this forces us to be very explicit about which protocols we expect to be implemented at certain points in the code.

However, this rarely reveals anything interesting, and quickly becomes a chore.

How do we express disjoint types to avoid this kind of annotation, while still being careful enough to not lose soundness?