[red knot] Fix narrowing for '… is not …' type guards, add '… is …' type guards (#13758)

## Summary

- Fix a bug with `… is not …` type guards.
 
  Previously, in an example like
  ```py
  x = [1]
  y = [1]
  
  if x is not y:
      reveal_type(x)
  ```
  we would infer a type of `list[int] & ~list[int] == Never` for `x`
  inside the conditional (instead of `list[int]`), since we built a
  (negative) intersection with the type of the right hand side (`y`).
  However, as this example shows, this assumption can only be made for
  singleton types (types with a single inhabitant) such as `None`.
- Add support for `… is …` type guards.

closes #13715

## Test Plan

Moved existing `narrow_…` tests to Markdown-based tests and added new
ones (including a regression test for the bug described above). Note
that will create some conflicts with
https://github.com/astral-sh/ruff/pull/13719. I tried to establish the
correct organizational structure as proposed in
https://github.com/astral-sh/ruff/pull/13719#discussion_r1800188105

crates/red_knot_python_semantic/resources/mdtest/narrow/conditionals_is.md

@@ -0,0 +1,29 @@
+# Narrowing for `is` conditionals
+
+## `is None`
+
+```py
+x = None if flag else 1
+
+if x is None:
+    # TODO the following should be simplified to 'None'
+    reveal_type(x)  # revealed: None | Literal[1] & None
+
+reveal_type(x)  # revealed: None | Literal[1]
+```
+
+## `is` for other types
+
+```py
+class A:
+    ...
+
+x = A()
+y = x if flag else None
+
+if y is x:
+    # TODO the following should be simplified to 'A'
+    reveal_type(y)  # revealed: A | None & A
+
+reveal_type(y)  # revealed: A | None
+```

crates/red_knot_python_semantic/resources/mdtest/narrow/conditionals_is_not.md

@@ -0,0 +1,40 @@
+# Narrowing for `is not` conditionals
+
+## `is not None`
+
+The type guard removes `None` from the union type:
+
+```py
+x = None if flag else 1
+
+if x is not None:
+    reveal_type(x)  # revealed: Literal[1]
+
+reveal_type(x)  # revealed: None | Literal[1]
+```
+
+## `is not` for other singleton types
+
+```py
+x = True if flag else False
+reveal_type(x)  # revealed: bool
+
+if x is not False:
+    # TODO the following should be `Literal[True]`
+    reveal_type(x)  # revealed: bool & ~Literal[False]
+```
+
+## `is not` for non-singleton types
+
+Non-singleton types should *not* narrow the type: two instances of a
+non-singleton class may occupy different addresses in memory even if
+they compare equal.
+
+```py
+x = [1]
+y = [1]
+
+if x is not y:
+    # TODO: should include type parameter: list[int]
+    reveal_type(x)  # revealed: list
+```

crates/red_knot_python_semantic/resources/mdtest/narrow/match.md

@@ -0,0 +1,17 @@
+# Narrowing for `match` statements
+
+## Single `match` pattern
+
+```py
+x = None if flag else 1
+reveal_type(x)  # revealed: None | Literal[1]
+
+y = 0
+
+match x:
+    case None:
+        y = x
+
+# TODO intersection simplification: should be just Literal[0] | None
+reveal_type(y)  # revealed: Literal[0] | None | Literal[1] & None
+```

crates/red_knot_python_semantic/src/types.rs

@@ -463,6 +463,57 @@ impl<'db> Type<'db> {
         self == other
     }
 
+    /// Return true if there is just a single inhabitant for this type.
+    ///
+    /// Note: This function aims to have no false positives, but might return `false`
+    /// for more complicated types that are actually singletons.
+    pub(crate) fn is_singleton(self, db: &'db dyn Db) -> bool {
+        match self {
+            Type::Any
+            | Type::Never
+            | Type::Unknown
+            | Type::Todo
+            | Type::Unbound
+            | Type::Instance(..) // TODO some instance types can be singleton types (EllipsisType, NotImplementedType)
+            | Type::IntLiteral(..)
+            | Type::StringLiteral(..)
+            | Type::BytesLiteral(..)
+            | Type::LiteralString => {
+                // Note: The literal types included in this pattern are not true singletons.
+                // There can be multiple Python objects (at different memory locations) that
+                // are both of type Literal[345], for example.
+                false
+            }
+            Type::None | Type::BooleanLiteral(_) | Type::Function(..) | Type::Class(..) | Type::Module(..) => true,
+            Type::Tuple(tuple) => {
+                // We deliberately deviate from the language specification [1] here and claim
+                // that the empty tuple type is a singleton type. The reasoning is that `()`
+                // is often used as a sentinel value in user code. Declaring the empty tuple to
+                // be of singleton type allows us to narrow types in `is not ()` conditionals.
+                //
+                // [1] https://docs.python.org/3/reference/expressions.html#parenthesized-forms
+                tuple.elements(db).is_empty()
+            }
+            Type::Union(..) => {
+                // A single-element union, where the sole element was a singleton, would itself
+                // be a singleton type. However, unions with length < 2 should never appear in
+                // our model due to [`UnionBuilder::build`].
+                false
+            }
+            Type::Intersection(..) => {
+                // Intersection types are hard to analyze. The following types are technically
+                // all singleton types, but it is not straightforward to compute this. Again,
+                // we simply return false.
+                //
+                //   bool & ~Literal[False]`
+                //   None & (None | int)
+                //   (A | B) & (B | C)          with A, B, C disjunct and B a singleton
+                //
+                false
+            }
+        }
+    }
+
     /// Resolve a member access of a type.
     ///
     /// For example, if `foo` is `Type::Instance(<Bar>)`,
@@ -1510,6 +1561,7 @@ mod tests {
     enum Ty {
         Never,
         Unknown,
+        None,
         Any,
         IntLiteral(i64),
         BoolLiteral(bool),
@@ -1526,6 +1578,7 @@ mod tests {
             match self {
                 Ty::Never => Type::Never,
                 Ty::Unknown => Type::Unknown,
+                Ty::None => Type::None,
                 Ty::Any => Type::Any,
                 Ty::IntLiteral(n) => Type::IntLiteral(n),
                 Ty::StringLiteral(s) => Type::StringLiteral(StringLiteralType::new(db, s)),
@@ -1610,6 +1663,28 @@ mod tests {
         assert!(from.into_type(&db).is_equivalent_to(&db, to.into_type(&db)));
     }
 
+    #[test_case(Ty::None)]
+    #[test_case(Ty::BoolLiteral(true))]
+    #[test_case(Ty::BoolLiteral(false))]
+    #[test_case(Ty::Tuple(vec![]))]
+    fn is_singleton(from: Ty) {
+        let db = setup_db();
+
+        assert!(from.into_type(&db).is_singleton(&db));
+    }
+
+    #[test_case(Ty::Never)]
+    #[test_case(Ty::IntLiteral(345))]
+    #[test_case(Ty::BuiltinInstance("str"))]
+    #[test_case(Ty::Union(vec![Ty::IntLiteral(1), Ty::IntLiteral(2)]))]
+    #[test_case(Ty::Tuple(vec![Ty::None]))]
+    #[test_case(Ty::Tuple(vec![Ty::None, Ty::BoolLiteral(true)]))]
+    fn is_not_singleton(from: Ty) {
+        let db = setup_db();
+
+        assert!(!from.into_type(&db).is_singleton(&db));
+    }
+
     #[test_case(Ty::IntLiteral(1); "is_int_literal_truthy")]
     #[test_case(Ty::IntLiteral(-1))]
     #[test_case(Ty::StringLiteral("foo"))]

crates/red_knot_python_semantic/src/types/infer.rs

@@ -5421,53 +5421,6 @@ mod tests {
         Ok(())
     }
 
-    #[test]
-    fn narrow_not_none() -> anyhow::Result<()> {
-        let mut db = setup_db();
-
-        db.write_dedented(
-            "/src/a.py",
-            "
-            x = None if flag else 1
-            y = 0
-            if x is not None:
-                y = x
-            ",
-        )?;
-
-        assert_public_ty(&db, "/src/a.py", "x", "None | Literal[1]");
-        assert_public_ty(&db, "/src/a.py", "y", "Literal[0, 1]");
-
-        Ok(())
-    }
-
-    #[test]
-    fn narrow_singleton_pattern() {
-        let mut db = setup_db();
-
-        db.write_dedented(
-            "/src/a.py",
-            "
-            x = None if flag else 1
-            y = 0
-            match x:
-                case None:
-                    y = x
-            ",
-        )
-        .unwrap();
-
-        // TODO: The correct inferred type should be `Literal[0] | None` but currently the
-        // simplification logic doesn't account for this. The final type with parenthesis:
-        // `Literal[0] | None | (Literal[1] & None)`
-        assert_public_ty(
-            &db,
-            "/src/a.py",
-            "y",
-            "Literal[0] | None | Literal[1] & None",
-        );
-    }
-
     #[test]
     fn while_loop() -> anyhow::Result<()> {
         let mut db = setup_db();

crates/red_knot_python_semantic/src/types/narrow.rs

@@ -155,13 +155,24 @@ impl<'db> NarrowingConstraintsBuilder<'db> {
             let inference = infer_expression_types(self.db, expression);
             for (op, comparator) in std::iter::zip(&**ops, &**comparators) {
                 let comp_ty = inference.expression_ty(comparator.scoped_ast_id(self.db, scope));
-                if matches!(op, ast::CmpOp::IsNot) {
+                match op {
-                    let ty = IntersectionBuilder::new(self.db)
+                    ast::CmpOp::IsNot => {
-                        .add_negative(comp_ty)
+                        if comp_ty.is_singleton(self.db) {
-                        .build();
+                            let ty = IntersectionBuilder::new(self.db)
-                    self.constraints.insert(symbol, ty);
+                                .add_negative(comp_ty)
-                };
+                                .build();
-                // TODO other comparison types
+                            self.constraints.insert(symbol, ty);
+                        } else {
+                            // Non-singletons cannot be safely narrowed using `is not`
+                        }
+                    }
+                    ast::CmpOp::Is => {
+                        self.constraints.insert(symbol, comp_ty);
+                    }
+                    _ => {
+                        // TODO other comparison types
+                    }
+                }
             }
         }
     }