Inox does not compile on Scala 3.3.1 +

[sankalpgambhir]

Inox is currently on Scala 3.3.0, and fails to compile on 3.3.1 or higher. I noticed this while updated my build to update dependencies generally.

The following error is raised:

[error] -- Error: <working_dir>/src/main/scala/inox/solvers/SolverFactory.scala:207:14 
[error] 207 |        class NativeZ3OptImpl(override val program: p.type)
[error]     |              ^
[error]     |parent trait NativeZ3Optimizer has a super call which binds to the value inox.solvers.unrolling.AbstractUnrollingSolver.targetProgram. Super calls can only target methods.
[error] one error found

The error seems to be due to a pattern that was disallowed in Scala 3.3.1 (scala/scala3#16908) as in the following minimal example:

trait A              { def f: String }
trait B extends A    { def f = "B" }
trait C extends A    { override val f = "C" }
trait D extends A, B { def d = f }
trait E extends A, B { def d = super.f }

class O1 extends A, B, C, D // passes (why though?)
class O2 extends A, B, C, E // fails

A val overrides a def in a parent trait, and there is an ambiguous access through a subclass. I don't get why leaving out the super. causes it to work.

In any case, despite the error message, a simple search shows that the Inox code base has no instance of def targetProgram or super.targetProgram, so it's not obvious where this is coming from. I do not see any other clear super calls accessing vals either. It would need some more investigation.

This also seems to only happen for that single instance (and commenting it out leads to a successful compile) suggesting that the error is isolated, and not a more global pattern problem.

If anyone else has ideas about what is causing this, it would be helpful to hear them.

[samuelchassot]

Hey!
This is discussed here in my PR, #209, as I tried to bump to Scala 3.3.3 along with Stainless.
Given this issue, for now we decided to leave it as is, as it does not seem trivial to solve.

[samuelchassot]

This also seems to only happen for that single instance (and commenting it out leads to a successful compile) suggesting that the error is isolated, and not a more global pattern problem.
This is good news!

[sankalpgambhir]

Oh thanks, I was not in the loop on that! My bad for not checking the open PRs. I mostly wanted to leave this here so I have a documented source so I don't forget about the details. I will keep passively looking into it while I'm working on Inox.

[samuelchassot]

NP! Okay, sounds good! Thanks :)

[sankalpgambhir]

Okay I have a (shady) fix for this. In src/main/scala/inox/solvers/z3/NativeZ3Optimizer.scala, change every instance of targetProgram to aliased and define:

private val aliased: targetProgram.type = targetProgram

(the access permissions don't matter, checked)

Which is obviously useless, but it works. It is likely an issue with how the compiler checks these accesses. I'll try to minimize and look into dotty sometime later.

It's a band-aid fix but would allow us to update if we want to. I've tested it on 3.3.3. What do you think @samuelchassot ?

Exact diff:

---
diff --git a/src/main/scala/inox/solvers/z3/NativeZ3Optimizer.scala b/src/main/scala/inox/solvers/z3/NativeZ3Optimizer.scala
index 187295e94..110ccfb1a 100644
--- a/src/main/scala/inox/solvers/z3/NativeZ3Optimizer.scala
+++ b/src/main/scala/inox/solvers/z3/NativeZ3Optimizer.scala
@@ -16,9 +16,11 @@ trait NativeZ3Optimizer extends Z3Unrolling with AbstractUnrollingOptimizer  { s
 
   override val name = "native-z3-opt"
 
-  override protected val underlying = NativeZ3Solver.synchronized(new Underlying(targetProgram, context)(using targetSemantics))
+  val aliased: targetProgram.type = targetProgram
 
-  private class Underlying(override val program: targetProgram.type,
+  override protected val underlying = NativeZ3Solver.synchronized(new Underlying(aliased, context)(using targetSemantics))
+
+  private class Underlying(override val program: aliased.type,
                            override val context: Context)
                           (using override val semantics: targetSemantics.type)
     extends AbstractOptimizer with Z3Native {