I'm fairly inexperienced with Haskell, but essentially I've started working with DataKinds and GADTs. I have a GADT which represents a list that "knows" its length:
data NSL :: N -> * -> * where
Null :: NSL 'Zero a
More :: a -> NSL n a -> NSL ('Incr n) a
which is created from the natural data representation
data N :: * where
Zero :: N
Incr :: N -> N
So my question is, how do I create a function
fromList :: [a] -> NSL n a
I've tried working with Foldable and similar ideas, but I can't quite wrap my head around it.