Skip to content
Merged
Show file tree
Hide file tree
Changes from 15 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 @@ -180,16 +180,12 @@ This might require propagating constraints from other typevars.
def mutually_constrained[T, U]():
# If [T = U ∧ U ≤ int], then [T ≤ int] must be true as well.
given_int = ConstraintSet.range(U, T, U) & ConstraintSet.range(Never, U, int)
# TODO: no static-assert-error
# error: [static-assert-error]
static_assert(given_int.implies_subtype_of(T, int))
static_assert(not given_int.implies_subtype_of(T, bool))
static_assert(not given_int.implies_subtype_of(T, str))

# If [T ≤ U ∧ U ≤ int], then [T ≤ int] must be true as well.
given_int = ConstraintSet.range(Never, T, U) & ConstraintSet.range(Never, U, int)
# TODO: no static-assert-error
# error: [static-assert-error]
static_assert(given_int.implies_subtype_of(T, int))
static_assert(not given_int.implies_subtype_of(T, bool))
static_assert(not given_int.implies_subtype_of(T, str))
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,158 @@
# Constraint set satisfaction

```toml
[environment]
python-version = "3.12"
```

Constraint sets exist to help us check assignability and subtyping of types in the presence of
typevars. We construct a constraint set describing the conditions under which assignability holds
between the two types. Then we check whether that constraint set is satisfied for the valid
specializations of the relevant typevars. This file tests that final step: ensuring that a
constraint set is satisfied given a list of inferable and non-inferable typevars.

(Note that in this file, for ease of reproducibility, we explicitly list the typevars that are
inferable in each `satisfied_by_all_typevars` call; any typevar not listed is assumed to be
non-inferable.)

## Inferable typevars

When a typevar is in an inferable position, the constraint set only needs to be satisfied for _some_
valid specialization. The most common inferable position occurs when invoking a generic function:
all of the function's typevars are inferable, because we want to use the argument types to infer
which specialization is being invoked.
Comment on lines +17 to +20
Copy link
Member

Choose a reason for hiding this comment

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

This is great. Thanks for adding it


```py
from typing import final, Never
from ty_extensions import ConstraintSet, static_assert

class Super: ...
class Base(Super): ...
class Sub(Base): ...

@final
class Unrelated: ...
```

If a typevar has no bound or constraints, then it can specialize to any type. For an inferable
typevar, that means we just need a single type (any type at all!) that satisfies the constraint set.

```py
def unbounded[T]():
static_assert(ConstraintSet.always().satisfied_by_all_typevars(T))
static_assert(not ConstraintSet.never().satisfied_by_all_typevars(T))
static_assert(ConstraintSet.range(Never, T, Unrelated).satisfied_by_all_typevars(T))
static_assert(ConstraintSet.range(Never, T, Super).satisfied_by_all_typevars(T))
static_assert(ConstraintSet.range(Never, T, Base).satisfied_by_all_typevars(T))
static_assert(ConstraintSet.range(Never, T, Sub).satisfied_by_all_typevars(T))
```

If a typevar has an upper bound, then it must specialize to a type that is a subtype of that bound.
For an inferable typevar, that means we need a single type that satisfies both the constraint set
and the upper bound.

```py
def bounded[T: Base]():
static_assert(ConstraintSet.always().satisfied_by_all_typevars(T))
static_assert(not ConstraintSet.never().satisfied_by_all_typevars(T))
static_assert(ConstraintSet.range(Never, T, Super).satisfied_by_all_typevars(T))
Copy link
Member

@MichaReiser MichaReiser Oct 29, 2025

Choose a reason for hiding this comment

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

I don't think I understand why T <= Super satisfies T <= Base, given that Super isn't a subtype of Base. Or am I reading this the wrong way around? Or is the Never part important?

Copy link
Member Author

Choose a reason for hiding this comment

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

We discussed this sync — the key point is that the implication is in the other direction. (The typevar bounds/constraints need to imply the constraint set being checked.) So here, T must specialize to a subtype of Base. Base is a subtype of Super, so every valid specialization of T is also a subtype of Super. (Technically, this test is in the inferable section, so we only need one valid specialization of T to satisfy the constraint set. In this case, every valid specialization does, so you'll see that this same test also holds down in the non-inferable section.)

static_assert(ConstraintSet.range(Never, T, Base).satisfied_by_all_typevars(T))
static_assert(ConstraintSet.range(Never, T, Sub).satisfied_by_all_typevars(T))

# This succeeds because T can specialize to Never
Copy link
Member

Choose a reason for hiding this comment

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

I don't think I understand the why but I trust you on this

Copy link
Member Author

Choose a reason for hiding this comment

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

This is trying to show that Never is sneaky, especially for inferable typevars. Since T is inferable, we only need one specialization to satisfy the constraint set. Never is a valid specialization, since Never ≤ Base. And Never ≤ Unrelated, so the constraint set is satisfied for the T = Never case. That's enough for an inferable typevar.

The corresponding test in the non-inferable section fails, though, since there we need all valid specializations to satisfy the constraint set. And T = Base is a counter-example where it doesn't.

This tells me that it might help to change the structure of this file? Right now I have inferable/non-inferable as the top-level sections, and different kinds of typevar bounds/constraints as (unlabeled) subsections. Maybe instead I should have "unbounded", "bound", and "constrained" as the top-level sections, to more clearly call out how the behavior is different for inferable vs non-inferable?

Copy link
Member Author

Choose a reason for hiding this comment

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

This tells me that it might help to change the structure of this file?

I did this, and added more explanatory comments for each example. Hopefully that helps clarify the logic a bit.

constraints = ConstraintSet.range(Never, T, Unrelated)
static_assert(constraints.satisfied_by_all_typevars(T))

# If we explicitly disallow Never, then it fails
constraints = constraints & ~ConstraintSet.range(Never, T, Never)
static_assert(not constraints.satisfied_by_all_typevars(T))
```

