Kotlin190

[jlink]

Overview

Make jqwik kotlin module work with Kotlin 1.9.0

The problems are mostly about arbitrary types. While the Java implementation does not differentiate between nullable and non-nullable types, the Kotlin compiler assumes that they are non-nullable and deferes T & Any whereas the Kotlin functions use just T since the incoming arbitraries (or functions or whatever) could be nullable or non-nullable.

Problem

How to handle this type mismatch correctly?

---

I hereby agree to the terms of the jqwik Contributor Agreement.

[jlink]

@vlsi You seem to be knowledgeable about Kotlin's type system. At least more knowledgeable than I am.

Do you have a suggestion on how to solve this problem?

[vlsi]

The case is as follows: 1) jqwik adds "all types are not null by default".

@NonNullApi
package net.jqwik.api;

2) For example, the following Java code

public interface Arbitrary<T> {

effectively means

public interface Arbitrary<@NotNull T> {

3) I believe it expands to type parameters in java methods.

In other words, @NotNull makes no real difference here:

    public interface Combinator2<T1, T2> {
// I believe @NotNull is not needed as "R" is not nullable because there's package-level NotNullApi
        <R> Arbitrary<R> as(F2<T1, T2, @NotNull R> combinator);

---

At the same time, in Kotlin, type variables are nullable by default.

In other words, the following Kotlin declaration means T1, T2, and R could be nullable.

fun <T1, T2, R> combine(
    a1: Arbitrary<T1>,
    a2: Arbitrary<T2>,
    filter: ((T1, T2) -> Boolean)? = null,
    combinator: (v1: T1, v2: T2) -> R
): Arbitrary<R> = if (filter == null) {
    Combinators.combine(a1, a2).`as`(combinator)
}

That is why Arbitrary<nullable T1> is not compatible with jqwik's Arbitrary which requires its type parameter to be not-nullable.

---

So the solution depends on your intention for interface Arbitrary<T>. Do you expect that Arbitrary must always use non-nullable type parameter? In that case the following would work:

// T1: Any means "T1 is non-nullable"
fun <T1: Any, T2: Any, R: Any> combine(
    a1: Arbitrary<T1>,
    a2: Arbitrary<T2>,
    filter: ((T1, T2) -> Boolean)? = null,
    combinator: (v1: T1, v2: T2) -> R
): Arbitrary<R> = if (filter == null) {
    Combinators.combine(a1, a2).`as`(combinator)
}

Does that make sense?

[jlink]

So the solution depends on your intention for interface Arbitrary<T>. Do you expect that Arbitrary must always use non-nullable type parameter?

In most cases - one exception is injectNull(..) - Arbitrary<T> refers to either a nullable or non-nullable type and the result should have the same constraint.

I just noticed that removing

"-Xjsr305=strict", // For strict type warnings
"-Xjsr305=under-migration:strict",

from compiler options will allow me to leave the Kotlin code as is. I'm not sure though, how much type-safety I'm gonna lose on the Kotlin side then.

[vlsi]

At the same time, sometimes you have @NotNull which implies you expect that sometimes the same things might be nullable.

For instance:

<R> Arbitrary<R> as(F2<T1, T2, @NotNull R> combinator);

It suggests that "sometimes the third type parameter of F2 might be nullable". However, the current package-level @NotNullApi implies that all type parameters must be NOT null.

In other words, you might want replace

public interface F2<T1, T2, R> {

with

// org.jspecify:jspecify:0.3.0
import org.jspecify.annotations.Nullable;

// Allow T1, T2, R to be nullable depending on the actual usage sites
public interface F2<@Nullable T1, @Nullable T2, @Nullable R>

[jlink]

is org.jspecify.annotations.Nullable used differently than org.jetbrains.annotations.Nullable, which I'm currently using.

[vlsi]

In most cases - one exception is injectNull(..) - Arbitrary refers to either a nullable or non-nullable type and the result should have the same constraint.

I am afraid, the way to go is to declare

// Allow usage with nullable type
interface Arbitrary<@Nullable T> {
}

Even though you might "suppress" the warnings in jqwik's module, the very same issues would appear for all Kotlin users.

[vlsi]

org.jetbrains.annotations.Nullable, which I'm currently using.

JetBrains @Nullable is not applicable to type parameters for unknown reasons :-/

See

• https://github.com/gradle/gradle/issues/24767#issuecomment-1584914072
• https://youtrack.jetbrains.com/issue/KT-59352

[jlink]

Thanks for all the clarification @vlsi

My new strategy:

• Scrap this PR
• Move to 1.9.0 and disable strict type warning for Kotlin at the same time
• Replace jetbrains annotations with jspecify
• Get rid of the warnings in the Kotlin module one by one. I'm not sure that I'll really have to go with interface Arbitrary<@Nullable T>, but I'll see.

[jlink]

Doing step-by-step migration on main