Irregular type inference for `Nothing`

I just thought of perhaps a clearer way to express the issue. Below is a principle that seems natural:

The tightening of an upper / lower type bound of a covariant / contravariant type parameter should never loosen its inference.

In other words, for the covariant case, given a parametrized type A[+T <: U1], U1 >: U2, and a context in which T gets inferred to be I1, it should never be the case that, when A’s upper bound is tightened to U2, (i.e. A[+T <: U2]), T gets inferred to some different I2, not satisfying I2 <: I1, in the same context.

If that principle sounds unreasonable to anyone, I’d love to hear about it.

The irregular type inference mentioned in this thread not only violates this principle, but further violates type alias transparency, by having inference behave differently when the same upper bound (in this case, Any) is provided via an alias.

Hopefully, someone from the Scala team can chime in.