You have hit the "value restriction":
  http://caml.inria.fr/resources/doc/faq/core.en.html#eta-expansion

# let g = (fun x -> x) (fun x -> x);;
val g : '_a -> '_a = <fun>
# let g x = (fun x -> x) (fun x -> x) x;;
val g : 'a -> 'a = <fun>

Polymorphism annotation ( : 'a . 'a -> 'a ) have no use here, as you can easily see in the return type if the value is polymorphic (type variables 'a, implicitly quantified at the beginning of the type) or not ("weak" type variable '_a, which are just unknowns waiting to be unified).

On Sun, Aug 14, 2011 at 3:46 PM, Ruslan Ledesma Garza <ruslanledesmagarza@gmail.com> wrote:
Dear list,

Consider the following OCaml session.

       Objective Caml version 3.12.0

# let f : 'v . 'v -> 'v = fun x -> x;;
val f : 'a -> 'a = <fun>
# let g : 'v . 'v -> 'v = (fun x -> x) (fun x -> x);;
Error: This definition has type 'a -> 'a which is less general than
        'b. 'b -> 'b
#

Why doesn't OCaml generalize the type 'a -> 'a? According to the typing rules in "Principal type-schemes for functional programs" ( http://portal.acm.org/citation.cfm?id=582176 ), the type 'a -> 'a can be generalized.

Something similar happens in the following OCaml session.

       Objective Caml version 3.12.0

# let f : 'v . 'v -> 'v = fun x -> x;;
val f : 'a -> 'a = <fun>
# let h = f f;;
val h : '_a -> '_a = <fun>
# h 1;;
- : int = 1
# h h;;
Error: This expression has type int -> int
      but an expression was expected of type int
#

I want the type of h to be \forall 'a . 'a -> 'a.         :'(

Best regards,
Ruslán.




--
Caml-list mailing list.  Subscription management and archives:
https://sympa-roc.inria.fr/wws/info/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs