Type inference is confusing on pattern context for List<String>.map(jsonDecode)

[whesse]

Applying type inference on
List<String> a;
[ for (final {'event': String event} in a.map(jsonDecode)) switch(event) .... ];

gives an error where the type dynamic can't be inferred for the .map call.

Changing the call to .map<dynamic> makes the error go away.

The error is rather confusing, saying that it tries the candidate dynamic but it doesn't work.
The error (from tip-of-tree 'dart analyze', also is the same on stable 3.2.3) is

error • benchmarks.dart:3575:20 • Couldn't infer type parameter
          'T'.
          
          Tried to infer 'dynamic' for 'T' which doesn't work:
            Return
          type declared as 'Iterable<T>'
                        used where 
          'Iterable<Map<_, String>>' is required.
          The type 'dynamic' was
          inferred from:
            Parameter 'toElement' declared as     'T
          Function(String)'
                                  but argument is 'dynamic
          Function(String, {Object? Function(Object?, Object?)?
          reviver})'.
          
          Consider passing explicit type argument(s) to the
          generic.
          
           • could_not_infer

1 issue found.

Sample code showing the error is below:
The code runs without error, does not fail due to type inference failure.

 

import "dart:convert";

List<String> lines = [];

class BenchmarkParseResult {
  double counter;
  
  BenchmarkParseResult(this.counter);
}

List foo(int iterations) =>
   [
      for (final {'event': String event, 'counter-value': String counterString}
          in lines.map(jsonDecode))
        ...switch (event) {
          'cycles:u' => [
              BenchmarkParseResult(
                  double.parse(counterString) / iterations)
            ],
          'instructions:u' => [
              BenchmarkParseResult(
                  double.parse(counterString) / iterations)
            ],
          _ => [],
        }
    ];

void main() {
  print(foo(1));
}

Simpler cases do not give an error:

for (Map foo in lines.map<dynamic>(jsonDecode))
for (final foo in lines.map(jsonDecode))

The simple case without the pattern (or the control-flow expression) does give an error, but it is more comprehensible.
With the pattern instead, it gives the error shown above:

for (Map foo in <String>[].map(jsonDecode)) {}
for (final {'foo': int foo}  in <String>[].map(jsonDecode)) {}

The comprehensible error tries to propagate the Map type in to the jsonDecode argument:

The argument type 'dynamic Function(String, {Object? Function(Object?, Object?)? reviver})' can't be assigned
to the parameter type 'Map<dynamic, dynamic> Function(String)'.dart[argument_type_not_assignable]
(https://dart.dev/diagnostics/argument_type_not_assignable)

@johnniwinther @athomas

[stereotype441]

Thanks for the bug report, @whesse! I dug into it, and your test case highlights a subtle difference between type inference in the analyzer and the CFE. Here's what's happening:

• Both the analyzer and the CFE agree that the pattern type schema for the pattern {'event': String event, 'counter-value': String counterString} is Map<_, String> (where _ represents the "unknown" type schema), so they analyze the expression lines.map(jsonDecode) using a context of Iterable<Map<_, String>>.
• Since lines.map is a generic function with type Iterable<T> Function(T Function(String)), they both begin a round of type inference to determine the type parameter T.
• During the downwards inference stage, the context Iterable<Map<_, String>> is matched against Iterable<T>, forming the upper constraint T <: Map<_, String>.
• A preliminary solution to the type inference is performed (resulting in T = Map<_, String>), and this is used to analyze the arguments of lines.map. So jsonDecode is analyzed in the context Map<_, String> Function(String). Since this preliminary solution contains _, it's not fixed; type inference will later try to fill in a more precise type for _.
• It so happens that jsonDecode has type dynamic Function(String). (I'm simplifying a bit here; jsonDecode also accepts an optional argument, but it's not relevant to this analysis.) This type doesn't satisfy the context (because dynamic isn't a subtype of Map<_, String>), but that's ok; in Dart's type inference, contexts are not requirements, only suggestions.
• Now, the upwards inference stage happens; in this stage, the actual type of jsonDecode (dynamic Function(String)) is matched against the argument type of Map (T Function(String)), producing the lower constraint dynamic <: T.
• The upper and lower constraints are now combined to form dynamic <: T <: Map<_, String>. This is weird, because dynamic is not a subtype of Map<_, String>. Or, put another way, the upper and lower type constraints are contradictory, because there's no type that's "above" dynamic and "below" Map<_, String>, just like there's no number that's greater than 10 and less than 1.
• But the type inference algorithm doesn't notice...yet. It carries on with its rule for choosing a type T, which is: when there are both upper and lower constraints, the lower constraint is favored, so T is chosen to be dynamic.
• Now here is the point where the CFE and analyzer have different behavior. At this point, the analyzer checks whether the type it's chosen for T satisfies the constraints. It doesn't (because dynamic is not a subtype of Map<_, String>), so it gives an error message and that's that.
• The CFE, on the other hand, doesn't bother checking that T satisfies the constraints. As far as it's concerned, the only thing the constraints were useful for is in choosing the type T. Once T has been chosen, it just runs with the choice and sees if there are any compile-time errors.
• And choosing T to be dynamic doesn't result in any compile-time errors, because dynamic is special, and can basically be used for any pattern match.

