Existentials failing to typecheck when double-bounded

[s5bug]

Reproduction steps

Scala version: 2.13.10

@ def foo1(b: (T forSome { type T })): Box[T forSome { type T }] = new Box(b)
defined function foo1

@ def foo2[B](b: (T forSome { type T ; type X <: B })): Box[T forSome { type T ; type X <: B }] = new Box(b)
defined function foo2

@ def foo3[B](b: (T forSome { type T ; type X >: Box[T] <: B })): Box[T forSome { type T ; type X >: Box[T] <: B }] = new Box(b)
cmd23.sc:1: type mismatch;
 found   : (some other)T(in method foo3) where type (some other)T(in method foo3)
 required: T(in method foo) forSome { type T(in method foo3); type X >: ammonite.$sess.cmd11.Box[T(in method foo3)] <: B }
def foo3[B](b: (T forSome { type T ; type X >: Box[T] <: B })): Box[T forSome { type T ; type X >: Box[T] <: B }] = new Box(b)

    ^
Compilation Failed

@ def foo4(b: (T forSome { type T ; type X >: Box[T] })): Box[T forSome { type T ; type X >: Box[T] }] = new Box(b)
defined function foo4

@ def foo5(b: (T forSome { type T ; type X >: Box[T] })): (X forSome { type T ; type X >: Box[T] }) = {
>   val boxed: Box[T forSome { type T ; type X >: Box[T] }] = new Box(b)
>   val asX: (X forSome { type T ; type X >: Box[T] }) = boxed
>   asX
> }
defined function foo5

Problem

I expect that, because foo2 and foo4 compile (adding a lower bound or adding an upper bound to an existential doesn't interfere with typechecking) foo3 should also compile (if a lower bound is valid and an upper bound is valid, the same program should still be valid).

Note that T forSome { type T ; type X >: Box[T] <: B } is valid for typechecking. I wrote it trying to solve a problem posed by @lihaoyi:

class Box[T](t: T)
class Call[B <: Box[_]](ub: ???) { def value: B = Box(ub) }

object Foo extends Call[Box[Int]](1) // How to make this typecheck?
object Bar extends Call[Box[Int]]("not an int") // And this fail?

My idea was to use an existential to posit some type T such that Box[T] <: B. I know that one can replace evidence like implicit ev: A <:< B with a type parameter [X >: A <: B], making the method only callable if A <: B, and I figured this technique can be applied to existentials as well. The following typechecks:

class Box[T](t: T)
class Call[B <: Box[_]](ub: T forSome { type T ; type X >: Box[T] <: B })

object Foo extends Call[Box[Int]](1)

and the following fail:

val x: Box[Int] = Box(1)
object X extends Call[x.type](1)

object Y extends Call[Box[Int]]("not an int")

The problem is that one cannot implement def value: B with this signature, due to the unique double-bounded existential failure:

@ class Call[B <: Box[_]](b: (T forSome { type T ; type X >: Box[T] <: B })) {
>   def value: B = {
>     val original: Box[T forSome { type T ; type X >: Box[T] <: B }] = new Box[T forSome { type T ; type X >: Box[T] <: B }]
>     val simplifyToX: (X forSome { type T ; type X >: Box[T] <: B }) = original
>     val simplifyToB: B = simplifyToX
>     simplifyToB
>   }
> }
cmd1.sc:3: type mismatch;
 found   : (some other)T(in value original) where type (some other)T(in value original)
 required: T(in value original) forSome { type T(in value original); type X >: ammonite.$sess.cmd0.Box[T(in value original)] <: B }
    val original: Box[T forSome { type T ; type X >: Box[T] <: B }] = new Box[T forSome { type T ; type X >: Box[T] <: B }](b)

    ^
cmd1.sc:3: type mismatch;
 found   : ammonite.$sess.cmd0.Box[(some other)T(in value original) forSome { type (some other)T(in value original); type X >: ammonite.$sess.cmd0.Box[(some other)T(in value original)] <: B }]
 required: ammonite.$sess.cmd0.Box[T(in value original) forSome { type T(in value original); type X >: ammonite.$sess.cmd0.Box[T(in value original)] <: B }]

    val original: Box[T forSome { type T ; type X >: Box[T] <: B }] = new Box[T forSome { type T ; type X >: Box[T] <: B }](b)
                                                                      ^
cmd1.sc:4: type mismatch;
 found   : ammonite.$sess.cmd0.Box[T(in value original) forSome { type T(in value original); type X >: ammonite.$sess.cmd0.Box[T(in value original)] <: B }]
 required: X forSome { type T(in value simplifyToX); type X >: ammonite.$sess.cmd0.Box[T(in value simplifyToX)] <: B }
    val simplifyToX: (X forSome { type T ; type X >: Box[T] <: B }) = original
                                                                      ^
Compilation Failed

Yet foo5 shows that the original and simplifyToX steps should work, and (X forSome { type X <: U }) means that simplifyToB should work (as it seems to in this example).