RE: [Caml-list] typing of recursive modules in 3.10.2

[Josh Berdine <jjb@microsoft.com>]

[-- Attachment #1: Type: text/plain, Size: 2498 bytes --]

Hi Charles,

I don't know if it helps, and this doesn't address your concern over predictability, but your example will also typecheck if you annotate the argument of f with t:

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

I can't claim to be able to explain just why that helps, but without the annotation it seems that when typechecking structure B, the typechecker needs to know the type equality t = B.t directly, while either adding the annotation or destructing the pair causes the type definitions to be unfolded once.

The following threads seem to be related:
http://caml.inria.fr/pub/ml-archives/caml-list/2007/05/d9414d45a9a6f30f2609e08c43f011a0.en.html
http://caml.inria.fr/pub/ml-archives/caml-list/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 Ocaml 3.10.0 but does not with 3.10.2.<http://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,


[-- Attachment #2: Type: text/html, Size: 10150 bytes --]