Summary

Consider this example:

def _(val: int | None):
  if val is None:
    if True:
      return

  reveal_type(val) # revealed: int | None, should be just `int`

We expect that val should be narrowed to just int at the end. That is also what pyright and mypy do.

However, for that to happen, we currently depend on the branch with the val is None narrowing constraint not being merged into the main flow.

The decision to not merge is taken only when the body of the outer if has a reachability of ALWAYS_FALSE at the time of building the semantic index, as explained in the code below:

https://github.com/astral-sh/ruff/blob/ce0a32aadb16c9e2aea74013b5f0e105c2737253/crates/ty_python_semantic/src/semantic_index/use_def.rs#L956-L970

    pub(super) fn merge(&mut self, snapshot: FlowSnapshot) {
        // As an optimization, if we know statically that either of the snapshots is always
        // unreachable, we can leave it out of the merged result entirely. Note that we cannot
        // perform any type inference at this point, so this is largely limited to unreachability
        // via terminal statements. If a flow's reachability depends on an expression in the code,
        // we will include the flow in the merged result; the reachability constraints of its
        // bindings will include this reachability condition, so that later during type inference,
        // we can determine whether any particular binding is non-visible due to unreachability.
        if snapshot.reachability == ScopedReachabilityConstraintId::ALWAYS_FALSE {
            return;
        }
        if self.reachability == ScopedReachabilityConstraintId::ALWAYS_FALSE {
            self.restore(snapshot);
            return;
        }

Which basically means, that the body of the outer if needs to have a bare terminal statement, for None to be removed from val's initial type of int | None.

But in the above case, the terminal statement here, return, itself has a reachability constraint of True. In fact, in place of True any expression which statically evaluates to a truthy value will result in incomplete narrowing like above. But because we do not have access to type information at the time of building the semantic index, we cannot decide not to merge for such scenarios.

This issue also affects the ReturnsNever constraints that we use for handling calls like sys.exit() -- see this TODO in the tests.

To correctly narrow down val's type during type inference phase, one way could be the following:
During semantic index building, whenever we encounter a terminal statement, before marking the branch as unreachable, take the current reachability, negate it, and add the result as a narrowing constraint to the currently tracked bindings.
That way, during type inference, the inferred type of val would be the one which does not allow any terminal statements to be hit.