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

["Charles Hymans" <charles.hymans@gmail.com>]

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

Thanks for the answer and links, Josh.
I had also noticed that annotating the argument with type t solved the
problem.

However the current behavior of the type-checker is really awkward to me. I
hope it is improved in the future to make the use of recursive modules more
intuitive and less of a black art.

Best regards,


On Wed, Jun 11, 2008 at 11:25 AM, Josh Berdine <jjb@microsoft.com> wrote:

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

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