[Caml-list] module constraints bug?

[Caml-list] module constraints bug?

[Tyng-Ruey Chuang]

Dear all,

There seems to be a bug in the way o'caml handling higher-order modules
with constrained module arguments. Consider the following module types:

  module type T =
  sig
    type t
  end

  module type SELF = 
  sig
    module Self: T
  end

  module type F =
  sig
    module A: T

    module Eta: functor (X: SELF with module Self = A) ->
    sig
      val t2t: X.Self.t -> X.Self.t
    end
  end

In module type F, one specifies a functor Eta that takes in an argument X
containing a module Self. Self is to have the same implementation of module A,
which is also specified in F.

However, the following module ThisF cannot be type-checked by ocaml
to have module type F:

  module ThisF: F =
  struct
    module A = 
    struct
      type t = Pink | Blue
    end

    module Eta = functor (X: SELF with module Self = A) ->
    struct
      let t2t x = match x with A.Pink -> A.Blue | A.Blue -> A.Pink
    end
  end

The error message is reproduced below:

	...	

  Modules do not match:
    functor(X : sig module Self : sig type t = A.t = | Pink | Blue end end) ->
      sig val t2t : A.t -> A.t end
  is not included in
    functor(X : sig module Self : sig type t = A.t end end) ->
      sig val t2t : X.Self.t -> X.Self.t end   

	...

  Type declarations do not match:
    type t = A.t
  is not included in
    type t = A.t = | Pink | Blue     


However, if we change the module constraint to a type constraint
in the definition of Eta, as shown below in module ThatF,
then it will type-check.

          module ThatF: F =
          struct
            module A = 
            struct
              type t = Pink | Blue
            end

(* here *)  module Eta = functor (X: SELF with type Self.t = A.t) ->
            struct
              let t2t x = match x with A.Pink -> A.Blue | A.Blue -> A.Pink
            end
          end

Is this a bug or am I missing something?

The above is simplied code. In real code, I have many modules
defined in the module type SELF, and each of these module again defines
several parametric type constructors. So it is quite tedious
to spell out all the type constraints. 

best,
Tyng-Ruey Chuang

-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] module constraints bug?

[Xavier Leroy]

> There seems to be a bug in the way o'caml handling higher-order modules
> with constrained module arguments.

It's not a bug, it's the intended behavior of the "SIG with module A = M"
construct.  But I understand that in your particular example, this
behavior is not what you want!

"SIG with module A = M" means: take signature SIG and replace the
entry "module A : ..." in it with "module A : <principal signature of M>".
In your example:

>   module ThisF: F =
>   struct
>     module A = 
>     struct
>       type t = Pink | Blue
>     end
> 
>     module Eta = functor (X: SELF with module Self = A) ->
>     struct
>       let t2t x = match x with A.Pink -> A.Blue | A.Blue -> A.Pink
>     end
>   end

the principal signature of A is

  sig type t = A.t = Pink | Blue end

(a type t with two constructors Pink and Blue, and that is equal to A.t).

Hence, SELF with module Self = A expands to 

  sig module Self : sig type t = A.t = Pink | Blue end end

instead of what you expected:

  sig module Self : sig type t = A.t end end

and which corresponds to the non-principal signature for A

  sig type t = A.t end

> However, if we change the module constraint to a type constraint
> in the definition of Eta, as shown below in module ThatF,
> [i.e.   SELF with type Self.t = A.t]
> then it will type-check.

Yes, because "SELF with type Self.t = A.t" expands to what you expect:

  sig module Self : sig type t = A.t end end

Hope this makes the issue a bit clearer,

- Xavier Leroy
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr