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

[Leo White <lpw25@cam.ac.uk>]

Gabriel gives an accurate accout of what is going on. To me, it looks
like the type-checker should probably accept this, so I would submit it
as a bug (I suspect a missing call to Env.normalize_path somewhere, but
perhaps there is something more significant going on here).

Regards,

Leo

Gabriel Scherer <gabriel.scherer@gmail.com> writes:

> 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