On Wed, Sep 15, 2010 at 6:40 PM, Andreas Rossberg <rossberg@mpi-sws.org> wrote:
> Have a look at this variant of c.ml and its "potential" if it type-checked:
>>  let f = let xs = ref [] in fun x -> xs := x :: !xs in f 1; f 'a'

Interesting. If I would be a type checker, here's what I'd do.
1. "ref []" tells me that (xs : '_a), because I know refs can't be polymorphic.
2. "x :: !xs" tells me that (xs : '_a list) and (x : '_a)
3. "x -> x :: !xs" tells me that (f : '_a -> '_a list)
4. "f 1" tells me that (f : int -> int list)
5. "f 'a'" tells me... OOPS

Moreover, I'd have similar thoughts about a variant of a.ml (and a.ml
does typecheck!)
  let xs = ref [] in let f = fun x -> xs:=x::!xs in f 1; f 'a'

On the other hand, here's what I'd do for the original c.ml, which
with a few names added is
  let f = let x = ref () in fun y -> () in f 1; f 'a'
1. "ref ()" tells me that (x : unit ref)
2. "y -> ()" tells me that (f : 'a -> unit)
3. "f 1" returns ()
4. "f 'a'" return ()

In other words, I would have thought that in your example the problem
is that you tried to use a polymorphic reference. (And this problem
even appears in the FAQ.)

regards,
  radu