Philippe Veber wrote:
> Hi all,
> 
> is this behaviour of the type checker expected ?
> 
>         Objective Caml version 3.11.0
> 
> # let f g x y = g ~x ~y;;
> val f : (x:'a -> y:'b -> 'c) -> 'a -> 'b -> 'c = <fun>
> # let g ~y ~x = x + y;;
> val g : y:int -> x:int -> int = <fun>
> # f g;;
> Error: This expression has type y:int -> x:int -> int
>        but is here used with type x:'a -> y:'b -> 'c
> 
> If so, I'm tempted to fill a report to mantis anyway, to get this said
> in the manual (i've not seen anything for this case, but i might have
> missed something).

Imagine that any function has a unique runtime representation that only
accepts one particular order for its arguments.

Labeled arguments can only commute during function application when a
particular order is expected. Reordering is done solely by the compiler based
on the presence labels. If no particular order is expected (g ~x ~y in your
definition of f), then the type checker assumes something reasonable but must
make a choice. This is why the first argument of f is inferred to have type
(x:'a -> y:'b -> 'c) although a type annotation could change this.


I find this interesting:

# let f g x y =
  g ~x ~y + g ~y ~x
;;
    Characters 26-27:
    g ~x ~y + g ~y ~x
              ^
This function is applied to arguments in an order different from other calls.
This is only allowed when the real type is known.

# let f (g : x:_ -> y:_ -> _) x y =
  g ~x ~y + g ~y ~x
;;
    val f : (x:'a -> y:'b -> int) -> 'a -> 'b -> int = <fun>



Martin

-- 
http://mjambon.com/