Re: [Caml-list] types not equal when I expect them to be

[Gabriel Scherer <gabriel.scherer@gmail.com>]

Note that Bar is actually unnecessary. The following code exhibit the
exact same behavior:

  module Foo = struct
    module St = struct type t = string let compare = compare end
    module Map (* : Map.S with type key = St.t *)
      = Map.Make(St)
    (* module Map = Map.Make(struct type t = string let compare =
compare end) *)
  end

  module Pack = struct
    module Foo = Foo
  end

  let x : int Foo.Map.t = Pack.Foo.Map.empty

The important point is the interface of Map.Make when looked through
the environment (for example when rebound by `module F = Map.Make`,
then compiled with `ocamlc -i`):

  functor (Ord : Map.OrderedType) ->
    sig
      type key = Ord.t
      type 'a t = 'a Map.Make(Ord).t
      ...
    end

Note the `'a t = 'a Map.Make(Ord).t` part: this is the result of
a so-called "strenghening" operation, where the abstract types `t` in
the signature of the module `M` are noted to be equal to `M.t`; this
allows `N` to remain type-compatible with `M` when writing `module N =
M`.

Now the result of this strenghtening operation in your case is that
your module Map defined in Foo has in its signature:

  type 'a t = 'a Map.Make(Foo.St).t

The sorrow and non-intuitive point is that, after rebinding in Pack,
Pack.Foo gets the following signature:

  type 'a t = 'a Map.Make(Pack.Foo.St).t

Those two type are not path-compatible because `Pack.Foo.St` is not
a path syntactically equal to `Foo.St` -- I'm not sure why the
type-checker couldn't check path equality upto known module aliasing,
however.

Now, why your fixes work:

1. by adding the `: Map.S with type key = ...` signature to your
   Foo.Map module, you seal the module under the Map.S signature which
   has its type `'a t` *abstract*. This cancels the effects of
   strenghtening in the definition of `Foo.Map`. Now, in the
   definition of Pack, aliasing `module Foo = Foo` re-apply
   strenghtening, and you get a `Pack.Foo` module with `type 'a t =
   Foo.Map.t`, so those two are compatible.

2. by applying `struct type t = String let compare = compare` directly
   instead of naming it `Foo.St`, you apply a module that is not
   itself a path, so the typing rules change and you get `'a
   Foo.Map.t` abstract as in the first case.

3. You could also define `St` out of `Foo`, so that types in both Foo
   and Pack.Foo have `type 'a t = Map.Make(St).t`. You are surely
   aware that could similarly use stdlib's `String` directly which
   provides a `compare` operation.

I believe this explains the observed behaviour of the type-checker --
the experts will surely correct if I made technical mistakes. I'm not
sure however whether this behavior is expected (or could be considered
slightly buggy), or if it is imposed by theoretical restrictions or
implementation considerations.

On Thu, Mar 1, 2012 at 5:38 PM, Ashish Agarwal <agarwal1975@gmail.com> wrote:
> The following code fails to compile:
>
> ----- a.ml ----
> module Foo = struct
>   module St = struct type t = string let compare = compare end
>
>   module Map (* : Map.S with type key = St.t *)
>     = Map.Make(St)
>
>   (* module Map = Map.Make(struct type t = string let compare = compare end)
> *)
> end
>
> module Bar = struct
>   type t = int Foo.Map.t
> end
>
> module Pack = struct
>   module Foo = Foo
>   module Bar = Bar
> end
>
> open Pack
> let x : Bar.t = Foo.Map.empty
> ----
>
> $ ocamlc -c foo.ml
> File "foo.ml", line 20, characters 16-29: (* refers to Foo.Map.empty on last
> line *)
> Error: This expression has type
>          'a Pack.Foo.Map.t = 'a Map.Make(Pack.Foo.St).t
>        but an expression was expected of type
>          Pack.Bar.t = int Map.Make(Foo.St).t
>
>
> So Pack.Foo and Foo are not compatible. By trial and error, I found two ways
> to resolve the problem:
>
> 1) Provide an explicit signature for Foo.Map (uncomment the provided
> signature), or
> 2) Inline the structure passed to Map.Make (comment out first definition of
> Foo.Map and uncomment the second one)
>
> But I don't understand why. Can anyone explain the main points. Thank you.
>