If a typevar has constraints, then it must specialize to one of those specific types. (Not to a
subtype of one of those types!) For an inferable typevar, that means we need the constraint set to
be satisfied by any one of the constraints.

```py
def constrained[T: (Base, Unrelated)]():
static_assert(ConstraintSet.always().satisfied_by_all_typevars(T))
static_assert(not ConstraintSet.never().satisfied_by_all_typevars(T))
static_assert(ConstraintSet.range(Never, T, Unrelated).satisfied_by_all_typevars(T))
static_assert(ConstraintSet.range(Never, T, Super).satisfied_by_all_typevars(T))
Copy link
Member

Choose a reason for hiding this comment

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

Hmm, same here. Why is Super satisfying the constraint, given that it isn't Base or Unrelated?

Copy link
Member Author

Choose a reason for hiding this comment

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

Same as above. This is in inferable position, so we only need one specialization of T to satisfy the constraint set. T = Base does, so the check passes. Down below in the non-inferable section, the check fails, because T = Unrelated is a valid specialization that doesn't satisfy the constraint set.

static_assert(ConstraintSet.range(Never, T, Base).satisfied_by_all_typevars(T))
# Sub is not Base! Constraints must be exact, not subtypes
static_assert(not ConstraintSet.range(Never, T, Sub).satisfied_by_all_typevars(T))
```

## Non-inferable typevars

When a typevar is in a non-inferable position, the constraint set must be satisfied for _every_
valid specialization. The most common non-inferable position occurs in the body of a generic
function or class: here we don't know in advance what type the typevar will be specialized to, and
so we have to ensure that the body is valid for all possible specializations.

```py
from typing import final, Never
from ty_extensions import ConstraintSet, static_assert

class Super: ...
class Base(Super): ...
class Sub(Base): ...

@final
class Unrelated: ...
```

If a typevar has no bound or constraints, then it can specialize to any type. For a non-inferable
typevar, that means the constraint set must be satisfied for every possible type.

```py
def unbounded[T]():
static_assert(ConstraintSet.always().satisfied_by_all_typevars())
static_assert(not ConstraintSet.never().satisfied_by_all_typevars())
static_assert(not ConstraintSet.range(Never, T, Unrelated).satisfied_by_all_typevars())
static_assert(not ConstraintSet.range(Never, T, Super).satisfied_by_all_typevars())
static_assert(not ConstraintSet.range(Never, T, Base).satisfied_by_all_typevars())
static_assert(not ConstraintSet.range(Never, T, Sub).satisfied_by_all_typevars())
```

If a typevar has an upper bound, then it must specialize to a type that is a subtype of that bound.
For a non-inferable typevar, that means the constraint set must be satisfied for every type that
satisfies the upper bound.

```py
def bounded[T: Base]():
static_assert(ConstraintSet.always().satisfied_by_all_typevars())
static_assert(not ConstraintSet.never().satisfied_by_all_typevars())
static_assert(not ConstraintSet.range(Never, T, Unrelated).satisfied_by_all_typevars())
static_assert(ConstraintSet.range(Never, T, Super).satisfied_by_all_typevars())
static_assert(ConstraintSet.range(Never, T, Base).satisfied_by_all_typevars())
static_assert(not ConstraintSet.range(Never, T, Sub).satisfied_by_all_typevars())
```

If a typevar has constraints, then it must specialize to one of those specific types. (Not to a
subtype of one of those types!) For a non-inferable typevar, that means we need the constraint set
to be satisfied by all of those constraints.

