Description
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.