Adjust type inference of `??` in the empty context

[eernstg]

Thanks to @osa1 for bringing up this topic!

The expression e1 ?? e2 infers the type of e2 in the context type schema of the whole expression, if there is one. However, when there is no context type schema for the entire expression (that is, it's _), the static type of e1 is used as the context type schema for e2.

This implies that we get a more imprecise inference result when the type of e1 isn't greater or equal than the type of e2. For example, e1 could be a List<...> and e2 could be an iterable:

Iterable<X> getIterable<X>() => <X>[];

void main() {
  final List<int>? xs = null;
  var ys = xs ?? getIterable();
  print(ys.runtimeType); // `List<dynamic>`.
}

We could change the computation of the context type schema for e2 when e1 ?? e2 occurs in the empty context _:

Let S be the static type of e1 (inferred in the empty context _). Let S1 be the union-free erasure of S (so if S is List<T>? then S1 is List<T>, and similarly for FutureOr). If S1 is not an interface type then the context type for e2 is NonNull(S). Otherwise, let S2 be the unique type in the superinterface graph of S1 which has the greatest depth, and is also a supertype of the most special generic instantiation of the type of e2 after union-free erasure. If there is no such type then e2 again gets context type NonNull(S). Otherwise, let S3 be S2 with the union types of S added back in. Then NonNull(S3) is used as the context type for the inference of e2.

Edit: Computing S2 may incur approximately the same amount of work as performing type inference, so we might want to do something which is simpler, and a conservative approximation.

Note that S is actually a type, not a type schema, because it is the result of inference on e1. Also note that "unique, with the greatest depth" is the same criterion as the last item in the computation of UP, that is, the Dart 1 algorithm for the computation of the "least" upper bound. However, the treatment of type arguments in the type of e2 is different: They are essentially ignored. So we're looking for the most special (hence: most informative) supertype of the type of e1 for which we can hope to make the static type of e2 a subtype using inference.

In the example above, S is List<int>?, S1 is List<int>, S2 is Iterable<int>, and S3 is Iterable<int>?, which means that Iterable<int> is used as the context type for the inference of getIterable(), yielding getIterable<int>().

See #4518 for a situation where this really matters.

@dart-lang/language-team, WDYT?

[lrhn]

Using the union-free type will give be the NonNull I have wanted.
I don't know if removing a FutureOr is always desired. If you do maybeFutureOr ?? Future(...), then you may want the FutureOr<X> context type to guide the type inference of Future.

and is also a supertype of the most special generic instantiation of the type of e2 after union-free erasure.
...
Then NonNull(S3) is used as the context type for the inference of e2.

The text seems to use the type of e2 before it's inferred, so type inference of e2 depends on type inference of e2.

I think the best we can do is to take the static type of e1, remove nullability if possible (since the operator is ??), and then infer e2 in that context.

What we can then do is to change inference so that if you try to infer T for Iterable<T> with a "deniable context" of List<int>, it chooses Iterabler<int> (because the context type implements Iterable<int>, and we don't have to be assignable to it, but we should try to be as compatible with it as possible, otherwise why have a context).

This way the UP will be Iterable<int>, instead of ignoring the context and inferring Iterable<Object?>, and then etting that from the UP.

[eernstg]

The text seems to use the type of e2 before it's inferred, so type inference of e2 depends on type inference of e2.

No, we're not using the type of e2, we're using the set of types that e2 can have after inference. That is, we consider the set of all possible types that e2 has, if we give it all combinations of all bound-conforming type arguments at all locations where it accepts an actual type argument but none is specified, or it has a function literal with a parameter that does not have a declared type.

Then we're asking for a type in the superinterface graph of S1 which is a supertype of at least one of those potential types of e2. I specified that we should use the least type in this set of types, which may be a less powerful criterion than "must be a supertype of at least one of them" (because the least element may not exist), but in practice that's going to be something like List<Never> or Never Function(Object?), so I think it's OK.

I think the best we can do is to take the static type of e1, remove nullability if possible (since the operator is ??), and then infer e2 in that context.

That's the current approach, I'm trying to improve on that.

What we can then do is to change inference

That's exactly what I'm trying to avoid, because I expect that approach to be a much, much deeper change to the inference algorithm.

But you're right that we might want to do a similar thing for assignments to promoted variables in the case where the assigned expression isn't assignable to the current type of the variable. That's particularly useful in the case where a promotion has brought up one or more actual type arguments that aren't present in the declared type:

Iterable<X> getIterable<X>() => <X>[];

void main() {
  Object o = <int>[];
  if (o is Iterable<num?>) {
    // Now `Iterable<num?>` is a type of interest.
  }
  if (o is List<num?>) {
    o = getIterable(); // Inferred as `getIterable<dynamic>()`.
    print(o.runtimeType); // 'List<dynamic>'.
  }
}

The proposal would be to use context type Iterable<num?> and infer getIterable<num?>().

[eernstg]

The notion of "find the least element in the set of possible types obtained by type inference on e2" needs some amount of scrutiny (and it's new to the type inference algorithm, so it needs implementation as well ;-).

For example (thanks to @chloestefantsova for coming up with this):

X foo<X>(X x) => x;

void main() {
  e1 ?? foo(e3).bar();
}

In this example, the type of foo(e3) is going to be the inferred value of the type argument X (because that's the return type of foo). With the current inference we'd infer foo(e3) in the empty context and then get a result T for X, and that's the type of e3 as well as the type of foo(e3). Next, we inspect the interface of that type T and check that it has a bar member, which yields the type of foo(e3).bar(); and so on. This gets more complex if we consider receiver type inference, but it already illustrates that we can't hope to find "the least possible type produced by type inference" by anything which is substantially less complex than the full type inference algorithm, especially if we include receiver type inference.

We can handle special cases (a list literal can yield List<Never>, and similarly for other collection literals, and a constructor invocation C(...) can yield C<Never, Never, ... Never>), and the ultimate fallback can always be Never.

This would work (and it would probably handle the most common cases nicely), but it is not very principled.

I'm not convinced that there is a beautiful and complete solution to this issue in considering the reverse constraint (that is, in some specific situations using not just P <# Q [L] -> C, but also Q <# P [L] -> C when generating constraints). This would allow us to find a solution when the type of e1 is a subtype of the type of e2 in an expression like e1 ?? e2, but it won't work if the two types are incomparable:

sealed class A<X> {}
class B1<X> extends A<X> {}
class B2<X> extends A<X> {}

void main() {
  var x = B1<int>() ?? B2();
}

In this case there is no type argument S that will make B2<S> a subtype of B1<int>, and also no type argument that makes B2<S> a supertype of B1<int>. But if we could find the relevant supertype A<int> then inference would proceed just fine to turn B2() into B2<int>().

[lrhn]

The notion of "find the least element in the set of possible types obtained by type inference on e2" needs some amount of scrutiny

That sound probable. It seems to assume that e2 has a recognizable structure where all type inference will do is infer type arguments to something. That is, the basic structure of the static type can be derived from the syntax, we just have to figure out the type arguments.

If it's not, like the foo().bar() example, we need to know the static type of foo() to even know which type arguments bar might have. In the presence of extension members, that may depend on the exact type of foo(), List<String> and List<int> may have completely unrelated bar members.

(That's why I think it's safer to not start pondering about what types an expression may have before type inferring it.)

[eernstg]

Good point! ;-)

[Reprevise]

Would it be possible to fix the for loop variable being typed dynamic instead of String?

List<String>? items = null;
for (final item in (items ?? [])) {
  // 'item' is of type 'dynamic' instead of 'String' because the empty list is of type 'List<dynamic>'
}

[lrhn]

Would it be possible to fix the for loop variable

Anything is possible, but this one is a different issue. The problem here is that the expression has a context type scheme, which should be Iterable<_>.

Just like for (var x in y = e)..., there is an expression whose value is going to be used for two things, but we can only give it one context type scheme when we do inference.

That means that satisfying one context may make choices incompatible with the other context.

For ??, the context you get from the first operand is just a suggestion, not a requirement, but the context from the actual context may be a requirement, so we prefer the outer context.

So [] is type-inferred with a context of Iterable<_>, so it infers <dynamic>[].

To fix that, inference of ?? should either always use the non-nullable type of the first operand (not totally bad idea, since that type should always be assignable to the context type anyway), or it should somehow have access to more than one context type (maybe up to one required type, zero or more aspirational types, which it tries to satisfy too if possible).

The latter is just a loose idea, and may not make sense in practice.
The former is a change, and therefore a breaking change, but I think it might be worth it. The cases where you don't want something of the same type as the first operand, but where you could infer something of that type in the right context, feel hypothetical at best.