Variance checking is inconsistent when using curried type operators

[sstucki]

Dotty reports errors for some of the curried type operators defined below, but not for their uncurried versions.

object Curried {
  trait AllTrait[-B, +F[_ <: B]] { def apply[X <: B]: F[X] }

  type All[-B, +F[_ <: B]] = AllTrait[B, F]
  type AllCurried[-B] = [+F[_ <: B]] => AllTrait[B, F]  // fails

  type FooU[-X, +F[-_ <: X]] = X => F[X]
  type FooUCurried[-X] = [+F[-_ <: X]] => (X => F[X])   // fails
  type FooL[-X, +F[-_ >: X]] = X => F[X]
  type FooLCurried[-X] = [+F[-_ >: X]] => (X => F[X])   // ok

  type BarU[+X, -F[-_ <: X]] = F[X] => X
  type BarUCurried[+X] = [-F[-_ <: X]] => (F[X] => X)   // ok
  type BarL[+X, -F[-_ >: X]] = F[X] => X
  type BarLCurried[+X] = [-F[-_ >: X]] => (F[X] => X)   // fails
}

I think this is a variant of #6320 but this time triggered by variance annotations instead of bounds. Similar issues were already discussed in #1252.

I'm pretty sure that the errors are false positives (the uncurried versions are safe, and so are the curried ones). The problem is that we still lack a full theory of dependent higher-order subtyping with variances annotations, so it's difficult to know for sure.

For the first case (AllCurried), I'm convinced there should not be an error though. That case is simply an encoding of bounded universal quantification and we know that the specified variances are sound (from the corresponding typing rule of full F_<:) .

[anatoliykmetyuk]

The minimised version of this one looks funny. All the lines with type lambdas below fail:

trait A[-X]
type A0[-X] = [_ >: X] => A[X]
type A1[-X] = [_[_ <: X]] => A[X]
type A2[-X] = [_[_[_ >: X]]] => A[X]
type A3[-X] = [_[_[_[_ <: X]]]] => A[X]
type A4[-X] = [_[_[_[_[_ >: X]]]]] => A[X]
type A5[-X] = [_[_[_[_[_[_ <: X]]]]]] => A[X]

trait B[+X]
type B0[+X] = [_ <: X] => B[X]
type B1[+X] = [_[_ >: X]] => B[X]
type B2[+X] = [_[_[_ <: X]]] => B[X]
type B3[+X] = [_[_[_[_ >: X]]]] => B[X]
type B4[+X] = [_[_[_[_[_ <: X]]]]] => B[X]
type B5[+X] = [_[_[_[_[_[_ >: X]]]]]] => B[X]

All the code below succeeds:

trait A[-X]
type A0[-X] = [_ <: X] => A[X]
type A1[-X] = [_[_ >: X]] => A[X]
type A2[-X] = [_[_[_ <: X]]] => A[X]
type A3[-X] = [_[_[_[_ >: X]]]] => A[X]
type A4[-X] = [_[_[_[_[_ <: X]]]]] => A[X]
type A5[-X] = [_[_[_[_[_[_ >: X]]]]]] => A[X]

trait B[+X]
type B0[+X] = [_ >: X] => B[X]
type B1[+X] = [_[_ <: X]] => B[X]
type B2[+X] = [_[_[_ >: X]]] => B[X]
type B3[+X] = [_[_[_[_ <: X]]]] => B[X]
type B4[+X] = [_[_[_[_[_ >: X]]]]] => B[X]
type B5[+X] = [_[_[_[_[_[_ <: X]]]]]] => B[X]

[anatoliykmetyuk]

I think this is not a bug. Further minimised:

type Co0 = [+X] => [_ <: X] => Any
type Co1 = [+X, _ <: X] => Any
type Co2 = [+X, _ >: X <: X] => Any
type Co3 = [+X] => [_ >: X <: X] => Any

