Methods called from toString need a readonly receiver type

[Shreyas-BS]

Issue Description

Primitive int Readonly constant numbers when passed to the toString method as radix parameter creates this error. It is expecting the object to be also Readonly Type.

How to reproduce

Create an object of type Immutable or Mutable and add 2 toString functions (function overloading) differentiated by an int radix parameter. Call the toString with a constant number as a radix parameter inside the other toString function without.

Screen Shot / Recording

Sample Minimum test case code

import qual.Immutable;

@Immutable
public final class Demo {

    // private final @Immutable int value = 123;

    public @Immutable String toString() {
        return toString(10);
    }

    public @Immutable String toString(int radix) {
        return "Hello";
        // Usually it would be calling a function like this
        // return Integer.toString(this.value, radix);
    }
}

[wmdietl]

Thanks for the bug report!

Note that the receiver for toString() is @Readonly, according to

immutability/src/main/java/pico/typecheck/jdk.astub

Line 14 in 1a53cbb

String toString(@Readonly Object this);

The default receiver for the new method toString(int) is @Immutable, because the corresponding class is annotated as @Immutable.

So the actual receiver at the call site (@Readonly) is a supertype of the expected receiver type (@Immutable).
Therefore, you get an error.

So any method that you want to call from a @Readonly method also needs to have an @Readonly receiver.
Can you try doing that?

[Shreyas-BS]

I am not able to annotate the class with @readonly type and I am getting this error as Invalid annotation

Here is my code that I tried:

import qual.Readonly;

@Readonly
public final class Demo {

    public @Readonly String toString() {
        return toString(10);
    }

    public @Readonly String toString(@Readonly int radix) {
        return "Hello";
    }
}

[wmdietl]

You should annotate the receiver of the method, not the class.
Change the class back to @Immutable and then use String toString(@Readonly Demo this, int radix). The annotations on String and int are not necessary.