Should the pattern schema context cause assignability check failures?

[chloestefantsova]

I encountered an issue working on https://dart-review.googlesource.com/c/sdk/+/277004, and I have a question about pattern schemas and how they affect type inference in expressions.

Consider the following program. The variable b has the type num and is promoted to type int. Later it is used in a pattern assignment expression. In that expression the pattern schema is computed first, and it's (int), that is, a record type with one positional field of type int. That pattern schema is used as the context for (3.14,), and when it comes to the individual fields of that record literal, 3.14 is checked for assignability to the type of the field, which is inferred to be int. That check fails, and the CFE reports the compile-time error shown below.

test() {
  var (num b,) = (0,);
  b as int;
  b.isEven;
  (b,) = (3.14,);
  //b = 3.14;
}

// /tmp/asdf3.dart:5:11: Error: A value of type 'double' can't be assigned to a variable of type 'int'.
//   (b,) = (3.14,);

However, that behavior is different from non-pattern assignment. The line b = 3.14; doesn't produce a compile-time error. Additionally, some tests expect the pattern assignment expression to be accepted by the compiler, for example, the following: https://github.com/dart-lang/co19/blob/7b4f3e723211011878e185db6fa57fbafabd6bb7/LanguageFeatures/Patterns/type_inference_A26_t01.dart#L34-L37

So, my question is which one of the two behaviors is expected from the compiler?

[chloestefantsova]

/cc @eernstg

[eernstg]

That pattern schema is used as the context for (3.14,),

That's fine, the pattern type schema (int) can be used during type inference of an expression of any type, and that's not an error (that's just like the regular assignment b = 3.14 where 3.14 would be subject to type inference with context type int). So we're accepting the mismatch between a context type schema and an expression under type inference in general (and, in particular, we must accept this kind of mismatch in cases like an assignment that demotes a local variable).

When type inference is complete, the static type of the right hand side of the assignment is used to fill in the blanks of the pattern on the left hand side. In this case it's a record pattern, which means that there are no actual type arguments, so nothing happens to the top level of the pattern. Assignability is checked for the top level, and it succeeds: The initializing expression has type (int) and the required type of the record pattern is (Object?).

The pattern is then traversed, so we visit each field and fill in missing parts, and check assignability: The first positional field has declared type num, promoted type int, and matched value type double. It should be possible to demote the variable to num and report that the required assignability exists, just like the plain assignment b = 3.14.

I don't know how the demotion of b is handled in b = 3.14, but we'd want to use a similar treatment of each identifierPattern in a patternAssignment, such that demotion can occur in a patternAssignment just like it can occur in a regular assignment.

[chloestefantsova]

Thanks for the explanation, Erik! I have a question about one detail: why is the required type of the record pattern (Object?) and not (int) or (num)?

[eernstg]

That's exactly because the required type of a record pattern should "check the shape, but not the types". It's up to the individual subpatterns to ensure assignability (after coercions and/or demotions as needed) of each field of the initializing expression unto the corresponding field pattern.

The relevant spec location is here.

[chloestefantsova]

Thanks, Erik!