Dear all,

Here is a puzzle I run way to often in (yesterday was one of these) and
have not good solution to.

Suppose I have a module signature such as monoids:

module type M = sig  type t  val u:t  val p:t->t->t  end

And a functor:

module type ME = sig  type t  val ps:t list -> t  end
module ME (M:M) : ME with type t := M.t

All good and well. I now want to reuse my functor for list, which are a
monoid. But I can only get:

module type TYPE = sig type t end
module LEF (T:TYPE) : ME with type t = T.t list

By the way, I have no intuition why I cannot use a := (substitution) above
and am stuck with a type definition.

But that's not my question. What I really want is a module

module LE : ME with type t := 'a list

There are two problems here. First, I don't know how to define the
signature (which, expanded would be   sig val ps : 'a list list -> 'a list)
without copying. Second I don't know how to do write the module LE itself,
without boilerplate proportional to the number of function in the signature.

With local modules it is reasonably easy to implement LE without modifying
ME, by re-exporting every function as a function which instantiates LEF
(though I guess [u] would only work because list is covariant). But I would
rather the module LE to extend automatically as I extend the signature of
ME.

The thing is, this is just the commutation between forall-s and product-s.
So provided the functor instantiation is pure, then it is always possible
to do that. But I don't know of any modular way to do it.

So here's my question: how do you/would you solve this problem. If the
solution is compatible with 3.12, it's a plus.



/Arnaud