The question is, what do we want to happen? I can't find anything in https://github.com/dart-lang/language/blob/main/resources/type-system/inference.md specifying whether or not it should be an error if the set of type constraints is contradictory.

I can think of good arguments in both directions. On the one hand, if type inference comes up with contradictory type constraints, emitting an error seems like good thing, because mathematical systems like type theories are well known to behave in really weird and counterintuitive ways when trying to reason from a contradiction; it's probably better to just bail out and let the user decide what to do. On the other hand, the type produced by type inference in this case actually works just fine, and so producing an error message is really confusing for the user (as @whesse observed, the analyzer seems to be claiming that a type parameter of dynamic doesn't work, yet supplying an explicit type parameter of dynamic actually does work).

I think it's also worth considering whether we can glean some insights from this example into how type inference could be improved in the future. For example, we have been considering adding additional kinds of type schema "operators" to represent sets of types that aren't expressible using the current framework; if we had an operator coercibleTo(T) (representing any type that is usable where an expression of type T is expected), then maybe the context for the expression lines.map(jsonDecode) could have been Iterable<coercibleTo(Map<_, String>)>. Then the constraints for T would have been dynamic <: T <: coercibleTo(Map<_, String>), which isn't contradictory, because dynamic is coercible to Map<_, String>. But this idea would need a lot more careful thought.

In any case, I think these are questions for the language team.

TL/DR: if, during type inference, a set of contradictory type constraints is created, should that be a de facto compile-time error? Or should it only be a compile-time error if it leads to a set of types being chosen that cause problems in later analysis? The analyzer takes the former approach; the CFE takes the latter.

What do you think, @dart-lang/language-team?

[eernstg]

I would say that contradictory type constraints should be detected, and the situation should be considered to be a type inference failure ("could not solve the constraints").

