class Has (r :: *) (ft :: *) (f :: ft) (t :: *) where
(where ft stands for field type)?

class Has (r :: *) (f :: ft) (t :: *) where

would be my understanding of how it would be phrased under the current polymorphic kind system.

This could also solve the representation-hiding problem:

foo.field would use the string "field" as the field name, as in the
proposal on the wiki page.

But foo.Field (capital first letter) would use the constructor Field
that is in scope. If you don't want to export the field getter then
capitalise the first letter and don't export the constructor.

I like it. Between that and using Proxy rather than type application perhaps everyone can be made happy.

-Edward