SafeList.hs

{-# LANGUAGE GADTs #-}
module SafeList where

data Empty
data NonEmpty

class Emptiness e
instance Emptiness Empty
instance Emptiness NonEmpty

data List t s where
  Nil  :: List t Empty                                                                                
  Cons :: t -> List t s -> List t NonEmpty

safeHead :: List t NonEmpty -> t
safeHead (Cons h _) = h

safeTail :: Emptiness s1 => List t NonEmpty -> List t s1
safeTail (Cons _ tl@(Cons y ys)) = safeTail tl    -- OMG

SafeList1.hs

{-# LANGUAGE GADTs, EmptyDataDecls, KindSignatures #-}                                                

{-
 -  http://stackoverflow.com/questions/19698904/tail-function-for-safe-list-using-gadts
 -}

data NonEmpty a
data Empty

data SafeList :: * -> * -> * where
  Nil  :: SafeList t Empty
  Cons :: a -> SafeList a b -> SafeList a (NonEmpty b)

safeHead :: SafeList a (NonEmpty b) -> a
safeHead (Cons h _) = h

safeTail :: SafeList a (NonEmpty b) -> SafeList a b
safeTail (Cons _ t) = t