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

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

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