It’s tempting, after a bit of experience with using nice functional languages, and some time spent really understanding what’s going on with (for example) Pierce’s books on type systems, to think you actually have some idea of what you’re doing when implementing one.
Suppose you write:
foo :: a -> b foo x = x
This should be a type error, of course. But how is this error discovered, exactly?
Typical presentations of type systems gloss over many implementation details, and for good reason, but here is one “implementation detail” that isn’t so much an implementation detail. It is a very important part of how type checking must be done in polymorphic languages with type annotations. Yet, I have seen nothing describing it.
To answer my own question, the trick seems to be that the ‘a’ and ‘b’ in the explicit type aren’t type variables, they are Skolem constants. Unlike variables, which can be unified with anything, Skolem constants only unify with exactly themselves. (Well, of course a variable can unify with a Skolem constant, but the rewrite generated is always from the variable to the constant.) The above gets caught as a type error because at some point the type checker will try to unify the two different Skolem constants ‘a’ and ‘b’.
Have you heard of this before, in this context? Please tell me where you might have seen it. So far, the only likely place I know of that I haven’t checked is the definition of SML. Haskell 98 does not seem to mention it, though I just realized perhaps I should check literature on Haskell prior to that. To discover this was the answer, I had to dive right into the GHC source code, and I really shouldn’t have had to do that.