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.... although it seems to have been there: http://co-dan.github.io/base-docs/src/GHC-TypeLits.html