Re: [Caml-list] functor substitution gives error

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

On Mon, Sep 6, 2010 at 6:39 PM, Daniel Bünzli
<daniel.buenzli@erratique.ch> wrote:
> I think I just hit the same kind problem.
>
> This doesn't compile :
> ----
> module A : sig
>  type m
>  module M : sig
>    type t = m
>  end
> end = struct
>  module M = struct
>    module S = String
>    module Smap = Map.Make(S)
>    type t = int Smap.t
>  end
>  type m = M.t
> end
> ----
>
>  Type declarations do not match:
>         type t = int Smap.t
>       is not included in
>         type t = m
>
> However if I put S outside M, or if I specify the type of Smap it compiles :

At first, I thought this was a different problem, since there is no
"struct end".
However, this is actually the same problem.
To understand what is happening, you must look at what is inferred for
M.Smap.t in the different cases.

In the first and second case:
type 'a t = 'a Map.Make(S).t
If you specify the type of Smap it becomes:
type +'a t (just abstract)
or after strengthening (making types refer to their location)
type 'a t = 'a M.Smap.t

Here the problem is that S, by being only defined locally, plays the same
role as "struct end". The above type equation (in the first case) forbids
the stengthening of M.Smap.t, but later it has to be discarded because one
is not allowed to depend on a local module, meaning that we end up losing
a type equation. In the second case, this doesn't happen because S is no
longer local to M, and can be kept. And in the last one, by restricting the
type of Smap, you remove the type equation on Smap.t, allowing its
strengthening (only one type equation is allowed per type, so if there is
already one, strengthening cannot be done).

Since 3.12, there is a new compiler option, -no-app-funct, which disables
applicative functors, and as a result allows strengthening in more cases.
This solves your problem, but not Hendrik's, because his example
requires applicative functor to start with.

Jacques Garrigue

[Your 2 other versions]
> ----
> module A : sig
>  type m
>  module M : sig
>    type t = m
>  end
> end = struct
>  module S = String
>  module M = struct
>    module Smap = Map.Make(S)
>    type t = int Smap.t
>  end
>  type m = M.t
> end
> ----
>
> ----
> module A : sig
>  type m
>  module M : sig
>    type t = m
>  end
> end = struct
>  module M = struct
>    module S = String
>    module Smap = (Map.Make(S) : Map.S with type key = S.t)
>    type t = int Smap.t
>  end
>  type m = M.t
> end
> ----
>
> Daniel