Better error messages for transitively mutable classes

[mwookawa]

In the case of

trait C {}

object D { def build(bar: Int) = new D(bar)}
case class D(var foo: Int) { def setFoo = {foo = 5}}

object A { def build(bar: Int) = new A(bar) }
case class A(val abcd: Int) extends C { val abcde: D = D.build(0)}

case class B() { val foo: A = new A(0) 

I get the error 2020.10.02 14:20:45 INFO inox.package$FatalError: A mutable class (A) cannot have a non-@mutable and non-sealed parent (C)

I understand that this is because D is mutable and A refers to D. (further that abcde cannot point to the mutable object built by D). However, the error message I'm getting for this case with a complex codebase is really not very helpful, as I have to comb through all the referenced classes from class A to find the mutable class D, which often looks quite immutable at first glance. It's not obvious to me how to implement this in stainless/inox, but would it be possible to get at least some line numbers and a more elaborated error message for this case?

[jad-hamza]

Here I think the error is that you need to annotate @mutable trait C {}, and then you'll have other error messages.

[mwookawa]

yes, sorry, to be clearer, the issue is that once you put the @mutable annotation on C. you inherit (ho ho ho) two problems. the first is that the mutable annotation on C propagates to eg type variables, triggering things like #849. One also gets the error that abcde points to mutable object. however, let's say that D references 500 classes and there is a class hierarchy on D of depth 500. Figuring out where the mutability lies is not a very non-trivial problem, and the one I have. Yet, the only error message I get is that abcde refers to a mutable object.

does that make more sense?

[jad-hamza]

yes, sorry, to be clearer, the issue is that once you put the @mutable annotation on C. you inherit (ho ho ho) two problems. the first is that the mutable annotation on C propagates to eg type variables, triggering things like #849.

Hopefully we can find a solution to this!

One also gets the error that abcde points to mutable object. however, let's say that D references 500 classes and there is a class hierarchy on D of depth 500. Figuring out where the mutability lies is not a very non-trivial problem, and the one I have. Yet, the only error message I get is that abcde refers to a mutable object.

does that make more sense?

If I understand correctly, you don't want your D to be mutable, but it is because of some subclass? We should perhaps add an annotation forcing non-mutability and this could trigger some checks (like @pure for functions).

[mwookawa]

ooh, @immutable would be very helpful. another way to look at it is that i'd like to mark A immutable and have stainless tell me that it is actually mutable because of the reference to D (which is potentially mutable because of some reference to F, which .. G .. which etc.)