this actually works :D

gadt_of_prolog.ml

(*
nat(z).
nat(s(N)) :- nat(N).

plus(N, z, N).
plus(N, s(M), s(A)) :- plus(N, M, A).

mult(_, z, z).
mult(N, s(M), B) :- mult(N, M, A), plus(N, A, B).

?- mult(s(s(z)), s(s(z)), N), write(N). % s(s(s(s(z))))
*)

type    z = private Z'
type 'n s = private S'

type (_,_,_) plus =
  | PZ : ('n,z,'n) plus
  | PS : ('n,'m,'a) plus -> ('n,'m s,'a s) plus

type (_,_,_) mult =
  | MZ : (_,z,z) mult
  | MS : ('n,'m,'a) mult * ('n,'a,'b) plus -> ('n,'m s,'b) mult

(* small reflexivity proof to make sure we're correct etc *)
type (_,_) eq = Refl : ('a,'a) eq

let test (type n) : (z s s, z s s, n) mult -> (n, z s s s s) eq
  = fun (MS(MS(MZ,PZ),PS PS PZ)) -> Refl

gadt_plus_comm.ml

(* relies on definitions from the previous file *)

(* give s and z types runtime witnesses *)
type _ nat =
  | NZ : z nat
  | NS : 'a nat -> 'a s nat

(* helper lemmas *)
let rec plus_z : type a. a nat -> (z, a, a) plus
  = function
  | NZ -> PZ
  | NS x -> PS (plus_z x)

let rec plus_s : type a b c. a nat * b nat * (a, b, c) plus -> (a s, b, c s) plus
  = function
  | _, NZ, PZ -> PZ
  | x, NS y, PS z -> PS(plus_s(x, y, z))

(* proving the commutativity of addition :^) *)
let rec proof : type a b c. a nat * b nat * (a, b, c) plus -> (b, a, c) plus
  = function
  | x, NZ, PZ -> plus_z x
  | x, NS y, PS z -> plus_s(y, x, proof(x, y, z))