I don't know of any formalization of these "with" contraints, but the
current meaning is that typexpr must be a type in the outer
environment.  If the declaration "S with type t = typexpr" is written
in the environment E, typexpr must be a valid type in E (and thus
cannot refer to t).  The constraint is then propagated through the
module type S.  In fact, "t" here is not exactly considered a type
identifier, but rather an access path into the constrained module
type.  So, any reference to t in typexpr is considered a reference to
an upper definition of t, contrarily to what is done in type
declarations.

Therefore, you example is not correct in this setting, since the
references to t are wrong. It should not be too difficult to allow
datatype declarations though, while preserving this semantics, by
having a function for scoping datatypes non-recursively. I am not sure
about the gain of expressive power though, since for instance your
example would remain incorrect.

Last remark: "with" constraints do propagate datatype
declarations, as soon as you use modules instead of types.

For example:

# module A = struct type t = A | B of t end;;
# module type T = sig module A : sig type t end end;;

# module type T' = T with module A = A;;
module type T' = sig module A : sig type t = A.t = A | B of t end end


Cheers.

Christophe Raffalli writes:
 > 
 > Is there a good reason to have this in the grammar
 > mod-constraint ::=
 >    type [type-parameters]  typeconstr =  typexpr
 > | module module-path =  extended-module-path
 > 
 > instead of
 > mod-constraint ::=
 >    type typedef
 > | module module-path =  extended-module-path
 > 
 > Here is an example where this is useful:
 > 
 > Lets say you have  a nice module type and functor:
 > 
 > --
 > module type Ord =
 >    sig
 > 	type t
 > 	val compare : t -> t -> int
 >    end
 > 
 > module F(G:Ord) =
 >    struct
 > 	type t = Empty | Node of G.t * t * t
 > 	let compare = ... the code you want ...
 >    end
 > --
 > 
 > in a .mli you may want to write
 > 
 > --
 > module F : functor (G:Ord) -> Ord
 >    with type t = Empty | Node of G.t * t * t
 > --
 > 
 > And this is not legal because "with type" take a typeexpr and not a 
 > typedef. This is not very natural, bacause you have to move the 
 > definition of t outside F like in
 > --
 > type 'a tree = Empty | Node of 'a * 'a tree * 'a tree
 > module F(G:Ord) =
 >    struct
 > 	type t = G.t tree
 > 	let compare = ... the code you want ...
 >    end
 > --
 > 
 > in a .mli you can now write
 > --
 > type 'a tree = Empty | Node of 'a * 'a tree * 'a tree
 > module F : functor (G:Ord) -> Ord with type t = G.t tree
 > --
 > 
 > The same happends if you use recursive type
 > --
 > module F : functor (G:Ord) -> Ord with type t = (G.t * t) list
 > --
 > is not legal either.
 > 
 > -- 
 > Christophe Raffalli
 > Université de Savoie
 > Batiment Le Chablais, bureau 21
 > 73376 Le Bourget-du-Lac Cedex
 > 
 > tél: (33) 4 79 75 81 03
 > fax: (33) 4 79 75 87 42
 > mail: Christophe.Raffalli@univ-savoie.fr
 > www: http://www.lama.univ-savoie.fr/~RAFFALLI
 > ---------------------------------------------
 > IMPORTANT: this mail is signed using PGP/MIME
 > At least Enigmail/Mozilla, mutt or evolution
 > can check this signature
 > ---------------------------------------------
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners