Mark Shinwell wrote:
> 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.

You'd have to distinguish between terms which refer to polymorphic 
functions and terms whose type is only partially known.  I suspect it 
might be quite difficult to do that in a way that interacts 
satisfactorily with type inference.  Even the current design has a 
rather unfortunate dependence on the particular order of execution of 
the type inference algorithm.  For example, given a definition

    let h = fun ~x:() () -> ()

the following program is allowed

    let g f x = ([f; h], f x)

whereas the following rather similar program is not

    let g f x = (f x, [f; h])

If the type inference algorithm sees `[f; h]' first then it gives f a 
fully-known labeled type and allows it to be applied without a label 
when it subsequently encounters `f x'.  If it sees `f x' first then it 
assigns an unlabeled type to f, which subsequently fails to unify with 
the type of h.

I agree that the current behaviour is surprising, but I'm not sure that 
it's easy to make it much less surprising, even if you're willing to 
give up some expressiveness.

Jeremy.