Logic using GADTs in OCaml

logic.ml

(* Logic using GADTs *)
exception Axiom
type falso
type ex_falso = {ex_falso: 'p. falso -> 'p}
let ex_falso = {ex_falso = fun _ -> raise Axiom}
type 'p not = 'p -> falso
type ('a,'b) ior = Inl of 'a | Inr of 'b
(* NB: the unit -> below is essential for soundness *)
type classic = {classic: 'p. unit -> ('p, 'p not) ior}
type (_,_) eq = Refl : ('x,'x) eq

(* forall x, exists y, x = y *)
type 'a exeq = Exeq : ('x,'y) eq -> 'x exeq
type for_all_x_exists_y_eq_x_y = {faxy: 'x. 'x exeq}
let proof = {faxy = Exeq Refl}

(* Drinkers paradox: exists x, x drinks -> forall y, y drinks *)
type _ drinks
type all_drink = {all: 'y. unit -> 'y drinks}
type non_drinker = Nd : 'x drinks not -> non_drinker
type drinkers_paradox = Drinker : ('x drinks -> all_drink) -> drinkers_paradox
let proof {classic=c} =
  let ef = ex_falso.ex_falso in
  match c () with
  | Inl (Nd nd) -> Drinker (fun d -> ef (nd d))
  | Inr nnd -> Drinker (fun d ->
      {all = fun () -> match c() with
      | Inr nd -> ef (nnd (Nd nd))
      | Inl d -> d})