Math using implicits no longer works

[Katrix]

Compiler version

3.2.0-RC2

Minimized code

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]]

Output

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`.

Expectation

It compiles, as it did in Scala 2

[smarter]

Possible duplicate of #7586

[mbovel]

This example works if we disable the following divergence check:

https://github.com/lampepfl/dotty/blob/2f7c1076fd05e9e716e14cd806fa6863f5e9810f/compiler/src/dotty/tools/dotc/typer/Implicits.scala#L1184

sbt:scala3> scalac -Xprint:typer test.scala
...
[[syntax trees at end of                     typer]] // test.scala
package <empty> {
  ...
  final module class Test() extends Object() { this: Test.type =>
    def main(args: Array[String]): Unit = 
      {
        implicitly[Sum.Aux[Test._1, Test._3, Test._4]](
          Sum.sum2[_0, Succ[Test._2], Succ[Test._3]](Sum.sum1[Succ[Test._3]])
        )
        {
          implicitly[Sum.Aux[Test._2, Test._3, Test._5]](
            Sum.sum2[Succ[_0], Succ[Test._2], Succ[Test._4]](
              Sum.sum2[_0, Succ[Succ[Test._2]], Succ[Test._4]](
                Sum.sum1[Succ[Test._4]]
              )
            )
          )
          ()
        }
      }
  }
}

Content of test.scala (click to view)

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
}

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: Aux[A, Succ[B], C]): Aux[Succ[A], B, C] = new Sum[Succ[A], B] { type Out = C }
}

object Test {
  type _1 = Succ[_0]
  type _2 = Succ[_1]
  type _3 = Succ[_2]
  type _4 = Succ[_3]
  type _5 = Succ[_4]

  def main(args: Array[String]): Unit = {
    implicitly[Sum.Aux[_1, _3, _4]]
    implicitly[Sum.Aux[_2, _3, _5]]
  }
}

Could the divergence check be too strict?

[Katrix]

So I came back to this again to check if it's still a problem with 3.4.0. Seems like it is. However, I also noticed that changing sum2 to this made it compile. Could that give insight into where the problem lies?

  implicit def sum2[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 }