From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 5A4307FC18 for ; Mon, 16 Feb 2015 19:03:35 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of lpw25@cam.ac.uk) identity=pra; client-ip=131.111.8.140; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="lpw25@cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of lpw25@cam.ac.uk) identity=mailfrom; client-ip=131.111.8.140; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="lpw25@cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of postmaster@ppsw-40.csi.cam.ac.uk designates 131.111.8.140 as permitted sender) identity=helo; client-ip=131.111.8.140; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="postmaster@ppsw-40.csi.cam.ac.uk"; x-conformance=sidf_compatible; x-record-type="v=spf1" X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0AbAQALMOJUnIwIb4NchDKDA6xoBpg/AoEXQwEBAQEBARABAQEBAQgLCQkULoQMAQEBAwEjSA4FCwsYAgIFIQICDwEEDTwTiBkDCQgEtyqRMg1FhGMBAQgBAQEBHoEhhGOFCIJDgXczB4JogUIFlymBRoEYi3GCRoM+hBBvgkMBAQE X-IPAS-Result: A0AbAQALMOJUnIwIb4NchDKDA6xoBpg/AoEXQwEBAQEBARABAQEBAQgLCQkULoQMAQEBAwEjSA4FCwsYAgIFIQICDwEEDTwTiBkDCQgEtyqRMg1FhGMBAQgBAQEBHoEhhGOFCIJDgXczB4JogUIFlymBRoEYi3GCRoM+hBBvgkMBAQE X-IronPort-AV: E=Sophos;i="5.09,589,1418079600"; d="scan'208";a="121999168" Received: from ppsw-40.csi.cam.ac.uk ([131.111.8.140]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 16 Feb 2015 19:03:34 +0100 X-Cam-AntiVirus: no malware found X-Cam-ScannerInfo: http://www.cam.ac.uk/cs/email/scanner/ Received: from host86-159-4-23.range86-159.btcentralplus.com ([86.159.4.23]:46762 helo=study.localdomain) by ppsw-40.csi.cam.ac.uk (smtp.hermes.cam.ac.uk [131.111.8.156]:587) with esmtpsa (PLAIN:lpw25) (TLSv1.2:AES128-GCM-SHA256:128) id 1YNQ18-0002c7-jd (Exim 4.82_3-c0e5623) (return-path ); Mon, 16 Feb 2015 18:03:34 +0000 From: Leo White To: Gabriel Scherer Cc: Carl Eastlund , caml users References: X-Face: "XWxb[u_Z\PA_Y?9@|IA!!+jTb(/290-*ea/Un$I0B98.$n%eL.;2w*,z]WR#T:,p[ NBd++M7l]#7zj7!{~iw $W-"/=|dVjhT[D{4~gE}gK<2`.6fs!;uqqud]vs2N/3^m7{aS1V, Date: Mon, 16 Feb 2015 18:03:23 +0000 In-Reply-To: (Gabriel Scherer's message of "Sun, 15 Feb 2015 11:26:56 +0100") Message-ID: <87a90d68es.fsf@study.localdomain> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] Weird type error involving 'include' and applicative functors Gabriel gives an accurate accout of what is going on. To me, it looks like the type-checker should probably accept this, so I would submit it as a bug (I suspect a missing call to Env.normalize_path somewhere, but perhaps there is something more significant going on here). Regards, Leo Gabriel Scherer writes: > That is one of the dark corners of the module system. > > I don't know whether an ideal type-checker should accept your last > definition or not. It is non-intuitive that some are accepted and > others rejected; some things in the module system are non-intuitive > for good reasons, some others because of implementation limitations, > and it's not always clear to non-experts which is which).=CB=99But I can > explain why the last definition is harder for the type-checker to > accept than the other. > > # module A =3D struct > module T =3D struct end > module C =3D struct > include Make(T) > end > include C > end > ;; > module A : > sig > module T : sig end > module C : sig type t =3D Make(T).t end > type t =3D Make(T).t > end > > # module B =3D struct > module C =3D struct > module T =3D struct end > include Make(T) > end > include C > end > ;; > module B : > sig > module C : sig module T : sig end type t =3D Make(T).t end > module T =3D C.T > type t =3D Make(T).t > end > > > Note the important difference in the inferred signatures in both > cases. Both modules have > type t =3D Make(T).t > but, in the first case, this is the *same module T* that is mentioned > in the signature of T, while in the second case, there are two > different modules, C.T and T (the latter being generated by the > "include", with an equation that it is equal to the former). > > The reasoning to check against your signature > sig > type t > module C : S with type t =3D t > end > is thus more complicated in the second case: the type-checker would > need to use the equation (T =3D C.T) to check that indeed C.t is equal > to t. > > I think this is due to the rather contorted way you define C first in > the implementations and include it later, while in the signature first > define t and then C. Note that the following signature, which is > morally equivalent, accepts both implementations (and thus all the > functors in your file): > sig > module C : S > type t =3D C.t > end > > > On Fri, Feb 13, 2015 at 10:40 PM, Carl Eastlund > wrote: >> This seems to be a compiler bug, but let me know if I've missed somethin= g. >> The behavior I see is that Make_ok1 and Make_ok2 compile fine, but the v= ery >> similar functor Make_bad does not. I get this compile error: >> >> =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D >> >> Error: Signature mismatch: >> Modules do not match: >> sig >> module C : sig module T : sig end type t =3D Make(T).t= end >> module T =3D C.T >> type t =3D Make(T).t >> end >> is not included in >> sig type t module C : sig type t =3D t end end >> In module C: >> Modules do not match: >> sig module T : sig end type t =3D Make(T).t end >> is not included in >> sig type t =3D C.t end >> In module C: >> Type declarations do not match: >> type t =3D Make(T).t >> is not included in >> type t =3D t >> >> =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D >> >> And here is the code: >> >> =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D >> >> module type S =3D sig type t end >> module Make (M : sig end) : S =3D struct type t end >> >> module Make_ok1 (M : sig end) : sig >> >> type t >> module A : S with type t =3D t >> >> end =3D struct >> >> module A =3D struct >> include Make (struct end) >> end >> include A >> >> end >> >> module Make_ok2 (M : sig end) : sig >> >> type t >> module B : S with type t =3D t >> >> end =3D struct >> >> module T =3D struct end >> module B =3D struct >> include Make (T) >> end >> include B >> >> end >> >> module Make_bad (M : sig end) : sig >> >> type t >> module C : S with type t =3D t >> >> end =3D struct >> >> module C =3D struct >> module T =3D struct end >> include Make (T) >> end >> include C >> >> end >> >> =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D >> >> -- >> Carl Eastlund