math - OCaml での型レベルの算術演算

Question

わかりました、より多くのタイプのハッカーの失敗。:) :P

（ランタイム）を取り除き、代わりに静的にチェックするという1週間の追跡の中でassert(n > 0)、私はこのモジュールを思いつきました：

module Nat : sig 
  type z
  type 'n s

  type ('a, 'n) nat = 
          Zero : ('a, z) nat 
        | Succ : ('a, 'n) nat -> ('a, 'n s) nat 

  val add : ('a, 'n) nat -> ('a, 'n s) nat

end = struct          
  type z
  type 'n s
  type ('a, 'n) nat = 
          Zero : ('a, z) nat 
        | Succ : ('a, 'n) nat -> ('a, 'n s) nat 

  let add n = Succ n

  (*  
  let rec to_int n = function 
        | Succ a -> 1 + (to_int a)
        | Zero -> 0
        *)
end

これにより、数値が独自の型でエンコードされた Peano 数値が得られます。

# Zero;;
- : ('a, Nat.z) Nat.nat = Zero
# Succ (Zero);;
- : ('a, Nat.z Nat.s) Nat.nat = Succ Zero
# add (Succ Zero);;
- : ('_a, Nat.z Nat.s Nat.s) Nat.nat = Succ (Succ Zero) 

ただし、最後の関数to_intはコンパイルされません。

Error: This pattern [Zero -> 0] matches values of type ('a, z) nat
   but a pattern was expected which matches values of type
     ('a, ex#0 s) nat

これは、 z と s が異なる型だからだと思います。同じタイプにして、ファントムタイプのままにすることはできますか？

(重複の可能性: ocaml の型レベル整数)