Using GADT types to encode the facts:

- zero is a natural number
- successor of a natural number is a natural number
- zero adds to whatever natural number is that number
- if
`a`

and`b`

sums to`c`

, then succ. of`a`

and`b`

sums to succ. of`c`

.

Then GADT values are just the proof terms of the facts encoded by their types.

But all these good wishes are suspended by the error message:

Error: In this definition, a type variable cannot be deduced

from the type parameters.

It refers to the type definition of `nat`

. What are the problems with the code?

```
(* use toplevel to show the error *)
type 'a s;;
type z;;
type _ nat =
| Zero : z nat
| Succ : 'a nat -> 'a s nat;;
let two_is_nat : z s s nat = Succ (Succ Zero);;
type (_ , _, _) add =
| Monoid : (z nat, 'a nat , 'a nat) add
| Step : ('a nat, 'b nat, 'c nat) add -> ('a s nat, 'b nat, 'c s nat) add
let zero_plus_one_is_one : (z nat, z s nat , z s nat) add
= Monoid
let one_plus_one_is_two : (z s nat, z s nat, z s s nat) add
= Step Monoid
let two_plus_one_is_three : (z s s nat, z s nat, z s s s nat) add
= Step (Step Monoid)
```