[Haskell-cafe] to make a statically known sized non-empty list

[Markus Läll]

Hi haskell-cafe,

so for fun and profit I was trying to make a non-empty list data type,
where the size of the non-empty prefix would be known for the type-system
with the following code, but it fails with an error "No instance for
(Functor (NonEmpty * a)) ..." for the last line. To me it seems that all
should be known, but something must be missing..

data Nat = Zero | Succ Nat

data family   NonEmpty (n :: Nat) a
data instance NonEmpty Zero       a = Tail [a]
data instance NonEmpty (Succ n)   a = Head a (NonEmpty n a)

instance Functor (NonEmpty Zero) where
   fmap f (Tail xs) = Tail (fmap f xs)
instance Functor (NonEmpty (Succ a)) where
   fmap f (Head x xs) = Head (f x) (fmap f xs)

-- 
Markus Läll
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20131024/35e03cbd/attachment.html>