GADT typing

gadt_matching.ml

module One = struct
  type t
end

module Two = struct
  type t
end

module Tag_incomplete_match = struct
  type one = One.t
  type two = Two.t

  type (_, _) t =
    | A : (one, string) t
    | B : (two, int) t

  let get_one (type v) (x : (one, v) t) : v =
    match x with
    | A -> "a"

  let get_two (type v) (x : (two, v) t) : v =
    match x with
    | B -> 2

  let get (type s v) (x : (s, v) t) : v =
    match x with
    | A as x' -> get_one x'
    | B as x' -> get_two x'
end

module Tag_complete_match = struct
  type one
  type two

  type (_, _) t =
    | A : (one, string) t
    | B : (two, int) t

  let get_one (type v) (x : (one, v) t) : v =
    match x with
    | A -> "a"

  let get_two (type v) (x : (two, v) t) : v =
    match x with
    | B -> 2

  let get (type s v) (x : (s, v) t) : v =
    match x with
    | A as x' -> get_one x'
    | B as x' -> get_two x'
end

more_detailed_gadt_example.ml

module One : sig
  type t

  val get : t -> string
end = struct
  type t = string

  let get x = x
end

module Two : sig
  type t

  val get : t -> int
end = struct
  type t = int

  let get x = x
end

module Tag_incomplete_match = struct
  type one = One.t
  type two = Two.t

  type (_, _) t =
    | A : (one, string) t
    | B : (two, int) t

  let get_one (type v) (x : (one, v) t) : One.t -> v =
    match x with
    | A -> One.get

  let get_two (type v) (x : (two, v) t) : Two.t -> v =
    match x with
    | B -> Two.get

  let get (type s v) (x : (s, v) t) : s -> v =
    match x with
    | A as x' -> get_one x'
    | B as x' -> get_two x'
end