From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id 56A03BC57 for ; Tue, 7 Sep 2010 22:46:24 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AioBAKNBhkzRVdQ2kGdsb2JhbAChAAgVAQEBAQkJDAcRAx+mbItIhk6IHgEBAwWFOASEQYVXiGc X-IronPort-AV: E=Sophos;i="4.56,330,1280700000"; d="scan'208";a="67084737" Received: from mail-vw0-f54.google.com ([209.85.212.54]) by mail1-smtp-roc.national.inria.fr with ESMTP; 07 Sep 2010 22:46:23 +0200 Received: by vws7 with SMTP id 7so6070442vws.27 for ; Tue, 07 Sep 2010 13:46:23 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:received:sender:received :in-reply-to:references:date:x-google-sender-auth:message-id:subject :from:to:cc:content-type:content-transfer-encoding; bh=Lrz7eVmDcGCwISjVDOq68XRFSRwKHoEeE+Ur4/m/uhM=; b=yHeU8Z3n6KHig+eR/MJUQs8FTx3cxEZJjr/9AVCstHcRI9E6BcvCsKyNSBOffcPUpK uOcftxnl+HmC7fEVDIERTCNNfZ+TRmeV72SvTqKqfRxhMMZsXIaHZAutOPXUCLXcbELA XVTlkLbIM2HOf7OP+JqcIBcCcIuF0ZOmYjSrE= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type :content-transfer-encoding; b=jMomOREf8Eqy2vcYzSbaBf4IUOo82Yq7cSdTihZdaqvO7bvc7LOHfbW7JAdQegDMpi uyEk8SeapVk6+FwtzDQpmM3qbfRr0GE7/OX4qvxHuy2TnTGbTlmFnG02UA1iBJXzYDAj qHDVnl24YvOQwr6Vq5xx1nEskSMqtctHP0lL0= MIME-Version: 1.0 Received: by 10.220.76.200 with SMTP id d8mr402183vck.121.1283892383098; Tue, 07 Sep 2010 13:46:23 -0700 (PDT) Sender: jacques.garrigue@gmail.com Received: by 10.220.76.80 with HTTP; Tue, 7 Sep 2010 13:46:22 -0700 (PDT) In-Reply-To: References: <19588.45205.199003.965321@blau.inf.tu-dresden.de> Date: Wed, 8 Sep 2010 05:46:22 +0900 X-Google-Sender-Auth: YAPZ5tBeNC2T6hoTaoFDjwZR9LI Message-ID: Subject: Re: [Caml-list] functor substitution gives error From: Jacques Garrigue To: =?ISO-8859-1?Q?Daniel_B=FCnzli?= Cc: Hendrik Tews , caml-list@inria.fr Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Spam: no; 0.00; functor:01 bunzli:01 buenzli:01 sig:01 sig:01 struct:01 struct:01 restricting:01 compiler:01 applicative:01 functors:01 applicative:01 functor:01 wrote:01 abstract:01 On Mon, Sep 6, 2010 at 6:39 PM, Daniel B=FCnzli wrote: > I think I just hit the same kind problem. > > This doesn't compile : > ---- > module A : sig > type m > module M : sig > type t =3D m > end > end =3D struct > module M =3D struct > module S =3D String > module Smap =3D Map.Make(S) > type t =3D int Smap.t > end > type m =3D M.t > end > ---- > > Type declarations do not match: > type t =3D int Smap.t > is not included in > type t =3D m > > However if I put S outside M, or if I specify the type of Smap it compile= s : At first, I thought this was a different problem, since there is no "struct end". However, this is actually the same problem. To understand what is happening, you must look at what is inferred for M.Smap.t in the different cases. In the first and second case: type 'a t =3D 'a Map.Make(S).t If you specify the type of Smap it becomes: type +'a t (just abstract) or after strengthening (making types refer to their location) type 'a t =3D 'a M.Smap.t Here the problem is that S, by being only defined locally, plays the same role as "struct end". The above type equation (in the first case) forbids the stengthening of M.Smap.t, but later it has to be discarded because one is not allowed to depend on a local module, meaning that we end up losing a type equation. In the second case, this doesn't happen because S is no longer local to M, and can be kept. And in the last one, by restricting the type of Smap, you remove the type equation on Smap.t, allowing its strengthening (only one type equation is allowed per type, so if there is already one, strengthening cannot be done). Since 3.12, there is a new compiler option, -no-app-funct, which disables applicative functors, and as a result allows strengthening in more cases. This solves your problem, but not Hendrik's, because his example requires applicative functor to start with. Jacques Garrigue [Your 2 other versions] > ---- > module A : sig > type m > module M : sig > type t =3D m > end > end =3D struct > module S =3D String > module M =3D struct > module Smap =3D Map.Make(S) > type t =3D int Smap.t > end > type m =3D M.t > end > ---- > > ---- > module A : sig > type m > module M : sig > type t =3D m > end > end =3D struct > module M =3D struct > module S =3D String > module Smap =3D (Map.Make(S) : Map.S with type key =3D S.t) > type t =3D int Smap.t > end > type m =3D M.t > end > ---- > > Daniel