Re: [Caml-list] surprising type error with labels

["Mark Shinwell" <mshinwell@janestcapital.com>]

On Thu, Jun 19, 2008 at 10:58:59PM +0100, Jeremy Yallop wrote:
> Jake Donham wrote:
> >Why does
> >
> > ListLabels.find (fun _ -> true) [];;
> >
> >produce
> >
> > Characters 16-31:
> >   ListLabels.find (fun _ -> true) [];;
> >                   ^^^^^^^^^^^^^^^
> > This expression should not be a function, the expected type is
> > ('a -> 'b) list
> >
> >I thought the rule was that "if an application is total, labels may be
> >omitted." (4.1 in the manual). (I was trying to do module List =
> >ListLabels at the top of a file.) Thanks,
> 
> Applications of functions whose return types are type variables are 
> never considered total, since it's possible to pass extra arguments if 
> the type variable is instantiated to a function type.  For example, 
> ListLabels.find has type
> 
>    f:('a -> bool) -> 'a list -> 'a
> 
> If the type variable is instantiated to `bool -> bool', say, then you 
> can pass more than two arguments:
> 
>    ListLabels.find ~f:(fun f -> f false) [not] false

I'm not really sure that this behaviour (which is highly non-obvious from
the error message) is to do with applying future unlabelled arguments.
As far as I can see it's probably this way so you can apply future
_labelled_ arguments, meaning you can write things like:

# ListLabels.find [] (fun x -> x);;
- : f:((('a -> 'a) -> 'b) -> bool) -> 'b = <fun>

and also:

# ListLabels.find ~f:(fun (f:(z:int -> int)) -> true) ~z:42 [fun ~z -> 1];;
- : int = 1

(note that the ~z:42 has been commuted with the list).  This seems kinda
cool, but the code is somewhat obfuscated, and error messages are potentially
confusing as Jake witnessed.

Is there any theoretical reason why the compiler couldn't just deem
applications of the form given by the original poster as total, even though
it results in the loss of some expressibility?  Perhaps it would be easier
to improve the error messages in that case... or perhaps it just results in
too little expressibility for some reason.

Mark