Hello,
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.
Thanks for the response. Don't worry about responding back quickly. I wanted to give a quick response in order to give a better idea of what I'm trying to do. I am not intending to evaluate the expressions I'm creating. I really want Haskell to typecheck the expressions for me-- that is, I want to use the Haskell typechecker to statically typecheck my expressions (the intended use of this is to generate code). In a sense, your sample code bypasses the interesting/hard/troublesome part by not descending into the body of the Lam. Of course, using higher-order abstract syntax would be trivial if Haskell's type system coincided with that of the object language. On the other hand, HOAS tends to not work if the meta language doesn't match the object language. My intuition, mostly due to your work, is that Haskell's type class system can be used to effectively extend Haskell's type system; and I wanted to see if that would allow for a HOAS encoding of a language with a type system which doesn't match Haskell's.
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.''
I will take a closer look at this. thanks, Jeff