Peano.scala

object Peano {
  
  sealed trait Nat
  trait Zero extends Nat
  object ZeroV extends Zero
  case class Succ[A <: Nat](x: A) extends Nat

  trait Sum[A <: Nat, B <: Nat] {
    type Out <: Nat
  }

  object Sum {

    type Aux[A <: Nat, B <: Nat, C <: Nat] = Sum[A, B] {
      type Out = C
    }

    implicit def baseCase[B <: Nat]: Aux[Zero, B, B] =
      new Sum[Zero, B] {
        type Out = B
      }

    implicit def inductiveStep[A <: Nat, B <: Nat]
      (implicit sum: Sum[A, Succ[B]]): Aux[Succ[A], B, sum.Out] = new Sum[Succ[A], B] {
        type Out = sum.Out
      }

  }


  /*
    Doesn't compile as we can't convience the compiler that b.type =:= sum.Out 
    
    Do so we need to a concise way of constraining the Out member of Plus. Like the
    "Aux" type we use above, but I can't figure out the details.

     found   : b.type (with underlying type B)
     required: sum.Out
       case ZeroV => b
                     ^

  */
  def plus[A <: Nat, B <: Nat](a: A, b: B)
                              (implicit sum: Sum[A, B]): sum.Out = a match {
    case ZeroV => b
    // case Succ(q) => plus(q, Succ(b))
  }
  
  plus(ZeroV: Zero, Succ[Zero](ZeroV))

}

Here's a simple example of how to make it work:

package dep

import scala.language._

object Dep extends App {

  sealed trait Nat {
    type Plus[M <: Nat] <: Nat
    def plus[M <: Nat](m: M): Plus[M]
  }

  implicit object Z extends Nat {
    type Plus[M <: Nat] = M
    def plus[M <: Nat](m: M) = m
    override def toString = "Z"
  }

  type Z = Z.type

  case class S[N <: Nat](n: N) extends Nat {
    type Plus[M <: Nat] = S[N#Plus[M]]
    def plus[M <: Nat](m: M) = S(n plus m)
  }

  implicit def getS[N <: Nat](implicit n: N): S[N]= S(implicitly[N])

  type T0 = Z
  type T1 = S[T0]
  type T2 = S[T1]
  type T3 = S[T2]
  type T4 = S[T3]
  type T5 = S[T4]
  type T6 = S[T5]
  type T7 = S[T6]
  type T8 = S[T7]
  type T9 = S[T8]


  sealed trait Vect[+A, N <: Nat] {
    def ++[B >: A, M <: Nat](other: Vect[B, M]): Vect[B, N#Plus[M]]
    def length: N
  }

  final case object VNil extends Vect[Nothing, Z] {
    def ++[B, M <: Nat](other: Vect[B, M]) = other
    def length = Z
  }
  final case class VCons[A, B >: A, N <: Nat](b: B, xs: Vect[A, N]) extends Vect[B, S[N]] {
    def ++[C >: B, M <: Nat](other: Vect[C, M]) = VCons(b, xs ++ other)
    def length = S(xs.length)
  }

  val two: Vect[Int, T2] = VCons(1, VCons(2, VNil))
  val one: Vect[Int, T1] = VCons(3, VNil)
  val three: Vect[Int, T3] = two ++ one

}