Analyzer: No warning when mixing null-conditional and null-coalescing operators with wrong types

[jakobr-google]

dartanalyzer version 2.0.0-dev.14.0

The following code doesn't generate a warning:

bool fisk = null?.isEmpty ?? 'hest';

(yes, this is a reduced example.)

[bwilkerson]

What error are you expecting to see here?

My understanding of the logic is as follows. The static type of null is Null. Because Null does not implement a member named isEmpty, the static type of null?.isEmpty is dynamic. The static type of 'hest' is String. The static type of an expression of the form e1 ?? e2 is the least upper bound of the static type of e1 and the static type of e2, which in this case would be Object. The type Object is assignable (with an implicit downcast) to bool, hence there is no warning.

(Although I'm a bit surprised that there isn't a warning that Null doesn't implement isEmpty.)

[jakobr-google]

I expected it to tell me that the String ‘hest’ wasn’t assignable to a bool, like it does if I only use ??.

I probably reduced the example too much. The original code had a field of type String that might be null, and looked more like

bool fisk = textField?.contains(...) ?? ‘hest’

(This was part of a larger expression, and I deliberately put in a constant of the wrong type to check if the operators had the precedence I expected, and was surprised I didn’t get an error.)

[bwilkerson]

But I think the same logic still applies. In this case the static type of the variable initializer is the least upper bound of the static type of textField?.contains(...), which is bool, and 'hest', which is String. The least upper bound is still Object, hence no warning.

[leafpetersen]

The fact that you don't get an error on the method call to null is a bug, looks like it's fixed in the new front end. I thought we had an open issue for this, but don't see one.

The main issue is basically an instance of this: #25368 .

I had hoped we would be able to fix this in the new front end. The intention of this phrasing from the local type inference proposal:

• The expression e0 ?? e1 is inferred as m0 ?? m1 of type T in
  context K:
  • If e0 is inferred as m0 of type T0 in context K
  • And e1 is inferred as m1 of type T1 in context J
  • Where J is T0 if K is _ and otherwise K
  • Where T is the greatest closure of K with respect to ? if K is not
    _ and otherwise UP(T0, T1)

(and similarly for the conditional operator) was intended to imply that (in your example) "hest" should be inferred in context type bool, and hence generate an error, since it is not a valid downcast. It looks like this isn't fixed in the new front end though.

@stereotype441 @kmillikin

This issue bites people often enough that it would be really nice to fix it for 2.0, but if that's not feasible maybe we should treat this as a just an open bug?

[stereotype441]

@leafpetersen aha, I see two issues with the current front end implementation:
(1) It is missing the logic "Where T is the greatest closure of K with respect to ? if K is not _"; instead it always uses UP(T0, T1) for the type of e0 ?? e1. So in the example bool fisk = null?.isEmpty ?? 'hest';, the type of null?.isEmpty ?? 'hest' is UP(dynamic, String), which is dynamic. Oops :(

(2) Checking whether a downcast is valid is only done where necessary for soundness, so in the example bool fisk = null?.isEmpty ?? 'hest';, we check that dynamic (the type of null?.isEmpty ?? 'hest') is assignable to bool (the type of fisk). But we don't check that the type of 'hest' matches its context; it is not necessary due to (1).

We could fix this in the front end by fixing (1), and then we would be forced to update the logic for ?? to check for assignability of the RHS to restore soundness. Then we would get the expected error.

But your statement that ""hest" should be inferred in context type bool, and hence generate an error" (emphasis mine) makes me wonder if your intention was something more general than that. Was it your intention that every subexpression be checked for assignability to its context? Because that might require a more pervasive bug fix. Also, if that's the case, can you clarify what it would mean to check that a subexpression is assignable to its context, in the case where the context contains ??

[leafpetersen]

It's very clear that I need to (somehow!) make time to get back to the local type inference proposal, so I'll try to do that and get more comprehensive answers.

Yes, it is the intention that in general sub-expressions be checked for assignability to their context. Some examples:

  Object o;
  List<int> l = [o]; // checked/inferred as <int>[o as int];
  int x = o..toString(); // checked/inferred as (o as int).toString();
  int y = o == x ? o : x; // checked/inferred as ... ? o as int : x;

In general, I think the correctness criterion is that if you infer an expression m1 in context K, then either:

• inference/downcast insertion rewrites (possibly trivially) m1 to m2 of type T such that T is a subtype of the greatest closure of K.
• or you get a static error

So I think that answers your question about the context containing ?: you cast to the greatest closure, thereby manually enforcing the correctness property.

Does that make sense? Issues with it? In the analyzer implementation, we somewhat separate this out: inference figures out the types of things, and then you later look for sub-expressions that require downcasts.

This is one of the reasons this was never fixed in the analyzer - there's not really a place to write down the type of the conditional expression (for example) separately from the type of its sub-expressions, so there was no natural way to post-hoc check the type of the sub-expressions for downcasts. This is actually a concern given that the analyzer implementation is planned to stay around for a while - if we do fix this in the new front end, the analyzer will have to figure out a way to make this work.

This definitely isn't the highest priority issue, except in so far as we need the analyzer and the common front end to reasonably agree.

[bwilkerson]

... there's not really a place to write down the type of the conditional expression (for example) separately from the type of its sub-expressions ...

Every Expression node has a type. Could we record the type there?

[stereotype441]

@leafpetersen Ok, it looks like there are some small differences between what you intended and what I implemented in the new front end. I'm going to let this bug continue to refer to the specific case of ?? inference, and I've filed a new bug (#31792) for the more general case of ensuring that types are checked for assignability to their context.

[leafpetersen]

@bwilkerson

Every Expression node has a type. Could we record the type there?

Yes I think I'm speaking imprecisely above. I think this could probably be worked out, it was just not obvious how to do it given my level of understanding of the analyzer at the time (and also, it didn't slot in entirely naturally with the existing analyzer checking).

I think what you are proposing, which I think would work, is to annotate the super expression with a type, and the sub-expression with its own type, and make the error verifier check that given:

• a conditional expression of type T, each arm is assignable to T
• a ?? expression of type T, each branch is assignable to T
• a cascade expression of type T, the target is assignable to T

etc.

One wrinkle though is that eventually you'd like completion to give you good answers when you're typing inside of the conditional expression (or whatever). I imagine you could work it out though.

Another possibility would be to add a synthetic node in all of the places where this can come up (there probably aren't too many) and use that to record the typing change if any.

[srawlins]

FWIW, analyzer still reports no diagnostics for this code.

[lrhn]

Could someone explain where this reasoning goes wrong:

1. The static type of the null literal is Null.
2. The expression null?.isEmpty resolves the .isEmpty getter invocation against NonNull(Null).
3. NonNull(Null) is Never
4. .isEmpty is allowed on Never with type Never.
5. The static type of null?.isEmpty is therefore Never? (aka. Null according to Norm).
6. The static type of "hest" is String.
7. The static type of e1 ?? e2 where e1 and e2 have static types t1 and t2 is UP(NonNull(t1), t2).
8. UP(Never, String) is String.
9. Therefore the static type of e1?.isEmpty ?? "hest" is String.
10. Assigning String to a variable with static type bool is a compile-time error.

(We can move the compile-time error into the individual branches as well, requiring each to be assignable to the context type, but that shouldn't affect the static type of the expression. Neither expression depends on the context type in any way, other than perhaps not satisfying it, but that's still just a compile-time error.)

The one thing I can't find specified (in https://github.com/dart-lang/language/tree/master/resources/type-system or https://github.com/dart-lang/language/tree/master/accepted/2.12/nnbd) is step 7, the static type of e1 ?? e2.

If it's defined as anything else than (effectively) what I wrote, what is that then?

That is, I don't understand where the dynamic comes from, but I do want it to go away!

---

What I'd expect for type inference on e1 ?? e2 with context type C is something like:

• If e1 is inferred as m1 with static type T1 in context K1 (where K1 is _ if C is _ and C? otherwise) then
• It's a compile-time error if T1 is not assignable to K1.
• otherwise if e2 is inferred as m2 with static type T2 in context K2 (where K2 is NonNull(T1) if C is _ and C otherwise) then
• it's a compile time error if T2 is not assignable to K2.
• otherwise e1 ?? e2 is inferred m1 && m2 with static type UP(NonNull(T1), T2).

With that, the type of null?.isEmpty ?? "hest" should be String.