Browse thread
A bug(?) around phantoms in 3.11.0 b1 (Re: [Caml-list] OCaml version 3.11.0+beta1)
-
Jun Furuse
-
Jacques Garrigue
- Jun Furuse
-
Jacques Garrigue
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: | 2008-10-21 (09:21) |
From: | Jun Furuse <jun.furuse@g...> |
Subject: | Re: A bug(?) around phantoms in 3.11.0 b1 |
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 >