Nat.scala

sealed trait Nat
class _0 extends Nat
class Succ[T <: Nat]() extends Nat
def Succ[T <: Nat] = new Succ[T]()

object NatOps {
  trait Sum[T <: Nat, U <: Nat] { type R <: Nat }
  type Aux[T <: Nat, U <: Nat, S <: Nat] = Sum[T, U] { type R = S }
  
  implicit def sum0[U <: Nat] = new Sum[_0, U] { type R = U }
  
  implicit def sum[T <: Nat, U <: Nat](implicit s: Sum[T, U]) =
    new Sum[Succ[T], U] { type R = Succ[s.R] }
    
}

import NatOps._

type _1 = Succ[_0]
type _2 = Succ[_1]
type _3 = Succ[_2]
type _4 = Succ[_3]
type _5 = Succ[_4]

def chk[T <: Nat, U <: Nat, R <: Nat](implicit a: Aux[T, U, R]) = a

chk[_1, _3, _4]