Intersection types: explicit annotations and defaults on/for bounds

[aosen-xiong]

This is the finding when I do #1434.

For explicitly annotated intersection types, CF choose the primary annotation for the intersection from the first bound in the qualifier hierarchy, rather than computing a semantically meaningful qualifier such as the GLB of the bound annotations.

This makes diagnostics order-sensitive. In the Tainting Checker, @Untainted <: @Tainted, so it is surprising that:

(@Tainted Object & @Untainted I)

is treated as:

@Tainted Object & @Tainted I

and the explicit @Untainted annotation is reported as ignored.

Minimal Test Case

import org.checkerframework.checker.tainting.qual.Tainted;
import org.checkerframework.checker.tainting.qual.Untainted;

class TaintedIntersectionOrder {
    interface I {}

    void firstBoundTainted() {
        @Untainted Object x = (@Tainted Object & @Untainted I) null;
    }

    void firstBoundUntainted() {
        @Untainted Object x = (@Untainted Object & @Tainted I) null;
    }
}

Command

./checker/bin/javac \
  -processor org.checkerframework.checker.tainting.TaintingChecker \
  TaintedIntersectionOrder.java

Actual Output

TaintedIntersectionOrder.java:9: error: [assignment.type.incompatible] incompatible types in assignment.
        @Untainted Object x = (@Tainted Object & @Untainted I) null;
                              ^
  found   : @Tainted Object & @Tainted I
  required: @Untainted Object
TaintedIntersectionOrder.java:9: warning: [explicit.annotation.ignored] The qualifier @Untainted is ignored in favor of @Tainted. Either delete @Untainted or change it to @Tainted.
        @Untainted Object x = (@Tainted Object & @Untainted I) null;
                                                 ^
TaintedIntersectionOrder.java:14: warning: [explicit.annotation.ignored] The qualifier @Tainted is ignored in favor of @Untainted. Either delete @Tainted or change it to @Untainted.
        @Untainted Object x = (@Untainted Object & @Tainted I) null;
                                                   ^
1 error
2 warnings

Expected / Question
Is this intended behavior? If the intersection combines annotations from multiple bounds in the same hierarchy, should the primary annotation be computed using the qualifier hierarchy instead of depending on the first bound?

For Tainting, it seems like @Untainted Object & @Tainted I and @Tainted Object & @Untainted I should not produce opposite “ignored annotation” choices solely due to bound order.

How should this behave for hierarchies like PICO or viewpoint test checker, for example, @Immutable Object & @Mutable SomeInterface? If the qualifiers' GLB is bottom, should the Checker Framework reject the intersection type as uninhabitable, or is there a use case where such an intersection should remain expressible with a warning?

[cpovirk]

(For what it's worth, I've always found this a bit odd, too. In the JSpecify specification, we declare that each element of the intersection type has its own qualifier. We're lucky that we don't need to worry about questions like @Immutable & @Mutable there.)

[wmdietl]

This is the intended behavior. The two warnings are important and maybe we should reword them or make them errors.

It is not that order matters. We want only one annotation on the intersection type. We only take that first (explicit or defaulted) annotation and issue warnings if there are different explicit annotations on the other bounds.

The JSpecify model is what Java type use annotations allow. However, it is confusing: when I have an @Nullable IA & @NonNull IB bound, can I pass null or not? This is particularly annoying in a @NullMarked scope, where I'm forced to write @Nullable IA & @Nullable IB, repeating the @Nullable on both bounds, if I want to allow null values.

For a more complex lattice, computing the GLB would change the effective type further, making the code and resulting error messages harder to read.

The CF model only wants at most one annotation on the first bound. The other bounds are defaulted to that annotation, contrary to the usual defaults. Hopefully this reduces how many annotations have to be written and makes the code easier to read. This model does not complain about repeat @Nullable IA & @Nullable IB. No warning is issued for @Nullable IA & IB but the interpretation is different between the CF and JSpecify.

Given that JSpecify went the fine-grained route, we should revisit whether we still like the CF model.
We could:

• Keep things how they are.
• Change warnings to errors to enforce a single explicit annotation.
• Figure out a way to warn when the interpretation is different between the two models and suggest a fix. In JSpecify, instead of @Nullable IA & IB it is much clearer to simply write IA & IB. However, this still leaves the ambiguity between the two models.
• Allow explicit annotations on each bound, like in JSpecify, and issue a warning if the GLB of the bounds is different from the annotation/default on a bound.
• Any other options?

@cpovirk Please chime, especially with any positive points for the JSpecify model.

[cpovirk]

On the bright side, I'd expect @Nullable Foo & [@Nullable] Bar to be rare enough that we don't need to be too worried about it :) The only case I can recall is this one, which is the way it is only because it was part of the process of pulling a variant of the erasure trick seen in Collections.max/min.

Also, to get this out of my system: I occasionally think to myself "But what you want to write <U extends T & @Nullable SomeInterface>?" Then you would "need" to be able to annotate only SomeInterface without also annotating T¹.Then I remember that Java doesn't let you write T & SomeInterface to begin with :) So, if you have multiple bounds, they're necessarily classes/interfaces, and I agree that there's never a reason for you to give them different nullnesses.

Anyway, I see the JSpecify approach as being about the simplicity of the model: Especially for something that comes up this rarely, it's nice for our explanation of @NullMarked not to need to include another "exception" for intersection types. That's probably also slightly nicer for implementers in the nullness case. (I wouldn't normally put much stock in that, but again, for something that comes up so rarely, we might give relatively more weight to implementers vs. end users than usual.) Again, the non-nullness case is a different story, as you've explained.

One other point: In nullness discussions lately, I have been trying to look ahead more to a future in which we have nullness markers in Java. In that case, I would expect to be required to write IA? & IB?. Maybe part of the reason for that is that's it's easy to read @Nullable IA & IB as @Nullable (IA & IB), whereas it's harder to read IA? & IB as applying the ? to both. (I guess we could argue for IA & IB? so that you could at least read it as (IA & IB)?!)

Footnotes

1. Or maybe SomeInterface would default to nullable if T is declared as <T extends @Nullable Object>, and then anyone who doesn't want that would have to explicitly write @NonNull T & SomeInterface? ↩

[wmdietl]

Thanks for your comments, @cpovirk !

I suggest we keep the current model and see whether it will lead to any confusions. I agree this is likely a rare use case.

@aosen-xiong for #1434 use a simple intersection type with just one annotation and leave a comment to expand if we change our mind.