Bug with ? extends X

[GoogleCodeExporter]

Run:

javac -processor checkers.nullness.NullnessChecker bug.java

On the file "bug.java" with the content:

import java.util.ArrayList;
import java.util.Collections;
import java.util.Enumeration;
import java.util.List;
import java.util.Properties;
import java.util.Set;

class Bug extends Properties {
    @SuppressWarnings("unchecked")
    @Override
    public synchronized Enumeration<Object> keys() {
        // sort elements based on detector (prop key) names
        Set set = keySet();
        return (Enumeration<Object>) sortKeys(set);
    }

    static public Enumeration<?> sortKeys(Set<String> keySet) {
        List<String> sortedList = new ArrayList<String>();
        sortedList.addAll(keySet);
        Collections.sort(sortedList);
        return Collections.enumeration(sortedList);
    }
}

The result is:

bug.java:14: error: incompatible types in argument.
        return (Enumeration<Object>) sortKeys(set);
                                              ^
  found   : @Initialized @NonNull Set<? extends @Initialized @Nullable Object>
  required: @Initialized @NonNull Set<@Initialized @NonNull String>
1 error

This error message is unexpected, as the source has nothing to do with Nullness.

Original issue reported on code.google.com by weitz...@cs.washington.edu on 12 Nov 2013 at 6:45

[GoogleCodeExporter]

Initialization checking is performed as part of nullness checking, so this 
error message is not unexpected.  (See issue 271.)

If the error message is wrong, then that would be a valid bug that should be 
fixed.

Original comment by michael.ernst@gmail.com on 13 Nov 2013 at 12:57

• Changed state: Invalid

[GoogleCodeExporter]

I minimized the test a bit further:

import java.util.Set;

class Issue272 {
    void foo(Set set) {
        bar(set);
    }

    void bar(Set<String> set) {}
}

The source code doesn't mention nullness or initialization annotations 
explicitly, but those are still present thanks to defaulting.

We default implicit wildcards with their declared upper bounds - and the 
declared upper bound for type Set is @Nullable Object. Therefore, there is a 
mismatch between the defaulting of the explicit "Set<String>", which is 
interpreted as "Set<@NonNull String>" and the defaulted raw type.

Note that the code contains raw types and unchecked warnings.
The Checker Framework basically replaces raw types with wildcard instantiations.
(Java is actually cleverer with raw types, but so far it hasn't been a priority 
to implement that logic for annotated types.)

That is, the code looks like:

class Bug272 {
    void foo(Set<?> set) {
        bar(set);
    }

    void bar(Set<String> set) {}
}

Note that this code doesn't compile according to Java type rules for exactly 
the same reason.

I would also say that this issue is invalid.
Please let us know if this explanation clarified the issue.

Original comment by wdi...@gmail.com on 13 Nov 2013 at 5:30