Irregular type inference for `Nothing`

[Sporarum]

@Stephane

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.

I have some trouble wrapping my head around this, could you give an example ?
(With what you would like, and what happens currently)