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

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

[Carl Eastlund]

[-- Attachment #1: Type: text/plain, Size: 1730 bytes --]

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

[-- Attachment #2: Type: text/html, Size: 2855 bytes --]

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

[Gabriel Scherer]

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

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

[Leo White]

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

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

[Milan Stanojević]

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

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

[Milan Stanojević]

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

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

[Milan Stanojević]

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

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

[Jacques Garrigue]

On 2015/02/15 19:26, Gabriel Scherer wrote:
> 
> That is one of the dark corners of the module system.
[…]
> 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

This is indeed the gist of the problem. Matching against

    sig
      type t
      module C : S with type t = t
    end

introduces a kind of mutual recursion: C.t is defined as t in the enclosing
signature, but t is C.t in the internal one. As a result we get a kind of
double-vision problem. Namely, t inside the internal C is Make(T).t (with
T the one inside C), but in the enclosing signature, the t inside C
is Make(C.T).t. While logically the T inside C and C.T are the same module,
the typing rule in Leroy's paper do not say anything like that.

σ : {1,...,m} 􏰀→ {1,...,n} for all i ∈ {1,...,m}, E;D1;...;Dn ⊢ Dσ(i) <: Di′
---------------------------------------------------------------------------------------
          E ⊢ sig D1;…;Dn end <: sig D1′ ;...;Dm′ end

The definition in the premise must match without extra equations.
Here module aliases do not help.
What could help would be to strengthen the definitions in the premise, so
that T would be converted to C.T. But I don't know whether this is sound
or not, since this is not part of the current theory.

Jacques Garrigue


> 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

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

[Jacques Garrigue]

On 2015/02/24 13:38, Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> wrote:

>  While logically the T inside C and C.T are the same module,
> the typing rule in Leroy's paper do not say anything like that.
> 
> σ : {1,...,m} 􏰀→ {1,...,n} for all i ∈ {1,...,m}, E;D1;...;Dn ⊢ Dσ(i) <: Di′
> ---------------------------------------------------------------------------------------
>          E ⊢ sig D1;…;Dn end <: sig D1′ ;...;Dm′ end
> 
> The definition in the premise must match without extra equations.
> Here module aliases do not help.
> What could help would be to strengthen the definitions in the premise, so
> that T would be converted to C.T. But I don't know whether this is sound
> or not, since this is not part of the current theory.

More precisely, OCaml actually does a bit more than this rule, as it
strengthens abstract types. However there is no such thing as strengthening
for module aliases, as this would require having both a signature and an
alias for the same module. Allowing that could help solve this problem, but
this is not fixing a bug, rather extending the theory.

Jacques Garrigue