Re: [Caml-list] annotations and type-checking

[Aaron Bohannon <bohannon@cis.upenn.edu>]

Thank you for that link.  To boil it down, it seems (1) type variables
annotating top-level declarations are ignored, and (2) type variables
annotating local bindings are treated existentially (as if one had
written '_a, although that name itself is considered syntactically
ill-formed).

So if OCaml cannot do anything better than this, then why are type
variables even syntactically legal in annotations?  If backwards
compatibility is the issue, could it not at the very very least give a
compiler warning when they are used?

 - Aaron

On Wed, Jul 29, 2009 at 3:40 AM, Mark
Shinwell<mshinwell@janestcapital.com> wrote:
> 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
>