Soundness issue with variance and higher kinded types

[jpmartin2]

While playing around with dotty I encountered what seems to be a issue with the typechecker. Here's a minimal example where I was able to reproduce the issue:

case class Foo[+X[_]](will: X[Int]) {
  def foo[Y[_]](right: Foo[Y]) = Foo.doFoo(this, right)
}

class A[X] { def crash = true }
class B[X]

object Foo {
  def doFoo[X[_]](left: Foo[X], right: Foo[X]): Foo[X] = right

  def main(args: Array[String]): Unit = {
    val fooA = Foo(new A[Int])
    val fooB = Foo(new B[Int])
    // The type for this is inferred correctly to Foo[A|B]
    val fine = doFoo(fooA, fooB)
    // This throws a ClassCastException because fooB isn't a Foo[A]
    val oops: Foo[A] = fooA.foo(fooB)
    println(oops.will.crash)
  }
}

It seems like the type that dotty is inferring for foo is Foo[X], even though it should be Foo[X|Y], and because of this is allowing me to then use the result in ways I shouldn't be able to.

Also, I couldn't find a way to annotate foo to get it to typecheck and work. One variation I tried was this:

case class Foo[+X[_]](will: X[Int]) {
  def foo[Y[_]](right: Foo[Y]): Foo[X|Y] = Foo.foo(this, right)
}

object Foo {
  def foo[X[_],Y[_]](left: Foo[X], right: Foo[Y]): Foo[X|Y] = right
}

But I was met with

-- [E007] Type Mismatch Error: /tmp/scastie6848463800932418099/src/main/scala/main.scala:6:62 
6 |  def foo[X[_],Y[_]](left: Foo[X], right: Foo[Y]): Foo[X|Y] = right
  |                                                              ^^^^^
  |                                                   found:    Foo[Y](right)
  |                                                   required: Foo[X]
  |

I'd expect the required type should be Foo[X|Y] (or to be more precise Foo[[T] => X[T] | Y[T]]) , for which a Foo[Y] should be fine right? Or is there a problem using subtyping with higher kinded types like this?

Either way, the first example definitely seems like an issue of soundness.

[smarter]

Ouch, nice find! I think I figured it out the issue leading to the ClassCastException and will open a PR shortly. Your second example still fails to compile due to type inference having a hard time with unions in higher-kinded types, but let's take it one at a time.

[smarter]

Opened #2989 to track a problem related to your second example.