AnnotatedIntersectionTypes are not defaulted correctly

[CharlesZ-Chen]

given test case:

import org.checkerframework.checker.nullness.qual.Nullable;
import java.util.List;
public class Test {
    <E extends @Nullable Object>
    void test (E e) {
        e.toString();
    }    
}

The nullness checker will give a "dereference.of.nullable" error on e.toString(), because the erased type of type variable E would have an annotation @nullable from it's upper bound @Nullable Object as written in the source code.

However, if the upper bound of type variable E becomes an intersection type with @nullable, as below test case showed:

import org.checkerframework.checker.nullness.qual.Nullable;
import java.util.List;
public class Test {
    <E extends @Nullable Object & @Nullable List>
    void test2 (E e) {
        e.toString();
    } 
}

At this time nullness checker won't give any errors and pass this test case.

It seems nullness checker should be expected to give a consistent response for above two test cases, while currently it failed the first one but passed the second one.

Moreover, if add a print statement to print the annotations field of erased atm in AnnotatedTypeVariable#getErased():

@Override
        public AnnotatedTypeMirror getErased() {
            // |T extends A&B| = |A|
            AnnotatedTypeMirror atm = this.getUpperBound().getErased();
            System.out.println("===== typeVar: " + this + "\terased: " + atm + "\terasedAnnos: " + atm.getAnnotations());
            return atm;
        }

The result would be:

first test case:
typeVar: E extends @Initialized @Nullable Object
erased: @Initialized @Nullable Object
erasedAnnos: [@org.checkerframework.checker.initialization.qual.Initialized, @org.checkerframework.checker.nullness.qual.Nullable]

second test case:
typeVar: E extends @Initialized @Nullable Object & @Initialized @Nullable List
erased: @Initialized @Nullable Object & @Initialized @Nullable List
erasedAnnos: [@org.checkerframework.checker.initialization.qual.Initialized, @org.checkerframework.checker.nullness.qual.NonNull]

It seems in the second test case, the erased annotations is @nonnull, but the corresponding erased type is @Initialized @Nullable Object & @Initialized @Nullable List.

I tried to debug it, but it turns out the logic behind getErased() is quite complex. Does anyone have some idea about how to fix it?

Thanks!

[smillst]

The problem is that the explicit upper bound of a type variable is defaulted to @NonNull even when it is an intersection with annotations on all direct super types. So, an error is issued on a call to test2 with a null argument:

import java.util.List;
import org.checkerframework.checker.nullness.qual.Nullable;

public class Issue868 {
    <E extends @Nullable Object & @Nullable List> void test2(E e) {
        e.toString();
    }

    void use() {
        test2(null);
    }
}

Issue868.java:15: error: [type.argument.type.incompatible] incompatible types in type argument.
        test2(null);
             ^
  found   : null
  required: @Initialized @Nullable Object & @Initialized @Nullable List
1 error

I'll look into fix this.

[wmdietl]

This error still occurs in master.