[red-knot] Support for not equal narrowing

[Lexxxzy]

Summary

Planning to support type narrowing for != expression as stated in #13694.

Test Plan

Add tests in new md format.

[Lexxxzy]

I have a question: Why isn’t there a case for (1 positive, 1 negative) in the match statement of InnerIntersectionBuilder::build? It seems like (1 & ~0) is essentially just 1. Asking because for this example:

x = None if flag else 1
y = 0

if x != 1:
    y = x

    reveal_type(y) # revealed: None & ~Literal[1]

reveal_type(y) # revealed: Literal[0] | None & ~Literal[1]

y in if x != 1 scope should be just None. Also y should be Literal[0] | None outside of condition scope.

[github-actions]

ruff-ecosystem results

Linter (stable)

✅ ecosystem check detected no linter changes.

Linter (preview)

✅ ecosystem check detected no linter changes.

[sharkdp]

Thank you very much for working on this. I added a few comments. Let me know if you need any help.

[sharkdp]

I have a question: Why isn’t there a case for (1 positive, 1 negative) in the match statement of InnerIntersectionBuilder::build?

There is a case for that. The _ catch-all pattern. If there is a positive and a negative contribution, an intersection type needs to be built.

match (self.positive.len(), self.negative.len()) {
    (0, 0) => Type::Never,
    (1, 0) => self.positive[0],
    _ => {
        self.positive.shrink_to_fit();
        self.negative.shrink_to_fit();
        Type::Intersection(IntersectionType::new(db, self.positive, self.negative))
    }
}

There's still the question on how to simplify those intersection types. For example, A & ~A could be simplified to Never. Maybe this is what you had in mind. I will try to look into this soon.

It seems like (1 & ~0) is essentially just 1.

It is. This simplification is exactly what the (1, 0) branch does.

y in if x != 1 scope should be just None

If we ignore the problem that Literal[1] is not a singleton type (#13758), then yes. We would expect None & ~Literal[1] to be simplified to None. This is harder than the A & ~A case above. A & ~B == A is only true if A and B are disjoint.

[sharkdp]

@Lexxxzy I hope that you don't mind that I followed up on this myself. There was an additional point I hadn't thought about in my initial review. There actually is a difference in the narrowing-logic, compared to the not in branch. When we see

magic_number = 345
x = something()

if x is not magic_number:
    ...

we're not allowed to narrow the type by adding a ~Literal[345] constraint (because there could be other Python objects that also have the type Literal[345]). However, if we have a x != magic_number constraint, we are allowed to exclude Literal[345]. Because all inhabitants of Literal[345] would result in the condition being false.

y in if x != 1 scope should be just None. Also y should be Literal[0] | None outside of condition scope.

With #13775, both of these simplifications now work just as you expected.

[sharkdp]

This test is not related to the new feature here, but it's something I wanted to add. Using != narrowing, we can now construct "meaningful" large intersection types.

[sharkdp]

There are probably ways in which an intersection can be single-valued, but I did not invest time into it for now. I can add a TODO, if we think it's important.

[carljm]

I think an intersection would be single-valued if at least one type in its positive side is single-valued.

But I think this can only occur, given intersection simplification, if there is a single-valued type that is overlapping (not disjoint) with some other type, but neither is a subtype of the other. If they are disjoint, or if one is a subtype of the other, then they can't occur in the same intersection without one or both of them disappearing (unless they are disjoint and both on the negative side, which wouldn't make the intersection single-valued).

I have a hard time imagining that we'd ever introduce such a pair of types; I can't think of an example for any of our current single-valued types.

So I don't think this case is important :)

[carljm]

Looks great, thank you! One comment on the tests that should probably be addressed before landing.

[carljm]

This display could be improved, but I don't think that's a priority unless we see it causing unreadable types in real-world code.

[sharkdp]

This display could be improved

You mean int & ~Literal[1, 2, 3]? Or the general fact that we show intersection types to users? (which pyright and mypy don't seem to do?)

[carljm]

I meant condensed, yeah. I'm ok with showing intersection types to users. (Pyright and mypy will in some cases do so, but they format it like "subclass of A and B")

[carljm]

This test doesn't currently seem to make sense. The comparison here is against Literal[0], which is a single-valued type, and we will narrow for != 0, as shown just a couple tests above. This test is really just testing that Literal[1] and Literal[0] are disjoint, meaning the intersection Literal[1] & ~Literal[0] immediately simplifies to Literal[1]. So this test should either be removed, or re-titled to describe what it actually tests.

I do think we should add some tests here showing that we don't do wrong narrowings against non-single-valued types, particularly instance types. For example, a = A(); b = B(); if a != b: ... should not narrow to A & ~B.

[sharkdp]

This test doesn't currently seem to make sense

Absolutely. I just pushed the version which I had lying around locally already, but didn't commit+push because I got interrupted (sorry). I think it's more or less equivalent to what you proposed, but let me know if I should add something similar to a = A(); b = B(); if a != b: ....

[carljm]

The test you pushed looks sufficient!

[carljm]

I think an intersection would be single-valued if at least one type in its positive side is single-valued.

But I think this can only occur, given intersection simplification, if there is a single-valued type that is overlapping (not disjoint) with some other type, but neither is a subtype of the other. If they are disjoint, or if one is a subtype of the other, then they can't occur in the same intersection without one or both of them disappearing (unless they are disjoint and both on the negative side, which wouldn't make the intersection single-valued).

I have a hard time imagining that we'd ever introduce such a pair of types; I can't think of an example for any of our current single-valued types.

So I don't think this case is important :)