In Scala, is the transitive rule of covariance missing?

Question

E.g.

  trait AA[+X[n], +Y] {

    def x: X[Y] // [Error]: covariant type Y occurs in invariant position in type => X[Y] of method x
  }

This appears to be the wrong message, as X[Y] can be easily proven to be covariant:

if Y1 >:> Y2, +X1[n] >:> +X2[n] for all n, then:

Y1 >:> Y2

(covariance of X2) => X2[Y1] >:> X2[Y2]

(X1[Y1] >:> X2[Y1]) => X1[Y1] >:> X2[Y2]

What may have caused this error message?

Answer 1

You are missing one more +. Correct is

trait AA[+X[+n], +Y] {
  def x: X[Y]
}

Then the type X will be covariant (with respect to its type parameter n) and the position

  def x: X[...]
//         ^^^  <- this position

will be covariant and you'll be able to use covariant type parameter Y at this position.

On contrary, you declared invariant type X (w.r.t. n) and tried to use covariant type parameter Y at an invariant position.

There are different notions:

• covariant/contravariant/invariant type parameter (+T, -T, T)

• covariant/contravariant/invariant type, i.e. type constructor, with respect to its type parameter (T1 <: T2 => A[T1] <: A[T2], T1 <: T2 => A[T1] >: A[T2], or none of those)

• covariant/contravariant/invariant position according to the rules https://scala-lang.org/files/archive/spec/2.13/04-basic-declarations-and-definitions.html#variance-annotations

+X[n] is a covariant type parameter of AA but invariant type with respect to its type parameter n.

The following conclusion was incorrect:

(covariance of X2) => X2[Y1] >:> X2[Y2]

Also correct would be to make Y invariant

trait AA[+X[n], Y] {
  def x: X[Y]
}

---

By the way, yesterday Oleg Nizhnikov (@odomontois) had a training on variances (among other topics) https://youtu.be/l08tK1x89ho?t=7494 (starting from 2:04:54).