Weird type inference issue about sdk

[lukehutch]

Also, even for the first code example, if you replace String with int, the problem goes away, which is even more bizarre (I thought all types were treated more or less the same way by Dart...)

[lrhn]

The reason is pretty certainly that the context type of the part list literal is the empty context, _.
That makes the induced element type of the list also be _, which makes the context type of the spread expression be Iterable<_>. But maybe it's _ in the analyzer instead. Sounds like one of the differences @stereotype441 has looked at.

That difference in context type, combined with how inference works for ?? can explain what you see.

If ?? has a non-_ context type, then that becomes the context type of the second operand, so a context type of Iterable<_> makes the final [] infer as <dynamic>[].
A context type of _ makes ?? use the static type of the first operand, made non-null, as context for the second operand. Since the static type of the first operand is List<String>?, that makes the [] infer as <String>[].

Then the type of the ?? becomes List<dynamic> in one case and List<String> in the other, which propagates all the way out to the type of result.

The reason changing it to an arrow function makes a difference, is that the expression gets the return type as context type.

[lukehutch]

I didn't fully understand that, but VS Code shows no error, so the analyzer seems to be doing the intuitively right thing there. Why does the compiler have different behavior? There should be no behavioral difference between the two. I would also expect there to be no behavioral difference between the lambda and non-lambda case.

[eernstg]

Here's a very practical approach:

Consider an expression e that has a surprising static type. Inspect the subexpressions of e (including e itself) in order to detect whether they accept any actual arguments, but no such type arguments have been provided. In general, those missing type arguments will be provided implicitly by type inference.

Now provide those actual type arguments explicitly (expressing your intentions about those types). It's often enough to provide just one actual type argument list, and the rest then get inferred as desired, otherwise keep providing more actual type arguments until e has the expected static type (or it has a different type, which is now understood in more detail).

There's nothing wrong in providing actual type arguments — Dart type inference involves subtyping, and this means that there are no principal typings (there's no "universally best" choice of actual type arguments), and hence there may be a genuine need to provide some actual type arguments even in the most beautifully designed program.

For the original example, I'd recommend a simplification:

Map<int, List<String>> names = {};

List<String> getNames(int id) {
  var result = names[id] ?? [];
  return result;
}

This simplification allows the built-in choices in the type inference algorithm to get it right, so the static type of result will be List<String>, as desired.

However, if you really need to have the spread element and the enclosing list literal then you can provide a single actual type argument (bottom up):

Map<int, List<String>> names = {};

List<String> getNames(int id) {
  var result = [...names[id] ?? <String>[]];
  return result;
}