type Contra0 = [-X] => [_ >: X] => Any
type Contra1 = [-X, _ >: X] => Any
type Contra2 = [-X, _ >: X <: X] => Any
type Contra3 = [-X] => [_ >: X <: X] => Any

Output:

-- Error: ../issues/i6369/Sample.scala:1:13 ------------------------------------
1 |type Co0 = [+X] => [_ <: X] => Any
  |            ^^
  |covariant type parameter X occurs in contravariant position in [_$1 <: X] => Any
-- Error: ../issues/i6369/Sample.scala:4:13 ------------------------------------
4 |type Co3 = [+X] => [_ >: X <: X] => Any
  |            ^^
  |covariant type parameter X occurs in invariant position in [_$4 >: X <: X] => Any
-- Error: ../issues/i6369/Sample.scala:6:17 ------------------------------------
6 |type Contra0 = [-X] => [_ >: X] => Any
  |                ^^
  |contravariant type parameter X occurs in covariant position in [_$5 >: X] => Any
-- Error: ../issues/i6369/Sample.scala:9:17 ------------------------------------
9 |type Contra3 = [-X] => [_ >: X <: X] => Any
  |                ^^
  |contravariant type parameter X occurs in invariant position in [_$8 >: X <: X] => Any

The complaints are about the occurrence of the argument to the type lambda in the type bounds of the argument to the curried lambda.

It makes sense for the compiler to enforce variance checks in a curried lambda scenario since one may, e.g., call Co0[X] and the compiler will have to make subtyping judgements about that type:

type F = [+X] => [_ <: X] => Any

type C1 = F[Any    ] //= [_ <: Any    ] => Any
type C2 = F[Nothing] //= [_ <: Nothing] => Any

