Re: [Caml-list] Type constraints

[nakata keiko <keiko@kaba.or.jp>]

Damien Doligez wrote:

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

This does not answer to me why this works,

#type t = { t : 'a. 'a -> 'a}

#let v = let module M = struct let t x = x end in {t = M.t} in (v.t 5, v.t true)

Of cource, both of the following are not type checked,

#let v = let module M = struct let  t = x end in  M.t in (v 5, v true)

#let v : 'a -> 'a = let module M = struct let t x = x end in  M.t in (v 5, v true)

However, if I can write something like

#let v : 'a. 'a -> 'a = let module M = struct let t x = x end in  M.t in (v 5, v true)

then, it would be type checked ?

Regards,
Keiko.