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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 59C857FC18 for ; Sun, 15 Feb 2015 11:27:51 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.213.179; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.213.179 as permitted sender) identity=mailfrom; client-ip=209.85.213.179; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-ig0-f179.google.com) identity=helo; client-ip=209.85.213.179; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-ig0-f179.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0BKAgBKdOBUlLPVVdFbhDIEgn+uKZcAAoEGB0MBAQEBAQEQAQEBAQcLCwkSMIQNAQEEEhEdARsPDgEDDAYFCwMKAgImAgIiAREBBQEcBhMIGod2AQMRrBg+MYsugWuCd4tEChknDVSEcgEBAQEGAQEBAQEXAQUOgROJa4Q6MweCaIFCBZhvgRiON4F0EiOBDAmEET0xgkMBAQE X-IPAS-Result: A0BKAgBKdOBUlLPVVdFbhDIEgn+uKZcAAoEGB0MBAQEBAQEQAQEBAQcLCwkSMIQNAQEEEhEdARsPDgEDDAYFCwMKAgImAgIiAREBBQEcBhMIGod2AQMRrBg+MYsugWuCd4tEChknDVSEcgEBAQEGAQEBAQEXAQUOgROJa4Q6MweCaIFCBZhvgRiON4F0EiOBDAmEET0xgkMBAQE X-IronPort-AV: E=Sophos;i="5.09,580,1418079600"; d="scan'208";a="100116361" Received: from mail-ig0-f179.google.com ([209.85.213.179]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 15 Feb 2015 11:27:38 +0100 Received: by mail-ig0-f179.google.com with SMTP id l13so18673141iga.0 for ; Sun, 15 Feb 2015 02:27:36 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; bh=TtKVxTK46pzCHsnyGptj5WTLuwvJ1fFZTcYGCproblQ=; b=qI5tFSKQ4L/BIaSqkQPHjhGy4od6gL6waidnt5kPn+A02vXn3DTGwga4R7Pza1lrH0 4BA1j+9f1+JAvKCD4QnnBa1+7Umm/W6PjxTH2sikmKouIiSjKTYbQ8C41cSjww2qDPQ7 GC8tJF+PSSxFb1Rd8uATt71hu9g2bc3YWVK6rgc8cIi5wEMh/82T9CU3v7IjiYWcmGmd H4+1NUNHF8LmA3hMXjJSu2CbcU7ux0K7jFh6CLPHDMt1GnguHMXYCZHq1/mjcwTP8ox8 IQWIhM6fF6BkuH++DlwuAZqaZdsKdTiGS1k8+52SFqh20HccvJBFRBtNN+KM6ab/fO9Z lgXA== X-Received: by 10.50.62.110 with SMTP id x14mr15387800igr.2.1423996056789; Sun, 15 Feb 2015 02:27:36 -0800 (PST) MIME-Version: 1.0 Received: by 10.36.13.195 with HTTP; Sun, 15 Feb 2015 02:26:56 -0800 (PST) In-Reply-To: References: From: Gabriel Scherer Date: Sun, 15 Feb 2015 11:26:56 +0100 Message-ID: To: Carl Eastlund Cc: caml users Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] Weird type error involving 'include' and applicative functors 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 something. > The behavior I see is that Make_ok1 and Make_ok2 compile fine, but the ve= ry > 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