Overriding methods should inherit annotations

[GoogleCodeExporter]

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.

Let's have 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) {...}
}

We might now get errors for three reasons:
- we override a method with an incompatible declaration annotation, if
@DefaultDA and @DA are incompatible. For example, if Super.foo is
declared @Pure, also the overriding method must be pure.
(See e.g. Issue 271.)

- the defaulted return type might be incompatible, 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.

- the defaulted parameter type might be incompatible, 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, 
e.g. it would be interpreted as:

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

and the programmer doesn't have any annotation effort (but 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

• Blocking: #334

[GoogleCodeExporter]

Issue 333 has been merged into this issue.

Original comment by wdi...@gmail.com on 27 May 2014 at 3:55

[GoogleCodeExporter]

Original comment by michael.ernst@gmail.com on 1 Jun 2014 at 1:16

• Now blocking: #334