Using if (foo?.bar == somethingNotNull) should promote foo

[matanlurey]

Another surprise (to me):

void main() {
  String? foo = 'Foo';
  if (foo?.toUpperCase() == 'FOO') {
    // Error: foo might be null.
    print(foo.toUpperCase();
  }
}

[lrhn]

The only value comparisons which promote are != null and == null, and only on the variable itself.
So foo != null promotes foo, but foo == 'bar' does not, and foo?.something != null doesn't either.

Here you are deriving that because foo?.toUpperCase() is equal to a non-null value, then it must be a non-null value, and therefore foo must be non-null too. That's not expected to happen.

So, working as intended.

[matanlurey]

Why isn't that expected to happen? The above is a contrived case, but patterns like this are common enough:

if (foo?.isDelicious() == true) {
  print(foo.describeDeliciousness());
}

[rakudrama]

I find it slightly surprising that this does not work. Promotion of a local would happen if you manually desugared

if (foo?.something != null) ...

to

if (foo != null && foo.something != null) ...

so why should you have to do that yourself?

Not promoting foo == 'bar' makes some sense since without looking at the definition, you don't know what operator== does. We perform constant-folding on strings, so why not incorporate more properties of the primitive types into promotion?

With foo?.something == 'bar', along one path of possibilities you have null as an operand to ==.

[lrhn]

I'm not surprised we don't promote because I have memorized which operations can promote, and this isn't one of them.
There are lots of operations that imply something being non-null, and we don't recognize all of them, only the most direct ones.

If we consider foo?.bar ... equivalent to foo != null ? foo.bar ... : null for local variables (and equivalent to let x = foo in x != null ? x.bar ... : null for not-local-variables), then we could do promotion from the implicit, equivalent foo == null.
We haven't specified it, so we don't.

Generally, I really, really don't want to reason about code from syntactic equivalences. It gives surprising behavior (like ++x?.foo short-circuiting the ++ because it's equivalent to to x?.foo += 1, but we don't short-circuit other prefix operators. I think this was a bad result of using equivalences as basis for reasoning).
So, if we can generalize the rules so that localVar?.selectors != null promotes localVar without resorting to equivalence to something containing foo != null, then I'd be fine with doing so, but I don't think it's viable to try adding it to the initial release of null safety.

We also don't promote foo to non-null for foo == "bar" at all. We could, but we haven't specified it, so we don't.

https://nullsafety.dartpad.dev/5a783a27daed945ead642728a80229c6

[matanlurey]

Respectfully whether you personally want to reason about it isn't really the point of this issue - at least me and Stephen (likely more) consider this valid.

I suspect this pattern is very common across both external and Google packages and unless we intentionally want users to hand desugar to the longer-form code we should consider improving this.

I'm happy to wait for other responses, thanks!

[natebosch]

My intuition is that this feature would make users less confused than they would be without it. I'd be inclined to push on it, especially if we think we can do it relatively quickly. If we think it will take too long we should consider whether it will be breaking to release it later. @leafpetersen

[matanlurey]

Totally! I could also see at minimum adding some information to our migration guides (/cc @munificent) that highlight "these are cases you'd think would promote, but don't, here are some tracking issues for future versions of Dart". Otherwise I think users are going to think they did something wrong.

[lrhn]

Maybe I'm just not sure what the point of this issue is.

The described behavior is correct according to the specification, so all tools are working as intended and required. That makes it neither a bug, nor a tool enhancement issue, except perhaps to give better messages when encountering the pattern. (Read: I can't triage the issue because I don't know what action is requested.)

If we want to change the specified behavior, we should move the issue to the language repository.

[leafpetersen]

cc @stereotype441 Am I correct that this is one of the cases that would be handled if we explicitly track the "nonNull" sets?

[stereotype441]

cc @stereotype441 Am I correct that this is one of the cases that would be handled if we explicitly track the "nonNull" sets?

@leafpetersen Yes, I believe it would, and I would actually really enjoy the mental exercise of making it work.

But it would be quite a pandora's box to open, because the formulation we had with null() and nonNull() had a logical reasoning error that we never got around to patching: null(E) and nonNull(E) tracked the answers to the questions "what would be known about the state of all variables, at the time evaluation of E completes, if E evaluated to a null / non-null value?" But then, when analyzing an expression like E1 == E2, we were trying to synthesize information from null(E1)/nonNull(E1) and null(E2)/nonNull(E2), glossing over the fact that those models represented the state of the program at different times. Which meant that flow analysis would have produced unsound results if E2 had had any side effects on local variables.

If I were going to tackle this idea I would play with conservativeJoin to see if I could use it to cover up any soundness holes that arose from side effects of E2. I'd probably give myself about a 60% chance of success with that approach.

As a backup plan, I might consider using null()/nonNull(), but only trying to promote on equality checks of the form E1 == null, E1 != null, null == E2, and null != E2. We'd be able to handle those checks soundly because evaluating the literal null has no side effects. I'm pretty sure that would be sufficient to address this particular issue, but it would still fail to promote some expressions that theoretically could be promoted (e.g. a?.b == c + d, which in principle could promote a to non-nullable).

[munificent]

I'm not sure what the general behavior you're proposing is. There are plenty of other cases where a ?. in a subexpression of an if condition does not imply that when the overall condition is true then the receiver must have been non-null:

void main() {
  String? foo = 'Foo';
  if (foo?.toUpperCase() == null) { ... }
  if (foo?.toUpperCase() is Object?) { ... }
  if (foo?.toUpperCase().isEmpty ?? true) { ... }
  if (foo?.toUpperCase() == foo?.toUpperCase()) { ... }
  if ([foo?.toUpperCase()].isNotEmpty) { ... }
  if (Future.value(foo?.toUpperCase()) is Future) { ... }
}

What are the rules you have in mind for when ?. causes promotion on the receiver and when it doesn't?

[leafpetersen]

What are the rules you have in mind for when ?. causes promotion on the receiver and when it doesn't?

The general principle that I think @matanlurey and @rakudrama are going from is that:

• if you have a e1 == e2
• and e1 being non-null necessarily implies that some variable x is non-null
• and e2 is non-null
  - then you know that if the equality evaluates to true, then x is non-null.

One way to see this is:

• The combination of e2 not being null and e1 == e2 true implies e1 is non-null
• If e1 is non-null, then by hypothesis, we know that x is non-null

The specific instance of

• and e1 being non-null necessarily implies that some variable x is non-null
  that they are going from is that e1 is foo?.method():
• foo?.method() being non-null implies that foo is non-null.

That said, I'm really quite surprised that this is considered something that "obviously should work". You guys are better at reasoning about nullability than I am... I had to think about that one for a bit. :) That said, I do see the reasonableness of the foo?.isDelicious pattern that @matanlurey describes above.

I'm skeptical about pushing on this right now, we really need to get this feature out the door. If we do tackle this (now or later), I think it would likely be on a somewhat ad hoc basis. Presumably we want to notice that one of the arguments of the equality was "obviously" a non-nullable literal, and use that to gather some promotion information while traversing the other argument.

[stereotype441]

I'm not sure what the general behavior you're proposing is. There are plenty of other cases where a ?. in a subexpression of an if condition does not imply that when the overall condition is true then the receiver must have been non-null:

void main() {
  String? foo = 'Foo';
  if (foo?.toUpperCase() == null) { ... }
  if (foo?.toUpperCase() is Object?) { ... }
  if (foo?.toUpperCase().isEmpty ?? true) { ... }
  if (foo?.toUpperCase() == foo?.toUpperCase()) { ... }
  if ([foo?.toUpperCase()].isNotEmpty) { ... }
  if (Future.value(foo?.toUpperCase()) is Future) { ... }
}

What are the rules you have in mind for when ?. causes promotion on the receiver and when it doesn't?

Not sure who you're asking, but speaking for myself, whatever we do my number 1 requirement is that it has to be sound, and in all your examples there, it wouldn't be sound to promote because the if test would pass if foo is null.

The thing Leaf and I were talking about with null() and nonNull() is essentially what he proposed for flow analysis before I ripped it out to make it match the current implementation. It would involve reverting b901765 and then doing some yet-to-be-determined thing to fix the soundness issue I mentioned in my previous comment. The basic idea is that for each expression, flow analysis would track two additional pieces of information: (a) what do we know about the types of local variables if this expression evaluates to a non-null value?, and (b) what do we know about the types of local variables if this expression evaluates to a null value? That may sound like a lot but it's actually a pretty trivial extension of how today we track what we know about the types of local variables if expressions evalute to true/false. And then we would propagate this information through the code using similar rules to the rest of what flow analysis does.

So, for the example of if (foo?.bar == somethingNotNull), flow analysis would trivially know that if foo evaluates to a non-null value, that means that foo must have been a String. Propagating that through ?.bar, it would conclude that if foo?.bar evaluates to a non-null value, that means that foo must have been a String. Propagaing that through == somethingNotNull, it would conclude that if foo?.bar == somethingNotNull evaluates to true, that means that foo must have been a String. Therefore, foo gets promoted to String in the body of the if. But for your other examples, the chain of reasoning would break down in one way or another and we wouldn't do any promotion.

[lrhn]

If we track more inferences through null-aware accesses, I guess it would mean:

For x?.foo where X.foo is non-nullable:

• x?.foo is null implies x is null
• x?.foo is non-null implies x is non-null

For x?.foo where X.foo is nullable:

• x?.foo is non-null implies x is non-null

We then have to generalize that to arbitrary chains, including extension methods, but I do believe it's reasonably simple (if the selector is non-nullable it preserves the exact null-ness, if it's nullable, it preserves non-nullness, if it's ! (participating), then a previous selector is probably nullable, and we already lost nullness).

Would it also make something like x == null ? null : x.nonNullable be able to derive that x is null iff the entire result is null?

We would probably also want x == "foo" to promote x to String in general, if it does so in this example.
Comparing to a non-null value with == can promote just as well as != null.
(So can using identical instead of ==).

[stereotype441]

If we track more inferences through null-aware accesses, I guess it would mean:

For x?.foo where X.foo is non-nullable:

• x?.foo is null implies x is null
• x?.foo is non-null implies x is non-null

For x?.foo where X.foo is nonnullable:

• x?.foo is non-null implies x is non-null

We then have to generalize that to arbitrary chains, including extension methods, but I do believe it's reasonably simple (if the selector is non-nullable it preserves the exact null-ness, if it's nullable, it preserves non-nullness, if it's ! (participating), then a previous selector is probably nullable, and we already lost nullness).

Yeah, that's pretty much what I was thinking, but explained much more clearly. Thank you 😃. One minor correction: flow analysis never reasons about when a variable's value is null, because that's not really a useful promotion; it only reasons about when a variable's value is non-null. So I would drop the reasoning step that "x?.foo is null implies x is null", and then the remaining rules collapse simply to: "x?.foo is non-null implies x is non-null", regardless of the type of X.foo.

Would it also make something like x == null ? null : x.nonNullable be able to derive that x is null iff the entire result is null?

Yes, except with the caveat mentioned above, so the only reasoning it would do is that if the entire result is non-null, then x must have been non-null. It follows pretty trivially from the equation we used to have for nonNull(N) where N takes the form E1 ? E2 : E3, namely nonNull(N) = merge(nonNull(E2), nonNull(E3)). nonNull(E2) is "unreachable" (because the null literal can't be non-null), and nonNull(E3) promotes x to non-null (because it's in the "else" branch of an x == null test), so when you merge them, the unreachable model is discarded and you get a flow model that promotes x to non-null.

We would probably also want x == "foo" to promote x to String in general, if it does so in this example.
Comparing to a non-null value with == can promote just as well as != null.

Incidentally, this improvement could be done independently of whether or not we fix if (foo?.bar == somethingNotNull). (Of course with all the usual questions about whether we have run out of time to make changes like this).

(So can using identical instead of ==).

Ditto for this. Currently flow analysis doesn't pay attention to calls to identical, but it could.

[eernstg]

We would probably also want x == "foo" to promote x to String in general

We could probably do that for e == x where the static type of e is String or a few other built-in types (because we have special knowledge about the behavior of operator == on types that are built-in and sealed), but we can't prevent operator ==(_) => true;, so we cannot conclude anything from x == "foo". However, that's probably going to be too much of a special case.

We could exploit the knowledge that x is non-null after expressions like x.getter, x..getter, x.method<...>(...), x + y, -x, and so on when x has type dynamic, and getter and method aren't members of Object; but we probably don't want to special case dynamic, and we can't express the type "dynamic-without-null" without removing the permission to have dynamic invocations. Again too much of a special case.

In the end we actually just came up with a few cases (which may be taken as a hint that it's a viable proposal to add these "missing" cases, because there aren't so many):

Let es be an expression of the form x?.s or x?..s where s is a sequence of <selector> resp. <cascadeSection>, then x is known to be non-null in the true continuation of es == n where n has a non-nullable type, and n == es where n has a non-nullable type with primitive equality; and x is known to be non-null in the true continuation of identical(es, n) and identical(n, es) when n has a non-nullable type.

[lrhn]

True, we cannot generally infer anything about the type of x from x == y being true, except that if y is not nullable, then x is not null, and vice versa. (Well, except that y can be non-nullable and still be null in weak mode, but we generally ignore that for static checks).

[natebosch]

Here are two patterns that I think may be common:

if (x?.hasSomeField == true) {
  doSomething(x.someField);
}

if (x?.hasSomeField ?? false) {
  doSomething(x.someField);
}

The latter is recommended in Effective Dart so IMO it's the more important case to make work. After migration it would be nicer to see doSomething(x.someField!) over doSomething(x!.someField!).

[munificent]

Not sure who you're asking, but speaking for myself, whatever we do my number 1 requirement is that it has to be sound, and in all your examples there, it wouldn't be sound to promote because the if test would pass if foo is null.

Yes, that was my point. :) All of my examples were structurally similar to what @matanlurey was requesting but should clearly not promote. I was trying to understand what the boundary line was that put @matanlurey's example on the "promotes" side but left all of mine on the "does not promote" side.

