Cannot instantiate a non-mutable type parameter T in Option[T]

[mwookawa]

Given

@mutable trait B {}

case class A (var foo: Int) extends B { val baz: Int = foo }


object D {
  def bar(a: Option[B] = None()) { if(a.isDefined) {} } 

Stainless tosses out the exception 2020.10.01 12:39:20 INFO inox.package$FatalError: Cannot instantiate a non-mutable type parameter T in @library

Because I can't annotate Option[T] as Option[@mutable T], there's no obvious way to fix this. Are mutable classes in option types just not supported?

[jad-hamza]

Right, perhaps we should change it in the library. You can try adding the annotation here https://github.com/epfl-lara/stainless/blob/master/frontends/library/stainless/lang/Option.scala or making your own copy of this file with @mutable T.

Edit: Actually it might be best to have two different types, so that by default the pure Option can be assumed to be non mutable by Stainless (which makes some transformations simpler).

[mwookawa]

i tried the former, annotating the type variable, but got the same error message. thoughts?

[jad-hamza]

That's strange, is it maybe an issue with sbt caching? Can you try to define MyOption as a copy in your own file to see if it works?

[mwookawa]

I think it's doing this with bloop and sbt. (i'm finally running on macos). i'll try pasting

[mwookawa]

sorry for the delay. we've moved temporarily to a situation where this error hasn't yet popped up.