[red-knot] Do not assume that x != 0 if x inhabits ~Literal[0]

crates/red_knot_python_semantic/resources/mdtest/comparison/intersections.md

@@ -50,13 +50,17 @@ reveal_type(x)  # revealed: LiteralString
 if x != "abc":
     reveal_type(x)  # revealed: LiteralString & ~Literal["abc"]
 
-    reveal_type(x == "abc")  # revealed: Literal[False]
-    reveal_type("abc" == x)  # revealed: Literal[False]
+    # TODO: This should be `Literal[False]`
+    reveal_type(x == "abc")  # revealed: bool
+    # TODO: This should be `Literal[False]`
+    reveal_type("abc" == x)  # revealed: bool
     reveal_type(x == "something else")  # revealed: bool
     reveal_type("something else" == x)  # revealed: bool
 
-    reveal_type(x != "abc")  # revealed: Literal[True]
-    reveal_type("abc" != x)  # revealed: Literal[True]
+    # TODO: This should be `Literal[True]`
+    reveal_type(x != "abc")  # revealed: bool
+    # TODO: This should be `Literal[True]`
+    reveal_type("abc" != x)  # revealed: bool
     reveal_type(x != "something else")  # revealed: bool
     reveal_type("something else" != x)  # revealed: bool
 
@@ -79,10 +83,10 @@ def _(x: int):
     if x != 1:
         reveal_type(x)  # revealed: int & ~Literal[1]
 
-        reveal_type(x != 1)  # revealed: Literal[True]
+        reveal_type(x != 1)  # revealed: bool
         reveal_type(x != 2)  # revealed: bool
 
-        reveal_type(x == 1)  # revealed: Literal[False]
+        reveal_type(x == 1)  # revealed: bool
         reveal_type(x == 2)  # revealed: bool
 ```
 

crates/red_knot_python_semantic/resources/mdtest/type_api.md

@@ -23,12 +23,21 @@ def negate(n1: Not[int], n2: Not[Not[int]], n3: Not[Not[Not[int]]]) -> None:
     reveal_type(n2)  # revealed: int
     reveal_type(n3)  # revealed: ~int
 
-def static_truthiness(not_one: Not[Literal[1]]) -> None:
-    static_assert(not_one != 1)
-    static_assert(not (not_one == 1))
-
 # error: "Special form `knot_extensions.Not` expected exactly one type parameter"
 n: Not[int, str]
+
+def static_truthiness(not_one: Not[Literal[1]]) -> None:
+    # these are both boolean-literal types,
+    # since all possible runtime objects that are created by the literal syntax `1`
+    # are members of the type `Literal[1]`
+    reveal_type(not_one is not 1)  # revealed: bool
+    reveal_type(not_one is 1)  # revealed: bool
+
+    # But these are both `bool`, rather than `Literal[True]` or `Literal[False]`
+    # as there are many runtime objects that inhabit the type `~Literal[1]`
+    # but still compare equal to `1`. Two examples are `1.0` and `True`.
+    reveal_type(not_one != 1)  # revealed: bool
+    reveal_type(not_one == 1)  # revealed: bool
 ```
 
 ### Intersection
@@ -170,13 +179,11 @@ Static assertions can be used to enforce narrowing constraints:
 ```py
 from knot_extensions import static_assert
 
-def f(x: int) -> None:
-    if x != 0:
-        static_assert(x != 0)
+def f(x: int | None) -> None:
+    if x is not None:
+        static_assert(x is not None)
     else:
-        # `int` can be subclassed, so we cannot assert that `x == 0` here:
-        # error: "Static assertion error: argument of type `bool` has an ambiguous static truthiness"
-        static_assert(x == 0)
+        static_assert(x is None)
 ```
 
 ### Truthy expressions

crates/red_knot_python_semantic/src/types/infer.rs

@@ -5264,12 +5264,6 @@ impl<'db> TypeInferenceBuilder<'db> {
             };
 
             match (op, result) {
-                (ast::CmpOp::Eq, Some(Type::BooleanLiteral(true))) => {
-                    return Ok(Type::BooleanLiteral(false));
-                }
-                (ast::CmpOp::NotEq, Some(Type::BooleanLiteral(false))) => {
-                    return Ok(Type::BooleanLiteral(true));
-                }
                 (ast::CmpOp::Is, Some(Type::BooleanLiteral(true))) => {
                     return Ok(Type::BooleanLiteral(false));
                 }
@@ -5319,6 +5313,9 @@ impl<'db> TypeInferenceBuilder<'db> {
         // we would get a result type `Literal[True]` which is too narrow.
         //
         let mut builder = IntersectionBuilder::new(self.db());
+
+        builder = builder.add_positive(KnownClass::Bool.to_instance(self.db()));
+
         for pos in intersection.positive(self.db()) {
             let result = match intersection_on {
                 IntersectionOn::Left => {
@@ -5393,6 +5390,8 @@ impl<'db> TypeInferenceBuilder<'db> {
                 ast::CmpOp::LtE => Ok(Type::BooleanLiteral(n <= m)),
                 ast::CmpOp::Gt => Ok(Type::BooleanLiteral(n > m)),
                 ast::CmpOp::GtE => Ok(Type::BooleanLiteral(n >= m)),
+                // We cannot say that two equal int Literals will return True from an `is` or `is not` comparison.
+                // Even if they are the same value, they may not be the same object.
                 ast::CmpOp::Is => {
                     if n == m {
                         Ok(KnownClass::Bool.to_instance(self.db()))