Skip to content
Merged
Show file tree
Hide file tree
Changes from all 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
41 changes: 27 additions & 14 deletions crates/red_knot_python_semantic/resources/mdtest/call/union.md
Original file line number Diff line number Diff line change
Expand Up @@ -165,26 +165,39 @@ def _(flag: bool):
## Unions with literals and negations

```py
from typing import Literal, Union
from typing import Literal
from knot_extensions import Not, AlwaysFalsy, static_assert, is_subtype_of, is_assignable_to

static_assert(is_subtype_of(Literal["a", ""], Union[Literal["a", ""], Not[AlwaysFalsy]]))
static_assert(is_subtype_of(Not[AlwaysFalsy], Union[Literal["", "a"], Not[AlwaysFalsy]]))
static_assert(is_subtype_of(Literal["a", ""], Union[Not[AlwaysFalsy], Literal["a", ""]]))
static_assert(is_subtype_of(Not[AlwaysFalsy], Union[Not[AlwaysFalsy], Literal["a", ""]]))
static_assert(is_subtype_of(Literal["a", ""], Literal["a", ""] | Not[AlwaysFalsy]))
static_assert(is_subtype_of(Not[AlwaysFalsy], Literal["", "a"] | Not[AlwaysFalsy]))
static_assert(is_subtype_of(Literal["a", ""], Not[AlwaysFalsy] | Literal["a", ""]))
static_assert(is_subtype_of(Not[AlwaysFalsy], Not[AlwaysFalsy] | Literal["a", ""]))

static_assert(is_subtype_of(Literal["a", ""], Union[Literal["a", ""], Not[Literal[""]]]))
static_assert(is_subtype_of(Not[Literal[""]], Union[Literal["a", ""], Not[Literal[""]]]))
static_assert(is_subtype_of(Literal["a", ""], Union[Not[Literal[""]], Literal["a", ""]]))
static_assert(is_subtype_of(Not[Literal[""]], Union[Not[Literal[""]], Literal["a", ""]]))
static_assert(is_subtype_of(Literal["a", ""], Literal["a", ""] | Not[Literal[""]]))
static_assert(is_subtype_of(Not[Literal[""]], Literal["a", ""] | Not[Literal[""]]))
static_assert(is_subtype_of(Literal["a", ""], Not[Literal[""]] | Literal["a", ""]))
static_assert(is_subtype_of(Not[Literal[""]], Not[Literal[""]] | Literal["a", ""]))

def _(
x: Union[Literal["a", ""], Not[AlwaysFalsy]],
y: Union[Literal["a", ""], Not[Literal[""]]],
a: Literal["a", ""] | Not[AlwaysFalsy],
b: Literal["a", ""] | Not[Literal[""]],
c: Literal[""] | Not[Literal[""]],
d: Not[Literal[""]] | Literal[""],
e: Literal["a"] | Not[Literal["a"]],
f: Literal[b"b"] | Not[Literal[b"b"]],
g: Not[Literal[b"b"]] | Literal[b"b"],
h: Literal[42] | Not[Literal[42]],
i: Not[Literal[42]] | Literal[42],
):
reveal_type(x) # revealed: Literal[""] | ~AlwaysFalsy
# TODO should be `object`
reveal_type(y) # revealed: Literal[""] | ~Literal[""]
reveal_type(a) # revealed: Literal[""] | ~AlwaysFalsy
reveal_type(b) # revealed: object
reveal_type(c) # revealed: object
reveal_type(d) # revealed: object
reveal_type(e) # revealed: object
reveal_type(f) # revealed: object
reveal_type(g) # revealed: object
reveal_type(h) # revealed: object
reveal_type(i) # revealed: object
```

