I've been experimenting with a way to combine GADTs with polymorphic variants, for example to give invariants that all fields of a record use the same polymorphic variant tag (even if the type parameters are different).

For example to have the validation status as a parameter of a record, and have functions that only accept validated records (you could achieve something similar and probably simpler with functors):

  type validation = [`Valid | `Invalid]
  type valid = [`Valid]
  module V : sig
    type ('a, 'b) t
    val of_string : validate:(string -> 'a) -> string -> ('a, [> validation]) t
    val valid_or_exn : ('a, validation) t -> ('a, [> valid]) t
    val valid : ('a, valid) t -> 'a
  end = struct
  type (_,_) typ =
    | Invalid: exn -> ('a, [> `Invalid] as 'b) typ
    | Valid: 'a -> ('a, [> `Valid] as 'b) typ

  type ('a, 'b) t = { raw: string; value: ('a, 'b) typ }

  let of_string ~validate raw = { raw; value = try Valid (validate raw) with e -> Invalid e }

  let valid_or_exn s = match s.value with
    | Valid _ as v -> { s with value = v }
    | Invalid e -> raise e

  let valid ({ value = Valid v; raw = _ } : ('a, valid) t) = v
  end

  type 'b t = {
    x: (int, 'b) V.t;
    y: (string, 'b) V.t;
  }
  let (v:valid t) =
    let raw = {
      x = V.of_string ~validate:int_of_string "4";
      y = V.of_string ~validate:String.escaped "test\n"
    } in
    { x = V.valid_or_exn raw.x; y = V.valid_or_exn raw.y }

Looks like the compiler knows that the 'valid' function can't take 'Invalid' types given the proper type annotations on the polymorphic variant (without type annotations it gives a warning that the match is not exhaustive).