Unsoundness when inheriting conflicting type parameters

[szeiger]

This compiles without warnings in both Dotty master and Scala 2.12:

trait A[+X]
case class B[X](x: X) extends A[X]
class C[X](x: Any) extends B[Any](x) with A[X]
def f(a: A[Int]): Int = a match {
  case B(i) => i
  case _ => 0
}
f(new C[Int]("foo"))

There used to be unsoundness warnings but they are gone since (presumably) #3918 even though the pattern match is unsound.

Furthermore the following compiles without warnings:

trait A[+X] { def get: X }
case class B[X](x: X) extends A[X] { def get: X = x }
class C[X](x: Any) extends B[Any](x) with A[X]
def g(a: A[Int]): Int = a.get
g(new C[Int]("foo"))

In this case, which doesn't rely on pattern matching, the definition of C itself is unsound but Dotty accepts it anyway. Scala 2.12 rightfully complains:

scala> class C[X](x: Any) extends B[Any](x) with A[X]
<console>:14: error: overriding method get in trait A of type => X;
 method get in class B of type => Any has incompatible type
       class C[X](x: Any) extends B[Any](x) with A[X]
             ^

[szeiger]

Discussion leading to this ticket: https://gitter.im/lampepfl/dotty?at=5a81a707e217167e2c742a4f

[Blaisorblade]

The second one seems GADT-unrelated.

I disagree on “conflicting”: C refines a covariant type parameter, and I’m aware of no way to get issues from it without pattern matching (in Scalac) — this is an old bug (from my Scala’13 short paper, and there’s some issue for Scalac). As long as defining C is allowed, that pattern match (more precisely, the type refinement in that pattern match) should be forbidden — whether the compiler sees C or not (since it can be added later — unless there’s sealed).

Maybe defining C should indeed be forbidden but it’s not clear — that idea was ultimately rejected in the Scalac tracker (though I’m not sure the rationale for it was too compelling).
Maybe one could also separate more GADTs and normal classes, even though that’s irregular — I seem to recall Dotty’s sugar for ADTs has some special features anyway.

[smarter]

@Blaisorblade paper is a recommended read for this: http://lampwww.epfl.ch/%7Ehmiller/scala2013/resources/pdfs/paper5.pdf, section 4.3 gives some suggestions on how to fix this.
I think we should find a good criterion to disallow this kind of things:

class C[X](x: Any) extends B[Any](x) with A[X]

This will probably prevent some legitimate usecases but that's a small price to pay for soundness.

[Blaisorblade]

Finally found the old discussion on covariant type refinement for members. Back then it was unclear whether the expressiveness loss was tolerable. No clue how all this has evolved.
scala/bug#7093 (comment)