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=2.6 required=5.0 tests=AWL,DNS_FROM_RFC_POST, DNS_FROM_SECURITYSAGE,SPF_NEUTRAL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id 54096BBAF for ; Tue, 21 Oct 2008 11:21:17 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AhYDANs7/UjAXQIngWdsb2JhbACTMT4BARYip2R/h0oBAwEDg02DJw X-IronPort-AV: E=Sophos;i="4.33,456,1220220000"; d="scan'208";a="18989130" Received: from concorde.inria.fr ([192.93.2.39]) by mail1-smtp-roc.national.inria.fr with ESMTP; 21 Oct 2008 11:21:17 +0200 Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id m9L9LGqo001994 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Tue, 21 Oct 2008 11:21:16 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgwBAGM7/UjRVYC8kGdsb2JhbACTMT4BAQEBCQkMBxEDp2F/h0oBAwEDg02DJw X-IronPort-AV: E=Sophos;i="4.33,456,1220220000"; d="scan'208";a="18329284" Received: from fk-out-0910.google.com ([209.85.128.188]) by mail3-smtp-sop.national.inria.fr with ESMTP; 21 Oct 2008 11:21:16 +0200 Received: by fk-out-0910.google.com with SMTP id e30so2449230fke.9 for ; Tue, 21 Oct 2008 02:21:16 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:message-id:date:from:to :subject:cc:in-reply-to:mime-version:content-type :content-transfer-encoding:content-disposition:references; bh=11BRwlhJOyJgUS1lZBQ3poRXKogl/a/4gwGf60Jb33c=; b=hByMFC2ZHt2N594YAgbipVJKTV2sHfS+cRqfB/0iWLOVDB0bMDqcNvN1DdWSmuBW8M fyeoExEW0NddJOsGxVZYJENkT6lHDwH7zPTks/+tONDqOCtBtln1cog1fWjji6nO1M4r PiqO1oMLSnoAQ33fjRhSwxTMwnLnXoq4m4MMU= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:cc:in-reply-to:mime-version :content-type:content-transfer-encoding:content-disposition :references; b=U/xZo72/vTce5hd80aUtVeWKnZjGbCbwVGcZnMvmDkW8kazQsLt1wRoBcHWpmCps1S vSppCAeA8dPk8+vBHL4xeKY58EQUS/yT0UA0ExQYd1+tcBsUxy3J+EMaaPArJWELRz4i CRrnyL8AlXYCQaEU0dT8o8N40DNNctiIod0Qo= Received: by 10.181.203.11 with SMTP id f11mr1108262bkq.112.1224580876057; Tue, 21 Oct 2008 02:21:16 -0700 (PDT) Received: by 10.180.244.3 with HTTP; Tue, 21 Oct 2008 02:21:15 -0700 (PDT) Message-ID: <5160b4200810210221k731ddda5uc4dc70d687686c86@mail.gmail.com> Date: Tue, 21 Oct 2008 18:21:16 +0900 From: "Jun Furuse" To: "Jacques Garrigue" Subject: Re: A bug(?) around phantoms in 3.11.0 b1 Cc: caml-list@inria.fr In-Reply-To: <20081021.173208.220086361.garrigue@math.nagoya-u.ac.jp> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Content-Disposition: inline References: <5160b4200810210015q720ae14dx8cf4a5fa05ae6e30@mail.gmail.com> <20081021.173208.220086361.garrigue@math.nagoya-u.ac.jp> X-Miltered: at concorde with ID 48FD9F0C.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; furuse:01 furuse:01 bug:01 bug:01 compilable:01 sig:01 val:01 struct:01 unification:01 sig:01 val:01 struct:01 wrote:01 compile:01 compile:01 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 wrote: > 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 >