On Tue, 2005-11-15 at 14:45 +0300, Vsevolod Fedorov wrote:
> Hello!

>   (*   ^^^ This expression has type string -> unit but is here used with
> type int -> unit *)

Here is a simpler case:

let use (f: 'a -> unit) = f 1; f ""

The appearance of a 'free' type variable in the function
signature implicitly implies the quantification:

For all 'a . let use (f: 'a -> unit) =  f 1; f ""

which says, for each type 'a, there is a function 'use' ..

Inside a particular instance of use, 'a is fixed.

In Ocaml this design bug has been fixed for record and object fields:

type t = { f: 'a . 'a -> unit }
let use (wrap: t) = wrap.f 1; wrap.f ""

Here the quantifier is explicit and binds only the
type of the field f; and the record type t is entirely 
monomorphic.

Note that the first interpretation is necessary
in the first case, by considering:

let f (x:int) = ()
use f;

we simply cannot have the inner

f ""

type correctly. In the second case, you cannot
instantiate the field with that f, because it
is the wrong type -- the field requires the
function to be polymorphic.

With any luck this design bug will eventually be
properly fixed, so you can write:

let use (f: 'a . 'a -> unit) =  f 1; f ""

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net