Is Arbitrary<@Nullable T> correct/intended under JSpecify semantics?

[lcahmu]

Testing Problem

I assume that the intent of interface Arbitrary<@Nullable T> is to say that T could be a type that allows nulls, but a T that is @NonNull (whether explicitly or implicitly) is also acceptable. I assume this because classes like IntegerArbitrary ultimately extend Arbitrary<Integer>, where Integer is implicitly @NonNull. Also because Arbitrary.injectNull(..) explicitly adds @Nullable to the response type, which is redundant if T is already @Nullable, so there appears to be some expectation that it might not be.

I see that it's the JSpecify flavor of @Nullable that's being used here. I haven't used JSpecify myself so I could easily be misreading it, but some of its project discussions, such as this one and its documentation on "Other TYPE_USE annotation targets", seem to be saying that <@Nullable T> doesn't mean anything to JSpecify.

If it doesn't mean anything, then this seems harmless at first glance. I stumbled across this minor discrepancy in a project that's trying to use both JQwik and CheckerFramework. This combination worked just fine until I tried to update from JQwik 1.7 to 1.8, which is when the @Nullable annotations were introduced. Now, obviously, CheckerFramework is not JSpecify. It has it's own @Nullable annotations. But their semantics are close enough that ChekerFramework also accepts JSpecify's annotations in addition to its own. Close, but not exact: the relevant difference between the two is that while <@Nullable T> doesn't mean anything to JSpecify, it does mean something to CheckerFramework. Specifically, it means that T must allow nulls, which means that it will not accept the following:

Arbitrary<Integer> ints = Arbitraries.integers();  // error: [type.argument] incompatible type argument for parameter T of Arbitrary

CheckerFramework doesn't like this because Arbitraries.integers() returns an IntegerArbitrary, which, as noted above, ultimately extends Arbitrary<@NonNull Integer>. And since @NonNull Integer does not allow null, that violates the <@Nullable T> constraint that requires it to, so Checker rejects this assignment for having incompatible types. But since that very line appears more than once in the JQwik user guide, I have to assume that's intended to work.

Arbitrary was the first place I noticed this, but methods of Arbitraries, Combinators, and some other classes extending from Arbitrary also have similar @Nullable Ts in their type parameters.

Suggested Solution

The same JSpecify discussion linked above, and also its user guide, suggest that Arbitrary<T extends @Nullable Object> would correctly express the semantics that I assume were intended. It's also compatible with CheckerFramework, resolving the error that's currently produced by the one-line example above. I've been able to confirm this with CheckerFramework stubs. Stubbing also provides a workaround, even if a somewhat inconvenient one.

Discussion

Although it's CheckerFramework that motivates me here personally, compatibility has not been promised or even suggested anywhere, so I understand if it's not convincing. I would instead focus on the (lack of) meaning under JSpecify's own semantics, and treat any benefit toward CheckerFramework users as purely coincidental.

I also saw that nullability annotations were originally added for Kotlin compatibility. I have no idea how Kotlin would treat <T extends @Nullable Object>. If Kotlin doesn't read it in a way that's consistent with JSpecify's semantics and it came down to having to make a choice on which to support, I'd absolutely understand prioritizing Kotlin.

[jlink]

@lcahmu Thanks for writing up the details of this problem. The nullability annotations were initially introduced to improve type inference on the Kotlin side. So I've never really thought deeply about what the JSpecify (or JSR305 or jetbrains.* or Checker) annotations want to express. :-/

That said, the goal should be to make it work with both CheckerFramework and Kotlin. This gets more complicated with Kotlin 2.0, which no longer supports JSR 305. That's why jqwik 1.9.0 will get rid of the remaining JSR305 annotation. In fact 1.9.0-SNAPSHOT already has and I'd like you to try if you see the same problems with it that you've seen with 1.8.x. If that's the case, I'm happy to try out the T extends @Nullable Object suggestion and see if it is compatible with Kotlin 2.0.

[lcahmu]

Thanks @jlink! I was able to try the snapshot, but unfortunately I do still see the same errors.

[jlink]

Thanks @jlink! I was able to try the snapshot, but unfortunately I do still see the same errors.

Thanks. I'll try the suggested approach then. Hopefully in the days to come.

[jlink]

Sadly, Arbitrary<T extends @Nullable Object> is rejected by the compiler. I tried both Java 8 and 21; they fail with different error messages, but they both fail.

Arbitrary<? extends @Nullable T> seems to be possible, but I'd assume that suffers from the same problem as Arbitrary<@Nullable T> since a nullable annotation on a type variable does not have a meaning for JSpecify.

