Add inductively-defined Nat to base

The proposed addition is simple, add the following to base:

data Nat = Zero | Succ Nat

I will list the pros/cons I see below. Pros:

• Commonly defined throughout many packages, e.g. vinyl
• The inductive definition of 'Nat' is useful for correctness

(e.g. safeHead :: Vec a (S n) -> a; safeHead (Cons a as) = a)

Cons:

• '-XDependentHaskell' will most likely obviate any benefit brought about by type families involving Nat
• Looking at base, I'm not sure where this would go. Having it in its own module seems a tad strange. I am open to criticism concerning the usefulness of the idea or if anyone sees a Pro(s)/Con(s) that I am missing.