Covariant subtyping for read-only arrays

[GoogleCodeExporter]

With the -AinvariantArrays command-line option, the Checker Framework soundly 
enforces invariant subtyping for arrays:  given two different annotations @A 
and @B, then @A String [] is never a subtype of @B String [].

If an array is used in a read-only fashion, then Java's covariant subtyping is 
sound.  In fact, this rule is used in the Checker Framework's support for 
immutability type systems (definitely IGJ, and possibly Javari).  However, it 
is not used for other type systems.

The request for enhancement is to allow every type sytem to read and trust (but 
not verify) existing IGJ/Javari @ReadOnly annotations.  This would be unsound 
but would be a better and more explicit way of suppressing the warning than 
using @SuppressWarnings.  Furthermore, onec could then use the IGJ or Javari 
checker to regain soundness.

Here is a code example:

    /*>>> import checkers.nullness.quals.Nullable; */

    abstract class Variance
    {
        <T> void f1(String[] x)
        {
            print(x);  // <-- error here
        }

        abstract void print(/*@Nullable*/String[] y);
    }

With -AinvariantArrays, the Nullness Checker correctly reports an error:

java -jar binary/checkers.jar -processor checkers.nullness.NullnessChecker 
Variance.java -AinvariantArrays
Variance.java:7: error: incompatible types in argument.
            print(x);
                  ^
  found   : @Initialized @NonNull String @Initialized @NonNull []
  required: @Initialized @Nullable String @Initialized @NonNull []
1 error

The goal is to mark the parameter to "print" as a read-only reference so the 
Nullness Checker (and any other type system built using the Checker Framework) 
knows that the covariance is safe.

Original issue reported on code.google.com by michael.ernst@gmail.com on 31 Dec 2013 at 4:01

[GoogleCodeExporter]

This proposal should be equally applied to generic types, where it would be 
beneficial to allow:

List<String> <: @Readonly List<Object>

Original comment by wdi...@gmail.com on 14 May 2014 at 11:44

[GoogleCodeExporter]

The workaround I'm currently using:

    /*>>> import org.checkerframework.checker.nullness.qual.Nullable; */

    abstract class ReadOnlyArrayVariance
    {
        <T> void f1(String[] x)
        {
            print1(x);  // <-- no error
            print2(x);  // <-- error
        }

        abstract <T extends /*@Nullable*/String> void print1(T[] y);
        abstract void print2(/*@Nullable*/String[] y);
    }

It seems like having @Readonly trigger covariance in general seems slightly 
type unsafe.  For example, take the following incomplete List interface:

    interface List<T> {
        void append(T element);  // <-- mutates,   contravariant
        T get(int index);        // <-- read-only, covariant
        int indexOf(T element);  // <-- read-only, contravariant
    }

Though read-only often implies covariance, it doesn't always, as is the case 
for "indexOf".

Strangely, the real java.util.List doesn't use the type parameter in indexOf:

    int indexOf(Object element);

This seems to be generally the case for all Java collections types, though I 
haven't done an exhaustive search.  I don't know why they chose to do this.  
IntelliJ's analysis will actually assume that it's actually supposed to be "T" 
and warn you when you're not doing it right.

Original comment by kan...@cakoose.com on 22 May 2014 at 4:37