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

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

Oh, it seems Carl already did it. I'll mark mine as duplicate.

On Thu, Feb 19, 2015 at 1:21 PM, Milan Stanojević <milanst@gmail.com> wrote:
> 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