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

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

From: 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).

Point (1) is wrong. They are not ignored, they act as constraints.
Actually, their behaviour is uniform: they are always bound and
generalized at toplevel. This is true both for normal functions an
classes. The only exception is with modules, but it is not surprising
as modules work on a different level.

I can see only one really buggy behaviour in Alain's mail, the fact
that local modules did flush type variables. Fortunately, this has
been corrected.

> 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?

Because it is useful to be able to have type annotations sharing type
variables in different places in a term (for instance for different
arguments).

Jacques Garrigue

> 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