Skip to content
Open
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
Original file line number Diff line number Diff line change
Expand Up @@ -50,17 +50,13 @@ reveal_type(x) # revealed: LiteralString
if x != "abc":
reveal_type(x) # revealed: LiteralString & ~Literal["abc"]

# 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 == "abc") # revealed: Literal[False]
reveal_type("abc" == x) # revealed: Literal[False]
reveal_type(x == "something else") # revealed: bool
reveal_type("something else" == x) # revealed: bool

# 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 != "abc") # revealed: Literal[True]
reveal_type("abc" != x) # revealed: Literal[True]
reveal_type(x != "something else") # revealed: bool
reveal_type("something else" != x) # revealed: bool

Expand All @@ -76,6 +72,34 @@ if x != "abc":
reveal_type("abc" in x) # revealed: bool
```

A negative literal-string constraint does not exclude a runtime string with that value unless the
candidate already has known literal origin.

```py
from typing import Literal
from typing_extensions import LiteralString
from ty_extensions import Intersection, Not

def without_literal_origin(value: Intersection[str, Not[LiteralString]]) -> None:
reveal_type(value == "hello") # revealed: bool
reveal_type("hello" == value) # revealed: bool
```

A negative string-literal constraint likewise leaves the same runtime value possible, with or
without an explicit `str` constraint.

```py
def excluded_string_literal(value: Intersection[str, Not[Literal["hello"]]]) -> None:
reveal_type(value == "hello") # revealed: bool
reveal_type("hello" == value) # revealed: bool
reveal_type(value != "hello") # revealed: bool

def excluded_literal(value: Not[Literal["hello"]]) -> None:
reveal_type(value == "hello") # revealed: bool
reveal_type("hello" == value) # revealed: bool
reveal_type(value != "hello") # revealed: bool
```

#### Integers

```py
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -1681,6 +1681,59 @@ def preserve_custom_comparison(value: str | AlwaysEqual):
reveal_type(value) # revealed: Literal["a"] | AlwaysEqual
```

## String-literal origin and exclusions

A string without literal origin can equal a string literal without acquiring the literal's origin.
The successful branch remains reachable and preserves the original exclusion.

```py
from typing import Literal
from typing_extensions import LiteralString
from ty_extensions import Intersection, Not

def without_literal_origin(value: Intersection[str, Not[LiteralString]]) -> None:
if value == "hello":
reveal_type(value) # revealed: str & ~LiteralString
value.definitely_missing_attribute # error: [unresolved-attribute]

if "hello" == value:
reveal_type(value) # revealed: str & ~LiteralString

if value != "hello":
reveal_type(value) # revealed: str & ~LiteralString
else:
reveal_type(value) # revealed: str & ~LiteralString
```

Excluding a particular string literal also leaves its runtime value possible when literal origin is
not known. A different literal can still narrow the string normally.

```py
def without_literal_value(value: Intersection[str, Not[Literal["hello"]]]) -> None:
if value == "hello":
reveal_type(value) # revealed: str & ~Literal["hello"]

if value == "goodbye":
reveal_type(value) # revealed: Literal["goodbye"]
```

Optional alternatives that cannot compare equal are still removed without discarding the possible
string value.

```py
def optional_without_literal_origin(value: Intersection[str, Not[LiteralString]] | None) -> None:
if value == "hello":
reveal_type(value) # revealed: str & ~LiteralString
```

Once literal origin is known, excluding a string literal really does exclude its runtime value.

```py
def trusted_value_is_excluded(value: Intersection[LiteralString, Not[Literal["hello"]]]) -> None:
if value == "hello":
reveal_type(value) # revealed: Never
```

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

```py
Expand Down Expand Up @@ -2557,7 +2610,8 @@ strict-equality-semantics = true

