From 5226225dd72f0821f45864cb39e2755750c0c731 Mon Sep 17 00:00:00 2001
From: slyces <slyces.coding@gmail.com>
Date: Sat, 5 Oct 2024 22:06:49 +0200
Subject: [PATCH 1/8] [red-knot] test: add tests for truthy/falsy type
 narrowing

---
 crates/red_knot_python_semantic/src/types.rs  |   7 ++
 .../src/types/builder.rs                      | 119 +++++++++++++++++-
 .../src/types/infer.rs                        |  47 +++++++
 3 files changed, 172 insertions(+), 1 deletion(-)

diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs
index ce84a55e6dee02..b136b7849a6b99 100644
--- a/crates/red_knot_python_semantic/src/types.rs
+++ b/crates/red_knot_python_semantic/src/types.rs
@@ -245,6 +245,13 @@ pub enum Type<'db> {
     Unbound,
     /// The None object -- TODO remove this in favor of Instance(types.NoneType)
     None,
+    /// Type for narrowing a type to the subset of that type that is truthy (bool(x) == True).
+    /// Mainly used in intersections: `X & Truthy`. Example: for `list` it's all lists of `len > 0`
+    Truthy,
+    /// Type for narrowing a type to the subset of that type that is falsy (bool(x) == False).
+    /// Mainly used in intersections: `X & Falsy`. Example: for `int` it's the singleton
+    /// `IntLiteral[0]`.
+    Falsy,
     /// Temporary type for symbols that can't be inferred yet because of missing implementations.
     /// Behaves equivalently to `Any`.
     ///
