On Tue, Jul 28, 2009 at 05:47:25PM -0400, Aaron Bohannon wrote:
> Why do the first two programs type-check but the thrid one does not?

Dark corners of the type system.
 
> let f (x : 'a) : 'a = x in (f true, f 3);;

Explicit type variables in this situation are considered "global".  They are
not generalized until the type of the whole toplevel declaration has been
determined.  Consequentially, during type-checking of the body of your
let expression, 'a is not a generalized variable.

There is more detail on similar situations here:

http://caml.inria.fr/pub/ml-archives/caml-list/2002/06/a03da53be62c12671a891708c51e85f9.en.html

Mark