Original bug ID: 455
Reporter: administrator
Status: closed
Resolution: not a bug
Priority: normal
Severity: minor
Category: ~DO NOT USE (was: OCaml general)

Bug description

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