Missing variance checks in rhs of type aliases leads to unsoudness

[smarter]

This shouldn't compile because X appears covariantly in the rhs of type Id[-X] = X:

abstract class A {
  type Id[-X]
  def a: Id[Any]
  def b: Id[String] = a
}
class B extends A {
  type Id[-X] = X // error in scalac, compiles in dotty
  override def a = 1
}
object Test {
  def main(args: Array[String]): Unit = {
    val b = new B
    println(b.a)
    println(b.b)
    val x: String = b.b // ClassCastException at runtime
  }
}

scalac doesn't allow type Id[-X] = X and type Id[-X] <: X but allows type Id[-X] >: X, I haven't thought enough about it to know if that makes sense.

[smarter]

/cc @sstucki

[smarter]

Just had a discussion on this with @sstucki who made a very good observation, the scalac check are inconsistent:

type Foo[+X] <: X // OK
type Foo[+X] = X // OK
type Foo[+X] >: X // error: covariant type X occurs in contravariant position

Since type Foo[+X] = X should behave like type Foo[+X] >: X <: X then it shouldn't be allowed according to the scalac rules but it is.

@sstucki suggested that whether we are in a lower or upper-bound should not affect the variance check, because:

type  Bar[+X] >: One[X] <: Two[X]

is really:

type Bar >: [+X] => One[X] <: [+X] => One[X]

So X is not bounded in the left-hand-side so it cannot affect the variance.

[odersky]

Do we have examples where this causes a ClassCastException? If not, I would follow @sstucki's reasoning and recommend to close.

[smarter]

My initial example causes a ClassCastException in dotty, @sstucki's reasoning does not mean that we shouldn't check anything but that whether something is lower- or upper-bounded does not affect the check, doing this check in my initial example will prevent it from compiling as expected. I can prepare a PR for that.

[sstucki]

Here's a related issue, which doesn't involve variance annotations:

trait A                  { type L[Y <: Int]    >: Int    }
trait B                  { type L[Y <: String] >: String }
trait C extends A with B { type L[Y <: Any]    >: Any    }

The compiler reports

-- Error: ... -------
3 |trait C extends A with B { type L[Y <: Any]    >: Any    }
  |                                ^
  |overriding type L in trait B with bounds >: [Y <: String] => String <: [Y <: String] => Any;
  | type L with bounds >: [Y] => Any <: [Y] => Any has incompatible type

the problem is that, when the compiler checks that bounds of L declared in C conform to those declared in B, it compares the bound annotations of the type-lambdas that form those bounds. But when checking whether two lambdas are subtypes, their bounds need not be compared, as long as both lambdas have the same kind.

Concretely, here we want all the lambdas to have the (wider) kind (Y <: String) -> * which is the declared kind of L in the parent trait B:

[Y <: String] => String  has kind  (Y <: String) -> *
[Y <: String] => Any     has kind  (Y <: String) -> *
[Y] => Any               has kind  (Y <: Any) -> *   sub-kind of  (Y <: String) -> *
[Y] => Any               has kind  (Y <: Any) -> *   sub-kind of  (Y <: String) -> *

so all the bounds are well-kinded and their kinds conform to the signature in the parent class. Then we need to check that the definitions of the lambdas agree in this kind, which they do:

/* Lower bounds are checked contravariantly: */
  String <: Any  forall  Y <: String,  so  [Y <: String] => String <: [Y <: Any   ] => Any
/* Upper bounds are checked covariantly: */
  Any    <: Any  forall  Y <: String,  so  [Y <: Any   ] => Any    <: [Y <: String] => Any

I'm not sure whether this should be reported in a separate issue. The two issues are definitely related because in both cases kind-checking and subtyping are mixed up.