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"?