The two points in AntC's message suggest a possible compromise solution. Unless I've missed something, this allows nested fields, fixed type projections, and HR fields. The only restriction is that HR fields must be fixed type, though they can still be used in multiple records. 1. Use an associated type class for Has, to solve the nesting problem: class Has (r :: *) (x :: Symbol) where type GetField r x :: * getField :: r -> GetField r x (Maybe a fundep would also work, but I'm more used to thinking with associated types.) 2. Introduce a declaration for fixed type fields: field bar :: Bar is translated as: class Has_bar r where bar :: r -> Bar instance Has_bar r => Has r "bar" where GetType r "bar" = Bar getField = bar 3. Undeclared fields and those declared typeless don't have their own class: field bar is translated as bar :: Has r "bar" => r -> GetType r "bar" bar = getField 4. Now you can use HR fields, provided you declare them first: field bar :: forall b. b -> b is translated as: class Has_bar r where bar :: r -> forall b. b -> b instance Has_bar r => Has r "bar" where GetType r "bar" = forall b. b -> b getField = bar which doesn't look impredicative to me. Does this work, or have I missed something? Barney.