From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=1.4 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE, DNS_FROM_SECURITYSAGE autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id D9208BBAF for ; Tue, 21 Oct 2008 10:32:49 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AhUDAKAw/UjAXQImgWdsb2JhbACTbwEBFiKwE4NQ X-IronPort-AV: E=Sophos;i="4.33,456,1220220000"; d="scan'208";a="30566104" Received: from discorde.inria.fr ([192.93.2.38]) by mail4-smtp-sop.national.inria.fr with ESMTP; 21 Oct 2008 10:32:49 +0200 Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id m9L8Wmfw010676 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Tue, 21 Oct 2008 10:32:49 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ApoEAOgw/UiCNhAB/2dsb2JhbADEO4NQ X-IronPort-AV: E=Sophos;i="4.33,456,1220220000"; d="scan'208";a="18326785" Received: from kurims.kurims.kyoto-u.ac.jp ([130.54.16.1]) by mail3-smtp-sop.national.inria.fr with ESMTP; 21 Oct 2008 10:32:19 +0200 Received: from localhost (orion [130.54.16.5]) by kurims.kurims.kyoto-u.ac.jp (8.13.8/8.13.8) with ESMTP id m9L8WDrw020676; Tue, 21 Oct 2008 17:32:13 +0900 (JST) Date: Tue, 21 Oct 2008 17:32:08 +0900 (JST) Message-Id: <20081021.173208.220086361.garrigue@math.nagoya-u.ac.jp> To: jun.furuse@gmail.com Cc: caml-list@inria.fr Subject: Re: A bug(?) around phantoms in 3.11.0 b1 From: Jacques Garrigue In-Reply-To: <5160b4200810210015q720ae14dx8cf4a5fa05ae6e30@mail.gmail.com> References: <5160b4200810210015q720ae14dx8cf4a5fa05ae6e30@mail.gmail.com> X-Mailer: Mew version 4.2 on Emacs 22.2 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Miltered: at discorde with ID 48FD93B0.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; bug:01 bug:01 furuse:01 furuse:01 compilable:01 sig:01 val:01 struct:01 unification:01 sig:01 val:01 struct:01 compile:01 compile:01 compiles:01 Hi Jun, If it's a bug, it should go to mantis... but it's not one. From: "Jun Furuse" > 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