functor substitution gives error

functor substitution gives error

[Hendrik Tews]

Hi,

I have a strange compilation problem, which I suspect to be a
compiler bug. Consider the following nested functor application


module A(FreshGram : functor(Unit : sig end) -> Camlp4Syntax) : Camlp4Syntax =
  FreshGram(struct end)

module B(FreshGram : functor(Unit : sig end) -> Camlp4Syntax) : Camlp4Syntax =
  Printers_Ocaml_Make(A(FreshGram))


This compiles fine, however, when I manually inline functor A:


module C(FreshGram : functor(Unit : sig end) -> Camlp4Syntax) : Camlp4Syntax =
  Printers_Ocaml_Make(FreshGram(struct end))


I get a signature mismatch error in both 3.11.2 and 3.12. I would
appreciate any explanation for this behaviour.

As the names suggest the problem came up with in some Camlp4
code. Here is a striped down version, which reproduces the
problem:

==============================================================================
module type Loc = sig               (* simplified version of Camlp4.Sig.Loc *)
  type t
end

module type Camlp4Ast = sig              (* simplified Camlp4.Sig.Camlp4Ast *)
  module Loc : Loc
end

module type Camlp4Syntax = sig        (* simplified Camlp4.Sig.Camlp4Syntax *)
  module Loc : Loc
  module Ast : Camlp4Ast with module Loc = Loc
end

module type Printers_Ocaml_Make_Sig =      (* .mli of Camlp4/Printers/OCaml *)
  functor(Syntax : Camlp4Syntax) -> 
sig
  include Camlp4Syntax
    with module Loc = Syntax.Loc
    and module Ast = Syntax.Ast
end

module Printers_Ocaml_Make :                (* .ml of Camlp4/Printers/OCaml *)
  Printers_Ocaml_Make_Sig = functor(Syntax : Camlp4Syntax) ->
struct
  include Syntax
end


module A(FreshGram : functor(Unit : sig end) -> Camlp4Syntax) : Camlp4Syntax =
  FreshGram(struct end)

module B(FreshGram : functor(Unit : sig end) -> Camlp4Syntax) : Camlp4Syntax =
  Printers_Ocaml_Make(A(FreshGram))

module C(FreshGram : functor(Unit : sig end) -> Camlp4Syntax) : Camlp4Syntax =
  Printers_Ocaml_Make(FreshGram(struct end))
===============================================================================

The error occurs in the last line and says

Error: Signature mismatch:
       Modules do not match:
         sig
           module Loc : sig type t end
           module Ast : sig module Loc : sig type t end end
         end
       is not included in
         Camlp4Syntax
       Modules do not match:
         sig module Loc : sig type t = Ast.Loc.t end end
       is not included in
         sig module Loc : sig type t = Loc.t end end
       Modules do not match:
         sig type t = Ast.Loc.t end
       is not included in
         sig type t = Loc.t end
       Type declarations do not match:
         type t = Ast.Loc.t
       is not included in
         type t = Loc.t

The error goes away with the following version of Printers_Ocaml_Make_Sig:

module type Printers_Ocaml_Make_Sig = functor(Syntax : Camlp4Syntax) -> 
sig
  module Loc : Loc 
    with type t = Syntax.Loc.t

  module Ast : Camlp4Ast 
    with type Loc.t = Syntax.Ast.Loc.t
    and type Loc.t = Loc.t
end

IMHO both Printers_Ocaml_Make_Sig versions should be equivalent:
in the second version the include is spelled out and the module
constraints are expanded into type constraints. 

The error comes back if one changes the order of the type
constaints for module Ast.


Bye,

Hendrik

Re: [Caml-list] functor substitution gives error

[Daniel Bünzli]

I think I just hit the same kind problem.

This doesn't compile :
----
module A : sig
  type m
  module M : sig
    type t = m
  end
end = struct
  module M = struct
    module S = String
    module Smap = Map.Make(S)
    type t = int Smap.t
  end
  type m = M.t
end
----

 Type declarations do not match:
         type t = int Smap.t
       is not included in
         type t = m

However if I put S outside M, or if I specify the type of Smap it compiles :

----
module A : sig
  type m
  module M : sig
    type t = m
  end
