Check that inference for annotations on Class declarations is implemented correctly

From: Jonathan Burke

Hi Everyone,

Did we have a final decision as to what annotations on the class declaration mean? Is it just that all types must be below the declaration? Currently, I think declaration annotation just get added to any instance of the type. Should it just act like a bound?

It looks like the manual was update since we last asked this question. Here is what the manual says:

Writing an annotation on a class declaration makes that annotation implicit for all uses of the class (see Section 25.3). If you write class @MyQual MyClass { ... }, then every unannotated use of MyClass is@MyQual MyClass. A user is permitted to strengthen the type by writing a more restrictive annotation on a use of MyClass, such as @MyMoreRestrictiveQual MyClass.

So it seems that for inference, to handle this correctly we could treat it like a parametric (non-defaultable) type and infer whether or not it exists. Does that seem reasonable?

Jonathan

From: Michael Ernst

Right, that sounds right. The annotation being missing is different than it being present.

Thanks!

-Mike

From: Werner Dietl

Hi Jonathan,

I'm not quite sure what you mean with "infer whether or not it exists". The annotations on a class declaration (let's not call it a declaration annotation as that is a broader concept) has two meanings:

if a particular class is annotated, that annotation is implicit for all uses of the class, overriding the usual default; it is also an upper bound for possible type uses: only more restrictive qualifiers can be used explicitly.

if no annotation is given on a particular class, we still have an implicit annotation on the class declaration, per the discussion at

https://groups.google.com/d/msg/checker-framework-dev/vk2V6ZFKPLk/v3hENw-e7gsJ

"Default annotations on type declarations". This default is then used as an upper bound for all uses of the type, but it is not used implicitly for those uses. That is, the normal default is used for uses of the class, but that default still has to be more restrictive than the default on type declarations.

At least that's how the Checker Framework behaves at the moment. For inference this means that there is always a subtype constraint between the annotation on a type use and the (implicit or explicit) annotation on the type declaration. If there is an explicit annotation on the type declaration, inference doesn't need to change - but when determining whether the inferred result is equal to the default, the annotation on the declaration needs to be considered.

Does this agree with how you interpret this?

cu, WMD.

From: Jonathan Burke

Hi Werner,

I believe that does match what I was intending to implement. I'll take a closer look.

Jonathan

typetools / checker-framework-inference

Check that inference for annotations on Class declarations is implemented correctly #11