diff --git a/crates/red_knot_python_semantic/resources/mdtest/narrow/conditionals_is.md b/crates/red_knot_python_semantic/resources/mdtest/narrow/conditionals_is.md new file mode 100644 index 00000000000000..1f51771dc035c3 --- /dev/null +++ b/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 +``` diff --git a/crates/red_knot_python_semantic/resources/mdtest/narrow/conditionals_is_not.md b/crates/red_knot_python_semantic/resources/mdtest/narrow/conditionals_is_not.md new file mode 100644 index 00000000000000..481e70e6d38dc8 --- /dev/null +++ b/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 +``` diff --git a/crates/red_knot_python_semantic/resources/mdtest/narrow/match.md b/crates/red_knot_python_semantic/resources/mdtest/narrow/match.md new file mode 100644 index 00000000000000..b3218d2c6ed1b1 --- /dev/null +++ b/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 +``` diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs index f820331a21c35a..66347883b9d327 100644 --- a/crates/red_knot_python_semantic/src/types.rs +++ b/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()`, @@ -1514,6 +1565,7 @@ mod tests { enum Ty { Never, Unknown, + None, Any, IntLiteral(i64), BoolLiteral(bool), @@ -1530,6 +1582,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) => { @@ -1618,6 +1671,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"))] diff --git a/crates/red_knot_python_semantic/src/types/infer.rs b/crates/red_knot_python_semantic/src/types/infer.rs index 4b1c420bb47412..7b6debffc05198 100644 --- a/crates/red_knot_python_semantic/src/types/infer.rs +++ b/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(); diff --git a/crates/red_knot_python_semantic/src/types/narrow.rs b/crates/red_knot_python_semantic/src/types/narrow.rs index 8ca57af1168bcb..0f84b9c84ac2d4 100644 --- a/crates/red_knot_python_semantic/src/types/narrow.rs +++ b/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) { - let ty = IntersectionBuilder::new(self.db) - .add_negative(comp_ty) - .build(); - self.constraints.insert(symbol, ty); - }; - // TODO other comparison types + match op { + ast::CmpOp::IsNot => { + if comp_ty.is_singleton(self.db) { + let ty = IntersectionBuilder::new(self.db) + .add_negative(comp_ty) + .build(); + 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 + } + } } } }