```py
from enum import IntEnum, StrEnum
from typing import Any, Literal
from typing import Any, Literal, LiteralString
from ty_extensions import Intersection, Not

def broad(value: str):
if value == "a":
Expand All @@ -2571,6 +2625,13 @@ def inequality(value: str):
else:
reveal_type(value) # revealed: str

def without_literal_origin(value: Intersection[str, Not[LiteralString]]):
if value == "a":
reveal_type(value) # revealed: str & ~LiteralString

def trusted_value_is_excluded(value: Intersection[LiteralString, Not[Literal["a"]]]):
reveal_type(value == "a") # revealed: Literal[False]

def literal(value: Literal["a", "b"]):
if value == "a":
reveal_type(value) # revealed: Literal["a"]
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -1281,8 +1281,12 @@ def _(x: bool | str):

## LiteralString

Known literal-origin strings can safely narrow to the matching members of a literal tuple.

```py
from typing import Literal
from typing_extensions import LiteralString
from ty_extensions import Intersection, Not

def _(x: LiteralString):
if x in ("a", "b", "c"):
Expand All @@ -1297,6 +1301,24 @@ def _(x: LiteralString | int):
reveal_type(x) # revealed: (LiteralString & ~Literal["a"] & ~Literal["b"] & ~Literal["c"]) | int
```

A string without literal origin can match a tuple member without gaining that member's origin.

```py
def without_literal_origin(value: Intersection[str, Not[LiteralString]]) -> None:
if value in ("hello",):
reveal_type(value) # revealed: str & ~LiteralString
```

An excluded value cannot appear in a tuple when the candidate already has known literal origin.

```py
def trusted_value_is_excluded(value: Intersection[LiteralString, Not[Literal["hello"]]]) -> None:
reveal_type(value in ("hello",)) # revealed: Literal[False]

if value in ("hello",):
reveal_type(value) # revealed: Never
```

## enums

```py
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -526,21 +526,46 @@ def excluded_runtime_class(not_int: Not[int], other: UserId) -> None:

## `is` with string types

Identity comparisons preserve existing `LiteralString` narrowing and do not make negated string
literal comparisons unreachable.
Identity transfers known literal-string origin when the other operand already proves it.

```py
from typing import Literal
from typing_extensions import LiteralString
from ty_extensions import Not
from ty_extensions import Intersection, Not

def literal_string(value: object, text: LiteralString) -> None:
if value is text:
reveal_type(value) # revealed: LiteralString
```

A string without known literal origin can have the same runtime value as an excluded string literal.
Identity preserves the existing origin exclusion instead of making the successful branch
unreachable.

```py
def negated_string_literal(value: Not[Literal["hello"]]) -> None:
if value is "hello":
reveal_type(value) # revealed: ~Literal["hello"]

def negated_literal_string(value: Intersection[str, Not[LiteralString]]) -> None:
reveal_type(value is "hello") # revealed: bool

if value is "hello":
reveal_type(value) # revealed: str & ~LiteralString

if "hello" is value:
reveal_type(value) # revealed: str & ~LiteralString
```

When literal origin is already known, excluding a literal string also excludes that runtime value.

```py
def trusted_value_is_excluded(value: Intersection[LiteralString, Not[Literal["hello"]]]) -> None:
reveal_type(value is "hello") # revealed: Literal[False]
reveal_type("hello" is value) # revealed: Literal[False]

if value is "hello":
reveal_type(value) # revealed: Never
```

## `is` with `NewType`s
Expand Down
24 changes: 24 additions & 0 deletions crates/ty_python_semantic/resources/mdtest/narrow/match.md
Original file line number Diff line number Diff line change
Expand Up @@ -3330,6 +3330,30 @@ def test_match_value_sequence(value: object) -> None:
reveal_type(value[0]) # revealed: object
```

## String-literal origin in value patterns

A string without literal origin can match a literal value pattern without gaining literal origin.

```py
from typing import Literal
from typing_extensions import LiteralString
from ty_extensions import Intersection, Not