```py
def constrained[T: (Base, Unrelated)]():
static_assert(ConstraintSet.always().satisfied_by_all_typevars())
static_assert(not ConstraintSet.never().satisfied_by_all_typevars())
static_assert(not ConstraintSet.range(Never, T, Unrelated).satisfied_by_all_typevars())
static_assert(not ConstraintSet.range(Never, T, Super).satisfied_by_all_typevars())
static_assert(not ConstraintSet.range(Never, T, Base).satisfied_by_all_typevars())
static_assert(not ConstraintSet.range(Never, T, Sub).satisfied_by_all_typevars())

constraints = ConstraintSet.range(Never, T, Super) | ConstraintSet.range(Never, T, Unrelated)
static_assert(constraints.satisfied_by_all_typevars())
constraints = ConstraintSet.range(Never, T, Base) | ConstraintSet.range(Never, T, Unrelated)
static_assert(constraints.satisfied_by_all_typevars())
constraints = ConstraintSet.range(Never, T, Sub) | ConstraintSet.range(Never, T, Unrelated)
static_assert(not constraints.satisfied_by_all_typevars())

constraints = ConstraintSet.range(Super, T, Super) | ConstraintSet.range(Unrelated, T, Unrelated)
static_assert(not constraints.satisfied_by_all_typevars())
constraints = ConstraintSet.range(Base, T, Base) | ConstraintSet.range(Unrelated, T, Unrelated)
static_assert(constraints.satisfied_by_all_typevars())
constraints = ConstraintSet.range(Sub, T, Sub) | ConstraintSet.range(Unrelated, T, Unrelated)
static_assert(not constraints.satisfied_by_all_typevars())
```
53 changes: 45 additions & 8 deletions crates/ty_python_semantic/src/types.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4151,6 +4151,14 @@ impl<'db> Type<'db> {
))
.into()
}
Type::KnownInstance(KnownInstanceType::ConstraintSet(tracked))
if name == "satisfied_by_all_typevars" =>
{
Place::bound(Type::KnownBoundMethod(
KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(tracked),
))
.into()
}

Type::ClassLiteral(class)
if name == "__get__" && class.is_known(db, KnownClass::FunctionType) =>
Expand Down Expand Up @@ -6913,6 +6921,7 @@ impl<'db> Type<'db> {
| KnownBoundMethodType::ConstraintSetAlways
| KnownBoundMethodType::ConstraintSetNever
| KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)
| KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_)
)
| Type::DataclassDecorator(_)
| Type::DataclassTransformer(_)
Expand Down Expand Up @@ -7064,7 +7073,8 @@ impl<'db> Type<'db> {
| KnownBoundMethodType::ConstraintSetRange
| KnownBoundMethodType::ConstraintSetAlways
| KnownBoundMethodType::ConstraintSetNever
| KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_),
| KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)
| KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_),
)
| Type::DataclassDecorator(_)
| Type::DataclassTransformer(_)
Expand Down Expand Up @@ -10324,6 +10334,7 @@ pub enum KnownBoundMethodType<'db> {
ConstraintSetAlways,
ConstraintSetNever,
ConstraintSetImpliesSubtypeOf(TrackedConstraintSet<'db>),
ConstraintSetSatisfiedByAllTypeVars(TrackedConstraintSet<'db>),
}

pub(super) fn walk_method_wrapper_type<'db, V: visitor::TypeVisitor<'db> + ?Sized>(
Expand Down Expand Up @@ -10351,7 +10362,8 @@ pub(super) fn walk_method_wrapper_type<'db, V: visitor::TypeVisitor<'db> + ?Size
| KnownBoundMethodType::ConstraintSetRange
| KnownBoundMethodType::ConstraintSetAlways
| KnownBoundMethodType::ConstraintSetNever
| KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_) => {}
| KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)
| KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_) => {}
}
}

Expand Down Expand Up @@ -10419,6 +10431,10 @@ impl<'db> KnownBoundMethodType<'db> {
| (
KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_),
KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_),
)
| (
KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_),
KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_),
) => ConstraintSet::from(true),

