Heh. I was careful to say "caml", not "ocaml".   I'm aware that polymorphic
variants, objects, and (heh, I forgot) labels all violate the rule. And of
course, modules do.

Like I said: *caml* has this property.  Certainly caml-light, circa 1993
did, IIRC.

I remember having a nice discussion with Pierre Weis, where I asked him why
record-labels were generative, and he pointed this out to me.

--chet--


On Tue, Jan 23, 2018 at 12:35 PM, Jeremy Yallop <yallop@gmail.com> wrote:

> 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
>