Hello,
I'm beginning to think what I'm after is not possible...
I figure I should try to explain exactly what it is I'm after... Basically I'm trying to mix type hackery with HOAS. More specifically, here is a data type which I would like to use: data Exp a where Lam :: (Exp a -> Exp b) -> Exp (a -> b) App :: Exp (a -> b) -> Exp a -> Exp b Rcd :: (IsRecord (HCons (F l (Exp v)) r) => F l (Exp v) -> Exp r -> Exp (HCons (F l (Exp v)) r) Proj :: (HasLabel l r v) => l -> Exp r -> Exp v where F is a datatype constructor for record fields (as in the HList paper), IsRecord checks that the argument is an HList of F l v and has unique labels (also as in the HList paper); and HasLabel fishes the appropriate type out of a HList of fields. The catch is that I want GHC to infer my types, as well as check ascribed types. Thus I would like to be able to successfully infer a type for: Lam $ \x -> App (Proj l1 x) (Proj l2 x) for some given labels l1 and l2. However, I cannot figure out how to write HasLabel (or if it's even possible). Anyone have any thoughts on this? thanks, Jeff