Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[red-knot] Support for not equal narrowing #13749

Merged
merged 7 commits into from
Oct 21, 2024
Merged
Show file tree
Hide file tree
Changes from 6 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
# Narrowing for nested conditionals
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This test is not related to the new feature here, but it's something I wanted to add. Using != narrowing, we can now construct "meaningful" large intersection types.


```py
def int_instance() -> int: ...


x = int_instance()

if x != 1:
if x != 2:
if x != 3:
reveal_type(x) # revealed: int & ~Literal[1] & ~Literal[2] & ~Literal[3]
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This display could be improved, but I don't think that's a priority unless we see it causing unreadable types in real-world code.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This display could be improved

You mean int & ~Literal[1, 2, 3]? Or the general fact that we show intersection types to users? (which pyright and mypy don't seem to do?)

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I meant condensed, yeah. I'm ok with showing intersection types to users. (Pyright and mypy will in some cases do so, but they format it like "subclass of A and B")

```
Original file line number Diff line number Diff line change
@@ -0,0 +1,56 @@
# Narrowing for `!=` conditionals

## `x != None`

```py
x = None if flag else 1

if x != None:
reveal_type(x) # revealed: Literal[1]
```

## `!=` for other singleton types

```py
x = True if flag else False

if x != False:
reveal_type(x) # revealed: Literal[True]
```

## `x != y` where `y` is of literal type

```py
x = 1 if flag else 2

if x != 1:
reveal_type(x) # revealed: Literal[2]
```

## `x != y` where `y` is a single-valued type

```py
class A: ...


class B: ...


C = A if flag else B

if C != A:
reveal_type(C) # revealed: Literal[B]
```

## `!=` 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

if x != 0:
reveal_type(x) # revealed: Literal[1]
```
Copy link
Contributor

@carljm carljm Oct 21, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This test doesn't currently seem to make sense. The comparison here is against Literal[0], which is a single-valued type, and we will narrow for != 0, as shown just a couple tests above. This test is really just testing that Literal[1] and Literal[0] are disjoint, meaning the intersection Literal[1] & ~Literal[0] immediately simplifies to Literal[1]. So this test should either be removed, or re-titled to describe what it actually tests.

I do think we should add some tests here showing that we don't do wrong narrowings against non-single-valued types, particularly instance types. For example, a = A(); b = B(); if a != b: ... should not narrow to A & ~B.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This test doesn't currently seem to make sense

Absolutely. I just pushed the version which I had lying around locally already, but didn't commit+push because I got interrupted (sorry). I think it's more or less equivalent to what you proposed, but let me know if I should add something similar to a = A(); b = B(); if a != b: ....

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The test you pushed looks sufficient!

74 changes: 74 additions & 0 deletions crates/red_knot_python_semantic/src/types.rs
Original file line number Diff line number Diff line change
Expand Up @@ -667,6 +667,55 @@ impl<'db> Type<'db> {
}
}

/// Return true if this type is non-empty and all inhabitants of this type compare equal.
pub(crate) fn is_single_valued(self, db: &'db dyn Db) -> bool {
match self {
Type::None
| Type::Function(..)
| Type::Module(..)
| Type::Class(..)
| Type::IntLiteral(..)
| Type::BooleanLiteral(..)
| Type::StringLiteral(..)
| Type::BytesLiteral(..) => true,

Type::Tuple(tuple) => tuple
.elements(db)
.iter()
.all(|elem| elem.is_single_valued(db)),

Type::Instance(class_type) => match class_type.known(db) {
Some(KnownClass::NoneType) => true,
Some(
KnownClass::Bool
| KnownClass::Object
| KnownClass::Bytes
| KnownClass::Type
| KnownClass::Int
| KnownClass::Float
| KnownClass::Str
| KnownClass::List
| KnownClass::Tuple
| KnownClass::Set
| KnownClass::Dict
| KnownClass::GenericAlias
| KnownClass::ModuleType
| KnownClass::FunctionType,
) => false,
None => false,
},

Type::Any
| Type::Never
| Type::Unknown
| Type::Unbound
| Type::Todo
| Type::Union(..)
| Type::Intersection(..)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There are probably ways in which an intersection can be single-valued, but I did not invest time into it for now. I can add a TODO, if we think it's important.

Copy link
Contributor

@carljm carljm Oct 21, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think an intersection would be single-valued if at least one type in its positive side is single-valued.

But I think this can only occur, given intersection simplification, if there is a single-valued type that is overlapping (not disjoint) with some other type, but neither is a subtype of the other. If they are disjoint, or if one is a subtype of the other, then they can't occur in the same intersection without one or both of them disappearing (unless they are disjoint and both on the negative side, which wouldn't make the intersection single-valued).

I have a hard time imagining that we'd ever introduce such a pair of types; I can't think of an example for any of our current single-valued types.

So I don't think this case is important :)

| Type::LiteralString => false,
}
}

/// Resolve a member access of a type.
///
/// For example, if `foo` is `Type::Instance(<Bar>)`,
Expand Down Expand Up @@ -1965,6 +2014,31 @@ mod tests {
assert!(from.into_type(&db).is_singleton());
}

#[test_case(Ty::None)]
#[test_case(Ty::BooleanLiteral(true))]
#[test_case(Ty::IntLiteral(1))]
#[test_case(Ty::StringLiteral("abc"))]
#[test_case(Ty::BytesLiteral("abc"))]
#[test_case(Ty::Tuple(vec![]))]
#[test_case(Ty::Tuple(vec![Ty::BooleanLiteral(true), Ty::IntLiteral(1)]))]
fn is_single_valued(from: Ty) {
let db = setup_db();

assert!(from.into_type(&db).is_single_valued(&db));
}

#[test_case(Ty::Never)]
#[test_case(Ty::Any)]
#[test_case(Ty::Union(vec![Ty::IntLiteral(1), Ty::IntLiteral(2)]))]
#[test_case(Ty::Tuple(vec![Ty::None, Ty::BuiltinInstance("int")]))]
#[test_case(Ty::BuiltinInstance("str"))]
#[test_case(Ty::LiteralString)]
fn is_not_single_valued(from: Ty) {
let db = setup_db();

assert!(!from.into_type(&db).is_single_valued(&db));
}

#[test_case(Ty::Never)]
#[test_case(Ty::IntLiteral(345))]
#[test_case(Ty::BuiltinInstance("str"))]
Expand Down
8 changes: 8 additions & 0 deletions crates/red_knot_python_semantic/src/types/narrow.rs
Original file line number Diff line number Diff line change
Expand Up @@ -169,6 +169,14 @@ impl<'db> NarrowingConstraintsBuilder<'db> {
ast::CmpOp::Is => {
self.constraints.insert(symbol, comp_ty);
}
ast::CmpOp::NotEq => {
if comp_ty.is_single_valued(self.db) {
let ty = IntersectionBuilder::new(self.db)
.add_negative(comp_ty)
.build();
self.constraints.insert(symbol, ty);
}
}
_ => {
// TODO other comparison types
}
Expand Down
Loading