## Cannot use an argument as both a value and a type form
Expand Down
128 changes: 98 additions & 30 deletions crates/red_knot_python_semantic/src/types/builder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -97,37 +97,70 @@ impl<'db> UnionElement<'db> {
fn try_reduce(&mut self, db: &'db dyn Db, other_type: Type<'db>) -> ReduceResult<'db> {
match self {
UnionElement::IntLiterals(literals) => {
ReduceResult::KeepIf(if other_type.splits_literals(db, LiteralKind::Int) {
if other_type.splits_literals(db, LiteralKind::Int) {
let mut collapse = false;
let negated = other_type.negate(db);
literals.retain(|literal| {
!Type::IntLiteral(*literal).is_subtype_of(db, other_type)
let ty = Type::IntLiteral(*literal);
if negated.is_subtype_of(db, ty) {
collapse = true;
}
!ty.is_subtype_of(db, other_type)
});
!literals.is_empty()
if collapse {
ReduceResult::CollapseToObject
} else {
ReduceResult::KeepIf(!literals.is_empty())
}
} else {
// SAFETY: All `UnionElement` literal kinds must always be non-empty
!Type::IntLiteral(literals[0]).is_subtype_of(db, other_type)
})
ReduceResult::KeepIf(
!Type::IntLiteral(literals[0]).is_subtype_of(db, other_type),
)
}
}
UnionElement::StringLiterals(literals) => {
ReduceResult::KeepIf(if other_type.splits_literals(db, LiteralKind::String) {
if other_type.splits_literals(db, LiteralKind::String) {
let mut collapse = false;
let negated = other_type.negate(db);
literals.retain(|literal| {
!Type::StringLiteral(*literal).is_subtype_of(db, other_type)
let ty = Type::StringLiteral(*literal);
if negated.is_subtype_of(db, ty) {
collapse = true;
}
!ty.is_subtype_of(db, other_type)
});
!literals.is_empty()
if collapse {
ReduceResult::CollapseToObject
} else {
ReduceResult::KeepIf(!literals.is_empty())
}
} else {
// SAFETY: All `UnionElement` literal kinds must always be non-empty
!Type::StringLiteral(literals[0]).is_subtype_of(db, other_type)
})
ReduceResult::KeepIf(
!Type::StringLiteral(literals[0]).is_subtype_of(db, other_type),
)
}
}
UnionElement::BytesLiterals(literals) => {
ReduceResult::KeepIf(if other_type.splits_literals(db, LiteralKind::Bytes) {
if other_type.splits_literals(db, LiteralKind::Bytes) {
let mut collapse = false;
let negated = other_type.negate(db);
literals.retain(|literal| {
!Type::BytesLiteral(*literal).is_subtype_of(db, other_type)
let ty = Type::BytesLiteral(*literal);
if negated.is_subtype_of(db, ty) {
collapse = true;
}
!ty.is_subtype_of(db, other_type)
});
!literals.is_empty()
if collapse {
ReduceResult::CollapseToObject
} else {
ReduceResult::KeepIf(!literals.is_empty())
}
} else {
// SAFETY: All `UnionElement` literal kinds must always be non-empty
!Type::BytesLiteral(literals[0]).is_subtype_of(db, other_type)
})
ReduceResult::KeepIf(
!Type::BytesLiteral(literals[0]).is_subtype_of(db, other_type),
)
}
}
UnionElement::Type(existing) => ReduceResult::Type(*existing),
}
Expand All @@ -138,6 +171,8 @@ enum ReduceResult<'db> {
/// Reduction of this `UnionElement` is complete; keep it in the union if the nested
/// boolean is true, eliminate it from the union if false.
KeepIf(bool),
/// Collapse this entire union to `object`.
CollapseToObject,
/// The given `Type` can stand-in for the entire `UnionElement` for further union
/// simplification checks.
Type(Type<'db>),
Expand Down Expand Up @@ -195,6 +230,7 @@ impl<'db> UnionBuilder<'db> {
// containing it.
Type::StringLiteral(literal) => {
let mut found = false;
let ty_negated = ty.negate(self.db);
for element in &mut self.elements {
match element {
UnionElement::StringLiterals(literals) => {
Expand All @@ -207,8 +243,16 @@ impl<'db> UnionBuilder<'db> {
found = true;
break;
}
UnionElement::Type(existing) if ty.is_subtype_of(self.db, *existing) => {
return;
UnionElement::Type(existing) => {
if ty.is_subtype_of(self.db, *existing) {
return;
}
if ty_negated.is_subtype_of(self.db, *existing) {
// The type that includes both this new element, and its negation
// (or a supertype of its negation), must be simply `object`.
self.collapse_to_object();
return;
}
}
_ => {}
}
Expand All @@ -223,6 +267,7 @@ impl<'db> UnionBuilder<'db> {
// Same for bytes literals as for string literals, above.
Type::BytesLiteral(literal) => {
let mut found = false;
let ty_negated = ty.negate(self.db);
for element in &mut self.elements {
match element {
UnionElement::BytesLiterals(literals) => {
Expand All @@ -235,8 +280,16 @@ impl<'db> UnionBuilder<'db> {
found = true;
break;
}
UnionElement::Type(existing) if ty.is_subtype_of(self.db, *existing) => {
return;
UnionElement::Type(existing) => {
if ty.is_subtype_of(self.db, *existing) {
return;
}
if ty_negated.is_subtype_of(self.db, *existing) {
// The type that includes both this new element, and its negation
// (or a supertype of its negation), must be simply `object`.
self.collapse_to_object();
return;
}
}
_ => {}
}
Expand All @@ -251,6 +304,7 @@ impl<'db> UnionBuilder<'db> {
// And same for int literals as well.
Type::IntLiteral(literal) => {
let mut found = false;
let ty_negated = ty.negate(self.db);
for element in &mut self.elements {
match element {
UnionElement::IntLiterals(literals) => {
Expand All @@ -263,8 +317,16 @@ impl<'db> UnionBuilder<'db> {
found = true;
break;
}
UnionElement::Type(existing) if ty.is_subtype_of(self.db, *existing) => {
return;
UnionElement::Type(existing) => {
if ty.is_subtype_of(self.db, *existing) {
return;
}
if ty_negated.is_subtype_of(self.db, *existing) {
// The type that includes both this new element, and its negation
// (or a supertype of its negation), must be simply `object`.
self.collapse_to_object();
return;
}
}
_ => {}
}
Expand Down Expand Up @@ -298,6 +360,10 @@ impl<'db> UnionBuilder<'db> {
continue;
}
ReduceResult::Type(ty) => ty,
ReduceResult::CollapseToObject => {
self.collapse_to_object();
return;
}
};
if Some(element_type) == bool_pair {
to_add = KnownClass::Bool.to_instance(self.db);
Expand All @@ -317,12 +383,14 @@ impl<'db> UnionBuilder<'db> {
} else if element_type.is_subtype_of(self.db, ty) {
to_remove.push(index);
} else if ty_negated.is_subtype_of(self.db, element_type) {
// We add `ty` to the union. We just checked that `~ty` is a subtype of an existing `element`.
// This also means that `~ty | ty` is a subtype of `element | ty`, because both elements in the
// first union are subtypes of the corresponding elements in the second union. But `~ty | ty` is
// just `object`. Since `object` is a subtype of `element | ty`, we can only conclude that
// `element | ty` must be `object` (object has no other supertypes). This means we can simplify
// the whole union to just `object`, since all other potential elements would also be subtypes of
// We add `ty` to the union. We just checked that `~ty` is a subtype of an
// existing `element`. This also means that `~ty | ty` is a subtype of
// `element | ty`, because both elements in the first union are subtypes of
// the corresponding elements in the second union. But `~ty | ty` is just
// `object`. Since `object` is a subtype of `element | ty`, we can only
// conclude that `element | ty` must be `object` (object has no other
// supertypes). This means we can simplify the whole union to just
// `object`, since all other potential elements would also be subtypes of
// `object`.
self.collapse_to_object();
return;
Expand Down
Loading