[jlink]

@jibidus Is there a workaround for your situation? Like disabling CheckerFramework errors through comments or annotations?

[lcahmu]

Do you mean the Kotlin compiler? It's definitely legal Java on the class/interface declaration. I'll see if I can reproduce the error.

[vlsi]

Sadly, Arbitrary<T extends @Nullable Object> is rejected by the compiler. I tried both Java 8 and 21; they fail with different error messages, but they both fail.

What is the exact error message?

[vlsi]

% git log -1
commit 679109f38cc2151b5eb9fdf7d0b4c74c8bf47f14 (HEAD -> main, origin/main, origin/HEAD)
Author: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Date:   Mon Jun 3 07:50:47 2024 +0000

    Bump com.google.errorprone:error_prone_annotations from 2.27.1 to 2.28.0

% git diff
diff --git a/api/src/main/java/net/jqwik/api/Arbitrary.java b/api/src/main/java/net/jqwik/api/Arbitrary.java
index f76f8c7b4..baa91c28e 100644
--- a/api/src/main/java/net/jqwik/api/Arbitrary.java
+++ b/api/src/main/java/net/jqwik/api/Arbitrary.java
@@ -20,7 +20,7 @@ import static org.apiguardian.api.API.Status.*;
  */
 @API(status = STABLE, since = "1.0")
 @CheckReturnValue
