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

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

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