Unsound type propagation/refinement *without case classes*

[Blaisorblade]

Due to @odersky — he generalized the first part of #3989 without using case classes.
I reconstructed the example from its core (case b: B[_] => a.i), but that was tricky, hence this ticket.

trait A[+X]; class B[X](val x: X) extends A[X]
def f(a: A[Int]): Int =
  a match {
    case b: B[_] => b.x
  }
class C extends B[String]("") with A[Int]
f(new C())

Transcript:

scala> trait A[+X]; class B[X](val x: X) extends A[X]
// defined trait A
// defined class B
scala> def f(a: A[Int]): Int =
           a match {
             case b: B[_] => b.x
           }
def f(a: A[Int]): Int
scala> class C extends B[String]("") with A[Int]
// defined class C
scala> f(new C())
java.lang.ClassCastException: java.lang.String cannot be cast to java.lang.Integer
	at scala.runtime.BoxesRunTime.unboxToInt(BoxesRunTime.java:101)
	at rs$line$29$.f(rs$line$29:3)
	at rs$line$31$.<init>(rs$line$31:1)
	at rs$line$31$.<clinit>(rs$line$31)
	at rs$line$31.res5Show(rs$line$31)
	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.lang.reflect.Method.invoke(Method.java:498)
	at dotty.tools.repl.Rendering.valueOf(Rendering.scala:58)
	at dotty.tools.repl.Rendering.renderVal(Rendering.scala:79)
	at dotty.tools.repl.ReplDriver.$anonfun$displayDefinitions$8(ReplDriver.scala:281)
	at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
	at scala.collection.mutable.ResizableArray.foreach(ResizableArray.scala:59)
	at scala.collection.mutable.ResizableArray.foreach$(ResizableArray.scala:52)
	at scala.collection.mutable.ArrayBuffer.foreach(ArrayBuffer.scala:48)
	at scala.collection.TraversableLike.map(TraversableLike.scala:234)
	at scala.collection.TraversableLike.map$(TraversableLike.scala:227)
	at scala.collection.AbstractTraversable.map(Traversable.scala:104)
	at dotty.tools.repl.ReplDriver.displayMembers$1(ReplDriver.scala:281)
	at dotty.tools.repl.ReplDriver.$anonfun$displayDefinitions$15(ReplDriver.scala:308)
	at scala.Option.map(Option.scala:146)
	at dotty.tools.repl.ReplDriver.$anonfun$displayDefinitions$13(ReplDriver.scala:306)
	at dotty.tools.dotc.core.Periods.atPhase(Periods.scala:26)
	at dotty.tools.dotc.core.Phases.atPhase(Phases.scala:36)
	at dotty.tools.dotc.core.Phases.atPhase$(Phases.scala:35)
	at dotty.tools.dotc.core.Contexts$Context.atPhase(Contexts.scala:70)
	at dotty.tools.repl.ReplDriver.displayDefinitions(ReplDriver.scala:301)
	at dotty.tools.repl.ReplDriver.$anonfun$compile$2(ReplDriver.scala:238)
	at scala.util.Either.fold(Either.scala:188)
	at dotty.tools.repl.ReplDriver.compile(ReplDriver.scala:232)
	at dotty.tools.repl.ReplDriver.interpret(ReplDriver.scala:202)
	at dotty.tools.repl.ReplDriver.loop$1(ReplDriver.scala:150)
	at dotty.tools.repl.ReplDriver.$anonfun$runUntilQuit$1(ReplDriver.scala:154)
	at scala.util.DynamicVariable.withValue(DynamicVariable.scala:58)
	at scala.Console$.withErr(Console.scala:192)
	at dotty.tools.repl.ReplDriver.$anonfun$withRedirectedOutput$1(ReplDriver.scala:163)
	at scala.util.DynamicVariable.withValue(DynamicVariable.scala:58)
	at scala.Console$.withOut(Console.scala:163)
	at dotty.tools.repl.ReplDriver.withRedirectedOutput(ReplDriver.scala:163)
	at dotty.tools.repl.ReplDriver.runUntilQuit(ReplDriver.scala:154)
	at dotty.tools.repl.Main$.main(Main.scala:6)
	at dotty.tools.repl.Main.main(Main.scala)

The basic strategy is similar to #3989 (comment), but it's a bit trickier to exploit it. The compiler assumes that a: A[Int] is also a B[Int] while it can be, in fact, B[String] — or in general, it can be a B[X] for arbitrary X.

Since here no case classes are involved, we can't forbid definitions like C (they're too common), @odersky suggested that we simply deducing unsound constraints about X.

Conversely, for GADTs we can make the opposite tradeoff: forbid definitions like C and allow deducing (sound) constraints on type variables as usual.

I'm a bit concerned by the irregularity, but it's hard to think of anything better.

[Blaisorblade]

Fixed title, the AbstractMethodError was due to the 2nd part of #3989.

[liufengyun]

Debugging, see the following logs:

  ==> _(b.x) <:< Int
    ==> Int <:< Int LoApprox
      ==> scala.type(scala) <:< scala.type
      <== scala.type(scala) <:< scala.type   = true
    <== Int <:< Int LoApprox  = true
  <== _(b.x) <:< Int   = true

  ==> C <:< A[Int]
    ==> A[String & Int] <:< A[Int] LoApprox
      ==> <empty>.type(<empty>) <:< <empty>.type(<empty>)
      <== <empty>.type(<empty>) <:< <empty>.type(<empty>)   = true
      ==> String & Int <:< Int
        ==> Int <:< Int LoApprox
          ==> scala.type(scala) <:< scala.type
          <== scala.type(scala) <:< scala.type   = true
        <== Int <:< Int LoApprox  = true
      <== String & Int <:< Int   = true
    <== A[String & Int] <:< A[Int] LoApprox  = true
  <== C <:< A[Int]   = true

[Blaisorblade]

Thanks for taking a look!

So this is a close variant of https://github.com/lampepfl/dotty/pull/4013/files/7ae7560a70acb2715e102af08329ec7cb0c9c1a1..49f9dc6bf0567f4d429ec85777355429f2a6cbaa#diff-67f55293f2001c7ef140f0932e65023e, so I'm hoping that PR will fix this example as well. (EDIT: not yet done).

[odersky]

Compiling this on fix-#3989 I get:

-- [E007] Type Mismatch Error: i4014.scala:7:24 --------------------------------
7 | case b: B[_] => b.x
| ^^^
| found: _(b.x)
| required: Int
|

So it seems this is already covered.