Damien Bobillot <damien.bobillot@m4x.org> writes:

>      module Module : (sig val func : 'a -> 'b end) =
>      struct let func a = a end
>
> Here Module.func's type is 'a -> 'a. According to me 'a -> 'a is a
> subtype of 'a -> 'b, it's 'a -> 'b with 'a = 'b.

It's not a subtype because 'a -> 'b really means
   forall 'a 'b. 'a -> 'b
and not
   exists 'a 'b. 'a -> 'b

If identity function had type forall 'a 'b. 'a -> 'b, I could use it
to transform an integer to a string.

>      module Module : (sig val func : 'a -> 'a end) = struct
>          let l = ref []
>          let func a = List.assoc a !l

Here the type of func is
   '_a -> '_b
which means something like
   exists 'a 'b. 'a -> 'b
For details Google for "value polymorphism" or "imperative polymorphism".
(Why this is not explained in OCaml manual?)

This is not a subtype of forall 'a. 'a -> 'a.

-- 
   __("<         Marcin Kowalczyk
   \__/       qrczak@knm.org.pl
    ^^     http://qrnik.knm.org.pl/~qrczak/