diff --git a/crates/red_knot_python_semantic/src/types/builder.rs b/crates/red_knot_python_semantic/src/types/builder.rs
index 4dbfa6326e8ff6..c56e5c86a501ca 100644
--- a/crates/red_knot_python_semantic/src/types/builder.rs
+++ b/crates/red_knot_python_semantic/src/types/builder.rs
@@ -302,7 +302,7 @@ mod tests {
     use crate::db::tests::TestDb;
     use crate::program::{Program, SearchPathSettings};
     use crate::python_version::PythonVersion;
-    use crate::types::{KnownClass, UnionBuilder};
+    use crate::types::{BytesLiteralType, KnownClass, StringLiteralType, TupleType, UnionBuilder};
     use crate::ProgramSettings;
     use ruff_db::system::{DbWithTestSystem, SystemPathBuf};
 
@@ -425,6 +425,16 @@ mod tests {
         assert_eq!(u0.expect_union().elements(&db), &[unknown_ty, object_ty]);
     }
 
+    #[test]
+    fn build_union_truthy_falsy() {
+        let db = setup_db();
+
+        // `Truthy | Falsy` -> `Any` -- this probably should never happen in practice
+        let t0 = UnionType::from_elements(&db, [Type::Truthy, Type::Falsy]);
+
+        assert_eq!(t0, Type::Any);
+    }
+
     impl<'db> IntersectionType<'db> {
         fn pos_vec(self, db: &'db TestDb) -> Vec<Type<'db>> {
             self.positive(db).into_iter().copied().collect()
@@ -575,4 +585,111 @@ mod tests {
 
         assert_eq!(ty, Type::IntLiteral(1));
     }
+
+    /// Test all tpes where `X & Falsy` can be evaluated to specific literals.
+    #[test]
+    fn build_intersection_simplify_to_falsy_literals() {
+        let db = setup_db();
+
+        let falsy_int = IntersectionBuilder::new(&db)
+            .add_positive(KnownClass::Int.to_instance(&db))
+            .add_positive(Type::Falsy)
+            .build();
+        assert_eq!(falsy_int, Type::IntLiteral(0));
+
+        let empty_str = Type::StringLiteral(StringLiteralType::new(&db, "".into()));
+        let falsy_str = IntersectionBuilder::new(&db)
+            .add_positive(KnownClass::Str.to_instance(&db))
+            .add_positive(Type::Falsy)
+            .build();
+        assert_eq!(falsy_str, empty_str);
+
+        let falsy_literal_str = IntersectionBuilder::new(&db)
+            .add_positive(Type::LiteralString)
+            .add_positive(Type::Falsy)
+            .build();
+        assert_eq!(falsy_literal_str, empty_str);
+
+        let falsy_bool = IntersectionBuilder::new(&db)
+            .add_positive(KnownClass::Bool.to_instance(&db))
+            .add_positive(Type::Falsy)
+            .build();
+        assert_eq!(falsy_bool, Type::BooleanLiteral(false));
+
+        let empty_tuple = Type::Tuple(TupleType::new(&db, vec![].into()));
+        let falsy_tuple = IntersectionBuilder::new(&db)
+            .add_positive(KnownClass::Tuple.to_instance(&db))
+            .add_positive(Type::Falsy)
+            .build();
+        assert_eq!(falsy_tuple, empty_tuple);
+
+        let empty_bytes = Type::BytesLiteral(BytesLiteralType::new(&db, vec![].into()));
+        let falsy_bytes = IntersectionBuilder::new(&db)
+            .add_positive(KnownClass::Bytes.to_instance(&db))
+            .add_positive(Type::Falsy)
+            .build();
+        assert_eq!(falsy_bytes, empty_bytes);
+    }
+
+    #[test]
+    fn build_intersection_known_literals_and_truthy() {
+        let db = setup_db();
+
+        let hello_literal = Type::StringLiteral(StringLiteralType::new(&db, "hello".into()));
+        let hello_literal_and_truthy = IntersectionBuilder::new(&db)
+            .add_positive(hello_literal)
+            .add_positive(Type::Truthy)
+            .build();
+        assert_eq!(hello_literal_and_truthy, hello_literal);
+
+        let zero_and_truthy = IntersectionBuilder::new(&db)
+            .add_positive(Type::IntLiteral(0))
+            .add_positive(Type::Truthy)
+            .build();
+        assert_eq!(zero_and_truthy, Type::Never);
+
+        let none_and_truthy = IntersectionBuilder::new(&db)
+            .add_positive(KnownClass::NoneType.to_instance(&db))
+            .add_positive(Type::Truthy)
+            .build();
+        assert_eq!(none_and_truthy, Type::Never);
+    }
+
+    #[test]
+    fn build_intersection_truthy_and_falsy() {
+        let db = setup_db();
+
+        // `Truthy & Falsy` -> `Never`
+        let truthy_and_falsy = IntersectionBuilder::new(&db)
+            .add_positive(Type::Truthy)
+            .add_positive(Type::Falsy)
+            .build();
+        assert_eq!(truthy_and_falsy, Type::Never);
+
+        let truthy_and_falsy = IntersectionBuilder::new(&db)
+            .add_positive(Type::Truthy)
+            .add_positive(Type::Falsy)
+            .build();
+        assert_eq!(truthy_and_falsy, Type::Never);
+    }
+
+    #[test]
+    fn build_union_type_truthy_and_type_falsy() {
+        let db = setup_db();
+
+        // `X & Falsy | X & Truthy` -> `X`
+        let truthy_int = UnionBuilder::new(&db)
+            .add(KnownClass::Int.to_instance(&db))
+            .add(Type::Truthy)
+            .build();
+        let falsy_int = UnionBuilder::new(&db)
+            .add(KnownClass::Int.to_instance(&db))
+            .add(Type::Falsy)
+            .build();
+        let truthy_and_falsy = UnionBuilder::new(&db)
+            .add(truthy_int)
+            .add(falsy_int)
+            .build();
+        assert_eq!(truthy_and_falsy, KnownClass::Int.to_instance(&db));
+    }
 }
diff --git a/crates/red_knot_python_semantic/src/types/infer.rs b/crates/red_knot_python_semantic/src/types/infer.rs
index 3de456dded0653..7c9d824f452642 100644
--- a/crates/red_knot_python_semantic/src/types/infer.rs
+++ b/crates/red_knot_python_semantic/src/types/infer.rs
@@ -7630,6 +7630,53 @@ mod tests {
         Ok(())
     }
 
+    #[test]
+    fn bool_chain_narrows_falsy_and_truthy_types() -> anyhow::Result<()> {
+        let mut db = setup_db();
+
+        // In a chained boolean expression, we return a type early if and only if
+        // - `and` operator -> the left side is falsy
+        // - `or` operator -> the left side is truthy
+        db.write_dedented(
+            "/src/a.py",
+            r#"
+            def int_instance() -> int:
+                return 1
+
+            def str_instance() -> str:
+                return "str"
+
+            def bool_instance() -> bool:
+                return False
+
+            a = str_instance() and int_instance() and bool_instance()
+            b = bool_instance() or int_instance() or ""
+            c = int_instance() or 0
+            "#,
+        )?;
+
+        // str_instance() and int_instance() and "x"
+        // - str_instance() & Falsy => ""
+        // - int_instance() & Falsy => 0
+        // - bool_instance() is last => unchanged
+        assert_public_ty(&db, "/src/a.py", "a", r#"Literal[""] | Literal[0] | bool"#);
+        // bool_instance() or int_instance() or ""
+        // - bool_instance() & Truthy => True
+        // - int_instance() & Truthy => {int != 0}
+        // - "" is last => unchanged
+        assert_public_ty(
+            &db,
+            "/src/a.py",
+            "b",
+            "Literal[True] | int & Truthy | Literal[\"\"]",
+        );
+        // TODO: I don't know if red-knot can be smart enough to realise that
+        // `Literal[0]` = `int & Falsy`, which leads to:
+        // `int & Truthy | Literal[0]` = `int & Truthy | int & Falsy` = `int`
+        assert_public_ty(&db, "/src/a.py", "c", "int");
+        Ok(())
+    }
+
     #[test]
     fn bool_function_falsy_values() -> anyhow::Result<()> {
         let mut db = setup_db();

From 7e4176adf38502e7b7f1d4bddc1f9e7d9be2f5c0 Mon Sep 17 00:00:00 2001
From: slyces <slyces.coding@gmail.com>
Date: Sat, 5 Oct 2024 22:34:49 +0200
Subject: [PATCH 2/8] [red-knot] test: ensure that truthy/falsy is always
 positive intersection

---
 .../src/types/builder.rs                      | 27 +++++++++++++++++++
 1 file changed, 27 insertions(+)

diff --git a/crates/red_knot_python_semantic/src/types/builder.rs b/crates/red_knot_python_semantic/src/types/builder.rs
index c56e5c86a501ca..6349716e4285e5 100644
--- a/crates/red_knot_python_semantic/src/types/builder.rs
+++ b/crates/red_knot_python_semantic/src/types/builder.rs
@@ -692,4 +692,31 @@ mod tests {
             .build();
         assert_eq!(truthy_and_falsy, KnownClass::Int.to_instance(&db));
     }
+
+    #[test]
+    fn build_intersection_truthy_and_falsy_is_always_positive() {
+        let db = setup_db();
+
+        // `X & !Truthy` -> `X & Falsy`
+        let truthy_int_positive = IntersectionBuilder::new(&db)
+            .add_positive(KnownClass::Int.to_instance(&db))
+            .add_positive(Type::Truthy)
+            .build();
+        let falsy_int_negative = IntersectionBuilder::new(&db)
+            .add_positive(KnownClass::Int.to_instance(&db))
+            .add_negative(Type::Falsy)
+            .build();
+        assert_eq!(truthy_int_positive, falsy_int_negative);
+
+        // `X & !Falsy` -> `X & Truthy`
+        let falsy_int_positive = IntersectionBuilder::new(&db)
+            .add_positive(KnownClass::Int.to_instance(&db))
+            .add_positive(Type::Falsy)
+            .build();
+        let truthy_int_negative = IntersectionBuilder::new(&db)
+            .add_positive(KnownClass::Int.to_instance(&db))
+            .add_negative(Type::Truthy)
+            .build();
+        assert_eq!(falsy_int_positive, truthy_int_negative);
+    }
 }

From 29c6ab46d5ee0a20e7e8f30c556e5e4afadcc118 Mon Sep 17 00:00:00 2001
From: slyces <slyces.coding@gmail.com>
Date: Mon, 7 Oct 2024 15:06:17 +0200
Subject: [PATCH 3/8] [red-knot] feat: implement truthy/falsy cases in
 intersection/union

---
 crates/red_knot_python_semantic/src/types.rs  | 140 +++++-
 .../src/types/builder.rs                      | 410 ++++++++++++++----
 .../src/types/display.rs                      |   2 +
 .../src/types/infer.rs                        |  64 +--
 4 files changed, 492 insertions(+), 124 deletions(-)

diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs
index b136b7849a6b99..13bf878b814a61 100644
--- a/crates/red_knot_python_semantic/src/types.rs
+++ b/crates/red_knot_python_semantic/src/types.rs
@@ -400,6 +400,62 @@ impl<'db> Type<'db> {
         }
     }
 
+    /// Return the `Truthy` subset of this type (intersection with Truthy).
+    #[must_use]
+    pub fn truthy(&self, db: &'db dyn Db) -> Type<'db> {
+        IntersectionBuilder::build_truthy(db, *self)
+    }
+
+    /// Return the `Falsy` subset of this type (intersection with Truthy).
+    #[must_use]
+    pub fn falsy(&self, db: &'db dyn Db) -> Type<'db> {
+        self.falsy_set(db)
+            .unwrap_or_else(|| IntersectionBuilder::build_falsy(db, *self))
+    }
+
+    /// Returns, if it can be expressed, the set of values that are falsy in this type. This is
+    /// defined for some builtin types (e.g. int, str, ...)
+    #[must_use]
+    pub fn falsy_set(&self, db: &'db dyn Db) -> Option<Type<'db>> {
+        match self {
+            // Some builtin types have known falsy values
+            Self::Instance(class) if class.is_known(db, KnownClass::Bool) => {
+                Some(Self::BooleanLiteral(false))
+            }
+            Self::Instance(class) if class.is_known(db, KnownClass::Int) => {
+                Some(Self::IntLiteral(0))
+            }
+            Self::Instance(class) if class.is_known(db, KnownClass::Str) => {
+                Some(Self::StringLiteral(StringLiteralType::new(db, "".into())))
+            }
+            Self::Instance(class) if class.is_known(db, KnownClass::Bytes) => {
+                Some(Self::BytesLiteral(BytesLiteralType::new(db, vec![].into())))
+            }
+            Self::Instance(class) if class.is_known(db, KnownClass::Tuple) => {
+                Some(Self::Tuple(TupleType::new(db, vec![].into())))
+            }
+            Type::LiteralString => KnownClass::Str.to_instance(db).falsy_set(db),
+            Type::IntLiteral(_) => KnownClass::Int.to_instance(db).falsy_set(db),
+            Type::BooleanLiteral(_) => KnownClass::Bool.to_instance(db).falsy_set(db),
+            _ => None,
+        }
+    }
+
+    /// Returns, if it can be expressed, the set of values that are truthy in this type. This is
+    /// rarely defined, with the exception of the `builtins.bool` type.
+    #[must_use]
+    pub fn truthy_set(&self, db: &'db dyn Db) -> Option<Type<'db>> {
+        match self {
+            Type::Instance(class) if class.is_known(db, KnownClass::Bool) => {
+                Some(Type::BooleanLiteral(true))
+            }
+            Type::BooleanLiteral(_) => KnownClass::Bool.to_instance(db).truthy_set(db),
+            // There is no instance of `NoneType` that is truthy
+            Type::Instance(class) if class.is_known(db, KnownClass::NoneType) => Some(Type::Never),
+            _ => None,
+        }
+    }
+
     /// Return true if the type is a class or a union of classes.
     pub fn is_class(&self, db: &'db dyn Db) -> bool {
         match self {
@@ -493,6 +549,8 @@ impl<'db> Type<'db> {
             }
             Type::Unknown => Type::Unknown,
             Type::Unbound => Type::Unbound,
+            Type::Truthy => Type::Unknown,
+            Type::Falsy => Type::Unknown,
             Type::None => {
                 // TODO: attribute lookup on None type
                 Type::Todo
@@ -549,14 +607,21 @@ impl<'db> Type<'db> {
             Type::Any | Type::Todo | Type::Never | Type::Unknown | Type::Unbound => {
                 Truthiness::Ambiguous
             }
-            Type::None => Truthiness::AlwaysFalse,
-            Type::Function(_) => Truthiness::AlwaysTrue,
-            Type::Module(_) => Truthiness::AlwaysTrue,
+            Type::None | Type::Falsy => Truthiness::AlwaysFalse,
+            Type::Function(_) | Type::Module(_) | Type::Truthy => Truthiness::AlwaysTrue,
             Type::Class(_) => {
                 // TODO: lookup `__bool__` and `__len__` methods on the class's metaclass
                 // More info in https://docs.python.org/3/library/stdtypes.html#truth-value-testing
                 Truthiness::Ambiguous
             }
+            // Temporary special case for `None` until we handle generic instances
+            Type::Instance(class) if class.is_known(db, KnownClass::NoneType) => {
+                Truthiness::AlwaysFalse
+            }
+            // Temporary special case for `FunctionType` until we handle generic instances
+            Type::Instance(class) if class.is_known(db, KnownClass::FunctionType) => {
+                Truthiness::AlwaysTrue
+            }
             Type::Instance(_) => {
                 // TODO: lookup `__bool__` and `__len__` methods on the instance's class
                 // More info in https://docs.python.org/3/library/stdtypes.html#truth-value-testing
@@ -577,9 +642,23 @@ impl<'db> Type<'db> {
                 }
                 first_element_truthiness
             }
-            Type::Intersection(_) => {
-                // TODO
-                Truthiness::Ambiguous
+            Type::Intersection(intersection) => {
+                // The truthiness of the intersection is the intersection of the truthiness of its
+                // elements:
+                // - `Ambiguous` ∩ `Truthy` = `Truthy`
+                // - `Ambiguous` ∩ `Falsy` = `Falsy`
+                // - `Truthy` ∩ `Falsy` = `Never`  -- this should be impossible to build
+                intersection
+                    // Negative elements (what this intersection should not be) do not have an
+                    // influence on the truthiness of the intersection.
+                    // Or if they should, this should be simplified at build time.
+                    .positive(db)
+                    .iter()
+                    .map(|ty| ty.bool(db))
+                    // Stop at the first `Truthy`or `Falsy` since an intersection containing both
+                    // should simplify to the empty intersection at build time.
+                    .find(|truthiness| !truthiness.is_ambiguous())
+                    .unwrap_or(Truthiness::Ambiguous)
             }
             Type::IntLiteral(num) => Truthiness::from(*num != 0),
             Type::BooleanLiteral(bool) => Truthiness::from(*bool),
@@ -725,10 +804,12 @@ impl<'db> Type<'db> {
             Type::Todo => Type::Todo,
             Type::Unknown => Type::Unknown,
             Type::Unbound => Type::Unknown,
+            Type::Truthy | Type::Falsy => Type::Unknown,
             Type::Never => Type::Never,
             Type::Class(class) => Type::Instance(*class),
             Type::Union(union) => union.map(db, |element| element.to_instance(db)),
             // TODO: we can probably do better here: --Alex
+            // TODO: case of `type[X] & Truthy` or `type[X] & Falsy` should be straightforward
             Type::Intersection(_) => Type::Todo,
             // TODO: calling `.to_instance()` on any of these should result in a diagnostic,
             // since they already indicate that the object is an instance of some kind:
@@ -752,6 +833,7 @@ impl<'db> Type<'db> {
         match self {
             Type::Unbound => Type::Unbound,
             Type::Never => Type::Never,
+            Type::Truthy | Type::Falsy => Type::Unknown,
             Type::Instance(class) => Type::Class(*class),
             Type::Union(union) => union.map(db, |ty| ty.to_meta_type(db)),
             Type::BooleanLiteral(_) => KnownClass::Bool.to_class(db),
@@ -1459,6 +1541,52 @@ pub struct IntersectionType<'db> {
     negative: FxOrderSet<Type<'db>>,
 }
 
+impl<'db> IntersectionType<'db> {
+    /// If this is an intersection of `X & Truthy` (generalized to `(X & Y) & Truthy`), returns the
+    /// left side of the intersection (the type that intersects with `Truthy`).
+    fn truthy_of(self, db: &'db dyn Db) -> Option<Type<'db>> {
+        if self.positive(db).contains(&Type::Truthy) {
+            let builder = self
+                .positive(db)
+                .iter()
+                .filter(|ty| *ty != &Type::Truthy)
+                .fold(IntersectionBuilder::new(db), |builder, ty| {
+                    builder.add_positive(*ty)
+                });
+            Some(
+                self.negative(db)
+                    .iter()
+                    .fold(builder, |builder, ty| builder.add_negative(*ty))
+                    .build(),
+            )
+        } else {
+            None
+        }
+    }
+
+    /// If this is an intersection of `X & Falsy` (generalized to `(X & Y) & Falsy`), returns the
+    /// left side of the intersection (the type that intersects with `Falsy`).
+    fn falsy_of(self, db: &'db dyn Db) -> Option<Type<'db>> {
+        if self.positive(db).contains(&Type::Falsy) {
+            let builder = self
+                .positive(db)
+                .iter()
+                .filter(|ty| *ty != &Type::Falsy)
+                .fold(IntersectionBuilder::new(db), |builder, ty| {
+                    builder.add_positive(*ty)
+                });
+            Some(
+                self.negative(db)
+                    .iter()
+                    .fold(builder, |builder, ty| builder.add_negative(*ty))
+                    .build(),
+            )
+        } else {
+            None
+        }
+    }
+}
+
 #[salsa::interned]
 pub struct StringLiteralType<'db> {
     #[return_ref]
diff --git a/crates/red_knot_python_semantic/src/types/builder.rs b/crates/red_knot_python_semantic/src/types/builder.rs
index 6349716e4285e5..8ec0173bcc8193 100644
--- a/crates/red_knot_python_semantic/src/types/builder.rs
+++ b/crates/red_knot_python_semantic/src/types/builder.rs
@@ -29,7 +29,7 @@ use crate::types::{IntersectionType, Type, UnionType};
 use crate::{Db, FxOrderSet};
 use smallvec::SmallVec;
 
-use super::KnownClass;
+use super::{KnownClass, Truthiness};
 
 pub(crate) struct UnionBuilder<'db> {
     elements: Vec<Type<'db>>,
@@ -65,6 +65,7 @@ impl<'db> UnionBuilder<'db> {
                 let mut to_add = ty;
                 let mut to_remove = SmallVec::<[usize; 2]>::new();
                 for (index, element) in self.elements.iter().enumerate() {
+                    // Handle `True | False` -> `bool`
                     if Some(*element) == bool_pair {
                         to_add = KnownClass::Bool.to_instance(self.db);
                         to_remove.push(index);
@@ -74,6 +75,70 @@ impl<'db> UnionBuilder<'db> {
                         // supertype of bool. Therefore, we are done.
                         break;
                     }
+
+                    match (ty, *element) {
+                        // Handle `Truthy | Falsy` -> `Never`
+                        (Type::Truthy, Type::Falsy) | (Type::Falsy, Type::Truthy) => {
+                            to_add = Type::Never;
+                            to_remove.push(index);
+                            break;
+                        }
+                        // Handle `X & Truthy | X & Falsy` -> `X`
+                        (Type::Intersection(present), Type::Intersection(inserted)) => {
+                            // Detect `X & Truthy | Y & Falsy`
+                            if let (Some(present_ty), Some(inserted_ty)) =
+                                (present.truthy_of(self.db), inserted.falsy_of(self.db))
+                            {
+                                // If `X` = `Y`, we can simplify `X & Truthy | X & Falsy` to `X`
+                                if present_ty == inserted_ty {
+                                    to_add = present_ty;
+                                    to_remove.push(index);
+                                    break;
+                                }
+                            }
+
+                            // Detect `X & Falsy | Y & Truthy`
+                            if let (Some(present_ty), Some(inserted_ty)) =
+                                (present.falsy_of(self.db), inserted.truthy_of(self.db))
+                            {
+                                // If `X` = `Y`, we can simplify `X & Falsy | X & Truthy` to `X`
+                                if present_ty == inserted_ty {
+                                    to_add = present_ty;
+                                    to_remove.push(index);
+                                    break;
+                                }
+                            }
+                        }
+
+                        // Corner-case of the previous `X & Truthy | X & Falsy` -> `X`
+                        // Some `X & Truthy` or `X & Falsy` types have been simplified to a
+                        // specific subset of instances of the type.
+                        (Type::Intersection(inter), ty) | (ty, Type::Intersection(inter)) => {
+                            if let Some(inter_ty) = inter.truthy_of(self.db) {
+                                // 'X & Truthy | y' -> test if `y` = `X & Falsy`
+                                if let Some(falsy_set) = inter_ty.falsy_set(self.db) {
+                                    if falsy_set == ty {
+                                        to_add = inter_ty;
+                                        to_remove.push(index);
+                                        break;
+                                    }
+                                }
+                            }
+
+                            if let Some(inter_ty) = inter.falsy_of(self.db) {
+                                // 'X & Falsy | y' -> test if `y` = `X & Truthy`
+                                if let Some(truthy_set) = inter_ty.truthy_set(self.db) {
+                                    if truthy_set == ty {
+                                        to_add = inter_ty;
+                                        to_remove.push(index);
+                                        break;
+                                    }
+                                }
+                            }
+                        }
+                        _ => {}
+                    };
+
                     if ty.is_subtype_of(self.db, *element) {
                         return self;
                     } else if element.is_subtype_of(self.db, ty) {
@@ -189,6 +254,24 @@ impl<'db> IntersectionBuilder<'db> {
         }
     }
 
+    /// Creates an intersection builder with the given type & `Truthy` and returns the built
+    /// intersection type.
+    pub(crate) fn build_truthy(db: &'db dyn Db, ty: Type<'db>) -> Type<'db> {
+        Self::new(db)
+            .add_positive(ty)
+            .add_positive(Type::Truthy)
+            .build()
+    }
+
+    /// Creates an intersection builder with the given type & `Falsy` and returns the built
+    /// intersection type.
+    pub(crate) fn build_falsy(db: &'db dyn Db, ty: Type<'db>) -> Type<'db> {
+        Self::new(db)
+            .add_positive(ty)
+            .add_positive(Type::Falsy)
+            .build()
+    }
+
     pub(crate) fn build(mut self) -> Type<'db> {
         // Avoid allocating the UnionBuilder unnecessarily if we have just one intersection:
         if self.intersections.len() == 1 {
@@ -238,7 +321,16 @@ impl<'db> InnerIntersectionBuilder<'db> {
     /// Adds a negative type to this intersection.
     fn add_negative(&mut self, db: &'db dyn Db, ty: Type<'db>) {
         // TODO `Any`/`Unknown`/`Todo` actually should not self-cancel
+
+        // `[Type::Truthy]` and `[Type::Falsy]` should never be in the negative set, so we add
+        // their opposite to the positive set.
         match ty {
+            Type::Truthy => {
+                self.positive.insert(Type::Falsy);
+            }
+            Type::Falsy => {
+                self.positive.insert(Type::Truthy);
+            }
             Type::Intersection(intersection) => {
                 let pos = intersection.negative(db);
                 let neg = intersection.positive(db);
@@ -257,7 +349,7 @@ impl<'db> InnerIntersectionBuilder<'db> {
         }
     }
 
-    fn simplify(&mut self) {
+    fn simplify(&mut self, db: &'db dyn Db) {
         // TODO this should be generalized based on subtyping, for now we just handle a few cases
 
         // Never is a subtype of all types
@@ -271,6 +363,40 @@ impl<'db> InnerIntersectionBuilder<'db> {
             self.negative.clear();
         }
 
+        // If we have `Truthy` and all elements are always true, we can remove it
+        if self.positive.contains(&Type::Truthy)
+            && self
+                .positive
+                .iter()
+                .all(|ty| ty.bool(db) == Truthiness::AlwaysTrue)
+        {
+            self.positive.remove(&Type::Truthy);
+        }
+
+        // If we have `Falsy` and all elements are always false, we can remove it
+        if self.positive.contains(&Type::Falsy)
+            && self
+                .positive
+                .iter()
+                .all(|ty| ty.bool(db) == Truthiness::AlwaysFalse)
+        {
+            self.positive.remove(&Type::Falsy);
+        }
+
+        // If we have both `AlwaysTrue` and `AlwaysFalse`, this intersection should be empty.
+        if self
+            .positive
+            .iter()
+            .any(|ty| ty.bool(db) == Truthiness::AlwaysFalse)
+            && self
+                .positive
+                .iter()
+                .any(|ty| ty.bool(db) == Truthiness::AlwaysTrue)
+        {
+            self.positive.clear();
+            self.negative.clear();
+        }
+
         // None intersects only with object
         for pos in &self.positive {
             if let Type::Instance(_) = pos {
@@ -280,10 +406,60 @@ impl<'db> InnerIntersectionBuilder<'db> {
                 break;
             }
         }
+
+        // If an intersection is `X & Falsy`, try to replace it by the falsy set of `X`
+        // TODO: this doesn't handle the case `X & Y & Falsy` where `(X & Y)` would have a known
+        // falsy set (this doesn't happen yet, can it happen?)
+        if self.positive.len() == 2 && self.positive.contains(&Type::Falsy) {
+            self.positive.remove(&Type::Falsy);
+            let ty = self.positive.iter().next().unwrap();
+            if let Some(falsy) = ty.falsy_set(db) {
+                self.positive.clear();
+                self.positive.insert(falsy);
+            } else {
+                self.positive.insert(Type::Falsy);
+            }
+        }
+
+        // If an intersection is `X & Truthy`, try to replace it by the truthy set of `X`
+        // TODO: this doesn't handle the case `X & Y & Truthy` where `(X & Y)` would have a known
+        // truthy set (this doesn't happen yet, can it happen?)
+        if self.positive.len() == 2 && self.positive.contains(&Type::Truthy) {
+            self.positive.remove(&Type::Truthy);
+            let ty = self.positive.iter().next().unwrap();
+            if let Some(truthy) = ty.truthy_set(db) {
+                self.positive.clear();
+                self.positive.insert(truthy);
+            } else {
+                self.positive.insert(Type::Truthy);
+            }
+        }
+
+        // If an intersection is `X`, check for `y` in negatives where `y` is the truthy/falsy set
+        // of `X`
+        // TODO: same as above, does not handle a case like `X & Y & ~z`.
+        // TODO: we don't handle the case where the truthy/falsy set of `X` is multiple elements.
+        if self.positive.len() == 1 {
+            // Because our case is so narrow (len == 1), there's no need to simplify again
+            let ty = self.positive.iter().next().unwrap();
+            let truthy_set = ty.truthy_set(db).unwrap_or(Type::Never);
+            if self.negative.iter().any(|n| *n == truthy_set) {
+                self.positive.insert(Type::Falsy);
+                self.negative.retain(|n| n != &truthy_set);
+            }
+
+            // Query `ty` again to avoid borrowing multiple times as mutable & immutable
+            let ty = self.positive.iter().next().unwrap();
+            let falsy_set = ty.falsy_set(db).unwrap_or(Type::Never);
+            if self.negative.iter().any(|n| *n == falsy_set) {
+                self.positive.insert(Type::Truthy);
+                self.negative.retain(|n| n != &falsy_set);
+            }
+        }
     }
 
     fn build(mut self, db: &'db dyn Db) -> Type<'db> {
-        self.simplify();
+        self.simplify(db);
         match (self.positive.len(), self.negative.len()) {
             (0, 0) => Type::Never,
             (1, 0) => self.positive[0],
@@ -429,10 +605,12 @@ mod tests {
     fn build_union_truthy_falsy() {
         let db = setup_db();
 
-        // `Truthy | Falsy` -> `Any` -- this probably should never happen in practice
+        // `Truthy | Falsy` -> `Never` -- this probably should never happen in practice
         let t0 = UnionType::from_elements(&db, [Type::Truthy, Type::Falsy]);
+        let t1 = UnionType::from_elements(&db, [Type::Truthy, Type::Falsy, Type::IntLiteral(0)]);
 
-        assert_eq!(t0, Type::Any);
+        assert_eq!(t0, Type::Never);
+        assert_eq!(t1, Type::IntLiteral(0));
     }
 
     impl<'db> IntersectionType<'db> {
@@ -586,137 +764,197 @@ mod tests {
         assert_eq!(ty, Type::IntLiteral(1));
     }
 
-    /// Test all tpes where `X & Falsy` can be evaluated to specific literals.
+    /// Test all tpes where `X & Falsy` or `X & Truthy` can be replaced by specific literals.
     #[test]
-    fn build_intersection_simplify_to_falsy_literals() {
+    fn build_intersection_simplify_to_falsy_or_truthy_literals() {
         let db = setup_db();
 
-        let falsy_int = IntersectionBuilder::new(&db)
-            .add_positive(KnownClass::Int.to_instance(&db))
-            .add_positive(Type::Falsy)
-            .build();
+        let falsy_int = IntersectionBuilder::build_falsy(&db, KnownClass::Int.to_instance(&db));
         assert_eq!(falsy_int, Type::IntLiteral(0));
 
         let empty_str = Type::StringLiteral(StringLiteralType::new(&db, "".into()));
-        let falsy_str = IntersectionBuilder::new(&db)
-            .add_positive(KnownClass::Str.to_instance(&db))
-            .add_positive(Type::Falsy)
-            .build();
+        let falsy_str = IntersectionBuilder::build_falsy(&db, KnownClass::Str.to_instance(&db));
         assert_eq!(falsy_str, empty_str);
 
-        let falsy_literal_str = IntersectionBuilder::new(&db)
-            .add_positive(Type::LiteralString)
-            .add_positive(Type::Falsy)
-            .build();
+        let falsy_literal_str = IntersectionBuilder::build_falsy(&db, Type::LiteralString);
         assert_eq!(falsy_literal_str, empty_str);
 
-        let falsy_bool = IntersectionBuilder::new(&db)
-            .add_positive(KnownClass::Bool.to_instance(&db))
-            .add_positive(Type::Falsy)
-            .build();
+        let falsy_bool = IntersectionBuilder::build_falsy(&db, KnownClass::Bool.to_instance(&db));
         assert_eq!(falsy_bool, Type::BooleanLiteral(false));
 
         let empty_tuple = Type::Tuple(TupleType::new(&db, vec![].into()));
-        let falsy_tuple = IntersectionBuilder::new(&db)
-            .add_positive(KnownClass::Tuple.to_instance(&db))
-            .add_positive(Type::Falsy)
-            .build();
+        let falsy_tuple = IntersectionBuilder::build_falsy(&db, KnownClass::Tuple.to_instance(&db));
         assert_eq!(falsy_tuple, empty_tuple);
 
         let empty_bytes = Type::BytesLiteral(BytesLiteralType::new(&db, vec![].into()));
-        let falsy_bytes = IntersectionBuilder::new(&db)
-            .add_positive(KnownClass::Bytes.to_instance(&db))
-            .add_positive(Type::Falsy)
-            .build();
+        let falsy_bytes = IntersectionBuilder::build_falsy(&db, KnownClass::Bytes.to_instance(&db));
         assert_eq!(falsy_bytes, empty_bytes);
+
+        // Currently the only case of known `Truthy` set
+        let falsy_bool = IntersectionBuilder::build_truthy(&db, KnownClass::Bool.to_instance(&db));
+        assert_eq!(falsy_bool, Type::BooleanLiteral(true));
     }
 
+    /// Tests that we simplify
+    /// - When `X` -> `AlwaysTrue`: `X & Truthy` = `X`
+    /// - When `X` -> `AlwaysTrue`: `X & Falsy` = `Never`
+    /// - When `X` -> `AlwaysFalse`: `X & Truthy` = `Never`
+    /// - When `X` -> `AlwaysFalse`: `X & Falsy` = `X`
     #[test]
-    fn build_intersection_known_literals_and_truthy() {
+    fn build_intersection_with_truthy_or_falsy_simplifies_when_always_true_or_false() {
         let db = setup_db();
 
+        // `X` -> `AlwaysTrue` => `X & Truthy` = `X`
         let hello_literal = Type::StringLiteral(StringLiteralType::new(&db, "hello".into()));
-        let hello_literal_and_truthy = IntersectionBuilder::new(&db)
-            .add_positive(hello_literal)
-            .add_positive(Type::Truthy)
-            .build();
-        assert_eq!(hello_literal_and_truthy, hello_literal);
+        assert_eq!(
+            IntersectionBuilder::build_truthy(&db, hello_literal),
+            hello_literal
+        );
+
+        assert_eq!(
+            IntersectionBuilder::build_truthy(&db, KnownClass::FunctionType.to_instance(&db)),
+            KnownClass::FunctionType.to_instance(&db)
+        );
+
+        // `X` -> `AlwaysTrue` => `X & Falsy` = `Never`
+        assert_eq!(
+            IntersectionBuilder::build_falsy(&db, Type::IntLiteral(8)),
+            Type::Never
+        );
+
+        assert_eq!(
+            IntersectionBuilder::build_falsy(
+                &db,
+                Type::Tuple(TupleType::new(&db, vec![Type::IntLiteral(0)].into()))
+            ),
+            Type::Never
+        );
+
+        // `X` -> `AlwaysFalse` => `X & Truthy` = `Never`
+        // TODO: add a test case for `NoneType` when supported
+
+        let empty_string = Type::StringLiteral(StringLiteralType::new(&db, "".into()));
+        assert_eq!(
+            IntersectionBuilder::build_truthy(&db, empty_string),
+            Type::Never
+        );
 
-        let zero_and_truthy = IntersectionBuilder::new(&db)
-            .add_positive(Type::IntLiteral(0))
-            .add_positive(Type::Truthy)
-            .build();
-        assert_eq!(zero_and_truthy, Type::Never);
+        let empty_bytes = Type::BytesLiteral(BytesLiteralType::new(&db, vec![].into()));
+        assert_eq!(
+            IntersectionBuilder::build_truthy(
+                &db,
+                UnionType::from_elements(&db, [empty_string, empty_bytes])
+            ),
+            Type::Never
+        );
+
+        // `X` -> `AlwaysFalse` => `X & Falsy` = `X`
+        let empty_tuple = Type::Tuple(TupleType::new(&db, vec![].into()));
+        assert_eq!(
+            IntersectionBuilder::build_falsy(&db, empty_tuple),
+            empty_tuple
+        );
 
-        let none_and_truthy = IntersectionBuilder::new(&db)
-            .add_positive(KnownClass::NoneType.to_instance(&db))
-            .add_positive(Type::Truthy)
-            .build();
-        assert_eq!(none_and_truthy, Type::Never);
+        assert_eq!(
+            IntersectionBuilder::build_falsy(&db, empty_bytes),
+            empty_bytes
+        );
     }
 
+    /// Tests that `X & !y` where `y` is the only value in `X & Falsy` simplifies to `X & Truthy`
     #[test]
-    fn build_intersection_truthy_and_falsy() {
+    fn build_intersection_of_type_with_all_falsy_set_in_negatives() {
         let db = setup_db();
 
-        // `Truthy & Falsy` -> `Never`
-        let truthy_and_falsy = IntersectionBuilder::new(&db)
-            .add_positive(Type::Truthy)
-            .add_positive(Type::Falsy)
-            .build();
-        assert_eq!(truthy_and_falsy, Type::Never);
-
-        let truthy_and_falsy = IntersectionBuilder::new(&db)
-            .add_positive(Type::Truthy)
-            .add_positive(Type::Falsy)
-            .build();
-        assert_eq!(truthy_and_falsy, Type::Never);
+        let int_instance = KnownClass::Int.to_instance(&db);
+        assert_eq!(
+            IntersectionBuilder::new(&db)
+                .add_positive(int_instance)
+                .add_negative(Type::IntLiteral(0))
+                .build(),
+            IntersectionBuilder::build_truthy(&db, int_instance)
+        );
     }
 
     #[test]
-    fn build_union_type_truthy_and_type_falsy() {
+    fn build_intersection_truthy_and_falsy() {
         let db = setup_db();
 
-        // `X & Falsy | X & Truthy` -> `X`
-        let truthy_int = UnionBuilder::new(&db)
-            .add(KnownClass::Int.to_instance(&db))
-            .add(Type::Truthy)
-            .build();
-        let falsy_int = UnionBuilder::new(&db)
-            .add(KnownClass::Int.to_instance(&db))
-            .add(Type::Falsy)
-            .build();
-        let truthy_and_falsy = UnionBuilder::new(&db)
-            .add(truthy_int)
-            .add(falsy_int)
-            .build();
-        assert_eq!(truthy_and_falsy, KnownClass::Int.to_instance(&db));
+        // `Truthy & Falsy` -> `Never`
+        let truthy_and_falsy = IntersectionBuilder::build_truthy(&db, Type::Falsy);
+        assert_eq!(truthy_and_falsy, Type::Never);
     }
 
     #[test]
-    fn build_intersection_truthy_and_falsy_is_always_positive() {
+    fn build_intersection_truthy_and_falsy_cant_be_in_negative_elements() {
         let db = setup_db();
 
         // `X & !Truthy` -> `X & Falsy`
-        let truthy_int_positive = IntersectionBuilder::new(&db)
-            .add_positive(KnownClass::Int.to_instance(&db))
-            .add_positive(Type::Truthy)
-            .build();
         let falsy_int_negative = IntersectionBuilder::new(&db)
             .add_positive(KnownClass::Int.to_instance(&db))
             .add_negative(Type::Falsy)
             .build();
-        assert_eq!(truthy_int_positive, falsy_int_negative);
+        assert_eq!(
+            IntersectionBuilder::build_truthy(&db, KnownClass::Int.to_instance(&db)),
+            falsy_int_negative
+        );
 
         // `X & !Falsy` -> `X & Truthy`
-        let falsy_int_positive = IntersectionBuilder::new(&db)
-            .add_positive(KnownClass::Int.to_instance(&db))
-            .add_positive(Type::Falsy)
-            .build();
         let truthy_int_negative = IntersectionBuilder::new(&db)
             .add_positive(KnownClass::Int.to_instance(&db))
             .add_negative(Type::Truthy)
             .build();
-        assert_eq!(falsy_int_positive, truthy_int_negative);
+        assert_eq!(
+            IntersectionBuilder::build_falsy(&db, KnownClass::Int.to_instance(&db)),
+            truthy_int_negative
+        );
+    }
+
+    #[test]
+    fn build_union_of_type_truthy_and_type_falsy() {
+        let db = setup_db();
+
+        // `object & Falsy | object & Truthy` -> `X`
+        let object_instance = KnownClass::Object.to_instance(&db);
+        let object_truthy_and_object_falsy = UnionBuilder::new(&db)
+            .add(IntersectionBuilder::build_truthy(&db, object_instance))
+            .add(IntersectionBuilder::build_falsy(&db, object_instance))
+            .build();
+        assert_eq!(object_truthy_and_object_falsy, object_instance);
+
+        // `int & Falsy | int & Truthy` -> `X`
+        // This is a special case because we know that `int & False` is `{0}`, so `int & Falsy`
+        // gets simplified to `Literal[0]` - but the feature should hold.
+        let int_instance = KnownClass::Int.to_instance(&db);
+        let int_truthy_and_int_falsy = UnionBuilder::new(&db)
+            .add(IntersectionBuilder::build_truthy(&db, int_instance))
+            .add(IntersectionBuilder::build_falsy(&db, int_instance))
+            .build();
+        assert_eq!(int_truthy_and_int_falsy, int_instance);
+    }
+
+    /// Tests building a union between `X & Truthy | y` where `y` is the only value in `X & Falsy`
+    #[test]
+    fn build_union_of_type_truthy_and_falsy_set() {
+        let db = setup_db();
+
+        let int_instance = KnownClass::Int.to_instance(&db);
+        assert_eq!(
+            UnionBuilder::new(&db)
+                .add(IntersectionBuilder::build_truthy(&db, int_instance))
+                .add(Type::IntLiteral(0))
+                .build(),
+            int_instance
+        );
+
+        let str_instance = KnownClass::Str.to_instance(&db);
+        let empty_str = Type::StringLiteral(StringLiteralType::new(&db, "".into()));
+        assert_eq!(
+            UnionBuilder::new(&db)
+                .add(empty_str)
+                .add(IntersectionBuilder::build_truthy(&db, str_instance))
+                .build(),
+            str_instance
+        );
     }
 }
diff --git a/crates/red_knot_python_semantic/src/types/display.rs b/crates/red_knot_python_semantic/src/types/display.rs
index 91a9e5381ad968..208b3c22046656 100644
--- a/crates/red_knot_python_semantic/src/types/display.rs
+++ b/crates/red_knot_python_semantic/src/types/display.rs
@@ -100,6 +100,8 @@ impl Display for DisplayRepresentation<'_> {
                 }
                 f.write_str("]")
             }
+            Type::Truthy => f.write_str("Truthy"),
+            Type::Falsy => f.write_str("Falsy"),
         }
     }
 }
diff --git a/crates/red_knot_python_semantic/src/types/infer.rs b/crates/red_knot_python_semantic/src/types/infer.rs
index 7c9d824f452642..81b4425a1c6792 100644
--- a/crates/red_knot_python_semantic/src/types/infer.rs
+++ b/crates/red_knot_python_semantic/src/types/infer.rs
@@ -48,6 +48,7 @@ use crate::semantic_index::semantic_index;
 use crate::semantic_index::symbol::{NodeWithScopeKind, NodeWithScopeRef, ScopeId};
 use crate::semantic_index::SemanticIndex;
 use crate::stdlib::builtins_module_scope;
+use crate::types::builder::IntersectionBuilder;
 use crate::types::diagnostic::{TypeCheckDiagnostic, TypeCheckDiagnostics};
 use crate::types::{
     bindings_ty, builtins_symbol_ty, declarations_ty, global_symbol_ty, symbol_ty,
@@ -2471,13 +2472,23 @@ impl<'db> TypeInferenceBuilder<'db> {
                 } else {
                     let is_last = i == n_values - 1;
                     match (ty.bool(db), is_last, op) {
-                        (Truthiness::Ambiguous, _, _) => ty,
+                        // We only every return a type early in an `and` if it's a part of the
+                        // `falsy` subset of its type.
+                        (Truthiness::Ambiguous, false, ast::BoolOp::And) => {
+                            IntersectionBuilder::build_falsy(db, ty)
+                        }
+                        // We only every return a type early in an `and` if it's a part of the
+                        // `truthy` subset of its type.
+                        (Truthiness::Ambiguous, false, ast::BoolOp::Or) => {
+                            IntersectionBuilder::build_truthy(db, ty)
+                        }
+
                         (Truthiness::AlwaysTrue, false, ast::BoolOp::And) => Type::Never,
                         (Truthiness::AlwaysFalse, false, ast::BoolOp::Or) => Type::Never,
                         (Truthiness::AlwaysFalse, _, ast::BoolOp::And)
                         | (Truthiness::AlwaysTrue, _, ast::BoolOp::Or) => {
                             done = true;
-                            ty
+                            ty // Those types are already truthy/falsy
                         }
                         (_, true, _) => ty,
                     }
@@ -4125,7 +4136,7 @@ mod tests {
         assert_public_ty(&db, "src/a.py", "g", "bool");
         assert_public_ty(&db, "src/a.py", "h", "Literal[False]");
         assert_public_ty(&db, "src/a.py", "i", "Literal[True]");
-        assert_public_ty(&db, "src/a.py", "j", "@Todo | Literal[True]");
+        assert_public_ty(&db, "src/a.py", "j", "@Todo & Falsy | Literal[True]");
 
         Ok(())
     }
@@ -4245,15 +4256,15 @@ mod tests {
         // 2. A() < B() and B() < C()  - split in N comparison
         // 3. A() and B()              - evaluate outcome types
         // 4. bool and bool            - evaluate truthiness
-        // 5. A | B                    - union of "first true" types
-        assert_public_ty(&db, "src/a.py", "a", "A | B");
+        // 5. A & Falsy | B            - A instances are returned if and only if falsy
+        assert_public_ty(&db, "src/a.py", "a", "A & Falsy | B");
         // Walking through the example
         // 1. 0 < 1 < A() < 3
         // 2. 0 < 1 and 1 < A() and A() < 3   - split in N comparison
         // 3. True and bool and A             - evaluate outcome types
         // 4. True and bool and bool          - evaluate truthiness
-        // 5. bool | A                        - union of "true" types
-        assert_public_ty(&db, "src/a.py", "b", "bool | A");
+        // 5. Literal[False] | A              - the 'bool' type is returned if falsy => `False`
+        assert_public_ty(&db, "src/a.py", "b", "Literal[False] | A");
         // Short-cicuit to False
         assert_public_ty(&db, "src/a.py", "c", "Literal[False]");
 
@@ -5421,15 +5432,7 @@ mod tests {
         )
         .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",
-        );
+        assert_public_ty(&db, "/src/a.py", "y", "Literal[0] | None");
     }
 
     #[test]
@@ -7545,8 +7548,8 @@ mod tests {
         db.write_dedented(
             "/src/a.py",
             "
-            def foo() -> str:
-                pass
+            def str_instance() -> str:
+                return ''
 
             a = True or False
             b = 'x' or 'y' or 'z'
@@ -7554,8 +7557,8 @@ mod tests {
             d = False or 'z'
             e = False or True
             f = False or False
-            g = foo() or False
-            h = foo() or True
+            g = str_instance() or False
+            h = str_instance() or True
             ",
         )?;
 
@@ -7565,8 +7568,8 @@ mod tests {
         assert_public_ty(&db, "/src/a.py", "d", r#"Literal["z"]"#);
         assert_public_ty(&db, "/src/a.py", "e", "Literal[True]");
         assert_public_ty(&db, "/src/a.py", "f", "Literal[False]");
-        assert_public_ty(&db, "/src/a.py", "g", "str | Literal[False]");
-        assert_public_ty(&db, "/src/a.py", "h", "str | Literal[True]");
+        assert_public_ty(&db, "/src/a.py", "g", "str & Truthy | Literal[False]");
+        assert_public_ty(&db, "/src/a.py", "h", "str & Truthy | Literal[True]");
 
         Ok(())
     }
@@ -7578,13 +7581,13 @@ mod tests {
         db.write_dedented(
             "/src/a.py",
             "
-            def foo() -> str:
-                pass
+            def str_instance() -> str:
+                return ''
 
             a = True and False
             b = False and True
-            c = foo() and False
-            d = foo() and True
+            c = str_instance() and False
+            d = True and str_instance()
             e = 'x' and 'y' and 'z'
             f = 'x' and 'y' and ''
             g = '' and 'y'
@@ -7593,8 +7596,8 @@ mod tests {
 
         assert_public_ty(&db, "/src/a.py", "a", "Literal[False]");
         assert_public_ty(&db, "/src/a.py", "b", "Literal[False]");
-        assert_public_ty(&db, "/src/a.py", "c", "str | Literal[False]");
-        assert_public_ty(&db, "/src/a.py", "d", "str | Literal[True]");
+        assert_public_ty(&db, "/src/a.py", "c", r#"Literal[""] | Literal[False]"#);
+        assert_public_ty(&db, "/src/a.py", "d", "str");
         assert_public_ty(&db, "/src/a.py", "e", r#"Literal["z"]"#);
         assert_public_ty(&db, "/src/a.py", "f", r#"Literal[""]"#);
         assert_public_ty(&db, "/src/a.py", "g", r#"Literal[""]"#);
@@ -7608,9 +7611,6 @@ mod tests {
         db.write_dedented(
             "/src/a.py",
             r#"
-            def foo() -> str:
-                pass
-
             a = "x" and "y" or "z"
             b = "x" or "y" and "z"
             c = "" and "y" or "z"
@@ -7670,7 +7670,7 @@ mod tests {
             "b",
             "Literal[True] | int & Truthy | Literal[\"\"]",
         );
-        // TODO: I don't know if red-knot can be smart enough to realise that
+        // Corner case with some builtins with a defined `truthy` or `falsy` set of values
         // `Literal[0]` = `int & Falsy`, which leads to:
         // `int & Truthy | Literal[0]` = `int & Truthy | int & Falsy` = `int`
         assert_public_ty(&db, "/src/a.py", "c", "int");

From 4a33cca281f34ed33a8bc25b9c4517806f2cc226 Mon Sep 17 00:00:00 2001
From: slyces <slyces.coding@gmail.com>
Date: Mon, 7 Oct 2024 18:23:07 +0200
Subject: [PATCH 4/8] fixup! [red-knot] feat: implement truthy/falsy cases in
 intersection/union

---
 crates/red_knot_python_semantic/src/types.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs
index 13bf878b814a61..48b21b0622bc83 100644
--- a/crates/red_knot_python_semantic/src/types.rs
+++ b/crates/red_knot_python_semantic/src/types.rs
@@ -406,7 +406,7 @@ impl<'db> Type<'db> {
         IntersectionBuilder::build_truthy(db, *self)
     }
 
-    /// Return the `Falsy` subset of this type (intersection with Truthy).
+    /// Return the `Falsy` subset of this type (intersection with Falsy).
     #[must_use]
     pub fn falsy(&self, db: &'db dyn Db) -> Type<'db> {
         self.falsy_set(db)

From 8bc292886758691aae116fdd020470edf6aaa3d0 Mon Sep 17 00:00:00 2001
From: slyces <slyces.coding@gmail.com>
Date: Tue, 8 Oct 2024 13:55:10 +0200
Subject: [PATCH 5/8] [red-knot] fix: remove branches with NoneType (prefer
 Type::None now)

---
 crates/red_knot_python_semantic/src/types.rs | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs
index 48b21b0622bc83..8e7d339e84190e 100644
--- a/crates/red_knot_python_semantic/src/types.rs
+++ b/crates/red_knot_python_semantic/src/types.rs
@@ -614,10 +614,6 @@ impl<'db> Type<'db> {
                 // More info in https://docs.python.org/3/library/stdtypes.html#truth-value-testing
                 Truthiness::Ambiguous
             }
-            // Temporary special case for `None` until we handle generic instances
-            Type::Instance(class) if class.is_known(db, KnownClass::NoneType) => {
-                Truthiness::AlwaysFalse
-            }
             // Temporary special case for `FunctionType` until we handle generic instances
             Type::Instance(class) if class.is_known(db, KnownClass::FunctionType) => {
                 Truthiness::AlwaysTrue

From 2028c0e5513873409ee946d5d4fa1c7583bdcd00 Mon Sep 17 00:00:00 2001
From: Simon <slyces.coding@gmail.com>
Date: Tue, 8 Oct 2024 13:59:34 +0200
Subject: [PATCH 6/8] [red-knot] fix: use python symbols for intersection in
 comments

Co-authored-by: Alex Waygood <Alex.Waygood@Gmail.com>
---
 crates/red_knot_python_semantic/src/types.rs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs
index 8e7d339e84190e..2b3eea997ef31e 100644
--- a/crates/red_knot_python_semantic/src/types.rs
+++ b/crates/red_knot_python_semantic/src/types.rs
@@ -641,9 +641,9 @@ impl<'db> Type<'db> {
             Type::Intersection(intersection) => {
                 // The truthiness of the intersection is the intersection of the truthiness of its
                 // elements:
-                // - `Ambiguous` ∩ `Truthy` = `Truthy`
-                // - `Ambiguous` ∩ `Falsy` = `Falsy`
-                // - `Truthy` ∩ `Falsy` = `Never`  -- this should be impossible to build
+                // - `Ambiguous` & `Truthy` == `Truthy`
+                // - `Ambiguous` & `Falsy` == `Falsy`
+                // - `Truthy` & `Falsy` == `Never`  -- this should be impossible to build
                 intersection
                     // Negative elements (what this intersection should not be) do not have an
                     // influence on the truthiness of the intersection.

From 54ac97f1bf36f5d4dcc72a6e5d5f052cbd047510 Mon Sep 17 00:00:00 2001
From: slyces <slyces.coding@gmail.com>
Date: Tue, 8 Oct 2024 14:13:40 +0200
Subject: [PATCH 7/8] [red-knot] fix: logic issue with `falsy_set` and
 instances

- Fix a logic issue when dealing with the falsy/truthy set of instances
  (set of size 1).
- Introduce `TupleType::empty` and others as a convenience method.
---
 crates/red_knot_python_semantic/src/types.rs  | 77 ++++++++++++-------
 .../src/types/builder.rs                      | 14 ++--
 2 files changed, 58 insertions(+), 33 deletions(-)

diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs
index 2b3eea997ef31e..30888a23e666ab 100644
--- a/crates/red_knot_python_semantic/src/types.rs
+++ b/crates/red_knot_python_semantic/src/types.rs
@@ -418,26 +418,28 @@ impl<'db> Type<'db> {
     #[must_use]
     pub fn falsy_set(&self, db: &'db dyn Db) -> Option<Type<'db>> {
         match self {
-            // Some builtin types have known falsy values
-            Self::Instance(class) if class.is_known(db, KnownClass::Bool) => {
-                Some(Self::BooleanLiteral(false))
-            }
-            Self::Instance(class) if class.is_known(db, KnownClass::Int) => {
-                Some(Self::IntLiteral(0))
-            }
-            Self::Instance(class) if class.is_known(db, KnownClass::Str) => {
-                Some(Self::StringLiteral(StringLiteralType::new(db, "".into())))
-            }
-            Self::Instance(class) if class.is_known(db, KnownClass::Bytes) => {
-                Some(Self::BytesLiteral(BytesLiteralType::new(db, vec![].into())))
-            }
-            Self::Instance(class) if class.is_known(db, KnownClass::Tuple) => {
-                Some(Self::Tuple(TupleType::new(db, vec![].into())))
-            }
-            Type::LiteralString => KnownClass::Str.to_instance(db).falsy_set(db),
-            Type::IntLiteral(_) => KnownClass::Int.to_instance(db).falsy_set(db),
-            Type::BooleanLiteral(_) => KnownClass::Bool.to_instance(db).falsy_set(db),
-            _ => None,
+            Self::Instance(class) => match class.known(db) {
+                // For the following types, we know the logic for falsiness and can represent
+                // specific instances of that type, so we can give back a precise subset.
+                Some(KnownClass::Bool) => Some(Self::BooleanLiteral(false)),
+                Some(KnownClass::Int) => Some(Self::IntLiteral(0)),
+                Some(KnownClass::Bytes) => Some(Self::BytesLiteral(BytesLiteralType::empty(db))),
+                Some(KnownClass::Str) => Some(Self::StringLiteral(StringLiteralType::empty(db))),
+                Some(KnownClass::Tuple) => Some(Self::Tuple(TupleType::empty(db))),
+                _ => match self.bool(db) {
+                    // When a `__bool__` signature is `AlwaysFalse`, it means that the falsy set is
+                    // the whole type (that we had as input), and the truthy set is empty.
+                    Truthiness::AlwaysFalse => Some(*self),
+                    Truthiness::AlwaysTrue => Some(Type::Never),
+                    Truthiness::Ambiguous => None,
+                },
+            },
+            Type::LiteralString => Some(Self::StringLiteral(StringLiteralType::empty(db))),
+            _ => match self.bool(db) {
+                Truthiness::AlwaysFalse => Some(*self),
+                Truthiness::AlwaysTrue => Some(Type::Never),
+                Truthiness::Ambiguous => None,
+            },
         }
     }
 
@@ -446,12 +448,17 @@ impl<'db> Type<'db> {
     #[must_use]
     pub fn truthy_set(&self, db: &'db dyn Db) -> Option<Type<'db>> {
         match self {
-            Type::Instance(class) if class.is_known(db, KnownClass::Bool) => {
-                Some(Type::BooleanLiteral(true))
-            }
-            Type::BooleanLiteral(_) => KnownClass::Bool.to_instance(db).truthy_set(db),
-            // There is no instance of `NoneType` that is truthy
-            Type::Instance(class) if class.is_known(db, KnownClass::NoneType) => Some(Type::Never),
+            Type::None => Some(Type::Never),
+            Type::Instance(class) => match class.known(db) {
+                Some(KnownClass::Bool) => Some(Type::BooleanLiteral(true)),
+                _ => match self.bool(db) {
+                    // When a `__bool__` signature is `AlwaysTrue`, it means that the truthy set is
+                    // the whole type (that we had as input), and the falsy set is empty.
+                    Truthiness::AlwaysTrue => Some(*self),
+                    Truthiness::AlwaysFalse => Some(Type::Never),
+                    Truthiness::Ambiguous => None,
+                },
+            },
             _ => None,
         }
     }
@@ -1589,18 +1596,36 @@ pub struct StringLiteralType<'db> {
     value: Box<str>,
 }
 
+impl<'db> StringLiteralType<'db> {
+    pub fn empty(db: &'db dyn Db) -> Self {
+        Self::new(db, Box::default())
+    }
+}
+
 #[salsa::interned]
 pub struct BytesLiteralType<'db> {
     #[return_ref]
     value: Box<[u8]>,
 }
 
+impl<'db> BytesLiteralType<'db> {
+    pub fn empty(db: &'db dyn Db) -> Self {
+        Self::new(db, Box::default())
+    }
+}
+
 #[salsa::interned]
 pub struct TupleType<'db> {
     #[return_ref]
     elements: Box<[Type<'db>]>,
 }
 
+impl<'db> TupleType<'db> {
+    pub fn empty(db: &'db dyn Db) -> Self {
+        Self::new(db, Box::default())
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use super::{
diff --git a/crates/red_knot_python_semantic/src/types/builder.rs b/crates/red_knot_python_semantic/src/types/builder.rs
index 8ec0173bcc8193..706f3a65576d7d 100644
--- a/crates/red_knot_python_semantic/src/types/builder.rs
+++ b/crates/red_knot_python_semantic/src/types/builder.rs
@@ -772,7 +772,7 @@ mod tests {
         let falsy_int = IntersectionBuilder::build_falsy(&db, KnownClass::Int.to_instance(&db));
         assert_eq!(falsy_int, Type::IntLiteral(0));
 
-        let empty_str = Type::StringLiteral(StringLiteralType::new(&db, "".into()));
+        let empty_str = Type::StringLiteral(StringLiteralType::empty(&db));
         let falsy_str = IntersectionBuilder::build_falsy(&db, KnownClass::Str.to_instance(&db));
         assert_eq!(falsy_str, empty_str);
 
@@ -782,11 +782,11 @@ mod tests {
         let falsy_bool = IntersectionBuilder::build_falsy(&db, KnownClass::Bool.to_instance(&db));
         assert_eq!(falsy_bool, Type::BooleanLiteral(false));
 
-        let empty_tuple = Type::Tuple(TupleType::new(&db, vec![].into()));
+        let empty_tuple = Type::Tuple(TupleType::empty(&db));
         let falsy_tuple = IntersectionBuilder::build_falsy(&db, KnownClass::Tuple.to_instance(&db));
         assert_eq!(falsy_tuple, empty_tuple);
 
-        let empty_bytes = Type::BytesLiteral(BytesLiteralType::new(&db, vec![].into()));
+        let empty_bytes = Type::BytesLiteral(BytesLiteralType::empty(&db));
         let falsy_bytes = IntersectionBuilder::build_falsy(&db, KnownClass::Bytes.to_instance(&db));
         assert_eq!(falsy_bytes, empty_bytes);
 
@@ -833,13 +833,13 @@ mod tests {
         // `X` -> `AlwaysFalse` => `X & Truthy` = `Never`
         // TODO: add a test case for `NoneType` when supported
 
-        let empty_string = Type::StringLiteral(StringLiteralType::new(&db, "".into()));
+        let empty_string = Type::StringLiteral(StringLiteralType::empty(&db));
         assert_eq!(
             IntersectionBuilder::build_truthy(&db, empty_string),
             Type::Never
         );
 
-        let empty_bytes = Type::BytesLiteral(BytesLiteralType::new(&db, vec![].into()));
+        let empty_bytes = Type::BytesLiteral(BytesLiteralType::empty(&db));
         assert_eq!(
             IntersectionBuilder::build_truthy(
                 &db,
@@ -849,7 +849,7 @@ mod tests {
         );
 
         // `X` -> `AlwaysFalse` => `X & Falsy` = `X`
-        let empty_tuple = Type::Tuple(TupleType::new(&db, vec![].into()));
+        let empty_tuple = Type::Tuple(TupleType::empty(&db));
         assert_eq!(
             IntersectionBuilder::build_falsy(&db, empty_tuple),
             empty_tuple
@@ -948,7 +948,7 @@ mod tests {
         );
 
         let str_instance = KnownClass::Str.to_instance(&db);
-        let empty_str = Type::StringLiteral(StringLiteralType::new(&db, "".into()));
+        let empty_str = Type::StringLiteral(StringLiteralType::empty(&db));
         assert_eq!(
             UnionBuilder::new(&db)
                 .add(empty_str)

From 4ce78b9a8f3bd61a268fa825c2d0035a2944c594 Mon Sep 17 00:00:00 2001
From: slyces <slyces.coding@gmail.com>
Date: Tue, 8 Oct 2024 14:47:28 +0200
Subject: [PATCH 8/8] fixup! [red-knot] fix: logic issue with `falsy_set` and
 instances

---
 crates/red_knot_python_semantic/src/types.rs | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs
index 30888a23e666ab..5bf1051a9af196 100644
--- a/crates/red_knot_python_semantic/src/types.rs
+++ b/crates/red_knot_python_semantic/src/types.rs
@@ -448,7 +448,6 @@ impl<'db> Type<'db> {
     #[must_use]
     pub fn truthy_set(&self, db: &'db dyn Db) -> Option<Type<'db>> {
         match self {
-            Type::None => Some(Type::Never),
             Type::Instance(class) => match class.known(db) {
                 Some(KnownClass::Bool) => Some(Type::BooleanLiteral(true)),
                 _ => match self.bool(db) {
@@ -459,7 +458,11 @@ impl<'db> Type<'db> {
                     Truthiness::Ambiguous => None,
                 },
             },
-            _ => None,
+            _ => match self.bool(db) {
+                Truthiness::AlwaysFalse => Some(*self),
+                Truthiness::AlwaysTrue => Some(Type::Never),
+                Truthiness::Ambiguous => None,
+            },
         }
     }