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.0 required=5.0 tests=AWL,HTML_MESSAGE autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id E3404BBAF for ; Wed, 11 Jun 2008 11:25:35 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AscAAJA2T0jVx4q1fGdsb2JhbACCQjGNdYEpAQELBQIGBxGeOQ X-IronPort-AV: E=Sophos;i="4.27,623,1204498800"; d="scan'208,217";a="11876679" Received: from smtp-dub.microsoft.com ([213.199.138.181]) by mail2-smtp-roc.national.inria.fr with ESMTP; 11 Jun 2008 11:25:35 +0200 Received: from DUB-EXHUB-C301.europe.corp.microsoft.com (65.53.213.91) by DUB-EXGWY-E802.partners.extranet.microsoft.com (10.251.129.2) with Microsoft SMTP Server (TLS) id 8.1.240.5; Wed, 11 Jun 2008 10:25:32 +0100 Received: from EA-EXMSG-C332.europe.corp.microsoft.com ([169.254.2.240]) by DUB-EXHUB-C301.europe.corp.microsoft.com ([65.53.213.91]) with mapi; Wed, 11 Jun 2008 10:25:32 +0100 From: Josh Berdine To: Charles Hymans , "caml-list@yquem.inria.fr" Date: Wed, 11 Jun 2008 10:25:30 +0100 Subject: RE: [Caml-list] typing of recursive modules in 3.10.2 Thread-Topic: [Caml-list] typing of recursive modules in 3.10.2 Thread-Index: AcjLMArKKJWVWroSQq6vRSAtguqt3gAclHxQ Message-ID: <857DD0FDAC042B4485F9F5F4EA675104166C8EB605@EA-EXMSG-C332.europe.corp.microsoft.com> References: <676aba050806101227m1696d555n6f23f55f57af0db2@mail.gmail.com> In-Reply-To: <676aba050806101227m1696d555n6f23f55f57af0db2@mail.gmail.com> Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: acceptlanguage: en-US Content-Type: multipart/alternative; boundary="_000_857DD0FDAC042B4485F9F5F4EA675104166C8EB605EAEXMSGC332eu_" MIME-Version: 1.0 X-Spam: no; 0.00; recursive:01 typecheck:01 typechecker:01 bug:01 cheers:01 recursive:01 ocaml:01 sig:01 val:01 functor:01 sig:01 val:01 struct:01 struct:01 checker:01 --_000_857DD0FDAC042B4485F9F5F4EA675104166C8EB605EAEXMSGC332eu_ Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: quoted-printable Hi Charles, I don't know if it helps, and this doesn't address your concern over predic= tability, but your example will also typecheck if you annotate the argument= of f with t: let f (x : t) =3D A.g x I can't claim to be able to explain just why that helps, but without the an= notation it seems that when typechecking structure B, the typechecker needs= to know the type equality t =3D B.t directly, while either adding the anno= tation or destructing the pair causes the type definitions to be unfolded o= nce. The following threads seem to be related: http://caml.inria.fr/pub/ml-archives/caml-list/2007/05/d9414d45a9a6f30f2609= e08c43f011a0.en.html http://caml.inria.fr/pub/ml-archives/caml-list/2007/06/0d23465b5b04f72fedec= dd3bbf2c9d72.en.html There is also a related bug (4266) in the database. Cheers, Josh From: caml-list-bounces@yquem.inria.fr [mailto:caml-list-bounces@yquem.inri= a.fr] On Behalf Of Charles Hymans Sent: Tuesday, June 10, 2008 8:27 PM To: caml-list@yquem.inria.fr Subject: [Caml-list] typing of recursive modules in 3.10.2 Hi, I have encountered a behavior of the type checking of recursive modules whi= ch is hard for me to understand. Especially so, since the code used to compile with Ocaml 3.10.0 but does no= t with 3.10.2. And, an almost similar piece of code compile= s correctly. I tried to extract the smallest piece of code that exhibits the problem, bu= t it's still quite long. Sorry. Here is the code that does not type with 3.10.2: =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 BSig =3D sig type t val f: t -> unit end module type ASig =3D functor(B: BSig) -> sig type t val g: B.t -> unit end module Make(C: BSig) =3D struct type t =3D int let g _ =3D () end module MakeA =3D (Make: ASig) module rec A: sig type t val g: B.t -> unit end =3D MakeA(B) and B: sig type t =3D int * A.t val f: t -> unit end =3D struct type t =3D int * A.t let f x =3D A.g x (* does not type *) (* let f (a, b) =3D A.g (a, b) (* types correctly *) *) 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 Note that if function f is replaced by the commented version, then the type= checker succeeds. Even though, this code modification is only giving the a= dditional information that the argument of f is a pair. It would be nice for both versions of the code to compile, because the curr= ent behavior of the type checker seems to me not easily predictable. Thank you in advance for your help, --_000_857DD0FDAC042B4485F9F5F4EA675104166C8EB605EAEXMSGC332eu_ Content-Type: text/html; charset="us-ascii" Content-Transfer-Encoding: quoted-printable

