Subtype checking of type lambdas with bounds is too restrictive, part 2

[Blaisorblade]

Split out of #6320. This issue should stick to concrete examples and practical motivations (I'm looking at you @sstucki 😉 ) — longer-winded discussion should stick to #6320; we have an idea on how to fix this, but it might require significant changes to the subtype typechecker — threading an expected kind when comparing types. /cc @smarter. Once we have the best example we can come up with, I'd propose to tag others, e.g. Miles and Martin.

In Scala, when checking that Γ ⊢ F T1 <: F T2 (for some F), we might be too conservative, because T1 <: T2 might be false in general, but true under the context induced by F. For instance, [X] => [Y] => X <: [X] => [Y] => Y is false in general, but true under the right bounds. For an artificial example, as arguments of Foo.F below.

object Foo {
  type F[G[X, Y >: X <: X] >: Nothing <: Any]
  type G1[X,Y] =X
  type G2[X,Y]= Y
  implicitly[F[G1] <:< F[G2]] // fails
  implicitly[F[G1] <:< F[G1]] // succeeds
}

That code fails to compile today in either Scala or Dotty due to this issue.

Question: better motivation

Is anybody aware of have less artificial examples? I don't know any, and honestly it does not seem a priority, but as @sstucki spent some time arguing for this in theory, so I felt I should try to make the strongest and shortest case I could for it. I'm not yet happy with this, but it's progress.

Transcripts

$ dotr
Starting dotty REPL...
scala> object Foo {
     |   type F[G[X, Y >: X <: X] >: Nothing <: Any]
     |   type G1[X,Y] =X
     |   type G2[X,Y]=Y
     |   implicitly[F[G1] <:< F[G2]] // fails
     |   implicitly[F[G1] <:< F[G1]] // succeeds
     | }
5 |  implicitly[F[G1] <:< F[G2]] // fails
  |                             ^
  |Cannot prove that Foo.F[Foo.G1] <:< Foo.F[Foo.G2]..
  |I found:
  |
  |    $conforms[Nothing]
  |
  |But method $conforms in object Predef does not match type Foo.F[Foo.G1] <:< Foo.F[Foo.G2].

scala> object Foo {
     |   type F[G[X, Y >: X <: X] >: Nothing <: Any]
     |   type G1[X,Y] =X
     |   type G2[X,Y]=Y
     |   //implicitly[F[G1] <:< F[G2]] // fails
     |   implicitly[F[G1] <:< F[G1]] // succeeds
     | }
// defined object Foo

$ scala
scala> object Foo {
     |   type F[G[X, Y >: X <: X] >: Nothing <: Any]
     |   type G1[X,Y] =X
     |   type G2[X,Y]=Y
     |   implicitly[F[G1] <:< F[G2]] // fails
     | }
<console>:16: error: Cannot prove that Foo.F[Foo.G1] <:< Foo.F[Foo.G2].
         implicitly[F[G1] <:< F[G2]] // fails
                   ^

scala> object Foo {
     |   type F[G[X, Y >: X <: X] >: Nothing <: Any]
     |   type G1[X,Y] =X
     |   type G2[X,Y]=Y
     |   implicitly[F[G1] <:< F[G1]] }
defined object Foo

[sstucki]

Not really sure what the point of this issue is, but here's a slightly less silly example adapted from the OP (comment):

trait StillPrettySilly {

  type AppInt[+F[X <: Int]]  // could be defined as F[Int]
  type EtaExp[F[_]] = [X <: Int] => F[X]

  type ListUnbounded[X] = List[X]
  type ListBounded[X <: Int] = List[X]

  val lu: AppInt[ListUnbounded]
  val lb: AppInt[ListBounded]

  // These should all work -- eta-expansion should not matter!

  val lb1: AppInt[ListBounded]   = lu          // OK
  val lu1: AppInt[ListUnbounded] = lb          // fails
  val leu: AppInt[EtaExp[ListUnbounded]] = lb  // OK
}

[sstucki]

Note also that the above example should still work if AppInt is made invariant:

type AppInt[F[X <: Int]]

But that breaks lb1 as well since the compiler (incorrectly) treats AppInt[ListUnbounded] as a strict subtype of AppInt[ListBounded].