Flow analysis unnecessarily demotes for-each loop variables

[stereotype441]

The following code is currently rejected by flow analysis:

void forEachWithoutDeclLoopVar(Object x) {
  if (x is int) {
    x.isEven; // Verify that promotion occurred
    for (x in [0]) {
      x.isEven; // ERROR: `Object` has no method `isEven`
      break;
    }
  }
}

It seems like we should be able to do better than this, because [0] should be inferred as <int>[0], and therefore the implicit assignment to x in the for-each loop should not undo the promotion.

[stereotype441]

@johnniwinther I wasn't sure whether to classify this as area-front-end or area-analyzer since it's in _fe_analyzer_shared. I'm happy to work on this.

[johnniwinther]

I'm using epics more that area now so it's ok for me that it's area-front-end given it has the (now shared) Flow Analysis epic.

[leafpetersen]

@stereotype441 is this still planned?

[stereotype441]

I'm still hoping to get to this. There are a few related bugs with the treatment of "for each" loop variables that can probably all be fixed at once. But time is running short so I'm not 100% certain I will get to it before the beta release.

[stereotype441]

Looking into this more deeply, the problem is in the way type inference interacts with flow analysis. When type inference visits the loop for (x in [0]), it uses the declared type of x to figure out the context type it should use for inferring the type of [0]; the declared type of x is Object, so the context is List<Object>, and hence [0] is inferred as <Object>[0]. So the iterated values have static type Object, and hence the assignment of the iterated value to x demotes it.

I think what should happen instead is that the promoted type of x should be used to figure out the context type for [0], so the context will be List<int>, hence [0] will be inferred as <int>[0], and the iterated values will have static type int, and the assignment of the iterated value to x won't demote it. The reason I think it's better to use the promoted type is by analogy with how we handle ordinary assignments to promoted variables; had the program instead looked like this:

void f(List<Object> x) {
  if (x is List<int>) {
    x.first.isEven;
    x = [0];
    x.first.isEven;
  }
}

there would have been no error, because we would have used the promoted type List<int> as the inference context for inferring the type of [0].

@leafpetersen does this seem reasonable to you?

[eernstg]

I think it's already nearly a code smell to use an existing variable as the "counting" variable of a for statement, and we should probably expect some corners of the semantics in that case to be somewhat quirky.

In particular, I think that a local declaration like for (num i in [0]) makes it reasonable to say that num may influence the typing and semantics of [0]. But the remote case for (x in [0]) that we're focusing on here makes it much less readable because the typing of x (especially with promotion) isn't visible locally.

One obvious question to ask is what we will do about demotion:

void forEachWithoutDeclLoopVar(num x) {
  if (x is int) {
    x.isEven; // Verify that promotion occurred.
    for (x in [0]) {
      ... // Lots of stuff, then 50 lines later:
      x = 0.5; // `x` demoted to `num`; does this imply that `[0]` is `<num>[0]`?
    }
  }
}

Another inconvenient corner is promoted type variables:

void forEachWithoutDeclLoopVar<X extends num>(X x) {
  if (x is int) {
    x.isEven; // Justified by promotion to `X & int`.
    for (x in [0]) { // Error: `int` not assignable to `X`.
      x.isEven; // Error: `num` does not have an `isEven`.
    }
  }
}

