Need a way to selectively make an effect the default on all overrides

Currently, if a method is marked @UIEffect (explicitly or implicitly via @UIPackage or @UIType) the GUI Effect Checker makes this the default effect on overrides only for anonymous inner classes, not for overrides in named subclasses. In some large codebases, this means lots of repetition on such subtypes. We need a way to reduce this burden by making the annotations on overrides default to the effect of the original definition.

There are several possible approaches:

• Adding an @InheritedUIEffect
• Adding an optional boolean parameter for whether the annotation is inherited to the existing UIEffect annotation. If it defaults to false it's fully backwards-compatible, but either stub files or implementations could be marked @UIEffect(inherited = true) and this would give the desired behavior (which could still be overridden with a SafeEffect annotation)
• A global flag to make all UI effects inherited by default (probably unsound when linked with code checked without this)

The middle option is appealing for the fact that it separates two related but actually distinct pieces of information, allowing this with fine granularity:

// Implicitly, this inherited flag is overloading the annotation to provide
// two closely related but distinct pieces of information:
// 1. What's the effect of the methods in the class?
// 2. What's the default effect of *overrides* of those members?
// As a design principle, specifying them together makes sense (as opposed
// to adding another annotation to specify that a method's effect should be
// the default for overrides)
@UIEffect(inherited = true)
public interface Foo {
  public void m(); // UIEffect
}
public class Bar implements Foo {
  @Override
  public void m() { ... } // implicitly UIEffect due to inheritance flag
}

Jo D has suggested making it possible to do this for all methods in a class or all methods in a package. This could be done with similar flags for @UIPackage and @UIType, and/or by overloading @UIEffect to apply to classes and packages as well (which has the added benefit of reducing the number of annotations develops must remember).