I would like to propose that we add a new rule to the definition of UP just before the rules about intersection types, namely:
UP(X & B1, X & B2) =
B3, if B3 is a proper subtype of the bound of X,
where B3 is UP(B1a, B2a),
and B1a is the greatest closure of B1 with respect to X,
and B2a is the greatest closure of B2 with respect to X,
where the greatest closure is as defined in [inference.md].
X, otherwise.
The point is that the current rules cause UP(X & int, X & num) to yield X, but X & num is a result which is still sound, but more useful.
I would expect this change to be non-breaking in practice, but it is of course breaking in principle because it will change the type of some expressions (and in particular: some local variables) to a slightly more precise type.
munificent
commented
8 months ago
See https://github.com/dart-lang/sdk/issues/54013 for some background information.
I would like to propose that we add a new rule to the definition of
UPjust before the rules about intersection types, namely:The point is that the current rules cause
UP(X & int, X & num)to yieldX, butX & numis a result which is still sound, but more useful.I would expect this change to be non-breaking in practice, but it is of course breaking in principle because it will change the type of some expressions (and in particular: some local variables) to a slightly more precise type.