It sounds like there is a boundary based on flow analysis, though I have to admit it feels pretty subtle to me. Though maybe not any more subtle than the flow analysis we already do. I like that the cases where we could make the flow analysis smarter are expressions that do clearly have an operator related to null: ?. or maybe ??.

Here are two patterns that I think may be common:

if (x?.hasSomeField == true) {
  doSomething(x.someField);
}

if (x?.hasSomeField ?? false) {
  doSomething(x.someField);
}

The latter is recommended in Effective Dart so IMO it's the more important case to make work.

+1. Or even the simpler (though likely much less common):

test(bool? b) {
  if (b ?? false) {
    b + 1;
  }
}

[lrhn]

I guess the generalized rule could be that x?.chain can have implications x?.chain != null ⇒ x != null and x?.chain == null ⇔ x == null that we can deduce based on the nullability of the chain-selectors. Then we can make checks like ==null/is NonNullableType on the result promote the source variable if the inference guarantees that it's sound.

Also, we can treat x == nunNullValue as promoting the same way as x is! Null, like we treat x == null as the same as x is Null.
(We can also let x is NonNullableType promote to non-nullable, even when the type is not a subtype, so x is Object is equivalent to x != null).

Together, those would handle x?.check == true. That equality can only be true if x is non-null.

Not sure how to handle ??, though. A b ?? false can only be non-false if b is non-null, but that's a very specific pattern, and not something which generalizes to non-constant values (or even non-booleans).
if we unfold it to x != null ? x.check : false, I don't think we are able to do promotion on that either, unless we recognize the constant false and see that we can rewrite it as x != null && x.check. Not sure that's predictable enough to be something I'll hang promotions off, if a user wiggles just a little, they'll fall off the narrow plateau of promotability.

