A bug(?) around phantoms in 3.11.0 b1 (Re: [Caml-list] OCaml version 3.11.0+beta1)

A bug(?) around phantoms in 3.11.0 b1 (Re: [Caml-list] OCaml version 3.11.0+beta1)

[Jun Furuse]

Hi,

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

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

=
j

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

[Jacques Garrigue]

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

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

[Jun Furuse]

Hi Jacques,

Thanks for your insightful answer.

I misunderstood it was a new problem to 311, since here we use a
slightly older version (3.10dev0) for our work, which compiles the
code.

=
j

On Tue, Oct 21, 2008 at 5:32 PM, Jacques Garrigue
<garrigue@math.nagoya-u.ac.jp> wrote:
> 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
>