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.0 required=5.0 tests=AWL,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 discorde.inria.fr (discorde.inria.fr [192.93.2.38]) by yquem.inria.fr (Postfix) with ESMTP id 8C752BC69 for ; Wed, 21 Mar 2007 16:51:55 +0100 (CET) Received: from wx-out-0506.google.com (wx-out-0506.google.com [66.249.82.238]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l2LFpsX9000469 for ; Wed, 21 Mar 2007 16:51:54 +0100 Received: by wx-out-0506.google.com with SMTP id i26so409931wxd for ; Wed, 21 Mar 2007 08:51:53 -0700 (PDT) DKIM-Signature: a=rsa-sha1; c=relaxed/relaxed; d=gmail.com; s=beta; 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; b=ciE2xAx2d7nWWLJFxpiEVS/3G/jJRh93VxwkplHb0/d/b0mFtdu+dBhW2EmJQRYEdLeXCmpUt1ddm93OxzD89EYu37lCzxT1AHTZYUqYlYcHdH+qx1WxLa8oSlNkfGern9XhnwKsQCm2XySnKb2ePq6yP0tc0JlnKhk8nhiTLS4= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=abbuuSb9ucw3EVStIVp/aYSKVEij2fGWNiijqwVqZ+y4AOQsSamdLejvmw0VqbawV7z4djrytGJdHoc9uogIOT/itATUYSq/gBvXJAkyK7KgC3dgw7U/lG3+3lpI9Syh6oPeDHjbl69LpEHIBhzQlePd1RLeO93SFbMMA1bNkTQ= Received: by 10.90.55.19 with SMTP id d19mr2342761aga.1174492313225; Wed, 21 Mar 2007 08:51:53 -0700 (PDT) Received: by 10.90.115.19 with HTTP; Wed, 21 Mar 2007 08:51:53 -0700 (PDT) Message-ID: Date: Wed, 21 Mar 2007 10:51:53 -0500 From: "Derek Dreyer" To: "Stephen Weeks" Subject: Re: [Caml-list] question on type checking Cc: caml-list@yquem.inria.fr In-Reply-To: <604682010703201120j54305a8dmf7174f434cedfa96@mail.gmail.com> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Content-Disposition: inline References: <604682010703201120j54305a8dmf7174f434cedfa96@mail.gmail.com> X-j-chkmail-Score: MSGID : 4601549A.000 on discorde : j-chkmail score : X : 0/20 1 0.000 -> 1 X-Miltered: at discorde with ID 4601549A.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; bug:01 typechecker:01 typecheck:01 typechecker:01 sig:01 sig:01 bug:01 applicative:01 functor:01 variants:01 struct:01 struct:01 beginner's:01 ocaml:01 derek:98 This appears to be a bug in the typechecker. Perhaps a more obvious instance of the problem is if, after the (top-level) definition of S in your first example you write: module T = S let x = if true then T.A else S.A This clearly should typecheck, but instead you get the error message: > This expression has type S.t = F(S.Z).t but is here used with type > T.t = F(T.Z).t Huh? You mean S.t does not equal T.t when I just defined T = S? The problem is precisely that the typechecker is not properly selfifying (strengthening) the signature of S in processing "module T = S". When properly selfified, the signature of S (and thus also T) should be sig module Z : sig end module M : sig type t = F(S.Z) = A end type t = F(S.Z) = A end end but instead of F(S.Z), it's just doing F(Z). This wouldn't be an issue if the language tracked structure identities across renamings (since S.Z and T.Z are clearly the same structure), but it doesn't. In your second example, this bug didn't pop up because Z was not named, so M.t could not be characterized precisely through an applicative functor type of the form F().t. In your third example, this bug didn't pop up because you didn't rename the structure S (and hence tickle the signature strengthening bug). I'm guessing this bug should be easy to fix. Derek On 3/20/07, Stephen Weeks wrote: > Why does one of the programs below fail to type check while the other two minor > variants succeed? I would expect all three to succeed. > > ---------------------------------------------------------------------- > (* FAILS *) > module F (Z : sig end) = struct > type t = A > end > > module S = struct > module Z = struct end > module M = F (Z) > include M > end > > let f x = > let module S = S in > match x with > | S.A -> () > ---------------------------------------------------------------------- > (* WORKS *) > module F (Z : sig end) = struct > type t = A > end > > module S = struct > module M = F (struct end) > include M > end > > let f x = > let module S = S in > match x with > | S.A -> () > ---------------------------------------------------------------------- > (* WORKS *) > module F (Z : sig end) = struct > type t = A > end > > module S = struct > module Z = struct end > module M = F (Z) > include M > end > > let f x = > match x with > | S.A -> () > ---------------------------------------------------------------------- > > _______________________________________________ > Caml-list mailing list. Subscription management: > http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list > Archives: http://caml.inria.fr > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs >