[Checkers] Annotation defaults and declarative specification of type hierarchy

[Michael Ernst]

Mahmood-

I see that I can call QualifierDefaults.setAbsoluteDefaults to set the
default annotation for a checker.  It might be nice to permit a type system
designer to write a meta-annotation to specify this.

In particular, I would like to have the following type hierarchy:

             @PrototypeOrNot
            /               \
      (no qualifier)     @Prototype

Furthermore, I would like to avoid writing code.  (This is a mixture of
laziness and trying to understand the limits of specifying a type checker
declaratively.  I really think that users will be afraid of writing code.)

I think I can't do the above (without writing code), but I should be able
to use this type hierarchy

             @PrototypeOrNot
            /               \
      @NonPrototype     @Prototype

and make @NonPrototype the default, like so:

@TypeQualifier
@SubtypeOf(PrototypeOrNot.class)
public @interface Prototype {}

@TypeQualifier
@SubtypeOf(PrototypeOrNot.class)
public @interface NonPrototype {}

@TypeQualifier
@SubtypeOf()
public @interface PrototypeOrNot {}

To make @NonPrototype the default, I would write a meta-annotation somewhat
like @DefaultQualifier.  The meta-annotation really belongs on the checker
itself (or on the command line that invokes the Basic Checker?) but could
perhaps go on @NonPrototype.

What do you think of this?


(Or should I just write the code?)


(Speculation alert:  I wonder if it would be useful to have a @DisjointFrom
annotation as well as a @SubtypeOf annotation.  I really wanted to write
just

@TypeQualifier
@DisjointFrom(Unqualified.class)
public @interface Prototype {}

until I found the ugly usages that required @PrototypeOrNot.  It was just
those usages that made Jeff say that we couldn't just refactor the code
trivially.  Once I get the code fully annotated, then I will be able to
better understand whether we can eliminate @PrototypeOrNot; and if we can,
then we can perhaps eliminate prototype invariants from Daikon.)

I wonder whether this disjointness condition will be a common use case for
the Checker Framework.  If so, we should support it.)

                    -Mike