Hi Charles,

 

I don’t know if it helps, and this doesn’t addre= ss your concern over predictability, but your example will also typecheck if y= ou annotate the argument of f with t:

 

let f (x : t) =3D A.g x

 

I can’t claim to be able to explain just why that help= s, but without the annotation it seems that when typechecking structure B, the typechecker needs to know the type equality t =3D B.t directly, while eithe= r adding the annotation or destructing the pair causes the type definitions to be unfolded once.

 

The following threads seem to be related:<= /p>

http://caml.inria.fr/pub/ml-archives/caml-lis= t/2007/05/d9414d45a9a6f30f2609e08c43f011a0.en.html

http://caml.inria.fr/pub/ml-archives/caml-lis= t/2007/06/0d23465b5b04f72fedecdd3bbf2c9d72.en.html

 

There is also a related bug (4266) in the database.

 

Cheers,  Josh

 

 

From: caml-list-bounces@yquem.inria.fr [mailto:caml-list-bounces@yquem.inria.fr] = On Behalf Of Charles Hymans
Sent: Tuesday, June 10, 2008 8:27 PM
To: caml-list@yquem.inria.fr
Subject: [Caml-list] typing of recursive modules in 3.10.2

 

Hi,

 

I have encountered a behavior of the type checking of recursive modules which is hard for me to understand.

Especially so, since the code used to compile with Oca= ml 3.10.0 but does not with 3.10.2. And, an alm= ost similar piece of code compiles correctly.

 

I tried to extract the smallest piece of code that exh= ibits the problem, but it's still quite long. Sorry.

 

Here is the code that does not type with 3.10.2:<= /o:p>

=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<= /p>

 

module type BSig =3D
sig
  type t
  val f: t -> unit
end

module type ASig =3D functor(B: BSig) ->
sig
  type t
  val g: B.t -> unit
end

module Make(C: BSig) =3D
struct
  type t =3D int
  let g _ =3D ()
end

module MakeA =3D (Make: ASig)

module rec A:
sig
  type t
  val g: B.t -> unit
end
=3D MakeA(B)

and B:
sig
  type t =3D int * A.t
  val f: t -> unit
end
=3D
struct
  type t =3D int * A.t

  let f x =3D A.g x   (* does not type *)
(*
  let f (a, b) =3D A.g (a, b)   (* types correctly *) *)
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=

 

Note that if function f is replaced by the commented version, then the type checker succeeds. Even though, t= his code modification is only giving the additional information that the argument of f is a pair.

 

It would be nice for both versions of the code to compile, because the current behavior of the type checker se= ems to me not easily predictable.

 

Thank you in advance for your help,

 

--_000_857DD0FDAC042B4485F9F5F4EA675104166C8EB605EAEXMSGC332eu_--