The response to a type inference failure could vary: A compile-time error could be reported. Alternatively, dynamic could be used with every type variable whose constraints do not have a solution (if that's well-defined, we could have mutual dependencies between type variables via their bounds). I would prefer to have a warning if we do something like the latter. (I think we do both today, in different situations.)

However, I don't think we can ignore the fact that the constraints have been violated (say, if we have num <: X <: int and choose X to be num), because it could create soundness issues if an actual type argument in an instance creation or in an invocation of a generic method violates its bound. Those guys can't even be super-bounded!

[leafpetersen]

A couple of preliminary comments.

First, here's a simpler reproduction:

// The argument to this function will be checked in a context
// that looks like Map<_, String>
void mkMapContext<T>(Map<T, String> argument) {}

// This method returns a T where T is its argument type.
T id<T>(T x) => x;


void main() {
  dynamic d = <dynamic, String>{};
  mkMapContext(id(d));
}

Second: I'm not directly concerned about soundness here. Because of the dynamic nature of Dart, there are lots of places where inference (or other algorithms) may produce unsuitable types. There are type systems in which if inference succeeds, the program is well-typed: Dart does not have such a system. So in general, it is incumbent upon the front-ends to do the necessary assignability, bounds, and well-boundedness checks after inference. If they are not doing so correctly, that is of course potentially a soundness bug, but I don't think that's really the core of this issue.

Third: This is, I think, a consequence of the fact that in a few cases (mostly around implicit dynamic casts) context types are not requirements, but the subtype matching algorithm in inference essentially treats them as if they were. That is, when we have a context K and we're matching it against a type T solving for X, we treat the result as constraints on X even though in some sense it isn't a hard requirement. So for example, if K is int and T is just X, then subtype matching X <# int will yield the constraint that X <: int must be true. But that constraint is not actually a hard constraint in Dart, since choosing X to be dynamic will potentially also be a valid solution.

I don't immediately have in mind what the right answer here is. A couple of thoughts:

• We've talked about having dynamic not impose any constraints. That would "solve" this problem, but I think would cause both implementations to reject this code, since instead of dynamic, a Map type would be chosen, which would cause the jsonDecode argument to be rejected, I think.
• I think that probably the strict-inference option should reject this code as the analyzer does (indeed, I had initially thought that perhaps that the reason for the discrepancy was that the test was being run with strict-inference enabled, but that does not seem to be the case).
• I suspect that in most cases, the analyzer's additional check here will only reject code earlier, since choosing dynamic here will result in a valid solution for a type variable X only when the assignment is directly from X to something else. If the type variable is used in a composite type (e.g. Iterable<X>) then there is no valid implicit cast, and so the code will be rejected regardless. The only reason this example works is that the Iterable<X> is used in a for in loop which implicitly unwraps the Iterable before doing the assignment.

I think my weak preliminary thought is that this check should only be done when strict-inference is enabled, but I'm not sure about that. Some further analysis/discussion may be in order.

[lrhn]

I can see how we end up with dynamic <: T and T <: Map<X, String> for

void mkMapContext<X>(Map<X, String> argument) {} // Renamed type parameter to `X` to not have two `T`s.
T id<T>(T x) => x;
void main() {
  dynamic d = <dynamic, String>{};
  mkMapContext(id(d));
}

The mkMapContext imposes a context type of Map<X, String> on id(d), id imposes a context of T on d with T <: Map<X, String>, d has type dynamic so dynamic <: T.

My feeling is that it's a problem because the type system ignores implicit downcasts, and the code author does not.
The dynamic <: T is not a real requirement that can fail when the LHS is the type of an expression and the RHS is a context type. A dynamic is a valid type in that context, because it's assignable to T, whatever T ends up being, so it doesn't introduce any constraint.
It's more of a "the type was dynamic" marker than a real constraint.

I don't want to not introduce any constraint, because id(d) by itself should have type dynamic, So I probably want a different kind of constraint.
Say, for something like this, we introduce the constraint dynamic <:= T, which means dynamic has occurred and is assigned to T. That doesn't tell us what T is, but if we have no other constraint on T, we'll just use dynamic.
In either case we'll downcast the dynamic to T, which may just happen to be trivial.

Here we do have a constraint, T <: Map<X, String>.
I'd then try to solve dynamic <:= T and T <: Map<X, String> by choosing T = Map<X, String> and add the constraint dynamic <:= X. (So we'll downcast the dynamic to Map<X, String>, whatever X ends up being.)

When we then don't find any other constraints for X, we let X be dynamic, and the inference becomes:

  mkMapContext<dynamic>(id<Map<dynamic, String>>(d /* as Map<dynamic, String>*/));

I'm probably missing a lot of details, but it feels like something like this would match the actual behavior of the program, and how the auther is thinking about dynamic.
(I know I did, reading mkMapContext(id(d));, I filled in the dynamics exactly like that, solving Map<_, String> against dynamic by putting dynamic into the _, and not, e.g., using instantiate to bounds.)

[stereotype441]

