(* TEST * expect *) (* Leo's version *) module F(X : sig type t end) = struct type x = X.t type y = X.t type t = E of x type u = t = E of y end;; module M = F(struct type t end);; module type S = module type of M;; [%%expect{| module F : functor (X : sig type t end) -> sig type x = X.t type y = X.t type t = E of x type u = t = E of y end module M : sig type x type y type t = E of x type u = t = E of y end module type S = sig type x type y type t = E of x type u = t = E of y end |}] module rec M1 : S with type x = int and type y = bool = M1;; [%%expect{| Line 1, characters 0-58: 1 | module rec M1 : S with type x = int and type y = bool = M1;; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: This variant or record definition does not match that of type M1.t Constructors do not match: E of M1.x is not compatible with: E of M1.y The types are not equal. |}] let bool_of_int x = let (E y : M1.u) = (E x : M1.t) in y;; bool_of_int 3;; [%%expect{| Line 2, characters 28-32: 2 | let (E y : M1.u) = (E x : M1.t) in ^^^^ Error: Unbound module M1 |}] (* Also check the original version *) type (_,_) eq = Eq : ('a,'a) eq module F(X : Set.OrderedType) = struct type x = Set.Make(X).t and y = Set.Make(X).t type t = E of (x,x) eq type u = t = E of (x,y) eq end;; module M = F(struct type t let compare = compare end);; module type S = module type of M;; [%%expect{| type (_, _) eq = Eq : ('a, 'a) eq module F : functor (X : Set.OrderedType) -> sig type x = Set.Make(X).t and y = Set.Make(X).t type t = E of (x, x) eq type u = t = E of (x, y) eq end module M : sig type x and y type t = E of (x, x) eq type u = t = E of (x, y) eq end module type S = sig type x and y type t = E of (x, x) eq type u = t = E of (x, y) eq end |}] module rec M1 : S with type x = int and type y = bool = M1;; let (E eq : M1.u) = (E Eq : M1.t);; let cast : type a b. (a,b) eq -> a -> b = fun Eq x -> x;; cast eq 3;; [%%expect{| Line 1, characters 0-58: 1 | module rec M1 : S with type x = int and type y = bool = M1;; ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: This variant or record definition does not match that of type M1.t Constructors do not match: E of (M1.x, M1.x) eq is not compatible with: E of (M1.x, M1.y) eq The types are not equal. |}]