Above, C2 <: C1 (by covariance of F's X, since Nothing <: Any). Hence we should be able to do with C2 everything we can do with C1:

C1[String] - ok
C2[String] – not ok

Variance checks do not need to be enforced with non-curried lambdas since AFAIK there is no mechanics to provide arguments partially:

type Co1 = [+X, _ <: X] => Any

Above, we can't construct a type without providing both arguments. Hence the compiler does not need to make judgements about the subtyping of Co1 that was provided only the first argument.

The above reasoning, however, has an implication that curried lambdas are not equivalent to non-curried lambdas when variance comes into play. I'm not sure whether this is wrong or plausible, probably a theoretical input is needed here. Also I'm not sure how this reasoning plays with:

I'm convinced there should not be an error though. That case is simply an encoding of bounded universal quantification and we know that the specified variances are sound

@sstucki can you please elaborate?

Regarding my previous post, the <: flipping behaviour is due to (pseudocode):

type F[-X]
type G[+X] = F[F[X↓]↑]↓

When X is going specific, F[X] is going general and F[F[X]] is going specific. Hence not really related to the issue.

[sstucki]

Above, C2 <: C1 (...) Hence we should be able to do with C2 everything we can do with C1: ...

That's not how subtyping works. The rule of thumb is that, if C2 <: C1, then an instance of C2 should be able to do anything that an instance of C1 can do. For example, I can use 1, which is an instance of Int, as if it were an instance of Any. That's not the same thing as saying that I can use the type Int itself in any position where the type Any is expected. Here's a simple (and quite silly) counterexample:

type LowerBounded[X >: Any] = X
type Test1 = LowerBounded[Any]  // OK
type Test2 = LowerBounded[Int]  // fails

The actual rule for comparing type functions is that F <: G if F[X] <: G[X] for all types X that fit the signature of both F and G. The extra constraint that X has to fit the signature of both F and G is a kinding constraint. It does not make sense to compare F and G outside their respective domain of definition. In your example, String does not fit the signature of C2, so the application C2[String] is simply ill-kinded – this has nothing to do with variance.

Here's an analogy from mathematics. Consider the two functions f(x) = log(x) and g(x) = 2*x. The domain of definition of f is the set of the positive reals, while g is defined on all the reals, both positive and negative. If we want to compare f(x) and g(x) pointwise, we can only do so for positive numbers. It simply doesn't make sense to compare f(-1) and g(-1) because f(-1) is ill-defined. Another way to say this is that the parameter of f is lower-bounded. If f were a type function, we might use the notation f(x ≥ 0) = log(x) – but there is no such syntax for term-level functions. Bounded type functions work exactly the same way, except that we replace ≤ with <:.

There is a related discussion about this in #6320 – you may wanna have a look at that.

Variance checks do not need to be enforced with non-curried lambdas since AFAIK there is no mechanics to provide arguments partially: (...) Above, we can't construct a type without providing both arguments. Hence the compiler does not need to make judgements about the subtyping of Co1 that was provided only the first argument.

This may well be the reason why variance checks are not implemented for uncurried functions in the compiler, but it doesn't change the rules of subtyping, which should be the same for curried and uncurried definitions. Even if there is no special syntax for partial type application, I can partially apply a type explicitly via a type lambda [Y <: Any] => Co1[Any, Y] or by defining a type alias

type Co1 = [+X, _ <: X] => Any
type Co1Any[Y <: Any] = Co1[Any, Y]
type Co1Nothing[Y <: Nothing] = Co1[Any, Nothing]

And because these are all constant functions, Co1Any <: Co1Nothing and Co1Nothing <: Co1Any should still be true (for all type arguments that fit the signatures of both both functions).

I'm convinced there should not be an error though. That case is simply an encoding of bounded universal quantification and we know that the specified variances are sound

@sstucki can you please elaborate?

In a nutshell, AllTrait implements a bounded quantifier ∀X<:S.T from F-sub. The most general subtyping rule for such quantifiers is the one described by Pierce in TAPL in Fig. 26-2 (p. 395). That rule is contravariant in the bound S and covariant in the codomain T which is consistent with the variance annotations for AllTrait. In AllTrait, the type T is replaced by a bounded type operator F (since T may contain free occurrences of X).

As in Scala, there is no syntax in F-<: for partially applying ∀. F-sub also doesn't have (bounded) type lambdas or type definitions, so we cannot use the tricks I described above. The only formal system that I know of that has all the features you need to actually do this is the one described in my PhD thesis. In that system, you can indeed define the equivalent of

T1 = λX<:A1. ∀Y<:A1. B
T2 = λX<:A2 ∀Y<:A2. B

and show that T1 <: T2 provided

1. T1 and T2 have the same kind, and
2. A2 <: A1.

Let me know if that answers your question.

[anatoliykmetyuk]

Thanks for the detailed explanations!

So basically the type lambdas are compared by their output ranges, point-wise, and not by their input domains? Hence if the input domain of one lambda includes the input domain of another lambda, this won't influence the subtyping of the two lambdas, since we are comparing only their output ranges and only for the inputs they both can accept?

Hence, do you think we should not perform the variance checking for the type bounds of the arguments to type lambdas? Since the bounds do not participate in the subtyping rules for the type lambdas?

[sstucki]

@anatoliykmetyuk: sorry for the late reply.

So basically the type lambdas are compared by their output ranges, point-wise, and not by their input domains? Hence if the input domain of one lambda includes the input domain of another lambda, this won't influence the subtyping of the two lambdas, since we are comparing only their output ranges and only for the inputs they both can accept?

Correct. This is how it should be IMO, but AFAIK, it's not what's currently implemented. See #6320 for a related discussion.

Hence, do you think we should not perform the variance checking for the type bounds of the arguments to type lambdas? Since the bounds do not participate in the subtyping rules for the type lambdas?

The honest answer is: I don't know.

We're lacking a full theory of variance checking in the presence of lambdas with type bounds (it has not yet been developed). IMO, it probably does not make sense to try and fix this issue until we have such a theory. If you want to attempt a fix anyway, then my current best guess is that variance checking is probably not needed in arguments to type lambdas. But again, that's just a guess (based on the intuition given above).

[odersky]

We don't allow curried variance annotations anymore.