end = struct
  module S = String
  module M = struct
    module Smap = Map.Make(S)
    type t = int Smap.t
  end
  type m = M.t
end
----

----
module A : sig
  type m
  module M : sig
    type t = m
  end
end = struct
  module M = struct
    module S = String
    module Smap = (Map.Make(S) : Map.S with type key = S.t)
    type t = int Smap.t
  end
  type m = M.t
end
----

Daniel

Re: [Caml-list] functor substitution gives error

[Jacques Garrigue]

On 2010/09/06, at 18:12, Hendrik Tews wrote:

> Hi,
> 
> I have a strange compilation problem, which I suspect to be a
> compiler bug. Consider the following nested functor application
> 
> 
> module A(FreshGram : functor(Unit : sig end) -> Camlp4Syntax) : Camlp4Syntax =
>  FreshGram(struct end)
> 
> module B(FreshGram : functor(Unit : sig end) -> Camlp4Syntax) : Camlp4Syntax =
>  Printers_Ocaml_Make(A(FreshGram))
> 
> 
> This compiles fine, however, when I manually inline functor A:
> 
> 
> module C(FreshGram : functor(Unit : sig end) -> Camlp4Syntax) : Camlp4Syntax =
>  Printers_Ocaml_Make(FreshGram(struct end))
> 
> 
> I get a signature mismatch error in both 3.11.2 and 3.12. I would
> appreciate any explanation for this behaviour.

The reason is that the typing of modules is not closed under substitution.
More precisely, the use of anonymous modules (the "struct end" in your
code) is highly disruptive. It requires all modules around it to have
non-dependent signatures, whereas the ability to express dependency
is the great strength of  applicative functors...
Actually, all the theory was built assuming that there no anonymous modules.

The solution is easy enough: name all modules.

Here you just have to write:

  module Unit = struct end
  module C(FreshGram : functor(Unit : sig end) -> Camlp4Syntax) : Camlp4Syntax =
     Printers_Ocaml_Make(FreshGram(Unit))

Hope this helps.

Jacques Garrigue

> As the names suggest the problem came up with in some Camlp4
> code. Here is a striped down version, which reproduces the
> problem:
> 
> ==============================================================================
> module type Loc = sig               (* simplified version of Camlp4.Sig.Loc *)
>  type t
> end
> 
> module type Camlp4Ast = sig              (* simplified Camlp4.Sig.Camlp4Ast *)
>  module Loc : Loc
> end
> 
> module type Camlp4Syntax = sig        (* simplified Camlp4.Sig.Camlp4Syntax *)
>  module Loc : Loc
>  module Ast : Camlp4Ast with module Loc = Loc
> end
> 
> module type Printers_Ocaml_Make_Sig =      (* .mli of Camlp4/Printers/OCaml *)
>  functor(Syntax : Camlp4Syntax) -> 
> sig
>  include Camlp4Syntax
>    with module Loc = Syntax.Loc
>    and module Ast = Syntax.Ast
> end
> 
> module Printers_Ocaml_Make :                (* .ml of Camlp4/Printers/OCaml *)
>  Printers_Ocaml_Make_Sig = functor(Syntax : Camlp4Syntax) ->
> struct
>  include Syntax
> end
> 
> 
> module A(FreshGram : functor(Unit : sig end) -> Camlp4Syntax) : Camlp4Syntax =
>  FreshGram(struct end)
> 
> module B(FreshGram : functor(Unit : sig end) -> Camlp4Syntax) : Camlp4Syntax =
>  Printers_Ocaml_Make(A(FreshGram))
> 
> module C(FreshGram : functor(Unit : sig end) -> Camlp4Syntax) : Camlp4Syntax =
>  Printers_Ocaml_Make(FreshGram(struct end))
> ===============================================================================
> 
> The error occurs in the last line and says
> 
> Error: Signature mismatch:
>       Modules do not match:
>         sig
>           module Loc : sig type t end
>           module Ast : sig module Loc : sig type t end end
>         end
>       is not included in
>         Camlp4Syntax
>       Modules do not match:
>         sig module Loc : sig type t = Ast.Loc.t end end
>       is not included in
>         sig module Loc : sig type t = Loc.t end end
>       Modules do not match:
>         sig type t = Ast.Loc.t end
>       is not included in
>         sig type t = Loc.t end
>       Type declarations do not match:
>         type t = Ast.Loc.t
>       is not included in
>         type t = Loc.t
> 
> The error goes away with the following version of Printers_Ocaml_Make_Sig:
> 
> module type Printers_Ocaml_Make_Sig = functor(Syntax : Camlp4Syntax) -> 
> sig
>  module Loc : Loc 
>    with type t = Syntax.Loc.t
> 
>  module Ast : Camlp4Ast 
>    with type Loc.t = Syntax.Ast.Loc.t
>    and type Loc.t = Loc.t
> end
> 
> IMHO both Printers_Ocaml_Make_Sig versions should be equivalent:
> in the second version the include is spelled out and the module
> constraints are expanded into type constraints. 
> 
> The error comes back if one changes the order of the type
> constaints for module Ast.
> 
> 
> Bye,
> 
> Hendrik
> 
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

Re: [Caml-list] functor substitution gives error

[Hendrik Tews]

Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> writes:

   On 2010/09/06, at 18:12, Hendrik Tews wrote:

   > I have a strange compilation problem, which I suspect to be a
   > compiler bug. Consider the following nested functor application

   The reason is that the typing of modules is not closed under substitution.

I am really surprised by this! I was sure I hit a compiler
problem, especially because changing the order of the
with-constraints solved the problem.

   The solution is easy enough: name all modules.

May I suggest to put a few words about this in the ocaml
reference manual? 

Thanks for the hint,

Hendrik

Re: [Caml-list] functor substitution gives error

[Daniel Bünzli]

> The solution is easy enough: name all modules.

In my example all modules are named. Can you maybe provide an
explanation of what's happening ?

Best,

Daniel

Re: [Caml-list] functor substitution gives error

[Jacques Garrigue]

On Mon, Sep 6, 2010 at 6:39 PM, Daniel Bünzli
<daniel.buenzli@erratique.ch> wrote:
> I think I just hit the same kind problem.
>
> This doesn't compile :
> ----
> module A : sig
>  type m
>  module M : sig
>    type t = m
>  end
> end = struct
>  module M = struct
>    module S = String
>    module Smap = Map.Make(S)
>    type t = int Smap.t
>  end
>  type m = M.t
> end
> ----
>
>  Type declarations do not match:
>         type t = int Smap.t
>       is not included in
>         type t = m
>
> However if I put S outside M, or if I specify the type of Smap it compiles :

At first, I thought this was a different problem, since there is no
"struct end".
However, this is actually the same problem.
To understand what is happening, you must look at what is inferred for
M.Smap.t in the different cases.

In the first and second case:
type 'a t = 'a Map.Make(S).t
If you specify the type of Smap it becomes:
type +'a t (just abstract)
or after strengthening (making types refer to their location)
type 'a t = 'a M.Smap.t

Here the problem is that S, by being only defined locally, plays the same
role as "struct end". The above type equation (in the first case) forbids
the stengthening of M.Smap.t, but later it has to be discarded because one
is not allowed to depend on a local module, meaning that we end up losing
a type equation. In the second case, this doesn't happen because S is no
longer local to M, and can be kept. And in the last one, by restricting the
type of Smap, you remove the type equation on Smap.t, allowing its
strengthening (only one type equation is allowed per type, so if there is
already one, strengthening cannot be done).

Since 3.12, there is a new compiler option, -no-app-funct, which disables
applicative functors, and as a result allows strengthening in more cases.
This solves your problem, but not Hendrik's, because his example
requires applicative functor to start with.

Jacques Garrigue

[Your 2 other versions]
> ----
> module A : sig
>  type m
>  module M : sig
>    type t = m
>  end
> end = struct
>  module S = String
>  module M = struct
>    module Smap = Map.Make(S)
>    type t = int Smap.t
>  end
>  type m = M.t
> end
> ----
>
> ----
> module A : sig
>  type m
>  module M : sig
>    type t = m
>  end
> end = struct
>  module M = struct
>    module S = String
>    module Smap = (Map.Make(S) : Map.S with type key = S.t)
>    type t = int Smap.t
>  end
>  type m = M.t
> end
> ----
>
> Daniel