Jean-Christophe Filliâtre wrote:
> Despite the embedding you're mentioning, which could be added as follows
> 
>   module type ConstructRing =
>     functor (M : RIG) -> sig include RING val embed : M.t -> t end
> 
> I don't see what else you could add to the signature (unless you want to
> expose that the type t of the RING is a pair of type M.t * M.t; and even
> with that you couldn't expose the definitions of the operations in the
> signature).
> 
> All the properties you're expecting for the resulting ring are part of
> (logical) specifications, which cannot be expressed via ocaml types.
> You could do that in a richer type system (e.g. Coq).

Not quite. The universal property of the resulting ring R is this:
for any ring T, if f : M -> T is a function preserving 0, + and * then 
there is a unique function g : R -> T preserving 0, +, * and - such that
g (include x) = f x, where include is as above. This needs to be 
accounted for, and it's not just a logical specification.

Andrej