Type inference should consider asserts

[jamesderlin]

As I mentioned earlier in #35019, given assert(variable is Type), I would like variable to be inferred as Type.

@Hixie also mentioned this in #32360 (comment).

(I noticed #4410 also requested this, and it was apparently fixed, but I'm not sure if it regressed or if that was specific to DartPad or something.)

Additionally, the documentation for the avoid_as lint states:

If you know the type is correct, use an assertion or assign to a more narrowly-typed variable (this avoids the type check in release mode; as is not compiled out in release mode). If you don't know whether the type is correct, check using is (this avoids the exception that as raises).

Maybe "use an assertion" there doesn't mean a literal assert, but it's misleading at best. Furthermore, one of the reasons for the lint is to avoid an unnecessary runtime type check when the type is already known. However, I don't think there's a way to do that to the analyzer's satisfaction if I also have implicit-casts disabled: I can't use assert, I can't implicitly narrow the type, and I can't explicitly narrow the type with as.

[matanlurey]

I think this is just outdated docs, the avoid_as lint was written by/for the Flutter team, as was the documentation for it (at the time, based on Dart 1). I don't think assert(variable is Type) is ever going to do type promotion, as type promotion is part of Dart now/with reified types, so stripping it out in production is bad.

I'm also under the impression avoid_as should probably be removed, I remember reading that the VM team treats implicit casts and explicit casts similarly (in Dart 1 this is no longer the case).

I think the suggestion should probably be to do something like this:

void example1(Foo foo) {
  // I know this is always a SuperFoo
  var sfoo = foo as SuperFoo;
  // ...
}

void example2(Foo foo) {
  // This might be a Bar, so I'll need an upcast to do type promotion
  Object maybeBar = foo;
  if (maybeBar is Bar) {
    // ...
  }
}

[lrhn]

I agree that assert statements cannot do type promotion because they are not always executed. This means that the presence of an assert(x is Foo); doesn't actually ensure that x has type Foo afterwards when assertions are not enabled.

I hope that we may get a simple syntax for guaranteed run-time checks in the future which will promote, say x as Foo; used as a statement. This will check that x has type Foo and throw if not, and it is executed even if assertions are disabled (which also means that it always has a cost). Type promotion can work with that becuause it gurantess the type of the variable whenever it doesn't throw.

[jamesderlin]

Why must asserts be executed for type promotion to happen? The analyzer infers types without executing the code, no? Can the compiler not recognize assert(variable is Type); and promote variable after the assert is stripped out?

[matanlurey]

Analyzer and the compiler must guarantee the same thing. This is Dart 2 not Dart 1:

void example(Foo foo) {
  assert(foo is Bar);
  var items = [foo];
  print(items.runtimeType); // Should this print List<Foo> or List<Bar>?
}

[jamesderlin]

I was using the analyzer as an example. Why couldn't the compiler do the same thing?

Maybe let's set aside the assert aspect of this temporarily. I'd like an equivalent of a C++ static_cast<T>, where I affirm that a variable is of type T, where runtime cost is minimized, and where I expect UB if the variable isn't actually of that type. (That's a gross oversimplification of C++'s static_cast<T>, but those are the aspects I care about here.)

As a bonus it'd be nice if debug builds could throw AssertionError instead of triggering UB.

This doesn't have to use assert (although that'd be nice to avoid introducing some new keyword); it could be, say, some new assertIs<T>(x) construct that always does type promotion but that also does a runtime check in debug builds.

[matanlurey]

I was using the analyzer as an example. Why couldn't the compiler do the same thing?

Because of all the reasons already listed.

I'd like an equivalent of a C++ static_cast<T>

The last I heard the VM/Language team is firmly against this because of the easy ability to seg-fault.

If you are just looking for a more convenient syntax to do type promotion, @eernstg has some ideas.

[Hixie]

x as Foo;

This seems like a great idea. My only suggestion would be to tweak the syntax a little so it looks like this:

assert(x is Foo);

[lrhn]

Why must asserts be executed for type promotion to happen?

Type promotion only happens when the promoted static type is guaranteed to be a safe approximation of the run-time type.

The way to guarantee this is that the compiler can statically detect that the promoted code will only be executed when the type check succeeds.

Example:

Object x = ...;
if (x is Foo) {
  // Won't get here unless x *is* Foo.
}

We want to make type promotion smarter so it also recognizes control flow, so that:

{
  Object x = ...;
  if (x is! Foo) throw "badness"; // or return, or even other control flow.
  // Won't get here unless x is Foo.
}

The problem with assertions is that they are not always executed, so:

Object x = ...;
assert(x is Foo);
// *Can* get here when x is not Foo, if running in production mode.

