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
>