I think that indeed every Caml value is of exactly one type but then it is not so that the REPL reports the type of a value. Is 'a -> 'a a type before 'a has been bound? fun x -> x has type 'a -> 'a according to REPL while the type of fun x -> not x is bool -> bool. Is it correct to say that fun x -> not x is of type 'a -> 'a? Observe in a fresh REPL:

# let g = ref (fun x -> x);;
val g : ('_a -> '_a) ref = {contents = }
# g := (fun d -> not d);;
- : unit = ()
# (!g) true;;
- : bool = false
# g;;
- : (bool -> bool) ref = {contents = }
# g := (fun x -> x);;
- : unit = ()
# g;;
- : (bool -> bool) ref = {contents = }
# !g 38;;
This expression has type int but is here used with type bool

I need a theory of types! I can only imagine that just after let g = ref (fun x -> x);; the value referred to by g still had no type; which illustrates my claim that REPL has only reported a category of types when it responds ('_a -> '_a) ref. The command g := (fun d -> not d);; restricts not only !g but g as well! I wonder whether a program ever “gets thru compiling” while there are still ‘types’ with 'a’s in them.