First-class modules sub-typing

depth.ml

module type C = sig type 'a t = [>`C|`D] as 'a end
module type D = sig include C with type 'a t = [>`D] as 'a end
module rec C : C = C;;
module rec D : D = D;;
type c_t = (module C);;
type d_t = (module D);;
(fun (m : c_t) -> (m :> d_t)) (module C);;
- : d_t = <module>

width.ml

module type A = sig type a end;;
module type B = sig include A type b end;;
type a_t = (module A);;
type b_t = (module B);;
module A : A = struct type a = int end;;
module B : B = struct include A type b = string end;;
(fun (m : b_t) -> (m :> a_t)) (module B);;
- : a_t = <module>

But error for expansible variants:

module type M = sig type t = .. end
module type C = sig include M type t += C end
module type D = sig include C type t += D end
type m_t = (module M);;
type c_t = (module C);;
type d_t = (module D);;
module M : M = struct type t = .. end;;
module C : C = struct include M type t += C end;;
module D : D = struct include C type t += D end;;
(fun (m : c_t) -> (m :> d_t)) (module C);;
Error: Type c_t = (module C) is not a subtype of d_t = (module D) 

Note: _ C.t and _ D.t actually the same type. So not sure is the real in-depth subtyping there.

Constraints not working either:

module M1 : sig type +'a t constraint 'a = [`A|`B] end = struct type +'a t = [`A|`B] as 'a end;;
module M2 : sig type +'a t constraint 'a = [`A] end = struct type +'a t = [`A] as 'a end;;
module type M1 = module type of M1;;
module type M2 = module type of M2;;
(fun (m : (module M1)) -> (m :> (module M2))) (module M1);;
Error: Type (module M1) is not a subtype of (module M2) 

Doh, that ARE NOT the depth value subtyping examples, rather... Kinda type covariance.
The, by value, in-depth subtyping:

module type A = sig val v: [<`A|`B] end;;
module type B = sig val v: [<`B] end;;
type a_t = (module A);;
type b_t = (module B);;
module B : B = struct let v = `B end;;
let (module M) = (fun (m : b_t) -> (m :> a_t)) (module B) in M.v;;
Error: Type b_t = (module B) is not a subtype of a_t = (module A)

Still not working