Stainless crash with nested auto-tupling within a Some pattern

[KacperFKorban]

Version

Stainless version:

[  Info  ] Stainless verification tool (https://github.com/epfl-lara/stainless)
[  Info  ]   Version: 0.9.8.8-19-g20571da
[  Info  ]   Built at: 2024-09-10 14:09:10.727+0200
[  Info  ]   Stainless Scala version: 3.5.0
[  Info  ] Inox solver (https://github.com/epfl-lara/inox)
[  Info  ] Version: 1.1.5-177-ge1f8612
[  Info  ] Bundled Scala compiler: 3.5.0

Reproduction

minimization.scala:

import stainless.lang.*

def minimization(opt: Option[(Int, Int)]): Unit =
  opt match {
    case Some(l, r) => ()
    case _ => ()
  }

Output

Output after running stainless minimization.scala:

[  Info  ] Compiling with standard Scala 3.5.0 compiler front end...
  unhandled exception while running stainless on minimization.scala

  An unhandled exception was thrown in the compiler.
  Please file a crash report here:
  https://github.com/scala/scala3/issues/new/choose
  For non-enriched exceptions, compile with -Xno-enrich-error-messages.

     while compiling: minimization.scala
        during phase: stainless
                mode: Mode(ImplicitsEnabled)
     library version: version 2.13.14
    compiler version: version 3.5.0
            settings: -Wsafe-init true -classpath /home/kpi/stainless/frontends/dotty/target/universal/stage/lib/org.scala-lang.scala-library-2.13.14.jar:/home/kpi/stainless/frontends/dotty/target/universal/stage/lib/org.scala-lang.scala3-library_3-3.5.0.jar -color never -language List(implicitConversions)


[  Info  ] Preprocessing finished                                   
[  Info  ] Finished lowering the symbols                            
[  Info  ] Starting verification...
[  Info  ]  Verified: 0 / 0
[  Info  ] Done in 8.95s
[ Error  ] Stainless terminated with an error.
[ Error  ] Debug output is available in the file `stainless-stack-trace.txt`. If the crash is caused by Stainless, you may report your issue on https://github.com/epfl-lara/stainless/issues
[ Error  ] You may use --debug=stack to have the stack trace displayed in the output.

stainless-stack-trace.txt:

java.lang.AssertionError: assertion failed
	at scala.runtime.Scala3RunTime$.assertFailed(Scala3RunTime.scala:11)
	at stainless.frontends.dotc.CodeExtraction.extractPattern(CodeExtraction.scala:973)
	at stainless.frontends.dotc.CodeExtraction.extractMatchCase(CodeExtraction.scala:1060)
	at stainless.frontends.dotc.CodeExtraction.extractTree$$anonfun$15(CodeExtraction.scala:1779)
	at scala.collection.immutable.List.map(List.scala:247)
	at stainless.frontends.dotc.CodeExtraction.extractTree(CodeExtraction.scala:1779)
	at stainless.frontends.dotc.CodeExtraction.extractTreeOrNoTree(CodeExtraction.scala:1073)
	at stainless.frontends.dotc.CodeExtraction.extractFunction(CodeExtraction.scala:811)
	at stainless.frontends.dotc.CodeExtraction.extractStatic$$anonfun$1(CodeExtraction.scala:386)
	at scala.runtime.function.JProcedure1.apply(JProcedure1.java:15)
	at scala.runtime.function.JProcedure1.apply(JProcedure1.java:10)
	at scala.collection.immutable.List.foreach(List.scala:334)
	at stainless.frontends.dotc.CodeExtraction.extractStatic(CodeExtraction.scala:254)
	at stainless.frontends.dotc.CodeExtraction.extractObject(CodeExtraction.scala:452)
	at stainless.frontends.dotc.CodeExtraction.extractStatic$$anonfun$1(CodeExtraction.scala:336)
	at scala.runtime.function.JProcedure1.apply(JProcedure1.java:15)
	at scala.runtime.function.JProcedure1.apply(JProcedure1.java:10)
	at scala.collection.immutable.List.foreach(List.scala:334)
	at stainless.frontends.dotc.CodeExtraction.extractStatic(CodeExtraction.scala:254)
	at stainless.frontends.dotc.StainlessExtraction.tryExtractUnit(StainlessExtraction.scala:68)
	at stainless.frontends.dotc.StainlessExtraction.extractUnit(StainlessExtraction.scala:48)
	at stainless.frontends.dotc.DottyCompiler$ExtractionPhase.run(DottyCompiler.scala:48)
	at dotty.tools.dotc.core.Phases$Phase.runOn$$anonfun$1(Phases.scala:380)
	at scala.runtime.function.JProcedure1.apply(JProcedure1.java:15)
	at scala.runtime.function.JProcedure1.apply(JProcedure1.java:10)
	at scala.collection.immutable.List.foreach(List.scala:334)
	at dotty.tools.dotc.core.Phases$Phase.runOn(Phases.scala:373)
	at stainless.frontends.dotc.DottyCompiler$ExtractionPhase.runOn(DottyCompiler.scala:53)
	at dotty.tools.dotc.Run.runPhases$1$$anonfun$1(Run.scala:343)
	at scala.runtime.function.JProcedure1.apply(JProcedure1.java:15)
	at scala.runtime.function.JProcedure1.apply(JProcedure1.java:10)
	at scala.collection.ArrayOps$.foreach$extension(ArrayOps.scala:1323)
	at dotty.tools.dotc.Run.runPhases$1(Run.scala:336)
	at dotty.tools.dotc.Run.compileUnits$$anonfun$1(Run.scala:384)
	at dotty.tools.dotc.Run.compileUnits$$anonfun$adapted$1(Run.scala:396)
	at dotty.tools.dotc.util.Stats$.maybeMonitored(Stats.scala:69)
	at dotty.tools.dotc.Run.compileUnits(Run.scala:396)
	at dotty.tools.dotc.Run.compileSources(Run.scala:282)
	at dotty.tools.dotc.Run.compile(Run.scala:267)
	at dotty.tools.dotc.Driver.doCompile(Driver.scala:37)
	at dotty.tools.dotc.Driver.process(Driver.scala:201)
	at dotty.tools.dotc.Driver.process(Driver.scala:169)
	at stainless.frontends.dotc.DottyDriver.run(DottyCompiler.scala:74)
	at stainless.frontends.dotc.DottyCompiler$Factory$$anon$1.onRun(DottyCompiler.scala:171)
	at stainless.frontend.ThreadedFrontend$$anon$1.run(ThreadedFrontend.scala:34)
	at java.base/java.lang.Thread.run(Thread.java:840)

Expectation

Stainless should not crash and should terminate correctly since there is almost nothing to verify.

Workaround

import stainless.lang.*

def minimization(opt: Option[(Int, Int)]): Unit =
  opt match {
    case Some((l, r)) => () // add extra parentheses here
    case _ => ()
  }

Other notes

I think that the issue is in this line:

stainless/frontends/dotty/src/main/scala/stainless/frontends/dotc/CodeExtraction.scala

Line 1024 in bd9da42

case AppliedType(opt, List(underlying)) if opt.typeSymbol == optionClassSym || opt.typeSymbol == optionSymbol =>

changing the line to the following might help:

case AppliedType(opt, List(underlying)) if isOptionClassSym(opt.typeSymbol) || opt.typeSymbol.derivesFrom(optionSymbol) =>

(or changing the == to .derivesFrom)