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