Better utilizing GADT bounds for HKTs

[Linyxus]

This PR fixes #13257. Before this PR, the following code example could not compile:

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

It is sound to allow its compilation, since Int <: Const[A] <: F[A]. This PR changes the TypeComparer's behavior by trying to approximate the type constructor when GADT bounds is available. A global state is added to the TypeComparer to track whether HKT bounds have been used during type comparison, to properly handle the injectivity conditions.

[abgruszecki]

@Linyxus #13380 was merged, you can proceed with this PR.

[Linyxus]

@abgruszecki Hey Alex, I have finished the modification. Also, I add some additional code to allow the LHS HKT to be approximated to its GADT upper bound.

[abgruszecki]

Aside from the nitpick, the PR LGTM.