Overriding methods should inherit annotations

At the moment, the annotations on an overriding method are determined
independently of the annotations on the overridden method and the overriding
method is checked for correct behavioral subtyping.
This allows us to use the same defaulting scheme for all methods, making the
meaning of an un-annotated method uniform.
However, this also means that the annotation effort is higher than we might
want.

Consider a superclass that contains declaration and type annotations:

class Super {
  @DA
  @TA Object foo(@TB Object p) {...}
}

Let's assume these annotations do not correspond to the defaults for
those locations.

Now in a subclass we might want to override the method:

class Sub extends Super {
  @Override
  Object foo(Object p) {...}
}

This class will have normal defaulting applied, resulting in something like:

class Sub extends Super {
  @DefaultDA
  @Override
  @DefaultTA Object foo(@DefaultTA Object p) {...}
}

The Checker Framework might now issue errors for three reasons:

• incompatible method overriding, for the declaration annotation, if
  @DefaultDA and @DA are incompatible. For example, if Super.foo is
  declared @Pure, also the overriding method must be pure.

• incompatible return type, if @DefaultTA is a
  supertype of @TA. For example, if Super.foo returns @NonNull Object, the
  overriding method may not default to @Nullable Object.
  Return types may only get "narrower", i.e. change covariantly.

• incompatible parameter type, if @DefaultTA is a
  subtype of @TB. For example, if Super.foo takes @Nullable Object, the
  overriding method may not default to @NonNull Object.
  Parameter types may only get "wider", i.e. change contravariantly.

So far the Checker Framework philosophy was that the programmer must
make such annotations explicit to prevent any possible misunderstanding
in what the code actually means.

We could add an -AinheritAnnotations option, such that the defaulting for the
subclass would be changed to copy the annotations from an overridden method.
For example, the above unannotated code would be interpreted as:

class Sub extends Super {
  @DA
  @TA Object foo(@TB Object p) {...}
}

and the programmer doesn't have any annotation effort.

The potential downside is that the programmer might be confused by
error messages.

A few design considerations:

• Do we want to distinguish whether only declaration annotations are inherited
  from whether type annotations are?
• How does this feature interact with @DefaultQualifiers in scope?
• Can we make error messages depend on whether the annotation was
  inherited?

Original issue reported on code.google.com by wdi...@gmail.com on 2 Dec 2013 at 3:35

Review the proposed -AinheritAnnotations option and the defaulting and overriding behavior shown in the superclass and subclass examples. Resolve whether declaration and type annotations are inherited separately, how @DefaultQualifiers interacts, and whether diagnostics distinguish inherited annotations; the issue is done when these design questions have an agreed implementation and validation.