Consider using bounds information to restrict choices during inference

[leafpetersen]

In the presence of union types, inference may make a disjunctive choice during constraint resolution that later fails when the bounds on the type variable are checked. We might consider eagerly checking bounds to rule out infeasible choices, allowing alternative disjunctive branches to be chosen. Example due to @chloestefantsova

import 'dart:async';

foo<T extends Object>(T? t) => throw 42;

bar(FutureOr<Object?> x) => foo(x);

Note that we choose FutureOr<Object?> <: T as a solution by the right nullability rule, which later fails the bounds check, since FutureOr<Object?> <: T <: Object is not satisfiable.

If we rejected the initial constraint in the right type variable rule by checking the bound eagerly, a later choice of the left FutureOr rule would find a valid solution of Object.

cc @lrhn

[eernstg]

We've had several examples of requests for a better treatment of those near-union types, so this is certainly an interesting possibility.

Could we use a similar idea to enable a choice between T and MyClass during inference where a promoted type like T & MyClass occurs, cf. https://github.com/dart-lang/sdk/issues/43177?

I guess it is not a problem that the bound may be an F-bound: We just want to eliminate a choice whenever we can show that it won't work, and there is no soundness issue if we can't tell, and we choose a branch that turns out to fail later on.

[eernstg]

Here is an issue that matches 'using bounds information to restrict choices during inference': https://github.com/dart-lang/language/issues/3567. That issue isn't about union types, but it's certainly about using bounds information.

[leafpetersen]

Here is an issue that matches 'using bounds information to restrict choices during inference': #3567. That issue isn't about union types, but it's certainly about using bounds information.

I think that #3567 is unrelated to this, but for the record I filed #3572 as the canonical reference issue for that request. It's possible that a similar thing to what is being proposed in this issue could be applied to _ if we tracked bounds on unknown types, but I actually think that the correct thing to do is to compute the greatest closure prior to subtype matching which would have the same effect.