import org.checkerframework.checker.nullness.qual.*;

// This is how I propose the Collection interface be annotated:
interface Collection1<E extends @Nullable Object> {
    public void add(E elt);
}

class PriorityQueue1<E extends @NonNull Object> implements Collection1<E> {
    public void add(E elt) {
        // just to dereference elt
        elt.hashCode();
    }
}

class PriorityQueue2<E extends @NonNull Object> implements Collection1<E> {
    public void add(E elt) {
        // just to dereference elt
        elt.hashCode();
    }
}

// This is how the Collection interface is currently annotated
interface Collection2<E extends @NonNull Object> {
    public void add(E elt);
}

class PriorityQueue3<E extends @NonNull Object> implements Collection2<E> {
    public void add(E elt) {
        // just to dereference elt
        elt.hashCode();
    }
}

class Methods {
    static void addNull1(Collection1 l) {
        // Allowed, because upper bound of Collection1 is Nullable.
        // :: warning: [unchecked] unchecked call to add(E) as a member of the raw type Collection1
        l.add(null);
    }

    static void bad1() {
        addNull1(new PriorityQueue1());
    }

    // If the types are parameterized (as they should be)
    static <@Nullable E extends @Nullable Object> void addNull2(Collection1<E> l) {
        l.add(null);
    }

    static void bad2() {
        // :: error: (type.argument.type.incompatible)
        addNull2(new PriorityQueue1<@NonNull Object>());
    }

    public static void main(String[] args) {
        bad2();
    }

    static void bad3() {
        // :: error: (type.argument.type.incompatible)
        addNull2(new PriorityQueue2<@NonNull Object>());
    }

    // :: error: (type.argument.type.incompatible)
    static <@Nullable E> void addNull3(Collection2<E> l) {
        l.add(null);
    }
}