Re: [Caml-list] Type visibility limitation in recursive modules

["\"Márk S. Zoltán\"" <zoltan.s.mark@dravanet.hu>]

Márk S. Zoltán wrote:
> Behold the following code snippet:
>
> module rec Aleph :
>    sig
>        type t = Tag of Beth.t
>    end =
>    struct
>        type t = Tag of Beth.t
>    end
> and Beth :
>    sig
>        type t
>        val scandalous : Aleph.t
>    end =
>    struct
>        type t = Aleph.t list
>        let scandalous = Aleph.Tag((* HERE BE DRAGONS *) [])
>    end
>
> The compiler complains that the empty list after HERE BE DRAGONS has 
> type 'a list but it is used with type Beth.t. I'd expect the compiler 
> to discover that those types can be unified via 'a == Aleph.t, since 
> as far as I can tell, all necessary facts are visible at that point. 
> Replacing "Beth : sig type t ..." with "Beth : sig type t = Aleph.t 
> list ..." does away with the error, but I would very much like to keep 
> Beth.t an opaque type. Is this an intended behavior? And if it is 
> intended, is there a way to tell the compiler what I really want it to 
> do?
>
> Thanks in advance for any help.
>
>    Z-
The plot thickens. The following code provokes an error message stating 
explicitly that type t in Beth is not the same as Beth.t:
----------------------
module rec Aleph :
    sig
        type t = Tag of Beth.t
    end =
    struct
        type t = Tag of Beth.t
    end
and Beth :
    sig
        type t   
        val a_beth_t_value : t
        val scandalous : Aleph.t
    end =
    struct
        type t = Aleph.t list
        let a_beth_t_value = ([] : t)
          let scandalous = Aleph.Tag(a_beth_t_value)
    end
----------------------
$ ocamlc -i Anomaly.ml
File "Anomaly.ml", line 18, characters 33-49:
This expression has type t = Aleph.t list but is here used with type Beth.t
---------------------

The error message references the mention of a_beth_value in the let 
scandalous ... line. The ([] : t) construct in the previous line was 
necessary to trigger the 'This expression has type t = Aleph.t list ...' 
message, since a bare [] only triggers "This expression has type Aleph.t 
list but ...", without an indication that it knows that type t is 
Aleph.t list.

However, reexporting a_beth_t_value from Aleph satisfies the compiler:
--------------------
module rec Aleph :
    sig
        type t = Tag of Beth.t
        val a_reexported_beth_t_value : Beth.t
    end =
    struct
        type t = Tag of Beth.t
        let a_reexported_beth_t_value = Beth.a_beth_t_value
    end
and Beth :
    sig
        type t
        val a_beth_t_value : t
        val scandalous : Aleph.t
    end =
    struct
        type t = Aleph.t list
        let a_beth_t_value = []
          let scandalous = Aleph.Tag(Aleph.a_reexported_beth_t_value)
    end
--------------------
$ ocamlc -i Anomaly.ml
module rec Aleph :
  sig type t = Tag of Beth.t val a_reexported_beth_t_value : Beth.t end
and Beth : sig type t val a_beth_t_value : t val scandalous : Aleph.t end
--------------------

So far it sounds like the compiler acknowledges there is a type Beth.t 
and identifies it with type t in the sig of Beth, but fails to make the 
connection between this type and the Aleph.t list type expression inside 
the struct of Beth. But even that is only true if the type expression in 
question uses a built-in list; if I replace it with an algebraic type 
implementing my own list, even the original example starts working.

-------------------
module rec Aleph :
    sig
        type t = Tag of Beth.t
    end =
    struct
        type t = Tag of Beth.t
    end
and Beth :
    sig
        type t   
        val scandalous : Aleph.t
    end =
    struct
        type t = Cons of Aleph.t * t | Nil
          let scandalous = Aleph.Tag(Nil)
    end
-----------------
$ ocamlc -i Anomaly.ml
module rec Aleph : sig type t = Tag of Beth.t end
and Beth : sig type t val scandalous : Aleph.t end
-----------------

This is a bug, isn't it?

Cheers

    Z-