Jeff wrote:

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 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).

It seems likely that you have the uses for the inferred type of the above expression other than displaying it. You probably want to statically enforce certain constraints when applying these Lam expressions. That is, you want to apply Lam expressions only to the arguments that satisfy the inferred HasField constraints. Why not to enforce the constraints at that time then? The enclosed is a bit simplified version of the code that demonstrates the idea. It is the typed evaluator statically enforcing the HasField constraints. It does not use GADTs though as they don't add to expressiveness. It would be great if we could delay the more detailed discussion past the first week of Jan.

and TypeEq doesn't work on uninstantiated type vars; correct me if I'm wrong about these.

TypeEq may work on uninstantiated type vars; please see http://pobox.com/~oleg/ftp/Haskell/de-typechecker.lhs and the paragraph containing the phrase ``The ability to operate on and compare *unground* types with *uninstantiated* type variables is often sought but rarely attained. The contribution of this message is the set of primitives for nominal equality comparison and deconstruction of unground types.'' {-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-undecidable-instances #-} module J where data Lam f = Lam f data App f x = App f x data Proj l e = Proj l e data Rec1 = Rec1 (Int->Int) -- simplified data Rec2 = Rec2 Int -- simplified {- well-formednedd (well-typeness) rules class Exp a t | a -> t instance (Exp ea a, Exp eb b) => Exp (Lam (ea -> eb)) (a->b) instance (Exp f (a->b), Exp x a) => Exp (App f x) b instance (Exp e r, HasField l r v) => Exp (Proj l e) v instance Exp Rec1 Rec1 instance Exp Rec2 Rec2 -} data L1 = L1 data L2 = L2 class HasField l r v | l r -> v where flookup :: l -> r -> v instance HasField L1 Rec1 (Int->Int) where flookup _ (Rec1 x) = x instance HasField L2 Rec2 Int where flookup _ (Rec2 x) = x t1 = Lam $ \x -> App (Proj L1 x) (Proj L2 x) t2 = Lam $ \x -> App (Lam (\x -> x)) (Proj L2 x) class Eval e v | e -> v where eval :: e -> v -- big step, CBN semantics instance (Eval f (Lam (x->e2)), Eval e2 v) => Eval (App f x) v where eval (App f x) = let Lam f' = eval f in eval $ f' x instance (Eval e r, HasField l r v) => Eval (Proj l e) v where eval (Proj _ e) = flookup (undefined::l) $ eval e -- Those are values already instance Eval (Lam e) (Lam e) where eval = id instance Eval Rec1 Rec1 where eval = id instance Eval Rec2 Rec2 where eval = id t3 = eval $ App t2 (Rec2 1) -- The following gives the expected type error: Rec1 has no field L2 -- t4 = eval $ App t2 (Rec1 succ)