Circumventing OCaml's lack of empty pattern-matching cases when using gadts.

gistfile1.ml

type void = { ex_falso : 'a.'a }

module Eq = struct

  (** Leibniz equality. *)
  type (_,_) t = Refl : ('a,'a) t

  (** Variant of equality with a dummy case used to prove disequalities. *)
  type (_,_) u = Refl' : ('a,'a) u | Dummy : void -> ('a,'b) u

  let to_u : type a b. (a,b) t -> (a,b) u = function
    | Refl -> Refl'

  let of_u : type a b. (a,b) u -> (a,b) t = function
    | Refl' -> Refl
    | Dummy {ex_falso} -> ex_falso

end

type x = X
type y = Y

(** We should be able to [match x] with an empty list of cases, as
    there are no valid case. However, there is no way to express such a
    situation in OCaml. Instead we match on the dummy case. *)
let disequal_x_y : (x,y) Eq.t -> void = fun e ->
  match Eq.to_u e with
  | Eq.Dummy {ex_falso} -> ex_falso