For the type level gurus: I would like to define types Sum :: [Field] -> * (:::) :: String -> * -> Field used like this Sum '[ "foo" ::: a, "bar" ::: b, "baz" ::: c ] (I hope this makes sense. I'm not quite familiar with the syntax.) such that Sum '[ s1 ::: a1, ... ] unifies with Sum '[ s1 ::: b1, ... ] to give Sum '[ s1 ::: c1, ... ] where c1 is the unification of a1 and b1. If sn is absent from exactly one of the unificands then its type is copied over unchanged. If sn is absent from both then it is absent from the unification. The types should also be invariant under permutation of the list. This is perhaps a bit obscure so I'll explain the application. This is intended for the sumtype equivalent of a record type, so if we have Sum '[ "foo" ::: a, "bar" ::: b ] and Sum '[ "foo" ::: a, "baz" ::: c ] then I take take the sum of these sums and get something of type Sum '[ "foo" ::: a, "bar" ::: b, "baz" ::: c ] If it makes it easier than I am happy for Sum '[ s1 ::: a1, ... ] to unify with forall ak. Sum '[ s1 ::: a1, ..., sk ::: ak ] This is justified by forall b. Either a b being isomorphic to a. Is such a type possible? If so my next question will be about how to type deconstructors of such things, but let's start with a small first step! Thanks, Tom