Unsoundness when matching on a wildcard with bad bounds at definition site

[s5bug]

Compiler version

3.1.3, 3.2.0-RC1

Minimized code

trait Foo[X >: Any <: Nothing]

def andThenSub[A, B, C](f: A <:< B, g: B <:< C): A <:< C =
  f.andThen(g)

(None: Option[Foo[?]]) match {
  case _: Option[Foo[t]] =>
    val unsound: Any <:< Nothing = andThenSub[Any, t, Nothing](summon, summon)
    unsound("hi :)")
}

Output

java.lang.ClassCastException: class java.lang.String cannot be cast to class scala.runtime.Nothing$

Expectation

A compilation error on the definition of Foo.

Possibly related to #15568?

[s5bug]

Apologies, old title was from before I minimized away the alias :)