Re: [Caml-list] substituting recursive types inside a signature

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2015/11/03 05:01, Ashish Agarwal wrote:
> 
> $ cat foo.ml
> module M = struct
>   type t = A | B of u
>   and u = C of t
> end
> 
> module type N = sig
>   include module type of M
>     with type t = M.t
>     and type u = M.u
> end
> 
> $ ocamlc -c foo.ml
> File "foo.ml", line 8, characters 9-21:
> Error: This variant or record definition does not match that of type M.t
>        The types for field B are not equal.
> 
> I guess the "and" in the constraint doesn't make the constraints mutually recursive, so what does it do?

with constraints are handled incrementally. I.e., the code you wrote is exactly equivalent to:

   include (((module type of M) with type t = M.t) with type u = M.u)

It has always been that way. An interesting question is whether we could actually delay the checking to
after applying all the constraints. This would be a non-trivial change.

Jacques Garrigue