John F. Hughes wrote:
> I'd like it to work. In other words, I'd like a way to promise to the
> type system
> that A.t and B.t (within a COMBINE) are always the same.

module type COMBINE =
    sig
       module A : P
       module B : P with type t = A.t
    end;;

You need to keep the P1.t and P2.t fields public, otherwise the 
constraint cannot be checked:

module P1 = struct ... end;;
module P2 = struct ... end;;

or:

module P1 : P with type t = int = ...
module P2 : P with type t = int = ...

Btw, maybe you did it on purpose, but the type annotation in:

         let f x:Z.A.t = Z.B.foo x

is upon the result type of f, not its argument (in your case, it's the 
same).


Note also you don't need to combine the two structures in a single 
module, you can just define a functor with several arguments:

module Fun(A : P)(B : P with type t = A.t) = struct
   let f x = B.foo x
end


-- Alain