[munificent]

Not sure how to handle ??, though. A b ?? false can only be non-false if b is non-null, but that's a very specific pattern

It's very specific, but also explicitly suggested in "Effective Dart" so it may be worth handling explicitly.

[leafpetersen]

@stereotype441 How much work is this (either as a general feature, or to hit just the b ?? false case)? Given that this hits some common recommended patterns I'd be inclined to try to make this work if we can afford it, even if we have to do it as a post-beta minor breaking change.

[lrhn]

If we want to recognize x ?. selectors ?? e2 in a boolean context, so that x is promoted to non-null along one of the branches, then we need to know the boolean value of e2 at compile-time, so the special-case pattern will be:

 variable ?. selectors ?? literalBoolean 

and then the branch for ! literalBoolean will promote variable to non-null, because that value can only come from a selector implying that variable is non-null.

I wish we could recognize any constant boolean, but with bool.fromEnvironment, that seems unlikely. I'm also not sure whether the analyzer can know the values of any expression, even a constant one, before type inference is done.

We can potentially also recognize the expansion (variable != null ? variable.selectors : null) ?? literalBoolean.
That would probably mean recognizing a number of inferences between expresssions being nullable, non-nullable or Null, and certain boolean results. (Not going to try writing those rules out).

[stereotype441]

