Benjamin Franksen wrote:

I would be interested whether you can not only /check/ well-typedness, but also /establish/ it, i.e. is it possible to have the input to the type-checker be an /untyped/ representation (such as obtained by parsing a program in text form) and the output be a typed one (or else a type error)?

The original problem was to embed a domain-specific term language in Haskell and get the Haskell typechecker to flag meaningless terms when compiling code files. You, as I understand it, would like to do the same for terms read, at run-time, from files or received from (remote) sources. Right? Well, it seems that's where staging/TH can be useful. Rather then writing badfoo = Fix id in the source code, we can write badfoo = $(read_the_Foo_term "from-file") The typechecking will be performed by TH. It seems we have discussed that before: http://www.haskell.org/pipermail/haskell-cafe/2006-November/019193.html That article contains the complete working example. I think Alice developers can say quite a bit about this problem of type-safe pickling and especially unpickling. Perhaps we should move to Cafe?