Recursion on TypeNats

[Barney Hilken]

If you define your own type level naturals by promoting

data Nat = Z | S Nat

you can define data families recursively, for example

data family Power :: Nat -> * -> *
data instance Power Z a = PowerZ
data instance Power (S n) a = PowerS a (Power n a)

But if you use the built-in type level Nat, I can find no way to do the same thing. You can define a closed type family

type family Power (n :: Nat) a where
	Power 0 a = ()
	Power n a = (a, Power (n-1) a)

but this isn't the same thing (and requires UndecidableInstances).

Have I missed something? The user guide page is pretty sparse, and not up to date anyway.

If not, are there plans to add a "Successor" constructor to Nat? I would have thought this was the main point of using Nat rather than Int.

Barney.