(sorry, I meant to send this to the list, but only sent it to Wolfgang) Here is my understanding of the current state of the argument: Instead of Labels, there will be a new kind String, which is not a subkind of *, so its elements are not types. The elements of String are strings at the type level, written just like normal strings. If you want labels, you can define them yourself, either empty: data Label (a :: String) or inhabited data Label (a :: String) = Label these definitions give you a family of types of the form Label "name", in the first case empty (except for undefined), in the second case inhabited by a single element (Label :: Label "name") There are several similar proposals for extensible records defined using labels, all of which (as far as I can see) could be defined just as easily using the kind String. There is also a proposal for nonextensible records, using the same techniques, which has (almost) converged with Simon's latest version of TDNR records. The problem with all of these is dealing with higher-rank field types: the current implementation of impredicative polymorphism isn't general enough to allow update of polymorphic fields. It seems to me that, if we could solve the (hard) impredicativity problem, we would be very close to a design which would 1. be compatible with existing code 2. allow field names to be polymorphic 3. make the future addition of extensible records possible The question is, should we wait till someone solves the impredicativity problem, or go ahead with a cludgy design now? Barney.