exh.ml

(* This works *)
module W = struct
    type a
    type b

    type (_, _) t =
      | AA : (a, a) t
      | AB : (a, b) t
      | BB : (b, b) t

    type s = A of a
           | B of b

    type 'a w =
      | W : ('a, 'b) t * 'b -> 'a w

    let f : a w -> s = fun w -> match w with
      | W (AA, a) -> A a
      | W (AB, b) -> B b
end

(* This breaks *)

module rec A : sig
    type a
    val a : a
end = struct
    type a = unit
    let a = ()
end
and B : sig
    type b
    val b : b
end = struct
    type b = unit
    let b = ()
end
and T : sig
    type (_, _) t =
      | AA : (A.a, A.a) t
      | AB : (A.a, B.b) t
      | BB : (B.b, B.b) t
end = struct
    type (_, _) t =
      | AA : (A.a, A.a) t
      | AB : (A.a, B.b) t
      | BB : (B.b, B.b) t
end
and S : sig
    type s
    type _ w

    val wrap : ('a, 'b) T.t -> 'b -> 'a w

    val f : A.a w -> s
end = struct
    type s = A of A.a
           | B of B.b

    type 'a w =
      | W : ('a, 'b) T.t * 'b -> 'a w

    let wrap t b = W (t, b)

    let f : A.a w -> s = fun w -> match w with
      | W (T.AA, a) -> A a
      | W (T.AB, b) -> B b
    (* Compiler warned me the following match was missing, although I think it's
     * not well-typed: `w` should be of type `A.a w` as per the type signature,
     * and since the pair wrapped by `W` in a `'a w` should be of type
     * `('a, 'b) T.t * 'b`, i.e. `(A.a, 'b) T.t * 'b` in this case, the case of
     * `T.BB`, with type `(B.b, B.b) T.t` seems invalid?
     *)
      | W (T.BB, b) -> B b
end

(* Try to call `S.f` with a `T.BB` value, to make sure it's rejected *)
let demo () =
    let _ = S.f (S.wrap T.BB B.b) in
    ()

(* Error: This expression has type B.b S.w
 *       but an expression was expected of type A.a S.w
 *       Type B.b is not compatible with type A.a
 *)