"Difference Nats" and addition by recursion on the first / second argument

add.ml

type z = Z
type +'a s = S

type _ nat =
  | Z : ('l * 'l) nat
  | S : ('l * 'm) nat -> ('l * 'm s) nat

let rec add : type l m n . (l*m) nat -> (m*n) nat -> (l*n) nat =
  fun i1 i2 ->  match i2 with
    | Z -> i1
    | S i -> S (add i1 i) (* OK *)

let rec shift : type l m. (l*m) nat -> (l s * m s) nat = function
  | Z   -> Z
  | S i -> S (shift i)

let rec add2 : type l m n . (l*m) nat -> (m*n) nat -> (l*n) nat =
  fun i1 i2 ->  match i2 with
    | Z -> i1
    | S i -> add2 (S i1) (shift i)