The following example, derived from yours, is probably more surprised (I didn't understand your issue at first):

  # ((fun a -> a), (fun b -> b));;
  - : ('a -> 'a) * ('b -> 'b) = (<fun>, <fun>)
  # ((fun a -> a), (fun b -> b) (fun c -> c));;
  - : ('_a -> '_a) * ('_b -> '_b) = (<fun>, <fun>)

Here is how I explain this from the paper "Relaxing the value restriction", Jacques Garrigue, 2004:
  http://caml.inria.fr/about/papers.en.html
No guarantee that this matches the actual typing behavior.

There are two different typing rules: one for the form "let x = v in e", where a value is bound, all typing variables are generalized, and one other for the form "let x = e1 in e2", where an *expression* is bound, and all non-negative variables are generalized.

In the ((fun a -> a), (fun b -> b)) example, this is a value, everything gets generalized. In the ((fun a -> a), (fun b -> b) (fun c -> c)) example, this is not a value anymore, and both components use a type variable in negative position, so nothing gets generalized. In the ([], (fun b -> b) (fun c -> c)) example, this is not a value but [] is covariant in its type variable, so it still gets generalized.


On Fri, Dec 16, 2011 at 10:18 AM, Andrej Bauer <andrej.bauer@andrej.com> wrote:
Can someone explain this behavior?

# ([], (fun x -> x) (fun y -> y)) ;;
- : 'a list * ('_b -> '_b) = ([], <fun>)

# ((fun a -> a), (fun x -> x) (fun y -> y)) ;;
- : ('_a -> '_a) * ('_b -> '_b) = (<fun>, <fun>)

Why does the second component influence the first one (in a non-obvious way)?

With kind regards,

Andrej

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