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