Discrepancy in subtyping for covariant types with (bounded) wildcard arguments

[prolativ]

Compiler version

3.3.6, 3.7.2, 3.8.0-RC1-bin-20250731-fe6b7eb-NIGHTLY

Minimized code

trait Foo

trait Box[+A <: Any]
trait FooBox[+A <: Foo]

object Test {
  val x1 = implicitly[Box[Any] <:< Box[?]]
  val x2 = implicitly[Box[?] <:< Box[Any]]
  val y1 = implicitly[Box[Foo] <:< Box[?]]
  val y2 = implicitly[Box[?] <:< Box[Foo]]
  val z1 = implicitly[Box[Foo] <:< Box[? <: Foo]]
  val z2 = implicitly[Box[? <: Foo] <:< Box[Foo]]

  val a1 = implicitly[FooBox[Foo] <:< FooBox[?]]
  val a2 = implicitly[FooBox[?] <:< FooBox[Foo]]
  val b1 = implicitly[FooBox[Foo] <:< FooBox[? <: Foo]]
  val b2 = implicitly[FooBox[? <: Foo] <:< FooBox[Foo]]
}

Output

In scala 3:

[error] /var/folders/rp/f9y80jvs54lcy26rxnt2y2kw0000gn/T/Subtype.scala:10:43
[error] Cannot prove that Box[?] <:< Box[Foo].
[error]   val y2 = implicitly[Box[?] <:< Box[Foo]]
[error]                                           ^
[error] /var/folders/rp/f9y80jvs54lcy26rxnt2y2kw0000gn/T/Subtype.scala:12:50
[error] Cannot prove that Box[? <: Foo] <:< Box[Foo].
[error]   val z2 = implicitly[Box[? <: Foo] <:< Box[Foo]]
[error]                                                  ^

But when compiled with 2.13.16, the errors are:

[error] /var/folders/rp/f9y80jvs54lcy26rxnt2y2kw0000gn/T/Subtype.scala:10:12
[error] Cannot prove that Box[_] <:< Box[Foo].
[error]   val y2 = implicitly[Box[?] <:< Box[Foo]]
[error]            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[error] /var/folders/rp/f9y80jvs54lcy26rxnt2y2kw0000gn/T/Subtype.scala:15:12
[error] Cannot prove that FooBox[_] <:< FooBox[Foo].
[error]   val a2 = implicitly[FooBox[?] <:< FooBox[Foo]]
[error]            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Expectation

y2 is OK not to compile in both scala 2 and 3.
It seems however, that z2 should work in scala 3, as it does in scala 2.
In case of a2 scala 3 compiler seems to be right but someone else might confirm that this is a bug in scala 2