It is possible to implement safeTail
if you change the type structure a bit:
{-# LANGUAGE GADTs, EmptyDataDecls, KindSignatures #-}
data Safe a
data NotSafe
data MarkedList :: * -> * -> * where
Nil :: MarkedList t NotSafe
Cons :: a -> MarkedList a b -> MarkedList a (Safe b)
safeHead :: MarkedList a (Safe b) -> a
safeHead (Cons h _) = h
safeTail :: MarkedList a (Safe b) -> MarkedList a b
safeTail (Cons _ t) = t
The problem with the original safeTail :: MarkedList a Safe -> MarkedList a b
is that b
can be any type - not necessarily the same type that the tail of the list is marked with. This is fixed here by reflecting the list structure on the type level which allows the return type of safeTail
to be appropriately constrained.