Cast pattern executes even when operand subpattern is refuted

[fishythefish]

Example taken from tests/language/patterns/exhaustiveness/nullable_cast_test.dart in the SDK:

import 'dart:async';

exhaustiveNonNullableFutureOrTypeVariable2<T extends Object>(FutureOr<T?> o) =>
    switch (o) {
      FutureOr<T>() as FutureOr<T> => 0,
    };

main() {
  exhaustiveNonNullableFutureOrTypeVariable2<int>(
      Future<int?>.value(null));
}

This code is currently expected to throw. I find it unintuitive that the cast in a cast pattern will execute even when the operand is refuted. Can we change the semantics so that the cast only occurs if the pattern match on the operand succeeds?

[natebosch]

AFAICT this has been the design since we first considered cast patterns. https://github.com/dart-lang/language/pull/2475

This is confusing enough that even folks on the language team don't assume the implemented semantics.

Changing this would be breaking, because it can make some exhaustive cases non-exhaustive.

[leafpetersen]

I think if you think about it, this is the only correct semantics (or at least the only consistent semantics). Patterns execute "outside in". Would you expect this program to throw?

void main() {
  Object? x;
  x = null;
  (switch (x) {
    (_ as String)? => "First",
    _ => "Second"
  });
  print ("Didn't throw");
}

It doesn't because we first test for null with the outer pattern, then run the inner pattern. If we did the other order, it would throw.

What about this example?

void main() {
  Object? x;
  x = null;
  (switch (x) {
    (String y)! => "First",
    _ => "Second"
  });
  print ("Didn't throw");
}

Would you expect that to refute or to throw a null check error?

Finally, what about this one (your example):

void main() {
  Object? x;
  x = null;
  (switch (x) {
    (String y) as Object => "First",
    _ => "Second"
  });
  print ("Didn't throw");
}

All of these have the same structure, and all of them execute in the same way: outside in. All of the other pattern forms do the same.

[fishythefish]

Ack, and maybe I'd have different intuition looking at the AST vs. the actual syntax. Of course, I don't expect us to revamp the syntax this late.

I agree with your first example. I've heard some people call the null-check pattern syntax unintuitive because ? following a type makes it nullable, but ? following a subpattern causes the subpattern to match something non-null. However, I think it's straightforward to justify: if subpattern? matches something of type int?, for example, then the ?s "cancel", and subpattern matches int. This is basically why it's called "pattern matching" in the first place. This is also intuitive if you're used to pattern matching on algebraic data types, e.g. Maybe in Haskell: appending ? to a pattern in Dart is like prepending Just in Haskell.

Despite the visual similarity to the null-check case, I actually wish your second (and third) example didn't throw. Unlike ?, ! and as are side-effectful, and no matter how much I stare at these snippets, I find it hard to intuit that these operations are actually performed on x. (But maybe I should consider these analogous to lazy patterns in Haskell and then everything sort of makes sense.)

I have a little trouble justifying the current behavior with contrived examples. After all, the ! and as could have simply been applied to x in the scrutinee expression. Our website offers slightly less contrived examples for both null-assert and cast patterns, but in both cases, the subpattern is a variable pattern, which can't be refuted, so this issue doesn't apply. Does anyone happen to have an example where the current behavior is important/intuitive and the subpattern is refutable?

[munificent]

However, I think it's straightforward to justify: if subpattern? matches something of type int?, for example, then the ?s "cancel", and subpattern matches int. This is basically why it's called "pattern matching" in the first place.

Yeah, that's basically how the pattern syntax was designed overall, as it is in other languages. List patterns look like list literals, map patterns map literals, etc. Object patterns look like (but aren't!) constructors. Using that metaphor, ? sort of makes sense.

But then you're right that in the other patterns like !, the visual metaphor sort of breaks down.

Syntax design is hard and adding syntax to an existing language doubly so. We did our best to make it intuitive and consistent, but we only got so far and at some point you have to just sort of learn it. :-/

After all, the ! and as could have simply been applied to x in the scrutinee expression.

That only works if the pattern is applied to the scrutinee and not a destructured subcomponent of it. You couldn't move the ! over to the scrutinee expression in, say, here:

void decode(List<Object?> data) {
  var [name as String, age as int, info!] = data;
}

Does anyone happen to have an example where the current behavior is important/intuitive and the subpattern is refutable?

Using ! or as with a refutable subpattern is definitely much less common. But it's not unimaginable. It's hard to come up with good synthetic examples because casts themselves are sort of hard to contrive.