GADT bounds for higher-kinded variables do not appear to work

[smarter]

minimized code

class Foo[A]
class Inv[M[_]]
class InvFoo extends Inv[Foo]

object Test {
  def foo[F[_]](x: Inv[F]) = x match {
    case x: InvFoo =>
      val z: F[Int] = ??? : Foo[Int]
    case _ =>
  }
}

Compilation output

-- [E007] Type Mismatch Error: try/gadt.scala:27:22 ----------------------------
27 |      val z: F[Int] = ??? : Foo[Int]
   |                      ^^^^^^^^^^^^^^
   |            Found:    Foo[Int]
   |            Required: F[Int]
   |
   |            where:    F is a type in method foo which is an alias of Foo

expectation

It looks like the compiler correctly inferred that Fis equal to Foo but somehow wasn't able to use this knowledge to deduce that Foo[Int] <:< F[Int] ?

Whenever this is fixed, it'll be important to verify that the handling of higher-kinded variables is sound with respect to GADT bounds inference. When recording GADT constraints, we need subtype checking to only register necessary constraints and not sufficient constraints (see TypeComparer#either), this is not necessarily the case when we do partial unification (cf the infamous SI-2712) since we try every parent type until we find one that matches, and more than one parent could match: https://github.com/lampepfl/dotty/blob/b448db2454e003f1448a31746daed11001a2ec86/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L940-L943