@stereotype441 How much work is this (either as a general feature, or to hit just the b ?? false case)? Given that this hits some common recommended patterns I'd be inclined to try to make this work if we can afford it, even if we have to do it as a post-beta minor breaking change.

Probably a few days' work. Not sure when I can get to it though--let's talk priority in our meeting in a few minutes 😃

[stereotype441]

@natebosch found another example that I think would be addressed by this fix:

String? current
while((current = next()) != null && current.isNotEmpty) { // Error, should be current!.isNotEmpty

[lrhn]

This last one makes good sense. An assignment to a local variable is guaranteed to evaluate to the current value of that variable, so testing the value can be used to infer something about the variable.

If we introduce "binding assignments" or "local variable declarations" like (var x = y) != null that should also be allowed to promote x.

We could technically allow (x = y) != null to promote both x and y, but I think I'd just promote x.
I think one promotion per test is a reasonable constraint.
(Othewise it would allow (x = y = z = w) != null to promote all of them.)

[stereotype441]

I've started to work on this using the idea of tracking null and nonNull models of each expression. as @leafpetersen suggested back in #1224 (comment).

The rules I'm considering would look something like this:

• When encountering an expression e of the form e1?.method(args):
  • Let before(e1) = before(e)
  • Let before(args) = nonNull(e1)
  • Let nonNull(e) = after(args)
  • If method has a non-nullable return type, then let null(e) = null(e1). Otherwise let null(e) = join(null(e1), after(args)).
  • Let true(e) = false(e) = nonNull(e)
  • Let after(e) = join(null(e), nonNull(e))
• When encountering an expression e of the form e1 == e2:
  • Let before(e1) = before(e)
  • Let before(e2) = after(e1)
  • Let true(e) = join(rebase(nonNull(e1), nonNull(e2)), rebase(null(e1), null(e2)))
  • ...

But I'm running into troublesome interactions with unsound null checking. Consider this mixed-version program:

// Opted out
int f() => null;

// Opted in
int g() => f();

void test(int? x, Object? y, bool b) {
  if (x?.remainder(y as int) == g()) { // (1)
    if (b) { // (2)
      print(x.isEven); // (3)
    } else {
      print(y.isEven); // (4)
    }
  }
}

Using the above rules, what would happen during flow analysis is:

• after(y as int) = {x: int, y: int}
• notNull(x?.remainder(y as int)) = {x: int, y: int}
• true(x?.remainder(y as int) == g()) = {x: int, y: int}

Which means that both x and y would be promoted to int when x?.remainder(y as int) == g() evaluates to true. That means that both (3) and (4) would be accepted without error.

Now consider what happens at runtime. If test is called with x = null, then x?.remainder(y as int) evaluates to null without checking the type of y. Then, g() evaluates to f() which evaluates to null (this is allowed in spite of g having a non-nullable return type, because we are using unsound null checking). Therefore x?.remainder(y as int) == g() evaluates to true, so we proceed to (2).

If b is true, then we proceed to (3), and crash trying to evaluate x.isEven when x is null. That's ok, again because we allow this sort of thing with unsound null checking.

But if b is false, then we proceed to (4) and try to evaluate y.isEven without having checked the type of y. It could have any value whatsoever. Which means that this is a case where we've escalated from unsoundness that just involves null safety to a fullly unsound type system where anything goes. We've already taken great pains to avoid this kind of unsoundness escalation (see #1143).

I'll continue thinking about this and see if there's a way to get the functionality we want without the unsoundness escalation. My guess is that it will be possible, but it will involve something different than tracking the null and nonNull models the way Leaf suggested.

[eernstg]

Another request for a feature covered by this discussion occurred here: dart-lang/sdk#45015

void main() {
  final today = DateTime.now();
  DateTime? userDate;
  DateTime firstDate = (userDate?.isBefore(today) ?? false) ? userDate : today;
}

[jodinathan]

will this be in 2.15?

[stereotype441]

@jodinathan Sorry, no. The feature set for 2.15 has already been decided upon, and it doesn't include a fix for this.

[sigmundch]

I just came across this as well (cf #2356). After reading through the comments, I sense there is an intent here to eventually fix this, but it is not entirely clear if we've reached an agreement on that.

Could you clarify if that's the case?

[lrhn]

I think we agree that there are possibilities around some of the more common expression forms, but we do not have a concrete design for what to do to which expressions, which means no current concrete plan to actually do something.