Tuples/ADTs destruction generating errors

[Ef55]

Here are some crashes/errors caused by tuple/ADT destruction (i.e. val (x, y) = ...).
The ones not relying on stainless' library (i.e. the ones about tuples) do compile&run fine in Scala 3.0.2.

Top-level destruction

object Test {
  // Putting these inside a function makes it work
  def p: (Int, Int) = (1, 2)
  val (x, y) = p
}

stainless-stack-trace.txt

inox.package$FatalError: Cannot recover from missing dependencies at inox.package$FatalError$.apply(package.scala:24) at inox.Reporter.onFatal(Reporter.scala:43) at inox.Reporter.fatalError(Reporter.scala:54) at inox.Reporter.fatalError(Reporter.scala:111) at stainless.frontend.Recovery$.recover(Recovery.scala:110) at stainless.frontend.Preprocessing.transform(Preprocessing.scala:18) at stainless.frontend.SplitCallBack.$anonfun$6(SplitCallBack.scala:166) at stainless.extraction.utils.DebugSymbols.debug(DebugPipeline.scala:64) at stainless.extraction.utils.DebugSymbols.debug$(DebugPipeline.scala:29) at stainless.frontend.SplitCallBack$$anon$1.debug(SplitCallBack.scala:29) at stainless.frontend.SplitCallBack.processFunctions(SplitCallBack.scala:166) at stainless.frontend.SplitCallBack.processSymbols(SplitCallBack.scala:156) at stainless.frontend.SplitCallBack.endExtractions(SplitCallBack.scala:78) at stainless.frontend.ThreadedFrontend$$anon$1.run(ThreadedFrontend.scala:34) at java.lang.Thread.run(Thread.java:750)

Tuple type annotation

object Test {
  def f = {
    def p: (Int, Int) = (1, 2)
    val (x, y): (Int, Int) = p // Removing (Int, Int) makes it work
  }
}

stainless-stack-trace.txt

java.lang.ClassCastException: inox.ast.Types$TupleType cannot be cast to stainless.extraction.oo.Trees$ClassType at stainless.frontends.dotc.CodeExtraction.extractPattern(CodeExtraction.scala:955) at stainless.frontends.dotc.CodeExtraction.extractMatchCase(CodeExtraction.scala:986) at stainless.frontends.dotc.CodeExtraction.extractTree$$anonfun$15(CodeExtraction.scala:1631) at scala.collection.immutable.List.map(List.scala:246) at stainless.frontends.dotc.CodeExtraction.extractTree(CodeExtraction.scala:1631) at stainless.frontends.dotc.CodeExtraction.rec$2(CodeExtraction.scala:1124) at stainless.frontends.dotc.CodeExtraction.rec$2(CodeExtraction.scala:1105) at stainless.frontends.dotc.CodeExtraction.extractBlock(CodeExtraction.scala:1154) at stainless.frontends.dotc.CodeExtraction.extractTree(CodeExtraction.scala:1187) at stainless.frontends.dotc.CodeExtraction.extractTreeOrNoTree(CodeExtraction.scala:999) at stainless.frontends.dotc.CodeExtraction.extractFunction(CodeExtraction.scala:798) at stainless.frontends.dotc.CodeExtraction.extractStatic$$anonfun$1(CodeExtraction.scala:362) 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:333) at stainless.frontends.dotc.CodeExtraction.extractStatic(CodeExtraction.scala:396) at stainless.frontends.dotc.CodeExtraction.extractObject(CodeExtraction.scala:441) at stainless.frontends.dotc.CodeExtraction.extractStatic$$anonfun$1(CodeExtraction.scala:328) 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:333) at stainless.frontends.dotc.CodeExtraction.extractStatic(CodeExtraction.scala:396) at stainless.frontends.dotc.StainlessExtraction.liftedTree1$1(StainlessExtraction.scala:61) at stainless.frontends.dotc.StainlessExtraction.extractUnit(StainlessExtraction.scala:67) at stainless.frontends.dotc.DottyCompiler$ExtractionPhase.run(DottyCompiler.scala:43) at dotty.tools.dotc.core.Phases$Phase.runOn$$anonfun$1(Phases.scala:303) at scala.collection.immutable.List.map(List.scala:250) at dotty.tools.dotc.core.Phases$Phase.runOn(Phases.scala:304) at dotty.tools.dotc.Run.runPhases$4$$anonfun$4(Run.scala:205) 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$5(Run.scala:216) at dotty.tools.dotc.Run.compileUnits$$anonfun$1(Run.scala:224) at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18) at dotty.tools.dotc.util.Stats$.maybeMonitored(Stats.scala:67) at dotty.tools.dotc.Run.compileUnits(Run.scala:231) at dotty.tools.dotc.Run.compileSources(Run.scala:166) at dotty.tools.dotc.Run.compile(Run.scala:150) at dotty.tools.dotc.Driver.doCompile(Driver.scala:39) at dotty.tools.dotc.Driver.process(Driver.scala:199) at dotty.tools.dotc.Driver.process(Driver.scala:167) at stainless.frontends.dotc.DottyDriver.run(DottyCompiler.scala:53) at stainless.frontends.dotc.DottyCompiler$$anon$1.onRun(DottyCompiler.scala:124) at stainless.frontend.ThreadedFrontend$$anon$1.run(ThreadedFrontend.scala:32) at java.lang.Thread.run(Thread.java:750)

Elements type annotation

This just yields an error in the output

object Test {
  def f = {
    def p: (Int, Int) = (1, 2)
    val (x: Int, y: Int) = p // Again, removing type annotations solves the issue
  }
}

Test.scala:4:13: error: Invalid type TypeRef(TermRef(ThisType(TypeRef(NoPrefix,module class <root>)),object scala),class Int) for .isInstanceOf
               val (x: Int, y: Int) = p
                       ^^^
Starting verification...
Verified: 0 / 0
 stainless summary              
..................................................................................
total: 0    valid: 0    (0 from cache) invalid: 0    unknown: 0    time:     0.0 

The same with ADTs

These issues manifest with ADTs as well, e.g.

import stainless.collection.*

object Test {
  def l: List[Int] = List(0, 1, 2)
  val Cons(h: Int, t: List[Int]) = l
}

stainless-stack-trace.txt

inox.package$FatalError: Cannot recover from missing dependencies at inox.package$FatalError$.apply(package.scala:24) at inox.Reporter.onFatal(Reporter.scala:43) at inox.Reporter.fatalError(Reporter.scala:54) at inox.Reporter.fatalError(Reporter.scala:111) at stainless.frontend.Recovery$.recover(Recovery.scala:110) at stainless.frontend.Preprocessing.transform(Preprocessing.scala:18) at stainless.frontend.SplitCallBack.$anonfun$6(SplitCallBack.scala:166) at stainless.extraction.utils.DebugSymbols.debug(DebugPipeline.scala:64) at stainless.extraction.utils.DebugSymbols.debug$(DebugPipeline.scala:29) at stainless.frontend.SplitCallBack$$anon$1.debug(SplitCallBack.scala:29) at stainless.frontend.SplitCallBack.processFunctions(SplitCallBack.scala:166) at stainless.frontend.SplitCallBack.processSymbols(SplitCallBack.scala:156) at stainless.frontend.SplitCallBack.endExtractions(SplitCallBack.scala:78) at stainless.frontend.ThreadedFrontend$$anon$1.run(ThreadedFrontend.scala:34) at java.lang.Thread.run(Thread.java:750)