Safe List using GADT

safeList.scala

/*
{-#LANGUAGE GADTs, EmptyDataDecls #-}
-- (the EmptyDataDecls pragma must also appear at the very top of the module,
-- in order to allow the Empty and NonEmpty datatype declarations.)

data Empty
data NonEmpty

data SafeList a b where
     Nil :: SafeList a Empty
     Cons:: a -> SafeList a b -> SafeList a NonEmpty

safeHead :: SafeList a NonEmpty -> a
safeHead (Cons x _) = x
*/

type INothing <: Nothing

trait Empty
trait NonEmpty
trait SafeList[+A, -B]
case object Nil extends SafeList[INothing, Empty]
case class Cons[A, B](a: A, as: SafeList[A, B]) extends SafeList[A, NonEmpty]

def safeHead[A](as: SafeList[A, NonEmpty]): A =
  as match {
    case Cons(a, _) => a
  }

val empty = Nil
val xs = Cons(true, empty)
safeHead(empty) // type mismatch
safeHead(xs) // res0: Int = 10