Marc Weber wrote:

Do you know what a type indexed coproduct is ? (TIC.hs from HList) What is the purpose of this module?

In a regular Haskell record, we can retrieve the value of one of its components given the label. A type-indexed Product (TIP, or TIR) is a similar collection of values -- indexed not by their label but by their type. Given a TIP of an Int and a Char, we can retrieve either value just by specifying what return type we want (Int or Char). A type-indexed co-product, TIC, is a type-indexed sum. A TIC of Int and Char has the type of the union of Int and Char (think of Either Int Char). We can likewise ask for an Int element -- and receive either (Just val) or Nothing. Unlike (Either Int Char), we do not have to know whether Int is the first alternative of Either or the second one. We just ask for an Int. TIP and TIC have been introduced in M. Shields and E. Meijer. Type-indexed rows. (ref 31 of the HList paper) We wanted to show that HList can implement both. An implementation of TIC different from that of App C of the HList paper is used in the OOHaskell paper. That new implementation is based on nested Either datatypes rather than on Dynamics. The application is placing objects of two different types in the same list. There are two approaches: find the intersection of the object types and coerce objects to that intersection -- or find the union and inject objects into that union. The OOHaskell paper shows both approaches, with meet and joins of object types computed automatically.

Why the Proxy type has been introduced? Just to emphasize that we use the type as the index; to clarify the role of that argument. One can get be without them, their purpose is mere stylistic.