Hello, This message is essentially a repost of a message I sent to haskell-cafe which received no replies. 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). I suspect I need to be able to test for unifiability of type vars in order to pull this off. AFAIK, neither TypeCast nor TypeEq provide this since TypeCast just fails if its two arguments aren't unifiable, and TypeEq doesn't work on uninstantiated type vars; correct me if I'm wrong about these. Does anyone have any thoughts on this? thanks, Jeff