Overconstrained GADT bounds in presence of type bounds with non-variant type constructors

[mario-bucev]

Minimized code

@main def test: Unit = {
  class Foo
  class Bar
  
  trait UpBnd[+A]
  trait P extends UpBnd[Foo]
  
  def pmatch[A, T <: UpBnd[A]](s: T): A = s match {
    case p: P => new Foo
  }
  
  class UpBndAndB extends UpBnd[Bar] with P
  // ClassCastException: Foo cannot be cast to Bar
  val x = pmatch(new UpBndAndB)
}

Output

Click to expand

java.lang.ClassCastException: main$package$Foo$1 cannot be cast to main$package$Bar$1
	at main$package$.test(main.scala:14)
	at test.main(main.scala:1)
	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 sbt.Run.invokeMain(Run.scala:115)
	at sbt.Run.execute$1(Run.scala:79)
	at sbt.Run.$anonfun$runWithLoader$4(Run.scala:92)
	at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)
	at sbt.util.InterfaceUtil$$anon$1.get(InterfaceUtil.scala:10)
	at sbt.TrapExit$App.run(TrapExit.scala:257)
	at java.lang.Thread.run(Thread.java:748)

Expectation

The code should be rejected because we do not have enough information about A.

I think that having PatternTypeConstrainer#constrainSimplePatternType widen the type parameters of type constructors appearing in bounds should do the trick.

[mario-bucev]

Actually, I think that the widening should be done recursively, as just exploring the bounds may not be enough:

@main def test: Unit = {
  trait Foo
  trait Bar

  class FooBar extends Foo with Bar

  trait S[F[_]]
  trait TyCon[+A, B]

  def nested[XX <: Foo]: XX = {
    // Note: P[+XX <: Foo] extends S[[T] =>> TyCon[XX, T]] does not compile, so we nest it within this dummy function
    trait P extends S[[T] =>> TyCon[XX, T]]

    def patmat[F <: [A] =>> TyCon[Foo, A]](s: S[F]): XX = s match {
      case p: P => 
        // Inferred: Foo <:< XX (so Foo =:= XX), though it is not necessarly the case 
        new Foo{}
    }

    class Dyn extends P
    patmat(new Dyn)
  }
  // ClassCastException: main$package$$anon$1 cannot be cast to main$package$FooBar$1
  val got = nested[FooBar]
}