From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 C45C67EE48 for ; Thu, 19 Feb 2015 19:23:51 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of milanst@gmail.com) identity=pra; client-ip=209.85.223.178; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="milanst@gmail.com"; x-sender="milanst@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of milanst@gmail.com designates 209.85.223.178 as permitted sender) identity=mailfrom; client-ip=209.85.223.178; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="milanst@gmail.com"; x-sender="milanst@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-ie0-f178.google.com) identity=helo; client-ip=209.85.223.178; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="milanst@gmail.com"; x-sender="postmaster@mail-ie0-f178.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0BmAgDwKOZUlLLfVdFBGg6DSloEgwWwBI9ehXECgRoHQwEBAQEBARABAQEBBwsLCRIwhBABAQQSER0BGw8DCwEDDAYFCwMKAgIJHQICIQEBEQEFAQoSBhMIChCHeAEDEQ03rns+MYsugWuCd407ChknAwpUhFwBAQEBAQEEAQEBAQEBARUBBQ6BE4lugkSBdzMHgmiBQgWEWgqFYIhjhB+BRoEZOItLgkiBdBIjgQwJgiQcgRNbIDEBgkIBAQE X-IPAS-Result: A0BmAgDwKOZUlLLfVdFBGg6DSloEgwWwBI9ehXECgRoHQwEBAQEBARABAQEBBwsLCRIwhBABAQQSER0BGw8DCwEDDAYFCwMKAgIJHQICIQEBEQEFAQoSBhMIChCHeAEDEQ03rns+MYsugWuCd407ChknAwpUhFwBAQEBAQEEAQEBAQEBARUBBQ6BE4lugkSBdzMHgmiBQgWEWgqFYIhjhB+BRoEZOItLgkiBdBIjgQwJgiQcgRNbIDEBgkIBAQE X-IronPort-AV: E=Sophos;i="5.09,609,1418079600"; d="scan'208";a="100655198" Received: from mail-ie0-f178.google.com ([209.85.223.178]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 19 Feb 2015 19:23:50 +0100 Received: by iecar1 with SMTP id ar1so1963219iec.11 for ; Thu, 19 Feb 2015 10:23:49 -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=CKcBBIPMkFSPiK6g/2EeR/ua2dpmIQYo3whkDAy8Dt4=; b=DwtYpcmG193u3Se+pLCPNBzAlhB5DzRYlhD6eOLdPA4beoVsbgIu/52xBkkMVYZyrJ dQwmLmF6QPV+oDsarN/6tlc2+ZRaZLXUP2+A1C8BCCBJ7+qVRVMFrgxYfU1mNtO9ONUx FQn4WE+/4nXstAubD2PATO+iqCVpnkj2cUP5Mb/IxzkgpiaDGKMLWlZgcYuH8JuzTs4y HTRCl/Ai9utIBKdtdTdHh2lmpXPmWRCChWqw9q+7qhTr18HjkecqPhT64F5u/0t3L7oI cifF72373yzGeW5NsLN0/O3KC/UJL1gbTAUYsoxmwnAxeyvoM52QxnRIJguiqIimBlND dh2Q== X-Received: by 10.50.18.49 with SMTP id t17mr9148676igd.3.1424370229290; Thu, 19 Feb 2015 10:23:49 -0800 (PST) MIME-Version: 1.0 Received: by 10.64.168.5 with HTTP; Thu, 19 Feb 2015 10:23:09 -0800 (PST) In-Reply-To: References: <87a90d68es.fsf@study.localdomain> From: =?UTF-8?Q?Milan_Stanojevi=C4=87?= Date: Thu, 19 Feb 2015 13:23:09 -0500 Message-ID: To: Leo White Cc: Gabriel Scherer , Carl Eastlund , 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 Oh, it seems Carl already did it. I'll mark mine as duplicate. On Thu, Feb 19, 2015 at 1:21 PM, Milan Stanojevi=C4=87 = wrote: > I submitted a bug report. > http://caml.inria.fr/mantis/view.php?id=3D6788 > > > On Tue, Feb 17, 2015 at 4:40 PM, Milan Stanojevi=C4=87 wrote: >> It seems that type checker does know that C.T and T are aliases since >> this compiles >> >> module C =3D struct >> module T =3D struct end >> include Make (T) >> end >> include C >> >> let f (x : Make(Make(T)).t) : Make(Make(C.T)).t =3D x >> >> Somehow the fact that C.T =3D T is lost when checking against the signat= ure. >> >> >> >> >> On Mon, Feb 16, 2015 at 1:03 PM, Leo White wrote: >>> 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 c= an >>>> 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 somet= hing. >>>>> The behavior I see is that Make_ok1 and Make_ok2 compile fine, but th= e very >>>>> 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 >>> >>> -- >>> Caml-list mailing list. Subscription management and archives: >>> https://sympa.inria.fr/sympa/arc/caml-list >>> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners >>> Bug reports: http://caml.inria.fr/bin/caml-bugs