trait Nat { type N <: Nat } case class Succ[P <: Nat]() extends Nat { type N = Succ[P] } class _0 extends Nat with Serializable { type N = _0 } type _1 = Succ[_0] val _1: _1 = new _1 type _2 = Succ[_1] val _2: _2 = new _2 type _3 = Succ[_2] val _3: _3 = new _3 type _4 = Succ[_3] val _4: _4 = new _4 type _5 = Succ[_4] val _5: _5 = new _5 trait Sum[A <: Nat, B <: Nat] extends Serializable { type Out <: Nat } object Sum { def apply[A <: Nat, B <: Nat](implicit sum: Sum[A, B]): Aux[A, B, sum.Out] = sum type Aux[A <: Nat, B <: Nat, C <: Nat] = Sum[A, B] { type Out = C } implicit def sum1[B <: Nat]: Aux[_0, B, B] = new Sum[_0, B] { type Out = B } implicit def sum2[A <: Nat, B <: Nat, C <: Nat] (implicit sum : Sum.Aux[A, Succ[B], C]): Aux[Succ[A], B, C] = new Sum[Succ[A], B] { type Out = C } } implicitly[Sum.Aux[_1, _3, _4]] implicitly[Sum.Aux[_2, _3, _5]]

No given instance of type Playground.Sum.Aux[Playground._2, Playground._3, Playground._5] was found for parameter e of method implicitly in object Predef. I found: Playground.Sum.sum2[Playground.Succ[Playground._0], Playground.Succ[Playground._2] , Playground.Succ[Playground._4]]( /* missing */ summon[ Playground.Sum.Aux[Playground.Succ[Playground._0], Playground.Succ[Playground.Succ[Playground._2]] , Playground.Succ[Playground._4]] ] ) But no implicit values were found that match type Playground.Sum.Aux[Playground.Succ[Playground._0], Playground.Succ[Playground.Succ[Playground._2]] , Playground.Succ[Playground._4]]. Note: method sum2 in object Sum was not considered because it was not imported with `import given`.