Fail to utilize HKT GADT bounds for applied types

[Linyxus]

Compiler version

3.0.1

Minimized code

type Const = [X] =>> Int

trait Expr[F[_]]
case class ConstExpr() extends Expr[Const]

def foo[F[_], A](e: Expr[F]): F[A] = e match
  case _: ConstExpr => 0

Output

Found:    (0 : Int)
Required: F[A]

where:    F is a type in method foo which is an alias of [X] =>> Int

Expectation

By pattern matching we derive the GADT bound F := [X] =>> Int (as shown in the error message), but during type comparison the compiler will not recognize F[X] == Int for the applied type.

[Linyxus]

In the type comparison logic, only when both sides are HKTs will the GADT bounds for HKTs be used.

Actually a simple tweak will make the code compile:

type Const = [X] =>> Int
type Identity = [X] =>> X

trait Expr[F[_]]
case class ConstExpr() extends Expr[Const]
case class IdentityExpr() extends Expr[Identity]

def foo[F[_], A](e: Expr[F]): F[A] = e match
  case _: ConstExpr => 0 : Const[A]
                      // ^^^^^^^^^^

If we are comparing A <:< F[X] and F has a lower bound G, it would be safe to downcast and turn to compare A <:< G[X]. Should we add the downcasting logic in the type comparer?