Because of that, the type promotion isn't sound. It's not true that the value of x is always a Foo, so we cannot allow code to assume that it is.
If we had production asserts (ones that won't be disabled in production mode), then we could use those for promotion:

Object x = ...;
runtimeAssert(x is Foo);
// Won't get here unless x is Foo.

We don't have those, you'll have to write them as if (x is! Foo) throw AssertionError("nope");,
Or x as Foo;, which is existing syntax which throws if x is not a Foo (or null, at least until NNBD).

[a14n]

I'm also under the impression avoid_as should probably be removed

See dart-lang/linter#1401

[Hixie]

The problem with assertions is that they are not always executed

I'm suggesting that assert(x is Foo); should do exactly the same as x as Foo; is proposed to do in release builds.

[Hixie]

Or alternatively, I suggest that assert(x is Foo); followed by code that uses x and assumes that it is Foo should do exactly the same as x as Foo; followed by that code. That is, the assert signals to the compiler that it should add a type check the next time the type is used. (Maybe it could also propagate this backwards to catch cases like var x = Foo(); assert(x is Bar);.)

[lrhn]

If we make assert statements promote variables, then it assigns a new meaning to assert(x is Foo); , different from the current semantics: It is always executed, even in production mode.
I do not assume that you want all asserts to be executed in production mode, so we need to specify how to separate separate guaranteed-asserts from debug-mode-asserts.

If the only syntax which turns on "always executed" for an assert is an expression of the form x is Foo where x is a local variable, then you won't trigger on assert(x is List && x.length > 0);, which can promote. I think that is too confusing.

Or we could say that if if (condition) ... would promote any variable in the then-branch, then assert(condition); will be come a guaranteed assertion. Or maybe only if the variable is actually used in the guarded code.

I still fear that users will be confused as to which asserts are always executed and which are only executed in debug mode. For example, if a variable is assigned or captured in the guarded branch, then we do not promote. That would, in turn, make the assert into debug-only, so:

void foo(List otherList, dynamic o) {
  if (o is String) {
    otherList.remove(o);
  } else if (o is int) { 
    otherList.removeAt(o);
  } else {
    // Must be the third kind.
    assert(o is Set<String>);
    otherList.removeWhere((x) => o.contains(x));
  }
}

Here the closure will capture o, which disables type promotion for o, which again turns the assert into a debug-only assertion, likely to the author's surprise. The code still works because o has type dynamic, but you can accidentally slip a List<String> in there and not get caught.

With NNBD, a check like assert(x != null); can promote x to a non-nullable type, so that check will also be made a guaranteed assert. So, there might also be more production-time checks than necessary.

By using an existing syntax, and conditionally giving it a different meaning, we make it harder for the user to express their intent. It means that we can't tell them when they make a mistake because it might be intentional.

I think adding a separate syntax for guaranteed check will be better for users. Then they can say when they want the check to be always made, so we can tell them when it doesn't work anyway, instead of just going back to not checking.

[Hixie]

I agree that we shouldn't actually execute asserts. I'm saying we should use asserts as barriers that can imply contracts. The exception thrown by a contract violation would be on the next access, just like today, not on the assert. The assert itself isn't executed, but it's implications are taken into account by the compiler.

In your specific example in the last comment, assuming l is really o in the assert, I would have the compiler insert a type check (verifying that o is really a Set<String>) either when we do the capture or when we execute it (whichever is more efficient).

[lrhn]

This sounds like you don't want to execute the assert, but you want to insert the same test later anyway, if the variable is ever used at the promoted type. We will need to do that check because the VM may crash if it assumes a static type which isn't true.
A promotion which is not checked at run-time is unsound, so much that things may crash. That's why we only promote on operations that actually guarantee the promoted type. Unexecuted asserts are simply not enough.

Then we might as well just execute the assert, it is at least predictable and visible, and the reported failure can be directly understood by the user (and you can even have a custom message).
And then we might as well change assert to a new check function and nor overload assert with two meanings which depends on the following context.

(To take the opposite view for a moment, I have actually suggested that we should do unsafe promotion in more places. Any code of the form if (e is T) ... e should promote the type of e, even if e is a more complex expression or it is reading a public field. It's just not a safe promotion, so there will have to be an extra check at each use-point of the expression—perhaps optimizable by first checking that the value is identical to the previously tested value, and only after that checking the type of a new value. That kind of promotion could also handle asserts as unsafe signals of intent. I haven't been able to sell that idea, though, because it's too unobvious where it applies).

[jamesderlin]

I've noticed that with NNBD, casts now will promote the variable type in the current scope:

localVariable as Foo;
localVariable.someFooMethod();

and

someLocalNullable!;
someLocalNullable.someMethod();

[lrhn]

Yes, those casts promote because the check is an implicit branch where one branch throws.
They're basically equivalent to:

localVariable is Foo || throw ...
// and
someLocalNullable != null || throw ...

which both promote on the non-throwing branch.