GADT pattern matching produces conformance constraints instead of equality (HKTs)

[sir-wabbit]

object App {
  case class Box[F[_]](value: F[Int])
  sealed trait IsK[F[_], G[_]]
  final case class ReflK[F[_]]() extends IsK[F, F]

  def foo[F[_], G[_]](r: F IsK G, a: Box[F]): Box[G] = r match { case ReflK() => a }
  
  def main(args: Array[String]): Unit = {
    println(foo(ReflK(), Box(Option(10))))
  }
}

-- [E007] Type Mismatch Error: foo.scala:6:81 ----------------------------------
6 |  def foo[F[_], G[_]](r: F IsK G, a: Box[F]): Box[G] = r match { case ReflK() => a }
  |                                                                                 ^
  |                   found:    App.Box[F](a)
  |                   required: App.Box[G]
  |                   
  |                   where:    F is a type in method foo with bounds <: G[_]
  |                             G is a type in method foo with bounds <: F[_]
one error found

[Blaisorblade]

In Dotty type equality is just type conformance twice: A = B means A <: B and B <: A. But then constraint solving should unify variables if A <: B and B <: A.

So this seems a variant of #4176:

We end up with GADT constraints foo >:> S and S >:> foo but we don't have a mechanism to unify GADT constraints, so we end up with a loop in subtyping checks.

except that even with that bug, we should have F <: G or F <: [X] => G[X], and F <: G[_] looks wrong or misleading.