[Haskell-cafe] type hackery question

[jeff p]

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