Manuel M T Chakravarty:
This is problematic as the instance heads are distinguished only by the context; ie, both instances are for `Lacks m (N a r)'. Haskell's instance selection mechanism (with or without associated types) selects instances purely by looking at the arguments of the class; hence, you cannot use instance context as a kind of guard to guide instance selection.
A pity. Would resolving instance declarations as Horn clauses be useful to deal with any other examples of overlapping instances? If you don't mind the code for each new label being linear in the number of previous labels (so the total code is quadratic in the global number of labels) the idea can be rescued. Get rid of (:<:), and keep the same definitions of Constructor, Contains, Lacks, Disjoint and Empty, and the same instances of 'Lacks n Empty' and 'Disjoint Empty r'. For each label 'N', define:
data N a r = N a r
instance Contains N (N a r) where type Project N (N a r) = a type Delete N (N a r) = r project N (N x t) = x delete N (N x t) = t
instance Disjoint r s, Lacks N (Union r s) => Disjoint (N a r) s where type Union (N a r) s = Extend N a (Union r s) union (N x t) u = extend N x (union t u)
and for each previous label 'M', define:
instance Contains M r => Contains M (N a r) where type Project M (N a r) = Project M r type Delete M (N a r) = N a (Delete M r) project M (N x t) = project M t delete M (N x t) = N x (delete M t)
instance Lacks M r => Lacks M (N a r) where type Extend M b (N a r) = N a (Extend M b r) extend M y (N x t) = N x (extend M y t)
instance Lacks N (M a r) where type Extend N b (M a r) = N b (M a r) extend N y (M x t) = N y (M x t)
This saves the bother of fiddling with (:<:) but means that every time you import a module which declares labels you would have to generate code for the interactions between each new label and each existing one. At least it's not exponential! Barney.