The point is that names[id] is well typed already, but [] relies on type inference for its element type (so you'd often want to make that type argument explicit, because the static analysis has no information when it encounters [], except for that 'context type' which is a term that denotes the requirements from the "receivers" of the value of this expression).

You could also provide an actual type argument for the enclosing list:

Map<int, List<String>> names = {};

List<String> getNames(int id) {
  var result = <String>[...names[id] ?? []];
  return result;
}

This is again sufficient to make the type inference find the desired type arguments everywhere. However, it relies on type inference, and you do get more direct control over the typing if you use a bottom-up approach.

Finally, the most elegant and declarative approach could very well be to provide a suitable context type at the very top level, that is, as the declared type of the whole declaration:

Map<int, List<String>> names = {};

List<String> getNames(int id) {
  List<String> result = [...names[id] ?? []];
  return result;
}

This will again provide the right input to the type inference algorithm to get everything right (it's doing exactly the same thing as List<String> getNames(int id) => [...names[id] ?? []];, namely, providing a context type for the expression as a whole).

However, if you started looking into this topic exactly because type inference did not produce the expected and desired typing then you may be able to maintain more direct control of the typing by providing some type arguments in a bottom-up fashion.

[eernstg]

Oh, @lukehutch, and then perhaps read @lrhn's comment again, with these practical considerations in mind. ;-)

[lukehutch]

@eernstg yes, I am fully aware that providing type constraints ("bottom-up" as you phrase it) can cause type inference to work in cases like this, and in fact that's exactly how I solved the problem in my code before filing this issue. But I still filed the issue, because of the two problems I raised in my previous comment. There are what appear to the casual observer to be inconsistencies in behavior here.

I see type resolution to be a constraint satisfaction problem here, not a top-down vs bottom-up issue necessarily, and here there is only one "reasonable" interpretation of the type (one way that the type can be constrained) -- which the analyzer seems to find in the block case, and both the analyzer and the full ccompiler seem to find in the lambda case.

[eernstg]

that's exactly how I solved the problem in my code before filing this issue

@lukehutch, I'm sorry, I didn't intend to imply anything to the contrary!

By the way, I didn't mention the additional issue about the analyzer and the CFE arriving at different results. That's presumably a consequence of the issue reported as dart-lang/language#3650. The tools shouldn't disagree, and that is being fixed.

I see type resolution to be a constraint satisfaction problem

Dart type inference does indeed involve constraint solving.

However, it is still a fact that there's a lot of flexibility in the solution space for this constraint solving process. We could satisfy all the constraints of the declaration of result as follows, where T is any type which is a supertype of String, and S is any type which is a subtype of T (which is an infinite set):

Map<int, List<String>> names = {};

List<String> getNames(int id) {
  var result = <T>[...names[id] ?? <S>[]];
  return result;
}

So T could be dynamic or String? or FutureOr<Object> or a bunch of other things, and S could then be chosen from an infinite number of different values, it just has to be a subtype of T.

Many of these choices will make it an error to return result;. However, it's a fundamental design choice for Dart type inference that it is done for one expression at a time, not, e.g., for an entire function body for all missing type arguments simultaneously.

Dart uses some heuristics in order to make a choice (see this document for a more detailed and precise description of Dart type inference).

I suspect that the failure that you experienced will go away when dart-lang/language#3650 has been resolved.

However, I do not think we will ever have a situation where no Dart type inference results differ from the choice that the developer expected and desired, there will always be cases where the heuristics fail and some type arguments must be provided explicitly.

[lrhn]

What Erik says!
But just for completeness, the optimal solution here would be null-aware spread: [...? names[id]].

[lukehutch]

But just for completeness, the optimal solution here would be null-aware spread: [...? names[id]].

OK, that's a very cool language feature that I didn't know about! Thanks!

Dart type inference does indeed involve constraint solving.

Wow, I didn't realize it was that complex. Thanks for the links.

S could then be chosen from an infinite number of different values, it just has to be a subtype of T.

That's exactly what I would expect. However, absent some other constraint, I would expect in this case that S == T, i.e. S be the maximally general subtype of T.

However, I do not think we will ever have a situation where no Dart type inference results differ from the choice that the developer expected and desired, there will always be cases where the heuristics fail and some type arguments must be provided explicitly.

That makes perfect sense. If at the very least VS Code's error and warning displays could be brought into alignment with the compiler errors and warnings in all circumstances, I would be significantly happier here! Hopefully fixing that bug you linked will help with this specific situation.

Although I would also love to see the behavior in the lambda case brought into alignment with the behavior in the block code case. That presumably will not be fixed by the issue you linked. So maybe this issue I filed should be about that specifically.

[lrhn]

I would expect in this case that S == T

And it is. It's just that, depending on implementation, S may be dynamic, because [] is inferred in a context of type Iterable<_>, which doesn't limit they element type. If neither T nor S is supplied, there are lots of valid choices, even if they are equal.

If you write: var name = names[id]; var result = [... name != null ? name : []];, you should not be surprised that [] gets inferred as <dynamic>[], where the name branch has type List<String>. Then the result is List<UP(String, dynamic)> = List<dynamic>.

The names[id] ?? [] is very close to being the same thing as that, only with one extra heuristic added to inference, which only kicks in when there is no context type for the ?? expression. In that case, and only that case, will it use the non-null static type of the first operand as context type for the second operand.

What you see here is that one tool thinks it's in that special case, and the other doesn't. (That's a bug that will get fixed.)

[eernstg]

Just a couple of additional comments ...

I would expect in this case that S == T

Here's a section containing a few rules that allow the type inference algorithm to choose a result in the situation where we have many solutions available: https://github.com/dart-lang/language/blob/main/resources/type-system/inference.md#constraint-solution-for-a-type-variable.

The general gist of these rules is that we prefer to use the subtype rather than the supertype, if it is known. Otherwise we prefer the supertype, if it is known. Otherwise we choose the subtype (that is: subtype schema), unless it is completely unknown (that is, _). Otherwise we choose the supertype (even if it is not fully known, and even if it's completely unknown).

So with _ <: S <: T where S is a type variable that we're solving for and T is a known type, we'd bind S to T, as you mention.

However, we cannot always rely on choosing the most special or the most general type:

class A<X extends A<X>> {}
class B extends A<B> {}
class C extends B {}

void f<X extends A<X>>(X x) {}

void main() {
  f(C()); // Error, can't infer `X`.
  f<A<A<A<A<... /*infinitely*/ ...>>>>>(C()); // Well, an infinite type won't fit in 80 chars.
  f<B>(C()); // OK!
}

In this particular situation we should be able to use a heuristic (Kotlin finds a solution in a similar situation, and surely we'll sort that out), but we can't expect to have a complete solution in all situations.

The decidability and tractability issues connected with type inference for a language with subtyping are discussed in various papers, but Colored local type inference is particularly relevant to the approach taken in Dart, and Type inference with simple subtypes pretty much laid the foundation for this topic.

would also love to see the behavior in the lambda case brought into alignment with the behavior in the block

There's nothing special about the function body that starts with =>, the thing that matters is that the expression returned by that function has a non-trivial context type (which is the declared return type). You'd get exactly the same effect from declaring the type of the local variable:

Map<int, List<String>> names = {};

List<String> getNames(int id) {
  List<String> result = [...names[id] ?? []];
  return result;
}

[johnniwinther]

cc @chloestefantsova

[eernstg]

Perhaps this is as duplicate of dart-lang/language#3650? In that case @stereotype441 may already be working on a fix.

[chloestefantsova]

Perhaps this is as duplicate of dart-lang/language#3650?

I believe it is.

[lukehutch]

Here's another (probably) related example that I just ran into:

Shared code for the below examples:

class X {}

Future<List<X>> getXs() async => [X(), X()];

(1) Working case:

Future<List<X>> getXsOrEmpty(bool returnEmpty) async {
  return returnEmpty ? [] : await getXs();
}

(2) Non-working case (A value of type 'List<dynamic>' can't be returned from the function 'getXsOrEmpty' because it has a return type of 'Future<List<X>>'.):

Future<List<X>> getXsOrEmpty(bool returnEmpty) async {
  final result = returnEmpty ? [] : await getXs();
  return result;
}

At least from a user point of view (and even a usability point of view!), there should be no difference in the type inference behavior between these two examples.

The fix for the non-working case involves giving [] the type parameter:

  final result = returnEmpty ? <X>[] : await getXs();

[lrhn]

At least from a user point of view (and even a usability point of view!), there should be no difference in the type inference behavior between these two examples.

But there is.
Dart type inference is at the expression level, and it's one-pass. It does not look ahead to see how a variable being declared will later be used, and when it does see that later, it does not go back and change earlier decisions.

final result = returnEmpty ? [] : await getXs();

When the compiler is inferring this line, it doesn't know that the variable will later be returned and will then need to be a List<X>.
From only this context, there are no requirements, and choosing to infer <dynamic>[] for the list literal. Nothing it has seen so far suggests otherwise.

Moving an expression into a different context can affect type inference, since inference uses the context.
What means there is a very real difference between the two examples, because one expression has a completely different context type. It's just not the same program.

The fix is to insert the otherwise inferred type argument, because that makes the moved expression independent of the context.

[lukehutch]

Right, but the same fundamental type constraint satisfaction rules could work across the entire graph structure of the program, as long as type resolution proceeds monotonically (by propagating a wavefront of "dirty nodes" as each type becomes more constrained, like in a dynamic programming algorithm), rather than working linearly and unidirectionally as it does now.

Again I am referring only to the end user experience and expectation of using Dart. A user should not have to understand the subtlety of what you explained (and, consequently, I'm sure this is not the last time someone will file a bug related to the current behavior).