Re: [Caml-list] Type constraints

[Damien Doligez <damien.doligez@inria.fr>]

On 7 Dec 2004, at 19:08, Alain Frisch wrote:

> I still don't understand. Compare:
>
> # module M = struct let v = ref [] end;;
> module M : sig val v : '_a list ref end
> # module M : sig val v : 'a -> 'a end = struct let v x = x end;;
> module M : sig val v : 'a -> 'a end
>
> Of course, the type variable in the first example must not be 
> generalized, and it isn't. In the second example, there is no problem. 
> We get:
>
> # M.v;;
> - : 'a -> 'a = <fun>
>
> So why not give the same type scheme to:
>
> let module M : sig val v : 'a -> 'a end = struct let v x = x end in M.v

The typing algorithm is very simple (really!):

1. Type the module. Generalization occurs and the v field gets a
    polymorphic type.
2. Type "M.v".  This takes an instance of the polymorphic type.
3. Can we generalize it?  Look at the syntactic shape of the expression
    (in this case, let module ... in ...).  If it is always safe to
    generalize such expressions, OK.  If not, do not generalize.

That's the beauty of the Wright criterion: it's very easy to implement
and to understand (because it is syntactic), and works well in almost 
all
cases (with a little eta-expansion if needed).

So the answer to your original question is: the type is not generalized
because in some cases the let-module construct is not safely 
polymorphic.

Of course, there must be some criteria for generalizing more
expressions.  Check out Xavier's thesis for example.  They are usually
not worth the trouble.

-- Damien