@lrhn, I'm encouraged by your idea. Phrasing it another way, it seems like what you're doing is trying to encode the possibility of an implicit dynamic downcast into the type constraints, so that when it comes time to solve for the type variables, we can see that there is a solution rather than failing.

But I'm having trouble trying to generalize it so that it can apply to @whesse's initial example. Removing some non-essential parts for simplicity, we've got this:

import "dart:convert";

List<String> lines = [];

List foo(int iterations) => [
      for (final {'event': String event} in lines.map(jsonDecode))
        ...switch (event) {
          _ => [],
        }
    ];

void main() {
  print(foo(1));
}

In this case, we only have a single generic method to infer (lines.map), and the constraints are coming from:

• (downward inference, based on the incoming context) Iterable<T> <: Iterable<Map<_, String>>, therefore T <: Map<_, String>
• (upward inference, based on the type of jsonDecode) dynamic Function(String) <: T Function(String), therefore dynamic <: T

I can't figure out how to apply your <:= notation to this in a way that makes it work.

I have some ideas (along the lines of the coercibleTo operator I mentioned in my previous comment), but it seems like you might be onto something simpler than that, so I'd like to understand your approach better before diving into mine.

[lrhn]

Ack. It doesn't work because we don't actually have any dynamic-typed expressions here. We have a function context which expects a function which returns T, and a function which actually returns dynamic (not a static type, the actual reified return type of the runtime function), so in that case dynamic <: T is a strong requirement. (Which can be solved by making T be dynamic, if nothing else got in the way.)

So more cleverness might be needed. (I did say I was probably missing something.)

