[Haskell] type hacking hoas

[jeff p]

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