Infinite loop for given ev with match types on dependently typed method args

[MaximeKjaer]

Minimized code

This code implements type-level addition and multiplication on top of scala.compiletime.S. The testProd looks for given evidence that the multiplication commutes for two particular values.

import scala.compiletime.ops.int.S

object InfiniteLoopMatchType {
    def main(args: Array[String]): Unit = {
        testProd(2, 3) // Infinite loop on Dotty 0.20.0-RC1
    }

    def testProd(a: Int, b: Int)(using ev: (a.type * b.type) =:= (b.type * a.type)) = true

    type *[A <: Int, B <: Int] <: Int = A match {
        case 0 => 0
        case _ => MultiplyLoop[A, B, 0]
    }

    type MultiplyLoop[A <: Int, B <: Int, Acc <: Int] <: Int = A match {
        case 0 => Acc
        case S[aMinusOne] => MultiplyLoop[aMinusOne, B, B + Acc]
    }

    type +[A <: Int, B <: Int] <: Int = A match {
        case 0 => B
        case S[aMinusOne] => aMinusOne + S[B]
    }
}

Behavior

The compiler loops infinitely (or at least for a very long time, 20+ minutes).

Expectation

The compiler should be able to reduce 2 * 3 and 3 * 2 to 6, and trivially find an implicit for 6 =:= 6.

Narrowing down the issue

The following compiles instantly, which leads me to believe that the issue is with dependently typed methods:

val a: 2 = 2
val b: 3 = 3
implicitly[(a.type * b.type) =:= (b.type * a.type)]

Alternatively, the following definition of type addition compiles faster (~10s) but still quite slowly compared to the implicitly:

type +[A <: Int, B <: Int] <: Int = A match {
    case 0 => B
    case S[aMinusOne] => S[aMinusOne + B]
}

Related issues

I did not find any related issues.

[MaximeKjaer]

As a workaround for this issue, I have a draft implementation that adds a type +[X <: Int, Y <: Int] <: Int to scala.compiletime, and implements type-level addition in the compiler. Relying on a compiler implementation of addition rather than match types makes the above example compile instantly.

Would there be interest in a PR going in that direction?

[bishabosha]

I believe @propensive begun some work towards this https://github.com/propensive/dotty/tree/typelevel-singleton-literal-type-arithmetic

[nicolasstucki]

Now it takes around 1 minute to compile

[nicolasstucki]

Now it takes around 17 seconds to compile

[OlivierBlanvillain]

Nice, I think we can close this and maybe with a sligtly smaller regression test (17 sec might be a bit much)

[MaximeKjaer]

Indeed, the loop is no longer infinite, so I'm fine closing the issue. But 17 seconds still suggests that there is some unnecessary work happening somewhere. I think it's okay to consider this a performance optimization task for the backlog; if it's tracked by a regression test, then that's already nice.

I'll let you decide what to do with the issue tracking around this.

[nicolasstucki]

If we do testProd(2, 4) it grows quite a lot

[MaximeKjaer]

On my machine, testProd(2, 3) takes 30-ish seconds. I also get warnings about GC:

