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 A3C6A7EE48 for ; Thu, 19 Feb 2015 19:21:53 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of milanst@gmail.com) identity=pra; client-ip=209.85.223.171; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="milanst@gmail.com"; x-sender="milanst@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of milanst@gmail.com designates 209.85.223.171 as permitted sender) identity=mailfrom; client-ip=209.85.223.171; receiver=mail2-smtp-roc.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 (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-ie0-f171.google.com) identity=helo; client-ip=209.85.223.171; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="milanst@gmail.com"; x-sender="postmaster@mail-ie0-f171.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0B5AgCnKOZUm6vfVdFBGg6DSloEgwWwBIQDi1EKhXECgRoHQwEBAQEBARABAQEBAQYLCwkULoQQAQEEEhEdARsPAwsBAwwGBQsDCgICCR0CAiEBAREBBQEKEgYTEhCHeAEDEQ03rnk+MYsugWuCd407ChknAwpUhFwBAQEBAQUBAQEBAQEBFQEFDoETiW6CRIF3MweCLQwvEYExBYRaCoVgiGOEH4FGgRk4i0uCSIF0EiOBDAmDU1sgMQGCQgEBAQ X-IPAS-Result: A0B5AgCnKOZUm6vfVdFBGg6DSloEgwWwBIQDi1EKhXECgRoHQwEBAQEBARABAQEBAQYLCwkULoQQAQEEEhEdARsPAwsBAwwGBQsDCgICCR0CAiEBAREBBQEKEgYTEhCHeAEDEQ03rnk+MYsugWuCd407ChknAwpUhFwBAQEBAQUBAQEBAQEBFQEFDoETiW6CRIF3MweCLQwvEYExBYRaCoVgiGOEH4FGgRk4i0uCSIF0EiOBDAmDU1sgMQGCQgEBAQ X-IronPort-AV: E=Sophos;i="5.09,609,1418079600"; d="scan'208";a="122565906" Received: from mail-ie0-f171.google.com ([209.85.223.171]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 19 Feb 2015 19:21:52 +0100 Received: by iecat20 with SMTP id at20so1927268iec.12 for ; Thu, 19 Feb 2015 10:21:51 -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=JgAaTfYVZfMByH0T3e5KkFlqPkeTXG8yAqrk+9aTQvY=; b=TMqGnThFdzsNF+8vJOAEigo61zODInGGzYHPWNpihT1Huj9EkG3zzMhA5z5Y81eFfJ afewGa0j5Y0V3URrSp0jFiktBs5QS526fllNokipU8LhDhMlA7H/FL8SXO6mREgUm/oK /EeMlm4KDwd2TTn3RFyQhoy9YN3SwcF0taDcAgYg7J6/tWvYhl/3gCFtsgYWKvH3Oa2z YAY8rLoe4NFzObnykptTLXHpINwWekPvY3RCY4MmwUCntA+Ha6eD8lbB1UA7FZoGToF0 R2MUl31fO6avcJ6Qz4BDtt6IWhGbVNbJckCaq/mPWaloVUgcDKlc//UyFRDx3jrNP/1a LAgg== X-Received: by 10.42.250.11 with SMTP id mm11mr7831423icb.54.1424370111617; Thu, 19 Feb 2015 10:21:51 -0800 (PST) MIME-Version: 1.0 Received: by 10.64.168.5 with HTTP; Thu, 19 Feb 2015 10:21:11 -0800 (PST) In-Reply-To: References: <87a90d68es.fsf@study.localdomain> From: =?UTF-8?Q?Milan_Stanojevi=C4=87?= Date: Thu, 19 Feb 2015 13:21:11 -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 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 signatu= re. > > > > > 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 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 someth= ing. >>>> The behavior I see is that Make_ok1 and Make_ok2 compile fine, but the= 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