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. 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,