-public interface Arbitrary<@Nullable T> {
+public interface Arbitrary<T extends @Nullable Object> {

        @API(status = INTERNAL)
        abstract class ArbitraryFacade {

% ./gradlew jar
....
BUILD SUCCESSFUL in 28s

[lcahmu]

Like vlsi, I wasn't able to reproduce a compiler error. And the good news is that Kotlin does seem to understand <T extends @Nullable Object>, at least in some pretty surface-level experiments. The bad news is that this might be more sweeping than I'd thought: nearly every <T> throughout the codebase might need to be assessed. If the goal was just to address some Kotlin warnings that have already been addressed by <@Nullable T>, whatever JSpecify's intended semantics, then it might not be worthwhile. Inconvenient for me, but if I'm the only one running into this, I can deal.

There are a couple of possible workarounds for Checker. It is possible to disable checks in a limited scope with @SuppressWarnings annotations. It's also possible to provide Checker with one of a few different flavors of stub files to tell it what annotations it should use for any libraries that haven't provided their own. This works when it works, though I've personally found them to be a little tricky to maintain.

[vlsi]

IntelliJ IDEA produces warnings for <@Nullable T>, so it yet another motivation for the change.

[vlsi]

See https://errorprone.info/bugpattern/NullableTypeParameter

[jlink]

Like vlsi, I wasn't able to reproduce a compiler error.

Well, I tried a different thing:

public interface Arbitrary...
    default Arbitrary<T extends @Nullable Object> injectNull(double nullProbability) {
        return ArbitraryFacade.implementation.injectNull(Arbitrary.this, nullProbability);
    }

When going with

public interface Arbitrary<T extends @Nullable Object> {...}

How would the signature of injectNull look like?

injectNull is one of those places where Kotlin can differentiate between nullable and non-nullable, e.g.

var strings: Arbitrary<String> = String.any()
var nullableStrings: Arbitrary<String?> = String.any().injectNull(0.1)

Leaving out the ? for nullableStrings results in a type mismatch warning. I'd really love to keep this behaviour.

[jlink]

IntelliJ IDEA produces warnings for <@Nullable T>, so it yet another motivation for the change.

Interestingly, the warning appears here:

public interface Arbitrary<@Nullable T> { ... }

but not here:

default Arbitrary<@Nullable T> injectNull(double nullProbability) { ... }

[vlsi]

@jlink , the difference is as follows:

// Here `T` declares a **type variable**, so `@Nullable T` stands for "annotated type variable"
public interface Arbitrary<@Nullable T> {
    // Here `T` stands for a type, so `@Nullable T` stands for an "annotated type"
    default Arbitrary<@Nullable T> injectNull(double nullProbability) { ... }
}

Does it make sense?

---

How would the signature of injectNull look like?

// It means "it is allowable to implement Arbitrary when T is nullable and non-nullable"
public interface Arbitrary<T extends @Nullable Object> {
    // No matter which was T at the declaration time, injectNull always returns a null-producing Arbitrary
    default Arbitrary<@Nullable T> injectNull(double nullProbability)
}

---

Leaving out the ? for nullableStrings results in a type mismatch warning. I'd really love to keep this behaviour

Could you clarify why would you want to have the following? Sure injectNull returns an Arbitrary that might eventually produce null value. That means the users should be prepared to handle null values, so they should declare the type as Arbitrary<String?> rather than Arbitrary<String>.

val nullableStrings: Arbitrary<String> = String.any().injectNull(0.1)

[jlink]

Could you clarify why would you want to have the following? Sure injectNull returns an Arbitrary that might eventually produce null value. That means the users should be prepared to handle null values, so they should declare the type as Arbitrary<String?> rather than Arbitrary<String>.

val nullableStrings: Arbitrary<String> = String.any().injectNull(0.1)

Actually, I don't want it. It should be prevented by the time system - or at least get a warning as it is now. If I understand @lcahmu correctly,

default Arbitrary<@Nullable T> injectNull(double nullProbability)

does not work in the presence of CheckerFramework, but I might have misunderstood.

[vlsi]

@jlink , lcahmu mentions interface declarations, so they suggest patches like https://github.com/jqwik-team/jqwik/issues/575#issuecomment-2150674504

[vlsi]

By the way, it looks like "-Xnullability-annotations=@org.jspecify.annotations:strict" compiler option enables to surface nullability annotations mismatch at the build time.

[vlsi]

@jlink , here's a draft PR: https://github.com/jqwik-team/jqwik/pull/576

[lcahmu]

Just as @vlsi says. I believe it's generally anywhere type variables are declared, so:

public interface Arbitrary<T extends @Nullable Object> { ... }

but also things like:

default <U extends @Nullable Object> Arbitrary<U> map(Function<T, U> mapper) { ... }

The injectNull case isn't declaring a type variable and is already understood correctly by Checker as-is.

[jlink]

So I misunderstood. Good. Simplifies the solution.

[jlink]

The current solution (including @vlsi's pull request) has been published as 1.9.0-SNAPSHOT.

I'll probably clarify nullability and type variance issues in a few places, but it should hopefully work with CheckerFramework, @lcahmu. Maybe you can verify.

[lcahmu]

Looks good on a first pass! Checker is happy in my project at least, everything is compiling -- though obviously that doesn't necessarily generalize. I am getting some runtime failures, but right now I'm suspecting that's just from other changes between 1.7 and 1.8 that I haven't corrected for yet, probably not anything to do with these annotation updates. (JQwik isn't looking at these annotations when trying to match types, right?) I'll continue working through that and report back in the unlikely event that I find something, but for now... works on my machine!

[lcahmu]

Okay, I did run into a case where I can't tell whether or not it's an expected change from 1.7 to 1.8.

Consider a scenario with a wrapper class and a provider for it, and a property that holds only for a subset of values. The following works on all of 1.7.4, 1.8.5, and 1.9.0-SNAPSHOT (3db8e5f):

@Domain(WrapperProvider.class)
@Domain(DomainContext.Global.class)
public class GenericTest {
    public record Wrapper<T>(T value) { }

    @Property
    public <T> void property(@ForAll("reduced") Wrapper<T> wrapper) { }

    @Provide("reduced")
    public <T> Arbitrary<Wrapper<T>> provider(@ForAll Wrapper<T> wrapper) {
        return Arbitraries.just(wrapper);  // A real project would do something more substantial here, maybe filter()
    }

    // This would be at a higher level in a real project. Adapted from
    // https://jqwik.net/docs/1.8.5/user-guide.html#arbitrary-providers-for-parameterized-types
    public static class WrapperProvider extends DomainContextBase implements ArbitraryProvider {
        @Override
        public boolean canProvideFor(TypeUsage targetType) {
            return targetType.isOfType(Wrapper.class);
        }

        @Override
        public Set<Arbitrary<?>> provideFor(TypeUsage targetType, SubtypeProvider subtypeProvider) {
            TypeUsage t = targetType.getTypeArgument(0);
            return subtypeProvider.apply(t)
                    .stream()
                    .map((Arbitrary<?> arbitrary) -> arbitrary.map(Wrapper::new))
                    .collect(Collectors.toSet());
        }
    }
}

Changing the <T>s to <T extends @Nullable Object> works with 1.7.4 but breaks 1.8.5 and the current 1.9.0-SNAPSHOT.

-   public record Wrapper<T>(T value) { }
+   public record Wrapper<T extends @Nullable Object>(T value) { }

    @Property
-   public <T> void property(@ForAll("reduced") Wrapper<T> wrapper) { }
+   public <T extends @Nullable Object> void property(@ForAll("reduced") Wrapper<T> wrapper) { }

    @Provide("reduced")
-   public <T> Arbitrary<Wrapper<T>> provider(@ForAll Wrapper<T> wrapper) {
+   public <T extends @Nullable Object> Arbitrary<Wrapper<T>> provider(@ForAll Wrapper<T> wrapper) {
        return Arbitraries.just(wrapper);
    }

Cannot find an Arbitrary [reduced] for Parameter of type [@net.jqwik.api.ForAll(value="reduced", supplier=net.jqwik.api.ArbitrarySupplier.NONE.class) Wrapper<T>]

It does seem to be the annotation itself having some effect here. The error does not occur with <T extends Object> (other than IntelliJ complaining about it being redundant). But any annotation at all, not just nullability ones, will seem to cause the error:

public class GenericTest {
+   @Retention(RetentionPolicy.RUNTIME)
+   @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+   public @interface Dummy { }
+   
-   public record Wrapper<T>(T value) { }
+   public record Wrapper<T extends @Dummy Object>(T value) { }

    @Property
-   public <T> void property(@ForAll("reduced") Wrapper<T> wrapper) { }
+   public <T extends @Dummy Object> void property(@ForAll("reduced") Wrapper<T> wrapper) { }

    @Provide("reduced")
-   public <T> Arbitrary<Wrapper<T>> provider(@ForAll Wrapper<T> wrapper) {
+   public <T extends @Dummy Object> Arbitrary<Wrapper<T>> provider(@ForAll Wrapper<T> wrapper) {
        return Arbitraries.just(wrapper);
    }

Cannot find an Arbitrary [reduced] for Parameter of type [@net.jqwik.api.ForAll(value="reduced", supplier=net.jqwik.api.ArbitrarySupplier.NONE.class) Wrapper<T>]

[jlink]

@lcahmu Thanks for the example.

In general @Nullable (or other annotations) are not considered for type matching in jqwik.

Using T extends String also seems to work and correctly restricts the type. It looks like the annotation in the provider method's return type somehow breaks the matching algorithm. Looks like a bug. Hope I'll later today find the time to dive deeper.

[jlink]

@lcahmu It was a bug indeed, which I hopefully fixed in https://github.com/jqwik-team/jqwik/commit/4d419a3c97270ec4da80bb5a009e61d5ebc62522 The most recent snapshot deployment contains the fix.

[lcahmu]

Thanks @jlink that did seem to move things forward a bit. I've run into another possible issue that's blocking me from testing further, but it doesn't look directly related to nullability or annotations so I'll file that separately (#580).

Edit: I found a workaround while shrinking the issue to a simpler example to include with the issue. That has allowed me to continue testing.

[jlink]

Even with the current changes I get unexpected (for me) compiler warnings.

E.g.:

fun test() {
    val v1: Arbitrary<String?> = Arbitraries.just("1")
    val v2: Arbitrary<String?> = Arbitraries.just(null)

    // Compiler warning in IntelliJ for both assignments:
    // Type mismatch.
    //   Required: Arbitrary<String?>
    //   Found: Arbitrary<String>
}

This happens despite Arbitraries.just(..) having this interface definition:

public class Arbitraries...
    public static <T extends @Nullable Object> Arbitrary<T> just(T value) {
        return ArbitrariesFacade.implementation.just(value);
    }

Am I missing something or is IntelliJ's tooling just not working correctly with the @Nullable annotation?

[lcahmu]

Can now confirm that, at least in my project, everything seems to be working as expected now. Thanks so much for looking into these issues!

Not sure what's going on there with Kotlin though. I'm not sure if I'm missing some compiler settings somewhere (Kotlin isn't my day-to-day) but I'm not seeing those warnings. Instead, I'm seeing something else just as confusing/concerning though: I'm not seeing a warning where I would expect one: val v: Arbitrary<String> = Arbitraries.just(null)

I do see those same warnings if I change it back to <T> Arbitrary<T> just(T value) though.

[jlink]

The compiler option you need is: -Xnullability-annotations=@org.jspecify.annotations:strict

[jlink]

I tend to close this issue - and maybe open another one to tackle the confusing Kotlin type warnings.

[vlsi]

Am I missing something or is IntelliJ's tooling just not working correctly with the @Nullable annotation?

I guess IDEA's Kotlin plugin does not handle extends @Nullable ... yet. They might go for strict jspecify in Kotlin 2.1, and IDEA migrates to Kotlin frontend so soon IDE would produce the same warnings as the compiler.

[jlink]

Closing as fixed. @lcahmu Feel free to reopen if anything is missing.