def without_literal_origin(value: Intersection[str, Not[LiteralString]]) -> None:
match value:
case "hello":
reveal_type(value) # revealed: str & ~LiteralString
```

For a known literal-origin string, excluding the same literal makes the value pattern impossible.

```py
def trusted_value_is_excluded(value: Intersection[LiteralString, Not[Literal["hello"]]]) -> None:
match value:
case "hello":
reveal_type(value) # revealed: Never
```

## Enum equality semantics

Enum value patterns use the enum class's actual `__eq__` implementation. Members of an enum whose
Expand Down
29 changes: 29 additions & 0 deletions crates/ty_python_semantic/src/types/equality.rs
Original file line number Diff line number Diff line change
Expand Up @@ -695,6 +695,23 @@ fn evaluate_structural_comparison<'db>(
(other, Type::Union(union)) => {
evaluate_union_right(evaluator, other, union.elements(db), branch, operator)
}
// An excluded string literal rules out its runtime value only when the intersection
// already proves that the string has literal origin.
(Type::Intersection(intersection), Type::LiteralValue(literal))
| (Type::LiteralValue(literal), Type::Intersection(intersection))
if literal.is_string()
&& intersection
.positive(db)
.iter()
.any(|element| element.is_subtype_of(db, env, Type::literal_string()))
&& Type::Intersection(intersection).is_disjoint_from(
db,
env,
Type::LiteralValue(literal),
) =>
{
operator.result_from_equality(false)
}
(Type::Intersection(intersection), other) => evaluate_intersection_left(
evaluator,
Type::Intersection(intersection),
Expand Down Expand Up @@ -1301,6 +1318,18 @@ fn evaluate_intersection_left<'db>(
ComparisonResult::AlwaysTrue => any_true = true,
ComparisonResult::AlwaysFalse => any_false = true,
ComparisonResult::CanNarrow(narrowed) => {
// Literal-string origin is a static proof, not a runtime object property. An
// untrusted string can therefore equal a literal even when their static types
// are disjoint. Keep its original proof instead of making that branch unreachable.
if operator.condition_expects_equality(branch)
&& original.is_disjoint_from(db, &evaluator.env, narrowed)
&& original
.identity_comparison_truthiness(db, &evaluator.env, narrowed)
.may_be_true()
{
return ComparisonResult::Ambiguous;
}

any_narrowing = true;
builder.add_positive_in_place(narrowed);
}
Expand Down
17 changes: 12 additions & 5 deletions crates/ty_python_semantic/src/types/infer/comparisons.rs
Original file line number Diff line number Diff line change
Expand Up @@ -30,8 +30,9 @@ impl<'db> Type<'db> {
/// unsound.
///
/// Preserve negations that constrain the object itself, such as `~None`, `~SomeClass`, and
/// `~Literal[1]`. A `NewType` tag, type-variable selection, or type-guard proof can differ
/// between views. Retain the existing conservative handling of negated string types.
/// `~Literal[1]`. A `NewType` tag, type-variable selection, type-guard proof, or literal-string
/// origin can differ between views. A negated string literal excludes its runtime value only
/// when another constraint already establishes that the string has literal origin.
///
/// A type variable can also hide a `NewType` tag: even a variable bounded by `int` can be
/// instantiated as an integer `NewType`. Expand variables to their upcast bounds or constraints
Expand Down Expand Up @@ -73,20 +74,26 @@ impl<'db> Type<'db> {
union.map(db, env, |element| upcast(db, env, *element, visitor))
}
Type::Intersection(intersection) => {
let has_literal_string_origin = intersection
.positive(db)
.iter()
.any(|element| element.is_subtype_of(db, env, Type::literal_string()));
let mut builder = IntersectionBuilder::new(db, env);
for element in intersection.positive(db) {
builder = builder.add_positive(upcast(db, env, *element, visitor));
}
for element in intersection.negative(db) {
// Static tags and predicate proofs can differ between views. Retain the
// existing conservative handling of negated string types.
// Static tags, predicate proofs, and literal-string origin can differ
// between views. Once literal origin is known, an excluded string literal
// also excludes its runtime value and must be preserved.
match element.resolve_type_alias(db) {
Type::NewTypeInstance(_)
| Type::TypeVar(_)
| Type::TypeIs(_)
| Type::TypeGuard(_) => continue,
Type::LiteralValue(literal)
if literal.is_literal_string() || literal.is_string() =>
if literal.is_literal_string()
|| literal.is_string() && !has_literal_string_origin =>
{
continue;
}
Expand Down
Loading