I believe the use of the promoted type as the basis for the context for [0] would make it a List<X> (because we can't reify X & int), and then we wouldn't be able to have a 0 in the list because int isn't assignable to X.

I would actually recommend avoiding this tar pit as much as possible. I don't know about the breakage, but we might be able to say that an existing variable simply doesn't provide a context type for a for iterable at all.

Keeping the current behavior where the context type is based on the declared type of the existing variable seems slightly inconsistent (which is presumably the reason why this issue was created in the first place), but I still think that it's less confusing than the approach where we use the promoted type.

[stereotype441]

@eernstg

I think it's already nearly a code smell to use an existing variable as the "counting" variable of a for statement, and we should probably expect some corners of the semantics in that case to be somewhat quirky.

Agreed. I kinda wish the language didn't allow this at all.

In particular, I think that a local declaration like for (num i in [0]) makes it reasonable to say that num may influence the typing and semantics of [0]. But the remote case for (x in [0]) that we're focusing on here makes it much less readable because the typing of x (especially with promotion) isn't visible locally.

One obvious question to ask is what we will do about demotion:

void forEachWithoutDeclLoopVar(num x) {
  if (x is int) {
    x.isEven; // Verify that promotion occurred.
    for (x in [0]) {
      ... // Lots of stuff, then 50 lines later:
      x = 0.5; // `x` demoted to `num`; does this imply that `[0]` is `<num>[0]`?
    }
  }
}

My preference (and what I've implemented in https://dart-review.googlesource.com/c/sdk/+/162625) is that the type of [0] is inferred based on the promoted type of x on entry to the loop, so it would still be inferred as <int>[0]; it isn't demoted back to num until x = 0.5; is reached. I think that behavior makes sense if you think of how the loop is desugared:

T id1 = [0];
var id2 = id1.iterator;
while (id2.moveNext()) {
  x = id2.current;
  {
    ... // Lots of stuff, then 50 lines later:
    x = 0.5; // `x` demoted to `num`; does this imply that `[0]` is `<num>[0]`?
  }
}

We already have an inference rule for explicit assignments that uses the promoted type as the context, so if the user had written this code directly, the context for id2.current would have been int. I don't think it's a very big mental leap to expect this context to be wrapped in Iterable<> and applied to the iterable expression [0], because that's what we would have done if x had been a fresh variable of type int.

Another inconvenient corner is promoted type variables:

void forEachWithoutDeclLoopVar<X extends num>(X x) {
  if (x is int) {
    x.isEven; // Justified by promotion to `X & int`.
    for (x in [0]) { // Error: `int` not assignable to `X`.
      x.isEven; // Error: `num` does not have an `isEven`.
    }
  }
}

I believe the use of the promoted type as the basis for the context for [0] would make it a List<X> (because we can't reify X & int), and then we wouldn't be able to have a 0 in the list because int isn't assignable to X.

True, but we would have had precisely the same problem if we'd used the declared type of x as the basis for the context for [0], so I don't think this example tips the scales in either direction.

I would actually recommend avoiding this tar pit as much as possible. I don't know about the breakage, but we might be able to say that an existing variable simply doesn't provide a context type for a for iterable at all.

Do you have a motivating example for this idea? I don't believe it helps your promoted type variables example, because if we say that x doesn't provide any context for inference of [0], then it gets inferred as <int>[0], so it's still an error.

[eernstg]

I think that behavior makes sense if you think of how the loop is desugared

T id1 = [0];
var id2 = id1.iterator;
while (id2.moveNext()) {
  x = id2.current;
  {
    ... // Lots of stuff, then 50 lines later:
    x = 0.5; // `x` demoted to `num`; does this imply that `[0]` is `<num>[0]`?
  }
}

Right; the language specification doesn't say anything about the inference step on the iterable, but I don't think it will be hard to come up with a handful of context types (with cases T x in e, var x in e, x in e). So we would perform inference on e with that context type, yielding a new e1 of static type T, and then that's the T that we are using in the desugaring. So we should be able to keep the desugaring unchanged with null safety, and just add text about how we find T.

The models are now easy to express: We can use the promoted type of x at the beginning of the loop (or the beginning of the desugared code) as the context type, or the declared type, or we can use the empty context.

I'm not quite sure which model wins on consistency (we don't have any other mechanism in Dart where we are using exactly the same steps to find a context type), but it's probably not a big issue in practice. (Because developers will be nice and avoid writing code using the case x is e in the first place ;-).

We already have an inference rule for explicit assignments

I think we might want to make the element type of the iterable a type of interest: If the developer uses an iterable of S where S is a proper subtype of the declared/promoted type of x then I'd consider it useful and meaningful to get a promotion to S at the implicit assignment (if all the other constraints on promotion are satisfied, of course).

void forEachWithoutDeclLoopVar(num x) {
  x = 3.16; // The treatment of `x` doesn't help us getting to `int`.
  for (x in <int>[0]) { // But we _will_ assign int values to `x` in the loop.
    x.isEven; // So let's promote.
  }
}

If we take the original example then the effect would simply be that the assignment does not demote the variable, which means that we avoid contradicting the type which was flowing from x into the iterable, now when it comes back to x:

void forEachWithoutDeclLoopVar(num x) {
  if (x is int) {
    x.isEven; // Verify that promotion occurred.
    for (x in [0]) { // Assume this is inferred as `<int>[0]`.
      // Implicit assignment "x = id2.current" preserves promotion.
      x.isEven; // OK.
    }
  }
}

The promoted type int of x would influence the type T in the desugared code (turning [0] into <int>[0], and giving T the value List<int>), so id2.current would have the type int (and we don't use the context type because that expression is not subject to inference), and then x just keeps its promoted type after x = id2.current.

True, but we would have had precisely the same problem if we'd used
the declared type of x as the basis for the context for [0],

That is true. My point was that the promoted type didn't help us, even though it was good enough to allow x.isEven just one line earlier, and that may seem inconsistent and confusing.

I still suspect that we can avoid some confusion if we simply say that x in [0] does not provide a context type for the inference step applied to [0].

Do you have a motivating example

The motivation is not a specific example, it's the underlying principle: If we do not provide a context type for the iterable in the case x in e then e will be subject to inference in the same way even if we change the treatment of x slightly, and hence change the promoted type of x at the beginning of the loop.

This makes the code more stable, and it may force developers to be a bit more explicit on the type of the iterable (they may need to pass a type argument explicitly), and in this case I actually think that's a plus.

[leafpetersen]

I don't see a very good motivation for ignoring the promoted type here. In all other cases that I can think of where we use a variable, we use the promoted type of a variable to generate the context, it feels very inconsistent to ignore it here. Given that this is trivial to implement (in fact, already implemented) I'm in favor.

[eernstg]

Using the promoted type is more consistent, and we can lint the use of an existing variable in the first place.