type-level induction on Nat

[Henning Thielemann]

Am 16.03.2014 09:40, schrieb Christiaan Baaij:

> To answer the second question (under the assumption that you want
> phantom-type style Vectors and not GADT-style):

That works, someNatVal was the missing piece.


Now the natural next question is how to perform type-level induction on 
Nat. This page mentions the Nat1 type, a unary representation of natural 
numbers:
   https://ghc.haskell.org/trac/ghc/wiki/TypeNats/MatchingOnNats

Since the unary natural number kind so ubiquituous in examples, is there 
a recommended module to import it from, which also contains the 
injectivity magic of FromNat1? I cannot see it in:

http://hackage.haskell.org/package/base-4.7.0.0/candidate/docs/GHC-TypeLits.html

although it seems to have been there:
   http://co-dan.github.io/base-docs/src/GHC-TypeLits.html