It strikes me that there is a fairly major issue with the record proposal as it stands. Right now the class class Has (r :: *) (x :: Symbol) (t :: *) can be viewed as morally equivalent to having several classes class Foo a b where foo :: a -> b class Bar a b where bar :: a -> b for different fields foo, bar, etc. I'll proceed with those instead because it makes it easier to show the issue today. When we go to compose those field accessors, you very quickly run into a problem due to a lack of functional dependencies: When you go to define fooBar = foo.bar which is perfectly cromulent with existing record field accessors you get a big problem. fooBar :: (Foo b c, Bar a b) => a -> c The b that should occur in the signature isn't on the right hand side, and isn't being forced by any fundeps, so fooBar simply can't be written. Could not deduce (Foo b0 c) arising from a use of `foo' from the context (Bar a b, Foo b c) If you leave off the signature you'll get an ambiguity check error: Could not deduce (Foo b0 c) arising from the ambiguity check for `fooBar' from the context (Bar a b, Foo b c) bound by the inferred type for `fooBar': (Bar a b, Foo b c) => a -> c It strikes me that punting all functional dependencies in the record types to the use of equality constraints has proven insufficient to tackle this problem. You may be able to bandaid over it by including a functional dependency/type family class Has (r :: *) (x :: Symbol) where type Got r x :: * getFld :: r -> Got r x (or to avoid the need for type applications in the first place!) class Has (r :: *) (x :: Symbol) where type Got r x :: * getFld :: p x -> r -> Got r x This has some annoying consequences though. Type inference can still only flow one way through it, unlike the existing record accessors, and it would cost the ability to 'cheat' and still define 'Has' for universally quantified fields that we might have been able to do with the proposal as it stands. -Edward