[Haskell-cafe] How to convert a list to a vector encoding its length in its type?

[Martijn van Steenbergen]

David Menendez wrote:
>     data SomeNat where SomeNat :: (Nat n) => n -> SomeNat
>     toPeano :: Int -> SomeNat
> 
> or, equivalently, by using a higher-order function.
> 
>     toPeano :: Int -> (forall n. Nat n => n -> t) -> t

Nice! I thought the only way to create them was with a new datatype,
but this works too. I guess the nontrivial bit to think of is the 
introduction of a fresh type (t in this case). Thanks for this insight!

Martijn.