-AinvariantArrays and two-dimensional arrays

[GoogleCodeExporter]

If I try to typecheck the following code using the -AinvariantArrays 
command-line option:

  public static void main(String[] args) {
    assert any_null(new Object[][] { null }) == true;
  }

  public static boolean any_null(Object[] a) {
    return true;
  }

then I get the following error:

TwoDimensionalArray.java:7: error: [argument.type.incompatible] incompatible 
types in argument.
    assert any_null(new Object[][] { null }) == true;
                    ^
  found   : Object [] []
  required: Object []
1 error

A complete test case appears as 
checker-framework/checker/tests/nullness-invariantarrays/TwoDimensionalArray.jav
a (currently disabled).

Original issue reported on code.google.com by michael.ernst@gmail.com on 2 Jul 2015 at 5:46

[JonathanBurke]

I think I have a relatively simple fix for this but I want to make sure that I uphold the correct semantics.

Currently the TypeHierarchy assumes that if -AinvariantArrays is chosen, the TypeHierarchy requires both the underlying Java types of arrays and qualifiers to be equivalent. In this example, the component type (Object[]) of the input argument array is covariant to the component type (Object) of the formal parameter.

Is this the desired behavior? The alternative behavior would be to check the primary annotations of the array component invariantly and check any nested annotations using a subtyping check. In this case, only the subtype would have nested annotations so we would not continue.

[JonathanBurke]

Well, this example should fail regardless of whether or not the argument's component type is covariant in the Java type hierarchy. Because the array initializer has a component of NULL we set the component type of the argument to be @KeyForBottom. Which is different from the formal parameter. That is, the due to the PropagationTreeAnnotator, the type of the argument (new Object[][] { null }) becomes: @UnknownKeyFor Object @UnknownKeyFor [] @KeyForBottom [].

While the parameter (Object []) becomes: @UnknownKeyFor Object @UnknownKeyFor []

Of course, both of those qualifiers are invisible so the message you get looks like:

checker/tests/nullness-invariantarrays/TwoDimensionalArray.java:10: error: [argument.type.incompatible] incompatible types in argument.
    assert any_null(new Object[][] { null }) == true;
                    ^
  found   : Object [][]
  required: Object []

[mernst]

The any_null routine takes Object[] but only tests whether the elements are null -- any_null never side-effects its argument. Therefore, covariant subtyping is safe.

Should we use the @Covariant annotation on an array level to indicate this?

I don't think it currently is allowed to be written on an array level, but I think selective covariantce is an important feature to enable -AinvariantArrays.

Also, I find the @Covariant annotation syntax a bit odd. Why does it take a list of indices, rather than a programmer writing @Covariant on each relevant type parameter at the point of declaration?

[wmdietl]

We should discuss the relation to Issue 299: https://github.com/typetools/checker-framework/issues/299