The implicit downcast that I, as a reader, would expect here is at the destructuring assignment.
If the lines.map(jsonDecode) would infer Iterable<dynamic>, then everything works. That's the type it would have with no context type, so if we could give it that type with a context type too, if the context type is not actually useful in inferring something else, maybe we'd be fine. There are no implicit downcasts in Then thatdynamic` element type is the type of the value assigned to the declaration.

If we had just rejected a List<Map<String, dynamic>> where we expect a Map<String, String> element type, then that would be consistent. We can't statically ensure the type.
But we allow it, even if fully typed:

void main() {
  for (var {"a": String s} in <Map<String,dynamic>>[<String, dynamic>{"a": "b"}] as dynamic ) {
    print(s);
  }
  
  for (var {"a": String s} in <Map<String,dynamic>>[<String, dynamic>{"a": "b"}] as Iterable<dynamic>) {
    print(s);
  }

  for (var {"a": String s} in <Map<String,dynamic>>[<String, dynamic>{"a": "b"}] as Iterable<Map<dynamic, dynamic>>) {
    print(s);
  }
}

These all work. A for (T v in e)... allows e to be dynamic, in which case it's downcast to Iterable<dynamic> first, and if e it's an Iterable<T2>, then T2 doesn't necessarily need to be assignable to T, it needs to be destructurable to T. That's a lot of special casing, and no wonder it's hard to figure out what to do.
I assume this comes from the specification of for/in still being by syntactic desugaring, where for (decl in expr) body becomes:

  TypeOf(expr) $iterable = expr; // Compile-time error if `TypeOf(expr)` is not assignable to `Iterable<dynamic>`.
  var $iterator = $iterable.iterator; // Compile-time error if type of `$iterator` is not assignable to `Iterator<dynamic>`
  while ($iterator.moveNext()) { // Compile-time error if type of `$iterator.moveNext()` is not assignable to `bool`
    decl = $iterator.current; // Compile-time error if type of `$iterator.current` is not assignable to `decl`.
    { body }
  }

This desugaring happens post type-inference (has to, otherwise it cannot know the type of expr, and inferring on the desugared code would not give expr the correct context type), so the inference doesn't know about this desugaring.
But the static and runtime semantics do, which is why we allow expr to be any of dynamic, Iterable<dynamic> and Iterable<Map<dynamic, dynamic>>, because we are doing multiple assignments, each one being able to do dynamic downcast independently.

So to match runtime behavior, inference would have to understand this rewrite, and match it in the inference rules. Which is probably non-trivial.

So, let's try again. We introduce S <:= T in general, meaning "S assignable to T", which can be used as type parameter bound as well, so a type parameter can be X <:= T, remembering its constraint.
Then we say that the static typing of for/in is:

Let C be the context type induced by the declaration.
Introduce a type variable $E <:= C.
And a type variable $I <:= Iterable<$E>
And then we infer the iterable expression with context type $I, to type T, and add the constraint T <:= $I

Then we try to solve. Somehow (not my speciality, I'll admit, so I'll handwave).

For the var {"a": String a} in list.map(jsonDecode) case we get:

• $E <:= Map<_, String>, $I <:= Iterable<$E>, and infer list.map(jsonDecode) with context type $I.
• The assignment-requirement of $I is Iterable<$E>, which is useful to list.map, so we decide the T of map must be dynamic <: T <: $E <:= Map<_, String>, same as today. Except that the <:= constraint allows dynamic as a solution. So we choose dynamic as the type, and get list.map<dynamic>(jsonDecode).
• Then we go back and make $I be List<dynamic>, which is assignable to Iterable<$E> if dynamic <: $E, so $E becomes dynamic too.
• And then we assign dynamic to Map<_, String>, which needs an implicit downcast. And all is well.

As I said, "hand-waving".
I don't know where we'd want to insert the $E <:= T instead of just T as context type. Anywhere and everywhere? Could be unwieldy.
And I don't know how it will interact with the placement of implicit downcasts. If anything, it'll probably delay them as long as possible, because it can keep solving with dynamic <:= T for any T, until it reaches an actual constraint, like an assignment or argument position.

And I'm also not sure this isn't just "context type hints" with a more cumbersome syntax.

[chloestefantsova]

Say, for something like this, we introduce the constraint dynamic <:= T, which means dynamic has occurred and is assigned to T.

That's an interesting proposal. If we include coercions into the notion of the assignability constraint, we may finally solve the problem of giving a formal treatment to where assignments and the related checks and transformations actually happen in expressions.

[stereotype441]

I feel like we've had a lot of good discussion here about potential future improvements to type inference to allow @whesse's example to work without having to choose a solution to contradictory type constraints. I'm definitely interested in those discussions for the long term, but they all sound like big enough changes to the type system that we'd probably want to tackle one of them as a language-versioned type inference improvement. So perhaps we should move that discussion to a separate language issue.

In the shorter term, we have a situation right now, for the current language version (and all previous language versions that are still supported) where there is a difference in behavior between the analyzer and the front end: if type inference leads to contradictory constraints, the analyzer rejects the program outright, whereas the front end "solves" the contradictory constraints by picking the "lower" constraint, and only rejects the program if that choice leads to a static type error.

I would love for us to declare one of these two behaviors to be the "correct one", and make a fix so that the two implementations match. Let me try to make a stab at the pros and cons of each approach:

1. Reject any program that leads to contradictory type inference constraints. (This is what the analyzer currently does.) Pro: seems like a good idea from first principles. Also, it encourages users to add type arguments to clarify what behavior they want. Con: it's conceivable that some program in the wild could be broken by this change. However, this is mitigated by the fact that the analyzer already rejects such a program; therefore this approach would not be considered a breaking change according to our breaking change policy.
2. Don't consider contradictory type inference constraints to be a compile-time error per se; only reject the program if the existing algorithm for "solving" the constraints (picking the "lower" constraint) leads to a compile-time error for some other reason. (This is what the front end currently does.) Pro: guaranteed not to break any existing program. Con: might conceivably cause a program to be silently accepted that really doesn't behave the way the user expects.
3. Same as 2, except that if the analyzer is in strict inference mode, it rejects the program. (This is essentially what Leaf proposed above). Pro: non-breaking just like 2, but with the additional advantage that users who have already opted into strict inference will at least be alerted to the fact that something wonky is going on. Con: users who haven't opted into strict inference won't find out that something wonky is going on.

Personally, 3 is my first choice, and 2 is my second. But I could live with any of the three options.

[eernstg]

Personally, 3 is my first choice,

I'd prefer that one as well. It could then be strengthened to 1 later on.