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=0.0 required=5.0 tests=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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 956F9BBAF for ; Tue, 10 Jun 2008 21:27:22 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Aj8BAClyTkhC+Vyuc2dsb2JhbACCPjWPHQEMAwQECQ8FmV2FQw X-IronPort-AV: E=Sophos;i="4.27,618,1204498800"; d="scan'208";a="13792457" Received: from ug-out-1314.google.com ([66.249.92.174]) by mail3-smtp-sop.national.inria.fr with ESMTP; 10 Jun 2008 21:27:22 +0200 Received: by ug-out-1314.google.com with SMTP id m4so143605uge.18 for ; Tue, 10 Jun 2008 12:27:21 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:message-id:date:from:to :subject:mime-version:content-type; bh=+7/aastv2Oo+cRF5xKXkboIX3P7uthcLMYRdtCj1PE0=; b=RewI7H+fEqWO0I/xmZqCR9wJX9tzpXKp+Y2cabwzutiNzxtlAZ6nm8thyLBt5hYj8o qhElVN8ERvDEQxRtT2uFpxqgRAvRknctQL32HBUXT07nBfo9Qq76XpBd7Vr76RfhBTsA EOuTyFQwymXYXFqLPUBoRSfzXYFsxQKcftot4= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:mime-version:content-type; b=G1SHBuUtD6LBg5hZskC2eAImaLfOme2Ceo7OZM/MRnUh2NNp0kZn3WdWLrEm3kGxxR qVUf73udKnGkvo8vc9Z2Rg5szzcWQSh3F9PLhybYxqYRxV8rtymHC5JLprq0XMJ6XIx2 cIHVNGpQGDmo3SlBbQU/JDgV+5AxXyaazMe4U= Received: by 10.210.105.20 with SMTP id d20mr4435518ebc.38.1213126041613; Tue, 10 Jun 2008 12:27:21 -0700 (PDT) Received: by 10.210.39.11 with HTTP; Tue, 10 Jun 2008 12:27:21 -0700 (PDT) Message-ID: <676aba050806101227m1696d555n6f23f55f57af0db2@mail.gmail.com> Date: Tue, 10 Jun 2008 21:27:21 +0200 From: "Charles Hymans" To: caml-list@yquem.inria.fr Subject: typing of recursive modules in 3.10.2 MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="----=_Part_9688_17239201.1213126041598" X-Spam: no; 0.00; recursive:01 recursive:01 ocaml:01 sig:01 val:01 functor:01 sig:01 val:01 struct:01 struct:01 checker:01 checker:01 predictable:01 ocaml:01 functor:01 ------=_Part_9688_17239201.1213126041598 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Content-Disposition: inline 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 Ocaml 3.10.0 but does not with 3.10.2. And, an almost similar piece of code compiles correctly. I tried to extract the smallest piece of code that exhibits the problem, but it's still quite long. Sorry. Here is the code that does not type with 3.10.2: ======================================= module type BSig = sig type t val f: t -> unit end module type ASig = functor(B: BSig) -> sig type t val g: B.t -> unit end module Make(C: BSig) = struct type t = int let g _ = () end module MakeA = (Make: ASig) module rec A: sig type t val g: B.t -> unit end = MakeA(B) and B: sig type t = int * A.t val f: t -> unit end = struct type t = int * A.t let f x = A.g x (* does not type *) (* let f (a, b) = A.g (a, b) (* types correctly *) *) end ========================= 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 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 seems to me not easily predictable. Thank you in advance for your help, ------=_Part_9688_17239201.1213126041598 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Content-Disposition: inline
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 Ocaml 3.10.0 but does not with 3.10.2. And, an almost similar piece of code compiles correctly.
 
I tried to extract the smallest piece of code that exhibits the problem, but it's still quite long. Sorry.
 
Here is the code that does not type with 3.10.2:
=======================================
 
module type BSig =
sig
  type t
  val f: t -> unit
end

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

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

module MakeA = (Make: ASig)

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

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

  let f x = A.g x   (* does not type *)
(*
  let f (a, b) = A.g (a, b)   (* types correctly *)
*)
end

=========================
 
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 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 seems to me not easily predictable.
 
Thank you in advance for your help,
 
------=_Part_9688_17239201.1213126041598--