Type annotations and invariant collections

[GoogleCodeExporter]

The nullness checker reports an error for the following snippet. I think I 
understand how annotations on type parameters are used to qualify upper and 
lower bounds, and why that causes the error.

However, I would expect <T extends @NonNull Object super void> to behave in the 
same way as <T extends @NonNull Object super @NonNull void>, since in either 
case the upper bound @NonNull Object ensures that the type parameter must be 
instantiated with a non-null type. Could the checker infer a @NonNull 
annotation for the second example's lower bound, and allow my example to 
succeed?

import checkers.nullness.quals.*;
import java.util.List;

class Test {
  <T extends @NonNull Object> List<T> m(List<@NonNull T> l1) {
    return l1;
  }
}
...
error: [return.type.incompatible] incompatible types in return.
    return l1;
           ^
  found   : @Initialized @NonNull List<@NonNull T extends @Initialized @NonNull Object>
  required: @Initialized @NonNull List<T extends @Initialized @NonNull Object>

Original issue reported on code.google.com by cus...@google.com on 2 Apr 2014 at 3:42

[GoogleCodeExporter]

Original comment by michael.ernst@gmail.com on 15 Apr 2014 at 6:46

[GoogleCodeExporter]

Original comment by Jonathan...@gmail.com on 15 Apr 2014 at 6:49

[GoogleCodeExporter]

The interaction between type annotations and invariant subtyping for generics 
also causes some problems with @KeyFor, e.g.:

Set<String> getKeys(Map<String, String> map) {
  return map.keySet();
}

Currently gives the error:

Asd.java:6: error: [return.type.incompatible] incompatible types in return.
    return map.keySet();
                     ^
  found   : Set<@KeyFor("map") String>
  required: Set<String>

Original comment by cus...@google.com on 14 May 2014 at 11:25

[GoogleCodeExporter]

These are two separate issues, I think.
In #0:

found   : @Initialized @NonNull List<@NonNull T extends @Initialized @NonNull 
Object>
required: @Initialized @NonNull List<T extends @Initialized @NonNull Object>

these two types should actually be the same, as the use of @NonNull T shouldn't 
change the semantics here (as @NonNull is the bottom type).

In #3 there is a difference:

  found   : Set<@KeyFor("map") String>
  required: Set<String>

The found type argument is different from the expected type argument and, 
because Set is mutable, this must be forbidden.
If we had Issue 299 (extended also to generic types) we could allow the return, 
but would require that the result is used read-only:

@Readonly Set<String> getKeys(Map<String, String> map) {
  return map.keySet();
}

Alternatively, you could change the return type to:

Set<? extends String> getKeys(Map<String, String> map) {
  return map.keySet();
}

but that feels strange as String is a final class.

I can't think of an alternative that couldn't be abused to introduce 
unsoundness.
Any suggestions?

If we're fine with unsoundness for @KeyFor, we could add a flag to make that 
transition easier.

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

[GoogleCodeExporter]

Thanks, I see that the first issue is more about handling defaults.

Supporting @Readonly looks useful, especially if that logic could be expanded 
to allow covariant subtyping for immutable types. The result of map.keySet() is 
immutable, so allowing it to be converted to a Set<String> would be sound.

Original comment by cus...@google.com on 15 May 2014 at 12:01

[GoogleCodeExporter]

Revisiting the original message #0 and example:

  <T extends @NonNull Object> List<T> m(List<@NonNull T> l1) {
    return l1;
  }

In this case, @NonNull T and T have the same meaning: @NonNull is the bottom of 
the qualifier hierarchy and the qualifier on the upper bound.
I see two options:
1. We treat them the same, allowing two options to express the same type.
2. We forbid @NonNull T: the developer might expect that the qualifier makes a 
difference, whereas it is just adding noise.

I would prefer option 2.
Is my observation correct? Are there better options?

cu, WMD.

Original comment by wdi...@gmail.com on 13 Jul 2014 at 4:13

• Changed state: Accepted

[GoogleCodeExporter]

I believe your observation is correct.

My preference is for option 1.

I agree that the annotation, which repeats the default, is just adding noise.
We permit annotations that are the same as the default elsewhere in program 
code, and I feel it would be inconsistent and possibly confusing to forbid them 
here.

We should have one canonical display format for the annotations in messages, 
and I favor the explicit one for that purpose.

It could be nice to have a command-line option that causes the checker to issue 
a warning about redundant annotations (here and elsewhere).

Original comment by michael.ernst@gmail.com on 13 Jul 2014 at 7:23

[GoogleCodeExporter]

So this has been fixed using Option 1 that Werner has outlined.  It is pushed 
and will go out with release 1.9

Original comment by Jonathan...@gmail.com on 8 Apr 2015 at 10:28

• Changed state: Pushed

[GoogleCodeExporter]

Original comment by jtha...@cs.washington.edu on 18 Apr 2015 at 6:42

• Changed state: Fixed