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 8B4C37F798 for ; Tue, 17 Feb 2015 22:40:45 +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.172; 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.172 as permitted sender) identity=mailfrom; client-ip=209.85.223.172; 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-f172.google.com) identity=helo; client-ip=209.85.223.172; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="milanst@gmail.com"; x-sender="postmaster@mail-ie0-f172.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0DGAQCStONUlKzfVdFbDoNKWgSCf69zj1yFcQKBEwdDAQEBAQEBEAEBAQEHCwsJEjCEDQEBBBIRHQEbDwMLAQMMBgULAwoCAgkdAgIhAQERAQUBChIGExIQh3gBAxENrSY+MYsugWuCd40CChknAwpUhGABAQEBAQEEAQEBAQEBARUBBQ6BE4lugkSBdzMHgmiBQgWEVgqFWohVhBqBRoEYOIs5gkaBdBIjgQwJg1NbIDGCQwEBAQ X-IPAS-Result: A0DGAQCStONUlKzfVdFbDoNKWgSCf69zj1yFcQKBEwdDAQEBAQEBEAEBAQEHCwsJEjCEDQEBBBIRHQEbDwMLAQMMBgULAwoCAgkdAgIhAQERAQUBChIGExIQh3gBAxENrSY+MYsugWuCd40CChknAwpUhGABAQEBAQEEAQEBAQEBARUBBQ6BE4lugkSBdzMHgmiBQgWEVgqFWohVhBqBRoEYOIs5gkaBdBIjgQwJg1NbIDGCQwEBAQ X-IronPort-AV: E=Sophos;i="5.09,595,1418079600"; d="scan'208";a="122190974" Received: from mail-ie0-f172.google.com ([209.85.223.172]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 17 Feb 2015 22:40:44 +0100 Received: by iecvy18 with SMTP id vy18so44160248iec.6 for ; Tue, 17 Feb 2015 13:40:43 -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=tw5wx0efBAX3asnm2RCr9ZrfyyCigjNQzVlP/0rYg58=; b=zdUhoCBKTaW9cgc0EJuOuzAnL+fWuYJY7fYD5NiRs/kmcp1vM5pBS6flGVVDGBgwJJ OtkFZk7Geius01UeoKsy/CGW18FaGxT1lc3v4e2WbSK67ro1Edo7TbcMcnQpHNG2ggt6 LHQLbAyx0siS0WtzgfMbzfni/YWM7BAQknJX92LS26fh4zeYMyDKbwgZ7UJL+EdsQueH fBRyRSBHrZEl3jTiKeFf9Zm0i/aeu/zx6h8XTTp4Wx+vlvn/TC6qWAMohwteSW5S8dT9 zXqNOVvnBnl3Z8nB20N19AWTLxuOx9blPz0W34olCBAqdZ40VaawYvvneyw+j0kdM7eF lnlg== X-Received: by 10.107.46.32 with SMTP id i32mr38311762ioo.21.1424209243430; Tue, 17 Feb 2015 13:40:43 -0800 (PST) MIME-Version: 1.0 Received: by 10.64.168.5 with HTTP; Tue, 17 Feb 2015 13:40:03 -0800 (PST) In-Reply-To: <87a90d68es.fsf@study.localdomain> References: <87a90d68es.fsf@study.localdomain> From: =?UTF-8?Q?Milan_Stanojevi=C4=87?= Date: Tue, 17 Feb 2015 16:40:03 -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 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 signature. 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 somethi= ng. >>> 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