Analyzer and CFE inference disagreement

[leafpetersen]

For this code:

void main() {
  int Function(int) f;
  
  List<num> l;
  var a = l.map(f);
  int x = a;
}

the analyzer infers int as the type argument to map, and with an implicit downcast on the argument to map (from int -> int to num -> int), as witnessed by this error message:

[error] A value of type 'Iterable<int>' can't be assigned to a variable of type 'int'. (../../../tmp/ddctest.dart, line 11, col 11)

The CFE infers dynamic as the type argument to map, with the result that the argument to map is invalid (a cross cast from int -> int to num -> dynamic):

file:///Users/leafp/tmp/ddctest.dart:10:17: Error: A value of type '(dart.core::int) → dart.core::int' can't be assigned to a variable of type '(dart.core::num) → dynamic'.
Try changing the type of the left hand side, or casting the right hand side to '(dart.core::num) → dynamic'.
  var a = l.map(f);
                ^
file:///Users/leafp/tmp/ddctest.dart:11:11: Error: A value of type 'dart.core::Iterable<dynamic>' can't be assigned to a variable of type 'dart.core::int'.
Try changing the type of the left hand side, or casting the right hand side to 'dart.core::int'.
  int x = a;
          ^

I believe that the CFE behavior is correct for Dart 2. We intentionally push the context type down into sub-terms and insert casts to the context type (or to the greatest closure thereof), in order to avoid relying on least upper bound with the pathologies that result (e.g. giving no error message for String x = (b) ? 3 : []).

cc @jmesserly @stereotype441 @vsmenon to check my thinking on this.

[jmesserly]

We intentionally push the context type down into sub-terms and insert casts to the context type (or to the greatest closure thereof)

In Analyzer, resolution (type inference) happens as a separate phase before checking (type casts). So when it pushes down num -> ? it doesn't have the ability to remember that on the way back up. Essentially it's just upwards inference at this point, and it ends up matching int -> int against num -> S and infers int for S.

I guess CFE sees that an implicit cast is required to num -> dynamic, thus making the argument type num -> dynamic and preventing f from providing any information about S.

This does seem like it will result in more inference of dynamic, due to the greatest closure. That said, we do issue the error in this example, and that's nice.

FWIW, this program will behave the same in CFE as Analyzer:

void main() {
  Function(int) f;
  
  List<num> l;
  var a = l.map(f);
  int x = a;
}

I don't think it would be too difficult to have Analyzer match CFE. We'd need to check the downwards context type and the argument type, and if a cast was implied, discard the argument type in favor of the (greatest closure of the) context type.

[dgrove]

@stereotype441 any thoughts on this? (there are several internal instances of this issue)

[bwilkerson]

@stereotype441 ping

[stereotype441]

I spent some time tracing through this in the debugger, and my analysis is slightly different from both Leaf's and Jenny's. TL;DR: I agree that the CFE is behaving correctly and the analyzer is wrong, but I have a different reason to believe the reason the analyzer is wrong: it's due to a difference in the subtype matching algorithm that should have been benign, but isn't benign due to issue #31792. Because of the difficulty of fixing #31792, I think we should address the difference in subtype matching behavior first.

Both the analyzer and the common front end correctly try to infer the type of f in the context (num) -> ?. Since the actual type of f is (int) -> int, what's supposed to happen is that an assignability check should be performed to see if (int) -> int is assignable to (num) -> dynamic (which is the greatest closure of (num) -> ?). Since (int) -> int is neither a subtype nor a supertype of (num) -> dynamic, there should be an error.

But that's not what happens, because of issue #31792 (which affects both the analyzer and the front end). What actually happens is that the assignability check doesn't happen until later. So both the analyzer and the front end try to solve for the type parameter of map using the impossible-to-satisfy subtype constraint (int) -> int <: (num) -> T. Both implementations decompose this into two subtype checks: num <: int and int <: T.

Then the behavior diverges: the front end, on seeing that num <: int is impossible to satisfy, aborts the processing of the subtype constraint, so it results in no constraints for T, and thus infers T=dynamic. Then it does the assignability check, and sees that (int) -> int is not assignable to (num) -> dynamic. So it reports an error on the line var a = l.map(f);. For error recovery purposes, it goes ahead with the assumption that T=dynamic, so it infers a type of Iterable<dynamic> for a, and produces an assignment error for int x = a; saying that Iterable<dynamic> can't be assigned to int.

The analyzer, on the other hand, doesn't fully verify whether a subtype constraint is possible to satisfy. (It only checks whether there are incompatible constraints on any type variables, which there aren't in this case). So after num <: int fails, it goes ahead and processes int <: T. As a result, it infers T=int. Later, when it does the subtype check, it sees that (int) -> int is assignable to (num) -> int, so it produces no error at the line var a = l.map(f);. And at the line int x = a;, it complains that Iterable<int> can't be assigned to int.

Both behaviors are wrong, but the front end behavior is benign, because it doesn't lead to any correct programs being rejected or incorrect programs being allowed (notwithstanding the examples in #31792). The analyzer behavior is bad, because it means that if we comment out the line int x = a;, the code is accepted even though it shouldn't be.

If we were to fix issue #31792, then the difference in the subtype constraint matching algorithms would be benign, since it would never even attempt to solve a nonsense constraint like (int) -> int <: (num) -> T.

Unfortunately, fixing #31792 in the analyzer is non-trivial. I think a better short-term fix would be to replicate the common front end's current subtype matching behavior in the analyzer.

[jmesserly]

my analysis is slightly different from both Leaf's and Jenny's [...]
Unfortunately, fixing #31792 in the analyzer is non-trivial. I think a better short-term fix would be to replicate the common front end's current subtype matching behavior in the analyzer.

I think we may be suggesting the same thing :). Agree a full fix for #31792 would be too much. My idea was to do to a subtype check before we match types, and if the subtype check fails, don't match types. I think that's equivalent to your suggestion?

Fixing _matchSubtypeOf directly to compute subtyping as it matches would work as well. I figured it might be a bit tricky, since it will be doing more work (computing the boolean result value), and it'll need track any implied constraints so they can be discarded or rolled back if the subtype check fails. Throwing in a quick isSubtypeOf check before calling _matchSubtypeOf seems like it might be a little easier.

But regardless I agree with your analysis, and that a fix shouldn't wait for #31792

[stereotype441]

@jmesserly Ah, I misunderstood your suggestion. Glad we are on the same page :)

Yes, I agree that doing the subtype check before we match types would be equivalent to my suggestion, and easier to implement.

I'm not assigning the bug to myself yet, since I have limited time (I'm currently recovering from the flu and I have an upcoming vacation Apr 2-20). But I've added it to my list and if I have time I'm glad to do it. Otherwise, anyone else feel free to pick it up--it should be fairly easy to find the non-recursive callers of _matchSubtypeOf and make sure they do the necessary subtype check, and add a unit test (Leaf's example without the last line should do the trick).

[devoncarew]

To update: we don't believe this is a blocking issue for beta 3, and have moved this to beta 4. @leafpetersen will look at this as a target of opportunity for beta 3; in the event that he doesn't have cycles, @stereotype441 will take up in the beta 4 timeframe once he's back from vacation.

[bwilkerson]

@stereotype441 Will you still be able to look at this?

[stereotype441]

@bwilkerson Yes, I began working on this on Tuesday and I'm hoping to have a fix ready by early next week.

[stereotype441]

Fix out for review: https://dart-review.googlesource.com/c/sdk/+/53685