Out of Memory Error while Type Checking

[Capital-EX]

The Scala compiler can be made to run out of memory while attempting to type check code that uses generics. Even while using a heap size of 4GB this fairly short snippet of code will cause the type check to run (seemingly) forever. My hunch is that Scala is attempting to construct an infinite type for quot[A, S0, S1].

Compiler version

Scala 3.2.2

Minimized code

def dup[A, S](s : (A, S)) = (s._1, s)

def quote[A, S0, S1](s : (A, S0)) = ((s1 : S1) => (s._1, s1), s._2)

def apply[R, S](s : (S => R, S)) = s._1(s._2)

val s = apply (dup (quote (1, ())))

Output (click arrow to expand)

OpenJDK 64-Bit Server VM warning: Ignoring option MaxPermSize; support was removed in 8.0
OpenJDK 64-Bit Server VM warning: Ignoring option MaxPermSize; support was removed in 8.0
[info] welcome to sbt 1.8.2 (Oracle Corporation Java 11.0.18)
[info] loading settings for project mixin-madness-build-build from metals.sbt ...
[info] loading project definition from /home/exarch/Documents/projects-scala/mixin-madness/project/project
[info] loading settings for project mixin-madness-build from metals.sbt ...
[info] loading project definition from /home/exarch/Documents/projects-scala/mixin-madness/project
[success] Generated .bloop/mixin-madness-build.json
[success] Total time: 0 s, completed Mar 10, 2023, 10:23:38 PM
[info] loading settings for project root from build.sbt ...
[info] set current project to mixin-madness (in build file:/home/exarch/Documents/projects-scala/mixin-madness/)
[info] compiling 1 Scala source to /home/exarch/Documents/projects-scala/mixin-madness/target/scala-3.2.2/classes ...
[warn] In the last 10 seconds, 9.758 (98.8%) were spent in GC. [Heap: 0.18GB free of 4.00GB, max 4.00GB] 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.455 (98.3%) were spent in GC. [Heap: 0.05GB free of 4.00GB, max 4.00GB] 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.782 (99.6%) were spent in GC. [Heap: 0.01GB free of 4.00GB, max 4.00GB] 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.603 (99.8%) were spent in GC. [Heap: 0.01GB free of 4.00GB, max 4.00GB] 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.584 (100.0%) were spent in GC. [Heap: 0.00GB free of 4.00GB, max 4.00GB] 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.886 (99.9%) were spent in GC. [Heap: 0.00GB free of 4.00GB, max 4.00GB] Consider increasing the JVM heap using `-Xmx` or try a different collector, e.g. `-XX:+UseG1GC`, for better performance.
Exception in thread "classloader-cache-cleanup-0" java.lang.OutOfMemoryError: Java heap space
  | => rat sbt.internal.classpath.ClassLoaderCache$$Lambda$741/0x00000008005e8040.get$Lambda(Unknown Source)
        at java.base/java.lang.invoke.DirectMethodHandle$Holder.invokeStatic(DirectMethodHandle$Holder)
        at java.base/java.lang.invoke.Invokers$Holder.linkToTargetMethod(Invokers$Holder)
        at sbt.internal.classpath.ClassLoaderCache.sbt$internal$classpath$ClassLoaderCache$$clearExpiredLoaders(ClassLoaderCache.scala:79)
        at sbt.internal.classpath.ClassLoaderCache$CleanupThread.run(ClassLoaderCache.scala:113)
java.lang.OutOfMemoryError: Java heap space while typechecking /home/exarch/Documents/projects-scala/mixin-madjava.lang.OutOfMemoryError: Java heap space while typechecking /home/exarch/Documents/projects-scala/mixin-madness/src/main/scala/Main.scala
java.lang.OutOfMemoryError: Java heap space while compiling /home/exarch/Documents/projects-scala/mixin-madness/src/main/scala/Main.scala
[error] ## Exception when compiling 1 sources to /home/exarch/Documents/projects-scala/mixin-madness/target/scala-3.2.2/classes
[error] java.lang.OutOfMemoryError: Java heap space
[error] 
[error]            
java.lang.OutOfMemoryError: Java heap space
[error] [launcher] error during sbt launcher: java.lang.OutOfMemoryError: Java heap space

[odersky]

So, what remedy do you propose? Like most interesting languages, Scala does not guarantee termination of type checking.

[Capital-EX]

This is less about termination of type checking, and more potential errors in Scala approach to type checking. Many languages have non-terminating type checking, however only scala has resulted in this result.

However, one solution could be Idris's approach. Idris has full dependent typing and theorem proving, but distinguishes between total and non-total function. And restricts type-level programming to function Idris can prove are total. This may prove benfitial to Scala if there are plans for further dependent typing features.

But, Idris's type checker still halts with the message:

Error: Can't solve constraint between: (?a, ?s) -> ?c and ?a [no locals in scope].

Similar errors will be generated by Haskell, OCaml and F#.

Rust can detect that the type of apply would be cyclical and rejects it for having an infinite size:

error[E0308]: mismatched types
  --> src/main.rs:18:19
   |
18 |     let _ = apply(dup(quote((1,()))));
   |             ----- ^^^^^^^^^^^^^^^^^^ cyclic type of infinite size
   |             |
   |             arguments to this function are incorrect
   |
note: function defined here
  --> src/main.rs:13:4
   |
13 | fn apply<R: Clone, S: Clone>(s: (Rc<dyn Fn(R) -> S>, S)) -> R {
   |    ^^^^^                       -----------------------------

I've tested this expression in about a dozen languages so far, but Scala is the only one with this unusually behavior. I'm not sure if I could propose a fix without a deeper understanding of Scala's approach to type checking. Most languages with generics/templates/type-level programing/etc. will have non-terminating type checkers, however none fail while evaluating simple polymorphic types for generic functions.

However, a short term fix could be including a memory limit on top of the existing recursion. If this unique behavior is intended, I can close the this issue.