type-encoding of natural numbers

cnat.scala

trait CNat {
  type succ <: CNat   
  type pred <: CNat   
}

trait _0 extends CNat {
  type pred = _0   
  type succ = CSucc[_0]
}
 
trait CSucc[N <: CNat] extends CNat {
  type pred = N
  type succ = CSucc[CSucc[N]]
}

trait ApplyCNat[N <: CNat, B[_]] {
  type apply[A]
  def apply[A](a: A): apply[A]
}

implicit def apply_0[B[_]]: ApplyCNat[_0, B] = new ApplyCNat[_0, B] {
  type apply[A] = A
  def apply[A](a: A) = a
}

trait SuccCNat[B[_]] {
  type Succ[A] = B[A]
  def apply[A](a: A): Succ[A]
}

implicit def apply_succ[N <: CSucc[M], M <: CNat, B[_]](implicit n: ApplyCNat[M, B], b: SuccCNat[B]): ApplyCNat[N, B] = new ApplyCNat[N, B] {
  type apply[A] = B[n.apply[A]]
  def apply[A](a: A) = b(n(a))
}

implicit def succList: SuccCNat[List] = new SuccCNat[List] { 
  def apply[A](a: A) = List(a)
}
 
/////////////////////////////


import cbool._

scala> implicitly[ApplyCNat[_0, List]].apply(42)
res1: ApplyCNat[_0,List]#apply[Int] = 42

scala> implicitly[ApplyCNat[_0#succ, List]].apply(42)
res2: ApplyCNat[CSucc[_0],List]#apply[Int] = List(42)

scala> implicitly[ApplyCNat[_0#succ#succ, List]].apply(42)
<console>:12: error: could not find implicit value for parameter e: ApplyCNat[CSucc[CSucc[_0]],List]
              implicitly[ApplyCNat[_0#succ#succ, List]].apply(42)
                        ^

scala> apply_succ[_0#succ#succ, _0#succ, List](implicitly[ApplyCNat[_0#succ, List]], implicitly[SuccCNat[List]])
res3: cbool.ApplyCNat[cbool.CSucc[cbool.CSucc[cbool._0]],List] = cbool$$anon$2@6d6a72f2