On 23 January 2018 at 17:39, Chet Murthy <murthy.chet@gmail.com> wrote:
> That is, when you write a caml program and it fails to type-check, you can't make it type-check by adding "enough" type-annotations.

This hasn't been the case for a long time (perhaps ever), and it's
becoming less true with each release.  For example, all of the
following programs pass type checking as written, but are rejected if
the annotations are removed:

   (* 1 *)   let f (g : x:int -> y:int -> int) x y = (g ~x ~y, g ~y ~x)
   (* 2 *)   let rec f : 'a. 'a -> unit = fun x -> ignore (f 3, f "four")
   (* 3 *)   let f : [`A] -> unit = function `A -> () | _ -> .
   (* 4 *)   module type S = module type of struct let r : int list
ref = ref [] end
   (* 5 *)   let f (o : <m:'a.'a -> unit>) = (o#m (), o#m 2)
   (* 6 *)   let f z = let rec x = [| y; z |] and y : int = z in x
   (* 7 *)   let x : _ format6 = "%d" in Printf.sprintf x
   (* 8 *)   type a = A | B   type b = A   let x = (A : a) = B
   (* 9 *)   let f : (module S) = (module struct end)
   (* 10 *) module rec M : module type of struct let f : int -> int =
assert false end = struct let f = M.f end