I've been working hard this week, and I'm stumbled upon something which is probably of absolutely no surprise to anybody but me. Consider the following expression: (foo True, foo 'x') Is this expression well-typed? Astonishingly, the answer depends on where "foo" is defined. If "foo" is a local variable, then the above expression is guaranteed to be ill-typed. However, if we have (for example) foo :: x -> x as a top-level function, then the above expression becomes well-typed. I had never ever noticed this fact before. I'm still trying to bend my mind around exactly why it happens. As best as I can tell, top-level functions (and value constructors, for that matter) seem to get a "new" set of type variables each time they're used, but local variables each get a single type variable, so every mention of a local variable must be of the exact same type. Could this be what GHC's weird "forall" syntax is about? Does "forall x." mean that "x" gets replaced with a unique type variable each time? It's an interesting hypothesis... Anyway, not that anybody is likely to care, but I've just spent an entire week writing a program which can type-check simple Haskell expressions. As in, you type in an expression and give types to any free variables it involves (including value constructor functions), and it tells you the type of the expression and all its subexpressions. (Or tells you that it's ill-typed.) It turns out that this is radically less trivial than you'd imagine. (The ramblings above being just one of the issues I blundered into. Others include the subtleties of writing an expression parser, building a pretty-printer with bracketing that works correctly, and the fact that expression processing malfunctions horribly if you don't make all the variable names unique first...) Other issues were mostly related to the difficulty of constantly refactoring code because you're not quite sure what you're trying to do or how you're trying to do it. (And obscure type checker warnings about GADTs...) Well there we are. I don't suppose anybody will be overly impressed, but I'm glad to have finally got it to work. Now, if it could parse more than 10% of Haskell's syntax sugar, it might even be useful for something...