Example for Generalised Algebraic Datatypes in Haskell Used to create a safe list type

GADTs.hs

data Safe a = Safe a
data NotSafe = NotSafe
data SafeList a b where
  Nil :: SafeList a NotSafe
  Cons :: a -> SafeList a b -> SafeList a (Safe b)


safeHead :: SafeList a (Safe b) -> a
safeHead (Cons x _) = x
-- safeHead Nil = ???

-- safeHead is a total function!