Re: A bug(?) around phantoms in 3.11.0 b1

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

Hi Jun,

If it's a bug, it should go to mantis... but it's not one.

From: "Jun Furuse" <jun.furuse@gmail.com>
> I found a strange bug in 3.11.0 beta 1. The following typical example
> of phantom types does not compile any more. (It is compilable in
> 3.10.2, but not in release311):
> 
> module M : sig
>   type +'a t constraint 'a = [< `checked | `unchecked ]
>   val check : _ t -> [ `checked ] t
> end = struct
>   type +'a t = { x : int } constraint 'a = [< `checked | `unchecked ]
>   let check (t : _ t) = t (* actually it grants anything *)
> end

Actually, it doesn't compile in 3.10.2.
(At least, not in release310)
But it did compile until 3.10.0, and this was a bug.
Indeed, in the above 'a is a constrained variable, so its variance is
not inferred. The explicit variance is +'a, which doesn't cancel
unification.
(One might argue that we need a special variance to indicate types
that do not appear in the body...)

> A strange thing is that if I change the definition as follows it compiles!
> 
> module M : sig
>   type +'a t constraint 'a = [< `checked | `unchecked ]
>   val check : _ t -> [ `checked ] t
> end = struct
>   type u = { x : int } (* strange workaround *)
>   type +'a t = u constraint 'a = [< `checked | `unchecked ]
>   let check (t : _ t) = t (* actually it grants anything *)
> end

This is not strange. Here 'a t expand to u, where 'a is forgotten.
So the type annotation really removes the connection between input and
output types.
This is the right way to obtain what you wish.

Jacques