I think this is the right idea but reasoning about three sets is hard and it's hard to convince oneself that the implementation is correct for all cases.

I wonder if a simpler implementation would be possible with only two sets. Let's still call them asserted and retracted. We lift the invariant that asserted & retracted is empty, so it's possible for one variable to be in both. asserted is the set that we know is non-null at the very end of evaluating the expression (if no exception happens). retracted is the set that is retracted anywhere within the expression, even if it is later asserted. When we assert a variable, we add it to asserted but do not remove it from retracted. When we retract a variable, we add it to retracted and remove it from asserted. If we evaluate the expression to the very end, if a variable is in both asserted and retracted, we consider it asserted. When we're at a control flow point where the expression may not have executed to the end (because it threw an exception), we just clear the asserted set and keep only the retracted set. At control flow merges, we intersect asserted and union retracted. For a sequential composition (a1,r1) ; (a2,r2), we get ((a1-r2) | a2, r1|r2).

Do you think this would work or do you see any flaw in it?

I think maybe what I've described above are the current sets asserted and onceRetracted in this pull request. I guess the question is, if we have asserted and onceRetracted, can we get rid of retracted? (Then eventually we could rename onceRetracted to just retracted, to make the name shorter and simpler.)

In the above proposal:

• retracted means that the variable is set to null somewhere, anywhere in the expression
• asserted means that the variable is set to non-null after all program points that could set it to null (if any)

• retracted means that the variable is set to null somewhere, anywhere in the expression
• asserted means that the variable is set to non-null after all program points that could set it to null (if any)

This rule looks reasonable to me. I will think about more examples to double-check this.

TODO: some other improvements I want for flow typing but haven't been implemented yet:

• For definition like var a: String | Null = "", we should add a to asserted info immediately .
• We only considered Nothing body for if right now. We should consider this for other control expressions as well.