Type promotion in pattern `&&`

[lrhn]

The current type inference specification for patterns use the same mathed value type for both branches of an and-pattern.

That effectively means that the and-pattern cannot promote the matched value from the first clause to the second, and use the promoted type in the second clause.
Examples where that might be valuable could be:

num? x = ...;
if (x case != null & > 0) ...
// or
if (x case int() & > 0) ...

The former can be written as (>0)?, because we have an inline null-check, the latter cannot as easily.

Users will likely expect promotion for patterns like this.

Maybe it's as easy as saying:

* **Logical-and**, `e1 & e2`: Type check `e1` using `M` as the matched value type, 
   let `R1` be the required type of `e1`.
   Then type check `e2` using **GLB**(`M`,`R1`) as the matched value type, 
   and let `R2` be the required type of `e2`. 
   The required type of `e1 & e2` is **GLB**(`M`, `R1`, `R2`).

(Don't know if the or pattern needs work too, but case == null | <= 0 on an int? might be useful as well. Can't be expressed as simply as the above, so we might want to use our entire type promotion machinery, and treat the matched value as a variable. Which it is, since we cache the value it's even final.)

The workaround, which I never want to see happen:

extension Value<T> on T {
  T get value => this;
}
...
   if (x case int(value: > 0)) ...

Removing any incentive for that workaround is motivation enough to do something!

[munificent]

Yes, I'd like this to work too. Required type isn't the right property we want to use because the required type of cast and assert patterns is deliberately wide to allow them to be used in variable declarations. But I talked about this a bit here and it should be fairly straightforward for us to define a "demonstrated type" for each pattern that would work here.

Another way we could think of it as that we could treat the value flowing into an & pattern as getting implicitly bound to a hidden local variable first that the two sides read. Flow analysis on the LHS could then promote that variable and the RHS will see the promoted type.

There may be cases where that produces better results than just specifying that we do GLB on the matched value type and LHS's demonstrated type.

[stereotype441]

Yes, I'd like this to work too. Required type isn't the right property we want to use because the required type of cast and assert patterns is deliberately wide to allow them to be used in variable declarations. But I talked about this a bit here and it should be fairly straightforward for us to define a "demonstrated type" for each pattern that would work here.

+1 to this. I actually defined a notion of "demonstrated type" in my proposal for how to apply flow analysis to patterns (circulated internally but not yet published externally), so we're definitely on the same wavelength there.

Here's how I defined "demonstrated type" from that doc:

• Logical-or: the LUB of the demonstrated types of the sub-patterns, if that’s a subtype of the matched value type. Otherwise the matched value type.
• Logical-and: the GLB of the demonstrated types of the sub-patterns, if that’s a subtype of the matched value type. Otherwise the matched value type.
• Relational: the matched value type.
• Cast: the cast type, if it’s a subtype of the matched value type. Otherwise the matched value type.
• Null-check and null-assert: the matched value type, with nullability removed.
• Constant: the matched value type.
• Variable: the variable type, if it’s a subtype of the matched value type. Otherwise the matched value type.
• List, Map, and Object: same as the required type, if it’s a subtype of the matched value type. Otherwise the matched value type.
• Record: a record type formed from the demonstrated types of the sub-patterns, if it’s a subtype of the matched value type.
  Otherwise the matched value type.

(With the caveat that LUB and GLB have some surprising counterintuitive behaviour so we might want to do something different for logical-or and logical-and patterns).

Note all the caveats above that say "if it’s a subtype of the matched value type. Otherwise the matched value type." These establish the invariant that demonstrated type is always a subtype of matched value type, which is in alignment with how we handle promotion in ordinary is tests (we only promote the variable if its newly promoted type would be a subtype of its previous type).

Another way we could think of it as that we could treat the value flowing into an & pattern as getting implicitly bound to a hidden local variable first that the two sides read. Flow analysis on the LHS could then promote that variable and the RHS will see the promoted type.

I'm wary about this for reasons I'm having trouble putting my finger on. Maybe it's because flow analysis is built to model imperative logic, and patterns are about as non-imperative as Dart gets.

I'd be more inclined to go with something more along the lines of what @lrhn proposed, but rephrasing it slightly to make use of "demonstrated type", and dropping the GLBs (which become unnecessary due to the invariant I mentioned above):

• Logical-and, p1 & p2: Type check p1 using M as the matched value type, let D1 be the demonstrated type of p1.
  Then type check p2 using D1 as the matched value type, and let D2 be the demonstrated type of p2. The demonstrated type of p1 & p2 is D2.

[munificent]

All that sounds right to me.

[leafpetersen]

This is broadly in line with my thoughts as I read through the various discussions. My guess is that GLB probably does the wrong thing more often than the right thing. The interesting case for a & b is where the demonstrated type of a is more precise than the matched value type coming in. In that case, GLB becomes just the demonstrated type. In most other cases, it seems like using GLB is more likely to just confuse things than be what you want.

I'm not sure how we associate the & and | patterns, and I think that has an impact here. If we right associate them, then I think this becomes less important, since for the common case of a & b & c, you never actually use the result of the GLB computations, whereas for (a & b) & c you would check c using the GLB of the types from a and b.

[leafpetersen]

Thinking about this in the context of #2620, I think it's worth also thinking about this for a | b, where the failure of a refines the type for b. The example is == null | var x, where if we refine the type of the matched value using the failure of the LHS to match, we get promotion to the non-nullable version of the type on the RHS. Basically, in addition to a demonstrated type, there is a failure type, which indicates the thing that is known about the matched value type if the match fails. I'm not sure this is ever very useful outside of the == null case, so it may not be worth fully generalizing, but I think it may give a nice semantic framework for thinking about this.

[leafpetersen]

A couple more comments.

First, defining the failure type for or patterns also gives a framework for thinking about improving the matched value type in successive cases. That is, I would expect that p1 | p2 and case p1: ... ; case p2: ... should behave the same. And it would be nice if switch (3 as int?) {null => false, var x => x.isEven} worked.

Second, a note on the demonstrated type. I think for constants, we can do slightly better than just preserving the matched value type. That is, I think the constant pattern null could have a failure type of NONNULL(T) where T is the matched value type, and likewise a constant pattern with non-nullable type could have a demonstrated type of NONNULL(T). In general, it would be nice if == null | p and null | p behaved the same, and similarly for other cases. For primitive types (e.g. int) where we know that the equality operator on the constant is primitive, we could further choose to promote to the type of the constant. For example, we could say that 3 | var x checks var x with a matched value type of int, no matter what the matched value type was. This is a little ad hoc - not sure if it's worth it.

Lastly, the flow analysis sketch here defines an operation called factor which might be a useful building block for defining the "failure" type.

[munificent]

First, defining the failure type for or patterns also gives a framework for thinking about improving the matched value type in successive cases. That is, I would expect that p1 | p2 and case p1: ... ; case p2: ... should behave the same. And it would be nice if switch (3 as int?) {null => false, var x => x.isEven} worked.

Yes, and there's already a natural mechanism in the proposal to hang this behavior off of: invocation keys.

We already specify that any series of invocations is cached and subsequent "calls" to that same series of invocations uses the previously cached value. That way we can soundly do exhaustiveness checks in the presence of unknown types that could mutate under the hood.

The proposal even sketches out an analogy for how that caching works by desugaring a pattern to a series of late local variables:

main() {
  var list = [1, 2];

  late final $match = list;
  late final $match_length = $match.length;
  late final $match_length_eq2 = $match_length == 2;
  late final $match_0 = $match[0];
  late final $match_1 = $match[1];
  late final $match_0_eq1 = $match_0 == 1;
  late final $match_1_lt4 = $match_1 < 4;
  late final $match_0_isEven = $match_1.isEven;
  late final $match_0_isEven_eqtrue = $match_0_isEven == true;

  if ($match_length_eq2 &&
      $match_0_eq1 &&
      $match_length_eq2 &&
      $match_1_lt4) {
    print('first');
  } else if ($match_length_eq2 &&
      $match_0_isEven_eqtrue) {
    var a = $match_1;
    print('second $a');
  }
}

We could track whenever a pattern shows that the result of some invocation key has or does not have some type. Later patterns that access the same invocation key could then potentially see the value with a properly promoted type.

Doing this right gets pretty subtle, though. Within the same case, we should be able to safely promote later accesses of the same invocation key to any type shown by previous uses of that invocation key in that case. We know we can only get to the later ones if the previous ones matched.

Across cases is harder. This should be valid:

switch (3 as int?) {
  case null: print('null');
  case var x: print(x.isEven);
}

But this isn't:

switch ((3 as int?, 4)) {
  case (null, 5): print('null');
  case (var x, _): print(x.isEven);
}

Because here we only know that the previous case failed if we reach var x. We don't know that it failed because of the parallel null test. So doing negative promotion across cases will likely only work if the previous case has no other predicates that could possibly fail. That may be so brittle that it's not worth doing at all.

Even so, I do think it makes sense to do positive promotion within a single case, and I think invocation keys might be the right thing to hang that off of.

[stereotype441]

We could track whenever a pattern shows that the result of some invocation key has or does not have some type. Later patterns that access the same invocation key could then potentially see the value with a properly promoted type.

My only concern here is that it's a bunch of additional flow analysis work. Maybe that's a good thing though--a deep understanding of how flow analysis works is mostly siloed in my brain right now, and work like this might be a good excuse for someone else to become more familiar with it.

Doing this right gets pretty subtle, though. Within the same case, we should be able to safely promote later accesses of the same invocation key to any type shown by previous uses of that invocation key in that case. We know we can only get to the later ones if the previous ones matched.

Across cases is harder. This should be valid:

switch (3 as int?) {
  case null: print('null');
  case var x: print(x.isEven);
}

But this isn't:

switch ((3 as int?, 4)) {
  case (null, 5): print('null');
  case (var x, _): print(x.isEven);
}

Because here we only know that the previous case failed if we reach var x. We don't know that it failed because of the parallel null test. So doing negative promotion across cases will likely only work if the previous case has no other predicates that could possibly fail. That may be so brittle that it's not worth doing at all.

I'm actually less concerned about this. This is precisely the sort of thing that flow analysis already does really well, and I think it will just fall out of the algorithm.

[munificent]

@stereotype441, my understanding is that the type promotion stuff you're doing for patterns does handle this. Is there anything I need to do in the proposal for this? Can I (or you if you want the satisfaction) close the issue?