J Garrett Morris asked me | I also rather like the TDNR proposal, as it's rather similar to the | approach we're taking in Habit (our pet language at Portland State). | However, I'm curious as to why you don't want to quantify over name | resolution constraints. For example, why shouldn't: | | x f = f.x | | be a reasonable function? Yes, it would, and of course any impl of TDNR would need an internal constraint similar to your Select. In my original proposal I was hiding that, but it has to be there in the implementation. But you are right that making it explicit might be a good thing. Esp with Julien's new kind stuff (coming soon) we should be able to say class Select (rec :: *) (fld :: String) where type ResTy rec fld:: * get :: rec -> ResTy rec fld data T = MkT { x,y :: Int } instance Select T "x" where get (MkT {x = v}) = v And now we desugar f.x as get @T @"x" f where the "@" stuff is type application, because get's type is ambiguous: get :: forall rec fld. Select rec fld => rec -> ResTy rec fld Just like what Hobbit does really. You probably don't use the idea of extending to arbitrary other functions do you? (Which Ian does not like anyway.) Something like getIndex :: T -> Int getIndex (MkT x y) = x+y Then I'd like to be able to say t.getIndex So there's an implicit instance instance Select T "getIndex" where type ResTy T "getIndex" = Int get = getIndex It's a little unclear what operations should be in class Select. 'get' certainly, but I propose *not* set, because it doesn't make sense for getIndex and friends. So that would mean you could write a polymorphic update: f v = f { x = v } Restricting to record fields only would, I suppose, allow polymorphic update, by adding a 'set' method to Select. Simon