On Sep 1, 2006, at 3:29 PM, skaller wrote: > > let string_of_term dfns term = match term with > | #qualified_name_t as x -> string_of_qualified_name x This is, indeed, a practical reason why PM are so nice. In the same line of ideas, I wish I could do something like the following : module type S = sig type t val f : t -> int end module A (B : S with type t = [> ]) (C : S with type t = [> ]) : S with type t = [B.t | C.t] = struct type t = [ B.t | C.t ] let f x = match x with | #A.t as x -> A.f x | #B.t as x -> B.f x end Of course the example won't even compile, but I think it reflects the spirit of what I would like to do. I know this is just not possible due to a practical reason (#A.t is expanded to the constructors that it includes, and therefore, A.t has to be fully known at compile time, correct?). Is there a theoretical reason to have this constraint though? Andres