Summary

Rendered version of the test suite including a proper introduction to the topic / motivation: click.

This changeset adds support for precise type-inference and boundness-handling of definitions inside control-flow branches with statically-known conditions, i.e. test-expressions whose truthiness we can unambiguously infer as always false or always true. In code:

x = 1

if "z" in "haystack":  # Literal[False]
    x = 2

reveal_type(x)  # revealed: Literal[1]

and:

x = 1

if "y" in "haystack":  # Literal[True]
    x = 2

reveal_type(x)  # revealed: Literal[2]

Implementation

Visibility constraints, truthiness, negation

One option to implement this would have been to add special handling for a limited set of test-expressions in semantic index-building. We would then analyze expressions like sys.version_info >= (x, y), typing.TYPE_CHECKING, True and False without any type inference and consequently close down (or unconditionally open) branches whose truthiness we can analyze in this way. This would simplify the implementation, but is much less general than the approach taken here.

Instead, we collect all necessary information during semantic index building, and then re-analyze the control flow during type-checking. The way this works is by recording so-called visibility constraints for each binding and declaration. Note that these constraints are in some sense similar to narrowing constraints, but also work quite differently and are applied at different points in control flow. Consider the following example first. Note how visibility constraints can apply to bindings outside of the if-statement:

x = 1  # visibility constraint: ~test
if test:
    x = 2  # visibility constraint: test

    y = 2  # visibility constraint: test

use(x)
use(y)

The static truthiness of the test condition can either be always-false, ambiguous, or always-true. Similarly, if the visibility constraint of a binding evaluates to always-true/always-false, it will be either always visible or never visible. If the truthiness of the constraint is ambiguous, we need to consider both options (the binding could be visible or not). For the example above, this would result in the following type inference / boundness results for the uses of x and y:

Sequential constraints

Next, let's consider a sequence of multiple control flow elements:

x = 0

if test1:  
    x = 1

if test2:
    x = 2

The binding x = 2 is easy to analyze. Its visibility correponds to the truthiness of test2. For the x = 1 binding, things are a bit more interesting. It is always visible if test1 is always-true AND test2 is always-false. It is never visible if test1 is always-false OR test2 is always-true. Note the asymmetry in the logical operators here. We introduce a new constraint KleeneAnd(a, b), which is always-true if both a and b are always-true, always-false if either a or b are always-false, and ambiguous otherwise. Then we can formulate the constraint for the x = 1 binding as KleeneAnd(test1, ~test2).

The x = 0 binding can be handled similarly, with the difference that both test1 and test2 are negated:

x = 0  # KleeneAnd(~test1, ~test2)

if test1:  
    x = 1  # KleeneAnd(test1, ~test2)

if test2:
    x = 2  # test2

Merged (or parallel) constraints

Finally, let's consider this example of "parallel" control flow (where we have omitted the test condition for the outer control flow element, as it would only complicate the discussion; instead of if <…> you can also consider any other control-flow splitting element where we have no static analysis of which branch is taken)

x = 0

if <…>:
    if test1:
        x = 1
else:
    if test2:
        x = 2

use(x)

At the usage of x, i.e. after the control flow has been merged again, the visibility of the x = 0 binding behaves as follows: the binding is always visible if test1 is always-false OR test2 is always-false; and it is never visible if test1 is always-true AND test2 is always-true. Again, note the asymmetry. We introduce a new constraint KleeneOr(a, b) which is always-true if a is always-true OR b is always true; and always-false if a is always-false AND b is always-false. This allows us to annotate the bindings with the following constraints:

x = 0  # KleeneOr(~test1, ~test2)

if <…>:
    if test1:
        x = 1  # test1
else:
    if test2:
        x = 2  # test2

use(x)

Properties

We note that KleeneAnd and KleeneOr have the property that KleeneOr(~a, ~b) = ~KleeneAnd(a, b). This means we can, in principle, get rid of either of these two to simplify the representation.

However, we already apply negative constraints ~test1 and ~test2 to the "branches not taken" in the example above. This means that the tree-representation KleeneOr(~test1, ~test2) is much cheaper/shallower than basically creating ~KleeneAnd(~(~test1), ~(~test2)). Similarly, if we wanted to get rid of KleeneAnd, we would also have to create additional nodes. So for performance reasons, there is a certain "duplication" in the code between those two constraint types.

Other

This branch also includes:

• sys.platform support
• statically-known branches handling for Boolean expressions and while loops
• new target-version requirements in some Markdown tests which were now required due to the understanding of sys.version_info branches.

closes #12700
closes #15034

Performance

tomllib, -7%, needs to resolve one additional module (sys)

black, -6%

Test Plan

• New Markdown tests for the main feature in statically-known-branches.md
• New Markdown tests for sys.platform
• Adapted tests for EllipsisType, Never, etc