[warn] In the last 7 seconds, 5.223 (76.1%) were spent in GC. [Heap: 0.20GB free of 0.89GB, max 0.89GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance.

testProd(2, 4) exceeded the GC limit:

Stack trace

[info] compiling 1 Scala source to /home/maxime/code/dotty-bug-report/infinite-loop-match-types/target/scala-3.0.0-RC2/classes ...
[warn] In the last 10 seconds, 7.429 (79.3%) were spent in GC. [Heap: 0.20GB free of 0.89GB, max 0.89GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance.
[warn] In the last 8 seconds, 6.606 (84.0%) were spent in GC. [Heap: 0.14GB free of 0.89GB, max 0.89GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance.
[warn] In the last 10 seconds, 8.564 (94.6%) were spent in GC. [Heap: 0.12GB free of 0.89GB, max 0.89GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance.
[warn] In the last 10 seconds, 9.296 (98.5%) were spent in GC. [Heap: 0.11GB free of 0.89GB, max 0.89GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance.
[warn] In the last 10 seconds, 9.315 (99.7%) were spent in GC. [Heap: 0.11GB free of 0.89GB, max 0.89GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance.
[warn] In the last 10 seconds, 9.464 (99.9%) were spent in GC. [Heap: 0.11GB free of 0.89GB, max 0.89GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance.
[warn] In the last 10 seconds, 9.423 (99.6%) were spent in GC. [Heap: 0.11GB free of 0.89GB, max 0.89GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance.
[warn] In the last 10 seconds, 5.33 (55.4%) were spent in GC. [Heap: 0.11GB free of 0.89GB, max 0.89GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance.
java.lang.OutOfMemoryError: GC overhead limit exceeded while compiling /home/maxime/code/dotty-bug-report/infinite-loop-match-types/src/main/scala/InfiniteLoopMatchType.scala[warn] In the last 9 seconds, 8.894 (99.7%) were spent in GC. [Heap: 0.11GB free of 0.89GB, max 0.89GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance.

[error] ## Exception when compiling 1 sources to /home/maxime/code/dotty-bug-report/infinite-loop-match-types/target/scala-3.0.0-RC2/classes
[error] java.lang.OutOfMemoryError: GC overhead limit exceeded
[error] dotty.tools.dotc.core.Types$LazyRef$.apply(Types.scala:2805)
[error] dotty.tools.dotc.core.Types$TypeMap.mapOver(Types.scala:5270)
[error] dotty.tools.dotc.core.Substituters$.subst(Substituters.scala:23)
[error] dotty.tools.dotc.core.Substituters$.mapArgs$1(Substituters.scala:20)
[error] dotty.tools.dotc.core.Substituters$.mapArgs$1(Substituters.scala:20)
[error] dotty.tools.dotc.core.Substituters$.subst(Substituters.scala:20)
[error] dotty.tools.dotc.core.Types$Type.subst(Types.scala:1712)
[error] dotty.tools.dotc.core.Types$HKTypeLambda.newLikeThis$$anonfun$2(Types.scala:3778)
[error] dotty.tools.dotc.core.Types$HKTypeLambda$$Lambda$5253/1267711777.apply(Unknown Source)
[error] dotty.tools.dotc.core.Types$HKTypeLambda.<init>(Types.scala:3734)
[error] dotty.tools.dotc.core.Types$HKTypeLambda$.apply(Types.scala:3839)
[error] dotty.tools.dotc.core.Types$HKTypeLambda.newLikeThis(Types.scala:3778)
[error] dotty.tools.dotc.core.Types$HKTypeLambda.newLikeThis(Types.scala:3773)
[error] dotty.tools.dotc.core.Types$HKTypeLambda.newLikeThis(Types.scala:3772)
[error] dotty.tools.dotc.core.Types$LambdaType.derivedLambdaType(Types.scala:3335)
[error] dotty.tools.dotc.core.Types$LambdaType.derivedLambdaType$(Types.scala:3278)
[error] dotty.tools.dotc.core.Types$HKLambda.derivedLambdaType(Types.scala:3351)
[error] dotty.tools.dotc.core.Types$TypeMap.derivedLambdaType(Types.scala:5175)
[error] dotty.tools.dotc.core.Types$TypeMap.mapOverLambda(Types.scala:5194)
[error] dotty.tools.dotc.core.Types$TypeMap.mapOver(Types.scala:5219)
[error] dotty.tools.dotc.core.Substituters$.substParams(Substituters.scala:161)
[error] dotty.tools.dotc.core.Substituters$SubstParamsMap.apply(Substituters.scala:197)
[error] dotty.tools.dotc.core.Substituters$SubstParamsMap.apply(Substituters.scala:197)
[error] scala.collection.immutable.List.mapConserve(List.scala:472)
[error] dotty.tools.dotc.core.Types$TypeMap.mapOver(Types.scala:5285)
[error] dotty.tools.dotc.core.Substituters$.substParams(Substituters.scala:161)
[error] dotty.tools.dotc.core.Types$Type.substParams(Types.scala:1732)
[error] dotty.tools.dotc.core.Types$LambdaType.instantiate(Types.scala:3317)
[error] dotty.tools.dotc.core.Types$LambdaType.instantiate$(Types.scala:3278)
[error] dotty.tools.dotc.core.Types$HKLambda.instantiate(Types.scala:3351)
[error] dotty.tools.dotc.core.TypeApplications$.tryReduce$1(TypeApplications.scala:335)
[error] dotty.tools.dotc.core.TypeApplications$.appliedTo$extension(TypeApplications.scala:354)
[error]