Impredicative types in Scala via shapeless

gistfile1.scala

// See http://research.microsoft.com/en-us/um/people/simonpj/papers/boxy/boxy-icfp.pdf
object Impredicative extends App {
  import shapeless._
  import TypeOperators._
  
  object head extends (List ~> Id) {
    def default[T](l : List[T]) = l.head
  }
  
  def g(o : Option[List ~> Id]) = o match {
    case None => (0, '0')
    case Some(get) => (get(List(1, 2)), get(List('a', 'b', 'c')))
  }
  
  val gNone = g(None)
  assert(gNone == (0, '0'))
  
  val gSome = g(Option(head))
  assert(gSome == (1, 'a'))
}