From 09eeee99d471b6452cd09bcb6fa042f834365bdc Mon Sep 17 00:00:00 2001 From: David Peter Date: Tue, 15 Oct 2024 09:21:06 +0200 Subject: [PATCH 01/11] [red knot] Fix narrowing for 'is not' conditionals --- .../mdtest/narrow/conditionals_is.md | 26 +++++++ .../mdtest/narrow/conditionals_is_not.md | 37 ++++++++++ .../resources/mdtest/narrow/match.md | 17 +++++ crates/red_knot_python_semantic/src/types.rs | 73 +++++++++++++++++++ .../src/types/infer.rs | 47 ------------ .../src/types/narrow.rs | 21 ++++-- 6 files changed, 167 insertions(+), 54 deletions(-) create mode 100644 crates/red_knot_python_semantic/resources/mdtest/narrow/conditionals_is.md create mode 100644 crates/red_knot_python_semantic/resources/mdtest/narrow/conditionals_is_not.md create mode 100644 crates/red_knot_python_semantic/resources/mdtest/narrow/match.md 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..9e63e72bf70cf9 --- /dev/null +++ b/crates/red_knot_python_semantic/resources/mdtest/narrow/conditionals_is.md @@ -0,0 +1,26 @@ +# 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 +x = 345 +y = x if flag else None + +if y is x: + # TODO the following should be simplified to 'Literal[345]' + reveal_type(y) # revealed: Literal[345] | None & Literal[345] + +reveal_type(y) # revealed: Literal[345] | 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..f1acc45b2c8477 --- /dev/null +++ b/crates/red_knot_python_semantic/resources/mdtest/narrow/conditionals_is_not.md @@ -0,0 +1,37 @@ +# 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: + +```py +x = [1] +y = [1] + +if x is not y: + 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..0e4077398595e6 100644 --- a/crates/red_knot_python_semantic/src/types.rs +++ b/crates/red_knot_python_semantic/src/types.rs @@ -463,6 +463,55 @@ 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::Unbound + | Type::Module(..) + | Type::Instance(..) + | 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(..) => true, + Type::Tuple(tuple) => { + !tuple.elements(db).is_empty() + && tuple.elements(db).iter().all(|ty| ty.is_singleton(db)) + } + Type::Union(..) => { + // There are some rare edge cases where a union type might be a singleton type. + // For example, a union with just one element (which itself is a singleton). Or + // a union with an empty type (e.g. Never | None). Here, we assume that such + // types would have been simplified to a different representation earlier and + // simply return false. + 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 + } + Type::Todo => todo!(), + } + } + /// Resolve a member access of a type. /// /// For example, if `foo` is `Type::Instance()`, @@ -1514,6 +1563,7 @@ mod tests { enum Ty { Never, Unknown, + None, Any, IntLiteral(i64), BoolLiteral(bool), @@ -1530,6 +1580,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 +1669,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![Ty::None]))] + #[test_case(Ty::Tuple(vec![Ty::None, Ty::BoolLiteral(true)]))] + 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![]))] + 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..ffdb69059150ce 100644 --- a/crates/red_knot_python_semantic/src/types/narrow.rs +++ b/crates/red_knot_python_semantic/src/types/narrow.rs @@ -155,13 +155,20 @@ 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); + } + ast::CmpOp::Is => { + self.constraints.insert(symbol, comp_ty); + } + _ => { + // TODO other comparison types + } + } } } } From e241c422120ca11947828a40a82ddf5891120a42 Mon Sep 17 00:00:00 2001 From: David Peter Date: Tue, 15 Oct 2024 11:02:03 +0200 Subject: [PATCH 02/11] Move Type::Todo to the false-branch --- 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 0e4077398595e6..07b831bcab2f38 100644 --- a/crates/red_knot_python_semantic/src/types.rs +++ b/crates/red_knot_python_semantic/src/types.rs @@ -472,6 +472,7 @@ impl<'db> Type<'db> { Type::Any | Type::Never | Type::Unknown + | Type::Todo | Type::Unbound | Type::Module(..) | Type::Instance(..) @@ -508,7 +509,6 @@ impl<'db> Type<'db> { // false } - Type::Todo => todo!(), } } From 749f176ae510017f307809836dc96eada70d7db8 Mon Sep 17 00:00:00 2001 From: David Peter Date: Tue, 15 Oct 2024 11:11:17 +0200 Subject: [PATCH 03/11] The empty tuple type is a singleton type --- crates/red_knot_python_semantic/src/types.rs | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs index 07b831bcab2f38..113650a6fe0082 100644 --- a/crates/red_knot_python_semantic/src/types.rs +++ b/crates/red_knot_python_semantic/src/types.rs @@ -486,10 +486,7 @@ impl<'db> Type<'db> { false } Type::None | Type::BooleanLiteral(_) | Type::Function(..) | Type::Class(..) => true, - Type::Tuple(tuple) => { - !tuple.elements(db).is_empty() - && tuple.elements(db).iter().all(|ty| ty.is_singleton(db)) - } + Type::Tuple(tuple) => tuple.elements(db).iter().all(|ty| ty.is_singleton(db)), Type::Union(..) => { // There are some rare edge cases where a union type might be a singleton type. // For example, a union with just one element (which itself is a singleton). Or @@ -1672,6 +1669,7 @@ mod tests { #[test_case(Ty::None)] #[test_case(Ty::BoolLiteral(true))] #[test_case(Ty::BoolLiteral(false))] + #[test_case(Ty::Tuple(vec![]))] #[test_case(Ty::Tuple(vec![Ty::None]))] #[test_case(Ty::Tuple(vec![Ty::None, Ty::BoolLiteral(true)]))] fn is_singleton(from: Ty) { @@ -1684,7 +1682,6 @@ mod tests { #[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![]))] fn is_not_singleton(from: Ty) { let db = setup_db(); From e069381a237f0198b7e24a67118b19340eb3745d Mon Sep 17 00:00:00 2001 From: David Peter Date: Tue, 15 Oct 2024 13:18:16 +0200 Subject: [PATCH 04/11] Fix behavior for tuple types --- crates/red_knot_python_semantic/src/types.rs | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs index 113650a6fe0082..b6a99c9acd4316 100644 --- a/crates/red_knot_python_semantic/src/types.rs +++ b/crates/red_knot_python_semantic/src/types.rs @@ -486,7 +486,15 @@ impl<'db> Type<'db> { false } Type::None | Type::BooleanLiteral(_) | Type::Function(..) | Type::Class(..) => true, - Type::Tuple(tuple) => tuple.elements(db).iter().all(|ty| ty.is_singleton(db)), + 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(..) => { // There are some rare edge cases where a union type might be a singleton type. // For example, a union with just one element (which itself is a singleton). Or @@ -1670,8 +1678,6 @@ mod tests { #[test_case(Ty::BoolLiteral(true))] #[test_case(Ty::BoolLiteral(false))] #[test_case(Ty::Tuple(vec![]))] - #[test_case(Ty::Tuple(vec![Ty::None]))] - #[test_case(Ty::Tuple(vec![Ty::None, Ty::BoolLiteral(true)]))] fn is_singleton(from: Ty) { let db = setup_db(); @@ -1682,6 +1688,8 @@ mod tests { #[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(); From a95b4d57c1f75cc4d3d86c43a37bc491a326b6cc Mon Sep 17 00:00:00 2001 From: David Peter Date: Tue, 15 Oct 2024 13:21:16 +0200 Subject: [PATCH 05/11] Use custom type instead of LiteralInt --- .../resources/mdtest/narrow/conditionals_is.md | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) 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 index 9e63e72bf70cf9..1f51771dc035c3 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/narrow/conditionals_is.md +++ b/crates/red_knot_python_semantic/resources/mdtest/narrow/conditionals_is.md @@ -15,12 +15,15 @@ reveal_type(x) # revealed: None | Literal[1] ## `is` for other types ```py -x = 345 +class A: + ... + +x = A() y = x if flag else None if y is x: - # TODO the following should be simplified to 'Literal[345]' - reveal_type(y) # revealed: Literal[345] | None & Literal[345] + # TODO the following should be simplified to 'A' + reveal_type(y) # revealed: A | None & A -reveal_type(y) # revealed: Literal[345] | None +reveal_type(y) # revealed: A | None ``` From b425e6a34a46bc056f021738811c9c7feff54cb0 Mon Sep 17 00:00:00 2001 From: David Peter Date: Tue, 15 Oct 2024 13:23:10 +0200 Subject: [PATCH 06/11] Add explanation to 'is not' test --- .../resources/mdtest/narrow/conditionals_is_not.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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 index f1acc45b2c8477..4c196e31fcb71f 100644 --- 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 @@ -26,7 +26,9 @@ if x is not False: ## `is not` for non-singleton types -Non-singleton types should *not* narrow the type: +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] From da842bbc38e3d46c81e1e1f81c2209e7147134b5 Mon Sep 17 00:00:00 2001 From: David Peter Date: Tue, 15 Oct 2024 14:02:02 +0200 Subject: [PATCH 07/11] Add TODO comment --- .../resources/mdtest/narrow/conditionals_is_not.md | 1 + 1 file changed, 1 insertion(+) 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 index 4c196e31fcb71f..481e70e6d38dc8 100644 --- 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 @@ -35,5 +35,6 @@ x = [1] y = [1] if x is not y: + # TODO: should include type parameter: list[int] reveal_type(x) # revealed: list ``` From edfaf896e4d68a2da03871774c5f722d8a2f36e2 Mon Sep 17 00:00:00 2001 From: David Peter Date: Tue, 15 Oct 2024 14:09:24 +0200 Subject: [PATCH 08/11] Shorten comment regarding union types --- crates/red_knot_python_semantic/src/types.rs | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs index b6a99c9acd4316..8c6e2e7c4768a3 100644 --- a/crates/red_knot_python_semantic/src/types.rs +++ b/crates/red_knot_python_semantic/src/types.rs @@ -496,11 +496,9 @@ impl<'db> Type<'db> { tuple.elements(db).is_empty() } Type::Union(..) => { - // There are some rare edge cases where a union type might be a singleton type. - // For example, a union with just one element (which itself is a singleton). Or - // a union with an empty type (e.g. Never | None). Here, we assume that such - // types would have been simplified to a different representation earlier and - // simply return false. + // 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(..) => { From b219c6fc2c802d429d59fad3360f9b4f2dcccf36 Mon Sep 17 00:00:00 2001 From: David Peter Date: Tue, 15 Oct 2024 14:11:09 +0200 Subject: [PATCH 09/11] Add TODO comment --- 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 8c6e2e7c4768a3..c6d0757f9eab71 100644 --- a/crates/red_knot_python_semantic/src/types.rs +++ b/crates/red_knot_python_semantic/src/types.rs @@ -475,7 +475,7 @@ impl<'db> Type<'db> { | Type::Todo | Type::Unbound | Type::Module(..) - | Type::Instance(..) + | Type::Instance(..) // TODO some instance types can be singleton types (EllipsisType, NotImplementedType) | Type::IntLiteral(..) | Type::StringLiteral(..) | Type::BytesLiteral(..) From 79f809cd1361d76f9353438320e7963eb60cbc44 Mon Sep 17 00:00:00 2001 From: David Peter Date: Tue, 15 Oct 2024 14:13:38 +0200 Subject: [PATCH 10/11] Handle non-singleton 'is not' case --- .../red_knot_python_semantic/src/types/narrow.rs | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/crates/red_knot_python_semantic/src/types/narrow.rs b/crates/red_knot_python_semantic/src/types/narrow.rs index ffdb69059150ce..0f84b9c84ac2d4 100644 --- a/crates/red_knot_python_semantic/src/types/narrow.rs +++ b/crates/red_knot_python_semantic/src/types/narrow.rs @@ -156,11 +156,15 @@ impl<'db> NarrowingConstraintsBuilder<'db> { for (op, comparator) in std::iter::zip(&**ops, &**comparators) { let comp_ty = inference.expression_ty(comparator.scoped_ast_id(self.db, scope)); 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); + 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); From 9169e35175713706547d2e88625aacf6fe52bc59 Mon Sep 17 00:00:00 2001 From: David Peter Date: Tue, 15 Oct 2024 14:26:25 +0200 Subject: [PATCH 11/11] Modules are singleton types as well --- crates/red_knot_python_semantic/src/types.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs index c6d0757f9eab71..66347883b9d327 100644 --- a/crates/red_knot_python_semantic/src/types.rs +++ b/crates/red_knot_python_semantic/src/types.rs @@ -474,7 +474,6 @@ impl<'db> Type<'db> { | Type::Unknown | Type::Todo | Type::Unbound - | Type::Module(..) | Type::Instance(..) // TODO some instance types can be singleton types (EllipsisType, NotImplementedType) | Type::IntLiteral(..) | Type::StringLiteral(..) @@ -485,7 +484,7 @@ impl<'db> Type<'db> { // are both of type Literal[345], for example. false } - Type::None | Type::BooleanLiteral(_) | Type::Function(..) | Type::Class(..) => true, + 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 `()`