[red-knot] don't remove negations when simplifying constrained typevars (#17189)

For two non-disjoint types `P` and `Q`, the simplification of `(P | Q) &
~Q` is not `P`, but `P & ~Q`. In other words, the non-empty set `P & Q`
is also excluded from the type.

The same applies for a constrained typevar `[T: (P, Q)]`: `T & ~Q`
should simplify to `P & ~Q`, not just `P`.

Implementing this is actually purely a matter of removing code from the
constrained typevar simplification logic; we just need to not bother
removing the negations. If the negations are actually redundant (because
the constraint types are disjoint), normal intersection simplification
will already eliminate them (as shown in the added test.)

Author: carljm

crates/red_knot_python_semantic/resources/mdtest/generics/pep695.md

@@ -488,7 +488,7 @@ from knot_extensions import Not
 
 def remove_constraint[T: (int, str, bool)](t: T) -> None:
     def _(x: Intersection[T, Not[int]]) -> None:
-        reveal_type(x)  # revealed: str
+        reveal_type(x)  # revealed: str & ~int
 
     def _(x: Intersection[T, Not[str]]) -> None:
         # With OneOf this would be OneOf[int, bool]
@@ -521,14 +521,14 @@ def f[T: (P, Q)](t: T) -> None:
         reveal_type(t)  # revealed: P
         p: P = t
     else:
-        reveal_type(t)  # revealed: Q
+        reveal_type(t)  # revealed: Q & ~P
         q: Q = t
 
     if isinstance(t, Q):
         reveal_type(t)  # revealed: Q
         q: Q = t
     else:
-        reveal_type(t)  # revealed: P
+        reveal_type(t)  # revealed: P & ~Q
         p: P = t
 
 def g[T: (P, Q, R)](t: T) -> None:
@@ -539,7 +539,7 @@ def g[T: (P, Q, R)](t: T) -> None:
         reveal_type(t)  # revealed: Q & ~P
         q: Q = t
     else:
-        reveal_type(t)  # revealed: R
+        reveal_type(t)  # revealed: R & ~P & ~Q
         r: R = t
 
     if isinstance(t, P):
@@ -555,4 +555,16 @@ def g[T: (P, Q, R)](t: T) -> None:
         reveal_type(t)  # revealed: Never
 ```
 
+If the constraints are disjoint, simplification does eliminate the redundant negative:
+
+```py
+def h[T: (P, None)](t: T) -> None:
+    if t is None:
+        reveal_type(t)  # revealed: None
+        p: None = t
+    else:
+        reveal_type(t)  # revealed: P
+        p: P = t
+```
+
 [pep 695]: https://peps.python.org/pep-0695/

crates/red_knot_python_semantic/src/types/builder.rs

@@ -499,7 +499,6 @@ impl<'db> InnerIntersectionBuilder<'db> {
     fn simplify_constrained_typevars(&mut self, db: &'db dyn Db) {
         let mut to_add = SmallVec::<[Type<'db>; 1]>::new();
         let mut positive_to_remove = SmallVec::<[usize; 1]>::new();
-        let mut negative_to_remove = Vec::new();
 
         for (typevar_index, ty) in self.positive.iter().enumerate() {
             let Type::TypeVar(typevar) = ty else {
@@ -567,20 +566,13 @@ impl<'db> InnerIntersectionBuilder<'db> {
             // replace the typevar itself with the remaining positive constraint.
             to_add.push(remaining_constraint);
             positive_to_remove.push(typevar_index);
-            negative_to_remove.extend(to_remove);
         }
 
         // We don't need to sort the positive list, since we only append to it in increasing order.
         for index in positive_to_remove.into_iter().rev() {
             self.positive.swap_remove_index(index);
         }
 
-        negative_to_remove.sort_unstable();
-        negative_to_remove.dedup();
-        for index in negative_to_remove.into_iter().rev() {
-            self.negative.swap_remove_index(index);
-        }
-
         for remaining_constraint in to_add {
             self.add_positive(db, remaining_constraint);
         }