Recursion on TypeNats

[Barney Hilken]

> you want the following (which doesnt require undediable instances)
> 
> data Nat = Z | S Nat
> 
> type family U (x :: Nat) where 
>  U  0 = Z
>  U n = S (U (n-1))
> 
> this lets you convert type lits into your own peanos or whatever

Yes, you can do that, but why should you have to? Nat is already the natural numbers, so already has this structure. Why do we have to define it again, making our code that much less clear and readable?