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

["Milan Stanojević" <milanst@gmail.com>]

I submitted a bug report.
http://caml.inria.fr/mantis/view.php?id=6788


On Tue, Feb 17, 2015 at 4:40 PM, Milan Stanojević <milanst@gmail.com> wrote:
> It seems that type checker does know that C.T and T are aliases since
> this compiles
>
>   module C = struct
>     module T = struct end
>     include Make (T)
>   end
>   include C
>
>   let f (x : Make(Make(T)).t) : Make(Make(C.T)).t = x
>
> Somehow the fact that C.T = T is lost when checking against the signature.
>
>
>
>
> On Mon, Feb 16, 2015 at 1:03 PM, Leo White <lpw25@cam.ac.uk> wrote:
>> 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
>>
>> --
>> Caml-list mailing list.  Subscription management and archives:
>> https://sympa.inria.fr/sympa/arc/caml-list
>> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>> Bug reports: http://caml.inria.fr/bin/caml-bugs