Change flow anaylsis to only promote to proper subtypes

[stereotype441]

Flow analysis currently has the rule that type promotion only occurs when the type being tested is a subtype of the previously promoted type. This can lead to counterintuitive behaviors when the type being tested and the previously promoted type are mutual subtypes (see comment from @eernstg and comment from @lrhn on dart-lang/sdk#60609).

In the discussion on that issue, the three of us agreed that it would be better to change the rule so that type promotion only occurs when the type being tested is a proper subtype of the previously promoted type. For example, this would mean that a type that has been promoted to List<Object?> cannot be further promoted to List<dynamic> or List<void>, because these three types are all mutual subtypes.

I'm filing this as a separate issue to distinguish it from dart-lang/sdk#60609, which is primarily caused by a bug in the handling of switches (dart-lang/sdk#60496).

[stereotype441]

A side benefit of this change is that it will remove some ambiguity from the flow analysis spec: currently the definition of joinV specifies that the two promotedTypes lists (p1 and p2) should be intersected, with the justification that:

p1 and p2 are totally ordered subsets of a global partial order. Their intersection is a subset of each, and as such is also totally ordered.

To see why this is ambiguous, imagine that p1 = [List<Object?>, List<dynamic>] and p2 = [List<dynamic>, List<Object?>]. The intersection of these two should contain both List<Object?> and List<dynamic>, but it is not specified which should come first.

With this change, the ambiguity disappears, because p1 and p2 become strictly ordered, therefore their intersection will have a unique strict order.

[eernstg]

I think this is actually already implied by the specification: In the definition of 'x is promotable' (via type test or via assignment), it is required that "not S <: T", that is: the current type of the variable cannot be a subtype of the type to which we're promoting that variable.

[stereotype441]

@eernstg

I think this is actually already implied by the specification: In the definition of 'x is promotable' (via type test or via assignment), it is required that "not S <: T", that is: the current type of the variable cannot be a subtype of the type to which we're promoting that variable.

Good to know, thanks!

[stereotype441]

Fixed in dart-lang/sdk@bf6ddd2.