Package `@DefaultQualifier` overrides class `@DefaultQualifier`

[vlsi]

Sample:

package-info.java

@DefaultQualifier(value = NonNull.class, locations = TypeUseLocation.FIELD)
@DefaultQualifier(value = NonNull.class, locations = TypeUseLocation.PARAMETER)
@DefaultQualifier(value = NonNull.class, locations = TypeUseLocation.RETURN)
package org.apache.calcite.util;

import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.framework.qual.DefaultQualifier;
import org.checkerframework.framework.qual.TypeUseLocation;

Glossary.java

package org.apache.calcite.util;

import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.framework.qual.DefaultQualifier;
import org.checkerframework.framework.qual.TypeUseLocation;

@DefaultQualifier(
    value = Nullable.class,
    locations = TypeUseLocation.ALL
)
public interface Glossary {
  Glossary PATTERN = null;
  Glossary SQL2003 = null;
}

Error:

core/src/main/java/org/apache/calcite/util/Glossary.java:331: error: [assignment.type.incompatible] incompatible types in assignment.
  Glossary PATTERN = null;
                     ^
  found   : null
  required: @Initialized @NonNull Glossary

[smillst]

Here's a single file test case.

import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.framework.qual.DefaultQualifier;
import org.checkerframework.framework.qual.TypeUseLocation;

@DefaultQualifier(value = NonNull.class, locations = TypeUseLocation.FIELD)
@DefaultQualifier(value = NonNull.class, locations = TypeUseLocation.PARAMETER)
@DefaultQualifier(value = NonNull.class, locations = TypeUseLocation.RETURN)
public class Glossary {

    // :: error: (assignment.type.incompatible)
    Glossary PATTERN = null;

    @DefaultQualifier(value = Nullable.class, locations = TypeUseLocation.ALL)
    class Inner {
        Glossary SQL2003 = null;
    }
}

[cpovirk]

Coincidentally, I was just looking at this code. I am suspicious of this line: https://github.com/typetools/checker-framework/blob/874073fb9bf41a6d7f37116e63293653d8e8dd09/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java#L631

It looks to me like the higher priority (based on TypeUseLocation order) annotations from the enclosing element get added to the set of the child element, where they then take priority over ALL. Perhaps setting ALL on an element should prevent the earlier values from being added. Arguably even setting OTHERWISE should do that.

In fact, arguably defaulting should be more sophisticated still: Maybe I should be able to set EXPLICIT_UPPER_BOUND on a child element and have that override an existing UPPER_BOUND on the enclosing element, even though UPPER_BOUND has a higher priority. That is, maybe the child DefaultSet should never take on elements from the enclosing element's. Instead, maybe we should apply all the child-specific rules first and then apply all the rules on the enclosing types, working from the in out. That may be slower, though, and there are probably subtleties to this that I haven't understood yet.

A lot of this hinges on the precise meaning of:

If multiple DefaultQualifier annotations are in scope, the innermost one takes precedence.

[cpovirk]

(Huh, I wonder if even a default of FOO on a child necessarily wins over a default of FOO on an enclosing element. It seems as if both may get added to the DefaultSet, and the conflict may be resolved in favor of whichever default wins the AnnotationUtils.compareAnnotationMirrors comparison?)

[iMacTia]

Just bumped into this bug myself, surprised it hasn't been reported more often

[vlsi]

@iMacTia , It's probably time to migrate to jspecify nullability annotations, so I am not sure @DefaultQualifier issue is still important.

[iMacTia]

First time I hear about that standard, thank you for the pointer! Skimming through the linked website, I don't see an equivalent for @DefaultQualifier though that I could apply to the package (only @Nullable and @NonNull)

[vlsi]

@iMacTia , see @NullMarked, preferably at the package level: https://jspecify.dev/docs/applying/#2-add-nullmarked

Note: you have to duplicate @NullMarked for every individual package. jspecify does not have "once for all the subpackages" approach. The details and the reasoning are here: https://github.com/jspecify/jspecify/issues/745#issuecomment-2917589086

It would be great to have some tooling to detect "missing @NullMarked packages" though. @cpovirk , is there an option in checkerframework that would fail on a package that misses @NullMarked annotation?

---

For reference, Guava has switched to JSpecify in https://github.com/google/guava/pull/7572 JUnit, Spring Framework, Spring Boot are coming.

So it definitely is a time to move

---

I wonder if the issue should be closed as "not planned"

[iMacTia]

Thank you again for the insight @vlsi 🙇 My only concern is that what you state above doesn't match the documentation

The Checker Framework understands @Nullable and @NonNull, but not @NullMarked or @NullUnmarked.

Is that just a matter of the documentation being outdated? Can I use @NullMarked with Checker Framework as you suggested? Do I need a minimum version of CF maybe?

[vlsi]

Oh, I somehow assumed Checker Framework understood jspecify annotations.

Then it looks like the way to go could be going for jspecify's @Nullable + @NullMarked, add a top-level checkerframework's @DefaultQualifier, and use the CF to validate the annotations. Of course, the reference checker might be an option, however is not intended for production sounds sad.

It would enable proper verifications (including generics, multi-dimensional arrays) at a cost of having checker-qual.jar on the classpath.

[mernst]

@iMacTia I'm sorry you ran into this bug. We would like to fix it, but it hasn't been reported often. If you can contribute a pull request, that would be greatly appreciated. Otherwise, we will get to it when we have time.

The suggestion to switch to JSpecify is inappropriate for many users. The JSpecify specification is much weaker than what the Nullness Checker supports, so you will have to mix JSpecify annotations and Nullness Checker annotations. Users may find it easier to use just one set of annotations rather than mixing two. And, all checkers recognize the common JSpecify and Nullness Checker type annotations, so there is no tooling reason to prefer one over the other.