SafeListHead.scala

sealed trait Decidable[+Proof]
final case class Yes[Proof](proof: Proof) extends Decidable[Proof]
final case object No extends Decidable[Nothing]

sealed trait List[+A] {
  def nonEmpty: Decidable[this.type <:< ::[A]]
  def ::[AA >: A](value: AA): ::[AA] = new ::[AA](value, this)
}
final case object Nil extends List[Nothing] {
  def nonEmpty: Decidable[this.type <:< ::[Nothing]] = No
}
final case class ::[+A](head: A, tail: List[A]) extends List[A] {
  def nonEmpty: Decidable[this.type <:< ::[A]] = Yes(implicitly)
}

// Ideally this should be implemented as syntactic sugar in the compiler.
// You can just match on the Decidable instance yourself but it won't be
// as pretty.
case class ifʹ[P, A](dec: Decidable[P])(f: P => A) {
  def elseʹ(e: => A): A = dec match {
    case Yes(prf) => f(prf)
    case No => e
  }
}

def test[A](l: List[A]): Unit = {
  ifʹ (l.nonEmpty) { implicit proof =>
    // Now that we have a proof that `l` is non-empty in the scope, we
    // can call `l.head` safely as many times as we want.
    println(l.head)
  } elseʹ { 
    // l.head WON'T compile here, you need a proof object to call it
    println("empty!")
  }
}

test(1 :: 2 :: 3 :: Nil) // 1
test(Nil)                // empty!

// It would be ideal if the compiler could rewrite:
// ```scala
// if (expr: Decidable[P]) { A } else { B }
// ```
// into
// ```scala
// expr match {
//   case Yes($p1) =>
//     implicit val $p2 = $p1
//     { A }
//   case No =>
//     { B }
// } 
// ```

// P.S. This little guy ʹ is called MODIFIER LETTER PRIME and
// it is allowed in Java/Scala identifiers since it's technically
// a letter.
// http://www.fileformat.info/info/unicode/char/02b9/index.htm