Validation error: Type parameter variance

[lars-reimann]

Is your feature request related to a problem?

Type parameter variance is currently not checked vs. how the type parameter is used.

Desired solution

Add validation.

Possible alternatives (optional)

No response

Screenshots (optional)

No response

Additional Context (optional)

Behavior in Kotlin:

abstract class List<in T, out S> {
    abstract val a: (a: S) -> T
    abstract val b: List<S, T>
    abstract val c: T
    
    abstract fun f(
        p: (a: T) -> S,
        q: S,
        r: (x: (a: S) -> T) -> ((a: T) -> S)
    ): T
}

Type parameter S is declared as 'out' but occurs in 'in' position in type (S) -> T
Type parameter T is declared as 'in' but occurs in 'out' position in type (S) -> T
Type parameter S is declared as 'out' but occurs in 'in' position in type List<S, T>
Type parameter T is declared as 'in' but occurs in 'out' position in type List<S, T>
Type parameter T is declared as 'in' but occurs in 'out' position in type T
Type parameter T is declared as 'in' but occurs in 'out' position in type (T) -> S
Type parameter S is declared as 'out' but occurs in 'in' position in type (T) -> S
Type parameter S is declared as 'out' but occurs in 'in' position in type S
Type parameter S is declared as 'out' but occurs in 'in' position in type ((S) -> T) -> (T) -> S
Type parameter T is declared as 'in' but occurs in 'out' position in type ((S) -> T) -> (T) -> S
Type parameter T is declared as 'in' but occurs in 'out' position in type ((S) -> T) -> (T) -> S
Type parameter S is declared as 'out' but occurs in 'in' position in type ((S) -> T) -> (T) -> S
Type parameter T is declared as 'in' but occurs in 'out' position in type T

Observations: Each level of callables beyond the first flips the variance of a type parameter. For the parameter p of f, for example, we have to supply a value of type T, which then flows out of the class into the function.

It's probably beneficial to think of (S) -> (T) as Function2<in S, out T> and generally figure out how nesting of in/out modifiers works when determining in vs. out positions. We also have to figure out how something like List<List<S, T>, List<S, T>> works.

abstract class List<in T, out S> {
    abstract val a: List<
    	List<S, T>,
    	List<T, S>
    >
}

No errors in the above program. First idea:

1. Assign variance

.<
    in<in, out>,
    out<in, out>
>

2. Replace out<...> constructs by .<> constructs

.<
    in<in, out>,
    .<in, out>
>

3. Swap all variances inside an in<...> construct and replace it by a .<> construct

.<
    .<out, in>,
    .<in, out>
>

4. Repeat 2./3. from inside to outside.

=> in swaps variance, out maintains variance.

Correct programs:

abstract class List<in T, out S> {
    abstract val a: List<
    	Int,
    	List<Int,
    		List<Int,
    			List<T, S>
    		>
    	>
    >
}

Erroneous programs:

abstract class List<T, out S> {
    abstract val a: List<
    	List<Int,
    		List<Int,
    			List<T, S>
    		>
    	>,
    	Int
    >
}

Type parameter S is declared as 'out' but occurs in 'invariant' position in type List<List<Int, List<Int, List<T, S>>>, Int>

• Outer invariant enforces invariant
• Outer in swaps in/out
• Outer out maintains in/out