converting data-level natural numbers to type-level

[Henning Thielemann]

Am 15.03.2014 19:17, schrieb Erik Hesselink:

> I think most of the singletons stuff has been moved to the
> 'singletons' package [0].

Yes, that's it. It means that all Nat related functionality in 
'singletons' can be implemented using GHC.TypeLits - interesting.

Using the library I succeeded to convert type-level Nats to data-level 
Integer. Now I need the other way round. I want to implement:

withVector ::
    [a] ->
    (forall n. (KnownNat n) => Vector n a -> b) ->
    b

I want to have the (KnownNat n) constraint, since I want to call 'sing' 
within the continuation and this requires (KnownNat n). I guess, in 
order to implement withVector I need toSing, but this one does not give 
me a (KnownNat n). :-(

Thus I have two questions: What is the meaning of KnownNat and how can I 
implement "withVector"?