Add a way to specify a lower bound qualifier for uses of a particular type.

At the moment we make @Nullable @ImplicitFor java.lang.Void:

https://github.com/typetools/checker-framework/blob/master/checker/src/org/checkerframework/checker/nullness/qual/Nullable.java#L30

Take this example:

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

class VoidImplicit {
  class Visitor<T> {
    String visit(T p) { return ""; }
  }
  void take(Visitor<? extends Object> v) {}
  void bar() {
    take(new Visitor<Void>() {
        String visit(Void p) { return ""; }
      });
    take(new Visitor<@NonNull Void>() {
        String visit(@NonNull Void p) { return ""; }
      });
  }
}

Running the Nullness Checker against this gives:

VoidImplicit.java:9: error: [argument.type.incompatible] incompatible types in argument.
    take(new Visitor<Void>() {
         ^
  found   : VoidImplicit.@Initialized @NonNull <anonymous VoidImplicit$1>
  required: VoidImplicit.@Initialized @NonNull Visitor<? extends @Initialized @NonNull Object>
1 error

1. We deviate from our usual default of treating reference types @NonNull, because the only value that can occupy the Void type is null. Something is wrong with the above code: it doesn't make sense to pass a visitor that can only accept the null value to a method that only accepts visitors for non-null values.
   So far, so good: we get an error (even though using the anonymous class makes the argument type mismatch implicit).

2. More disturbing: why does making the @NonNull annotations explicitly make a difference?
   @ImplicitFor annotations should enforce semantic requirements of the type system, which cannot be changed by explicit annotations from the programmer.
   So I would have expected the same error, ignoring the explicit annotations, or giving an additional error that an explicit annotation is given for something that is implicitly annotated.

Thoughts? Is my understanding of the first or second point incorrect?

Start by reading the @ImplicitFor declaration in checker/src/org/checkerframework/checker/nullness/qual/Nullable.java and running the Nullness Checker on the VoidImplicit.java example. Determine the intended interaction between implicit and explicit qualifiers and the proposed lower-bound qualifier. Done requires an agreed semantic design and corresponding implementation or regression coverage.