Re: [Caml-list] Weird type error involving 'include' and applicative functors

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

That is one of the dark corners of the module system.

I don't know whether an ideal type-checker should accept your last
definition or not. It is non-intuitive that some are accepted and
others rejected; some things in the module system are non-intuitive
for good reasons, some others because of implementation limitations,
and it's not always clear to non-experts which is which).˙But I can
explain why the last definition is harder for the type-checker to
accept than the other.

# module A = struct
  module T = struct end
  module C = struct
    include Make(T)
  end
  include C
end
;;
module A :
  sig
    module T : sig  end
    module C : sig type t = Make(T).t end
    type t = Make(T).t
  end

# module B = struct
  module C = struct
    module T = struct end
    include Make(T)
  end
  include C
end
;;
module B :
  sig
    module C : sig module T : sig  end type t = Make(T).t end
    module T = C.T
    type t = Make(T).t
  end


Note the important difference in the inferred signatures in both
cases. Both modules have
    type t = Make(T).t
but, in the first case, this is the *same module T* that is mentioned
in the signature of T, while in the second case, there are two
different modules, C.T and T (the latter being generated by the
"include", with an equation that it is equal to the former).

The reasoning to check against your signature
  sig
    type t
    module C : S with type t = t
  end
is thus more complicated in the second case: the type-checker would
need to use the equation (T = C.T) to check that indeed C.t is equal
to t.

I think this is due to the rather contorted way you define C first in
the implementations and include it later, while in the signature first
define t and then C. Note that the following signature, which is
morally equivalent, accepts both implementations (and thus all the
functors in your file):
  sig
    module C : S
    type t = C.t
  end


On Fri, Feb 13, 2015 at 10:40 PM, Carl Eastlund
<ceastlund@janestreet.com> wrote:
> This seems to be a compiler bug, but let me know if I've missed something.
> The behavior I see is that Make_ok1 and Make_ok2 compile fine, but the very
> similar functor Make_bad does not.  I get this compile error:
>
> ========================================
>
>       Error: Signature mismatch:
>              Modules do not match:
>                sig
>                  module C : sig module T : sig  end type t = Make(T).t end
>                  module T = C.T
>                  type t = Make(T).t
>                end
>              is not included in
>                sig type t module C : sig type t = t end end
>              In module C:
>              Modules do not match:
>                sig module T : sig  end type t = Make(T).t end
>              is not included in
>                sig type t = C.t end
>              In module C:
>              Type declarations do not match:
>                type t = Make(T).t
>              is not included in
>                type t = t
>
> ========================================
>
> And here is the code:
>
> ========================================
>
> module type S = sig type t end
> module Make (M : sig end) : S = struct type t end
>
> module Make_ok1 (M : sig end) : sig
>
>   type t
>   module A : S with type t = t
>
> end = struct
>
>   module A = struct
>     include Make (struct end)
>   end
>   include A
>
> end
>
> module Make_ok2 (M : sig end) : sig
>
>   type t
>   module B : S with type t = t
>
> end = struct
>
>   module T = struct end
>   module B = struct
>     include Make (T)
>   end
>   include B
>
> end
>
> module Make_bad (M : sig end) : sig
>
>   type t
>   module C : S with type t = t
>
> end = struct
>
>   module C = struct
>     module T = struct end
>     include Make (T)
>   end
>   include C
>
> end
>
> ========================================
>
> --
> Carl Eastlund