[Caml-list] module constraints bug?

[Tyng-Ruey Chuang <trc@iis.sinica.edu.tw>]

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