Re: [Caml-list] functor substitution gives error

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

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