From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=1.9 required=5.0 tests=AWL,DNS_FROM_RFC_POST, RCVD_IN_SORBS_WEB autolearn=disabled version=3.1.3 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 76F6FBC69 for ; Mon, 24 Dec 2007 12:44:06 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAL8qb0fUKEUHh2dsb2JhbACBV443AQEBCAoply4 X-IronPort-AV: E=Sophos;i="4.24,203,1196636400"; d="scan'208";a="5998572" Received: from mail.dravanet.hu (HELO arwen.dravanet.hu) ([212.40.69.7]) by mail1-smtp-roc.national.inria.fr with ESMTP; 24 Dec 2007 12:44:06 +0100 Received: from arwen-vbmailshield (localhost.localdomain [127.0.0.1]) by arwen-vbmailshield (Postfix) with SMTP id 6F6981054 for ; Mon, 24 Dec 2007 12:44:05 +0100 (CET) Received: from arwen.dravanet.hu ([127.0.0.1]) by arwen ([192.168.69.23]) with SMTP (gateway) id A05ED657D04; Mon, 24 Dec 2007 12:44:05 +0100 Received: from [127.0.0.1] (212-40-82-191.adsl-pool.dravanet.hu [212.40.82.191]) by arwen.dravanet.hu (Postfix) with ESMTP id 22CFA416 for ; Mon, 24 Dec 2007 12:44:04 +0100 (CET) Message-ID: <476F9B82.2060103@dravanet.hu> Date: Mon, 24 Dec 2007 12:44:02 +0100 From: =?ISO-8859-1?Q?=22M=E1rk_S=2E_Zolt=E1n=22?= User-Agent: Thunderbird 2.0.0.9 (Windows/20071031) MIME-Version: 1.0 To: Caml Mailing List Subject: Re: [Caml-list] Type visibility limitation in recursive modules References: <476E6FB7.6040100@dravanet.hu> In-Reply-To: <476E6FB7.6040100@dravanet.hu> Content-Type: text/plain; charset=ISO-8859-1; format=flowed X-Antivirus: avast! (VPS 071215-0, 12/15/2007), Outbound message X-Antivirus-Status: Clean Content-Transfer-Encoding: quoted-printable X-VBMailShield: version 1.57.6 at arwen - template: default X-Spam: no; 0.00; recursive:01 sig:01 struct:01 sig:01 val:01 struct:01 compiler:01 compiler:01 val:01 ocamlc:01 ocamlc:01 bug:01 cheers:01 behold:98 wrote:01 M=E1rk S. Zolt=E1n wrote: > Behold the following code snippet: > > module rec Aleph : > sig > type t =3D Tag of Beth.t > end =3D > struct > type t =3D Tag of Beth.t > end > and Beth : > sig > type t > val scandalous : Aleph.t > end =3D > struct > type t =3D Aleph.t list > let scandalous =3D Aleph.Tag((* HERE BE DRAGONS *) []) > end > > The compiler complains that the empty list after HERE BE DRAGONS has=20 > type 'a list but it is used with type Beth.t. I'd expect the compiler=20 > to discover that those types can be unified via 'a =3D=3D Aleph.t, sinc= e=20 > as far as I can tell, all necessary facts are visible at that point.=20 > Replacing "Beth : sig type t ..." with "Beth : sig type t =3D Aleph.t=20 > list ..." does away with the error, but I would very much like to keep=20 > Beth.t an opaque type. Is this an intended behavior? And if it is=20 > intended, is there a way to tell the compiler what I really want it to=20 > do? > > Thanks in advance for any help. > > Z- The plot thickens. The following code provokes an error message stating=20 explicitly that type t in Beth is not the same as Beth.t: ---------------------- module rec Aleph : sig type t =3D Tag of Beth.t end =3D struct type t =3D Tag of Beth.t end and Beth : sig type t =20 val a_beth_t_value : t val scandalous : Aleph.t end =3D struct type t =3D Aleph.t list let a_beth_t_value =3D ([] : t) let scandalous =3D Aleph.Tag(a_beth_t_value) end ---------------------- $ ocamlc -i Anomaly.ml File "Anomaly.ml", line 18, characters 33-49: This expression has type t =3D Aleph.t list but is here used with type Be= th.t --------------------- The error message references the mention of a_beth_value in the let=20 scandalous ... line. The ([] : t) construct in the previous line was=20 necessary to trigger the 'This expression has type t =3D Aleph.t list ...= '=20 message, since a bare [] only triggers "This expression has type Aleph.t=20 list but ...", without an indication that it knows that type t is=20 Aleph.t list. However, reexporting a_beth_t_value from Aleph satisfies the compiler: -------------------- module rec Aleph : sig type t =3D Tag of Beth.t val a_reexported_beth_t_value : Beth.t end =3D struct type t =3D Tag of Beth.t let a_reexported_beth_t_value =3D Beth.a_beth_t_value end and Beth : sig type t val a_beth_t_value : t val scandalous : Aleph.t end =3D struct type t =3D Aleph.t list let a_beth_t_value =3D [] let scandalous =3D Aleph.Tag(Aleph.a_reexported_beth_t_value) end -------------------- $ ocamlc -i Anomaly.ml module rec Aleph : sig type t =3D Tag of Beth.t val a_reexported_beth_t_value : Beth.t end and Beth : sig type t val a_beth_t_value : t val scandalous : Aleph.t end -------------------- So far it sounds like the compiler acknowledges there is a type Beth.t=20 and identifies it with type t in the sig of Beth, but fails to make the=20 connection between this type and the Aleph.t list type expression inside=20 the struct of Beth. But even that is only true if the type expression in=20 question uses a built-in list; if I replace it with an algebraic type=20 implementing my own list, even the original example starts working. ------------------- module rec Aleph : sig type t =3D Tag of Beth.t end =3D struct type t =3D Tag of Beth.t end and Beth : sig type t =20 val scandalous : Aleph.t end =3D struct type t =3D Cons of Aleph.t * t | Nil let scandalous =3D Aleph.Tag(Nil) end ----------------- $ ocamlc -i Anomaly.ml module rec Aleph : sig type t =3D Tag of Beth.t end and Beth : sig type t val scandalous : Aleph.t end ----------------- This is a bug, isn't it? Cheers Z-