Evaluator crash because Scala accepts infeasible match case

[vkuncak]

This program, when evaluating evalMe, crashes with: [Internal] java.util.concurrent.ExecutionException: java.lang.RuntimeException: inox.ast.Definitions$ADTLookupException: Lookup failed for adt with symbol stainless.lang.Option$0 [Internal] Please inform the authors of Inox about this message

Note that there is a spurious Asub case in the pattern match of extraCaseHurt, which is entirely non-sensical from ADT point of view, but Scala does not make (cannot make?) the disjointness check to prove it is impossible. Interpreter should just not match the case and proceed, instead of failing.

object ExtraCasesEvalCrash { sealed abstract class A case class Asub() extends A

sealed abstract class B case class Bsub() extends B

def extraCaseHurt(x: B) : Int = x match { case Asub() => -4 case Bsub() => 42 } def evalMe: Int = extraCaseHurt(Bsub()) }

[samarion]

That error is symptomatic of a case match being represented as an UnapplyPattern instead of an ADTPattern. The issue could be either in extraction or in AdtSpecialization.scala if the specializer doesn't realize that Asub and Bsub are ADTs.

[vkuncak]

This seems fixed now.

[samarion]

I seem to be getting a different error:

[ Error  ] EvalMe.scala:9:10: error: constructor cannot be instantiated to expected type;
[ Error  ]  found   : ExtraCasesEvalCrash.Asub
[ Error  ]  required: ExtraCasesEvalCrash.B
               case Asub() => -4

[vkuncak]

Yes, I get this as well. This error is from scalac. I can't figure out why it was not there before. I assume that the front-end compiler version was bumped. In any case, the program is fine to be rejected, since one has no business matching on A when all you can get is B.

[samarion]

Oh, well it seems it's a scalac error. There still seems to be an issue with the dotty frontend though.