Re: [Caml-list] a question about Ocaml semantics

[Jeremy Yallop <yallop@gmail.com>]

On 26 May 2017 at 09:08, Matej Kosik
<5764c029b688c1c0d24a2e97cd764f@gmail.com> wrote:
> There's an Ocaml language feature I do not understand.
>
> E.g. in this example:
>
>   type 'a phantom = int
>   type t = { enter : 'a. 'a phantom -> int }
>   let f g = g.enter 2
>   let _ = f { enter = fun x -> 1 + x } (* ok *)
>   let _ = f { enter = (+) 1 }          (* fails to typecheck *)
>
> I don't get why, if we have:
>
>   type 'a phantom = int
>
> i.e. "'a phantom" is defined as an alias of "int",
> how is it possible that the following types:
>
>   { enter : 'a. 'a phantom -> int }
>
> is not equal to
>
>   { enter : 'a. int -> int }
>
> I've tried to find a corresponding section in the Reference Manual, but I failed.
> Where is this explained?

I'm not sure that the interaction of features here is documented
anywhere.  But your expectations seem reasonable to me.

The good news is that the behaviour changed in OCaml 4.04.0, and your
program is now accepted.  However, it's not clear (to me) that the
interaction between generalization, phantom types and variance is
quite optimal or consistent yet.  For example, I'd expect this similar
program to be accepted

   type 'a phantom = int
   let x : type a. a phantom -> int = (+) 1

but it's rejected by OCaml 4.04.1.