(
Expand All @@ -10431,7 +10447,8 @@ impl<'db> KnownBoundMethodType<'db> {
| KnownBoundMethodType::ConstraintSetRange
| KnownBoundMethodType::ConstraintSetAlways
| KnownBoundMethodType::ConstraintSetNever
| KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_),
| KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)
| KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_),
KnownBoundMethodType::FunctionTypeDunderGet(_)
| KnownBoundMethodType::FunctionTypeDunderCall(_)
| KnownBoundMethodType::PropertyDunderGet(_)
Expand All @@ -10441,7 +10458,8 @@ impl<'db> KnownBoundMethodType<'db> {
| KnownBoundMethodType::ConstraintSetRange
| KnownBoundMethodType::ConstraintSetAlways
| KnownBoundMethodType::ConstraintSetNever
| KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_),
| KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)
| KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_),
) => ConstraintSet::from(false),
}
}
Expand Down Expand Up @@ -10494,6 +10512,10 @@ impl<'db> KnownBoundMethodType<'db> {
(
KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(left_constraints),
KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(right_constraints),
)
| (
KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(left_constraints),
KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(right_constraints),
) => left_constraints
.constraints(db)
.iff(db, right_constraints.constraints(db)),
Expand All @@ -10508,7 +10530,8 @@ impl<'db> KnownBoundMethodType<'db> {
| KnownBoundMethodType::ConstraintSetRange
| KnownBoundMethodType::ConstraintSetAlways
| KnownBoundMethodType::ConstraintSetNever
| KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_),
| KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)
| KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_),
KnownBoundMethodType::FunctionTypeDunderGet(_)
| KnownBoundMethodType::FunctionTypeDunderCall(_)
| KnownBoundMethodType::PropertyDunderGet(_)
Expand All @@ -10518,7 +10541,8 @@ impl<'db> KnownBoundMethodType<'db> {
| KnownBoundMethodType::ConstraintSetRange
| KnownBoundMethodType::ConstraintSetAlways
| KnownBoundMethodType::ConstraintSetNever
| KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_),
| KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)
| KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_),
) => ConstraintSet::from(false),
}
}
Expand All @@ -10542,7 +10566,8 @@ impl<'db> KnownBoundMethodType<'db> {
| KnownBoundMethodType::ConstraintSetRange
| KnownBoundMethodType::ConstraintSetAlways
| KnownBoundMethodType::ConstraintSetNever
| KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_) => self,
| KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)
| KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_) => self,
}
}

Expand All @@ -10558,7 +10583,10 @@ impl<'db> KnownBoundMethodType<'db> {
KnownBoundMethodType::ConstraintSetRange
| KnownBoundMethodType::ConstraintSetAlways
| KnownBoundMethodType::ConstraintSetNever
| KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_) => KnownClass::ConstraintSet,
| KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)
| KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_) => {
KnownClass::ConstraintSet
}
}
}

Expand Down Expand Up @@ -10697,6 +10725,15 @@ impl<'db> KnownBoundMethodType<'db> {
Some(KnownClass::ConstraintSet.to_instance(db)),
)))
}

KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_) => {
Either::Right(std::iter::once(Signature::new(
Parameters::new([Parameter::variadic(Name::new_static("inferable"))
.type_form()
.with_annotated_type(Type::any())]),
Some(KnownClass::Bool.to_instance(db)),
)))
}
}
}
}
Expand Down
30 changes: 28 additions & 2 deletions crates/ty_python_semantic/src/types/call/bind.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ use std::fmt;
use itertools::{Either, Itertools};
use ruff_db::parsed::parsed_module;
use ruff_python_ast::name::Name;
use rustc_hash::FxHashSet;
use smallvec::{SmallVec, smallvec, smallvec_inline};

use super::{Argument, CallArguments, CallError, CallErrorKind, InferContext, Signature, Type};
Expand Down Expand Up @@ -162,7 +163,7 @@ impl<'db> Bindings<'db> {
}
}

self.evaluate_known_cases(db, dataclass_field_specifiers);
self.evaluate_known_cases(db, argument_types, dataclass_field_specifiers);

// In order of precedence:
//
Expand Down Expand Up @@ -284,7 +285,12 @@ impl<'db> Bindings<'db> {

/// Evaluates the return type of certain known callables, where we have special-case logic to
/// determine the return type in a way that isn't directly expressible in the type system.
fn evaluate_known_cases(&mut self, db: &'db dyn Db, dataclass_field_specifiers: &[Type<'db>]) {
fn evaluate_known_cases(
&mut self,
db: &'db dyn Db,
argument_types: &CallArguments<'_, 'db>,
dataclass_field_specifiers: &[Type<'db>],
) {
let to_bool = |ty: &Option<Type<'_>>, default: bool| -> bool {
if let Some(Type::BooleanLiteral(value)) = ty {
*value
Expand Down Expand Up @@ -1176,6 +1182,26 @@ impl<'db> Bindings<'db> {
));
}

Type::KnownBoundMethod(
KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(tracked),
) => {
let inferable: Option<FxHashSet<_>> = overload
.arguments_for_parameter(argument_types, 0)
.map(|(_, ty)| {
ty.as_typevar()
.map(|bound_typevar| bound_typevar.identity(db))
})
.collect();
let Some(inferable) = inferable else {
continue;
};

let result = tracked
.constraints(db)
.satisfied_by_all_typevars(db, InferableTypeVars::One(&inferable));
overload.set_return_type(Type::BooleanLiteral(result));
}

Type::ClassLiteral(class) => match class.known(db) {
Some(KnownClass::Bool) => match overload.parameter_types() {
[Some(arg)] => overload.set_return_type(arg.bool(db).into_type(db)),
Expand Down
Loading
Loading