Skip to content

Commit 0827f40

Browse files
committed
construct constraints with typevars in fixed order
1 parent c4aee80 commit 0827f40

3 files changed

Lines changed: 103 additions & 9 deletions

File tree

crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -602,6 +602,32 @@ def _[T, U]() -> None:
602602
reveal_type(~union | union)
603603
```
604604

605+
## Typevar ordering
606+
607+
Constraints can relate two typevars — i.e., `S ≤ T`. We could encode that in one of two ways:
608+
`Never ≤ S ≤ T` or `S ≤ T ≤ object`. In other words, we can decide whether `S` or `T` is the typevar
609+
being constrained. The other is then the lower or upper bound of the constraint.
610+
611+
To handle this, we enforce an arbitrary ordering on typevars, and always place the constraint on the
612+
"later" typevar. For the example above, that does not change how the constraint is displayed, since
613+
we always hide `Never` lower bounds and `object` upper bounds. But in the case of `S ≤ T ≤ U`, we
614+
end up with an ambiguity. Depending on the typevar ordering, that might display as `S ≤ T ≤ U`, or
615+
as `(S ≤ T) ∧ (T ≤ U)`.
616+
617+
```py
618+
from typing import Never
619+
from ty_extensions import range_constraint
620+
621+
def f[S, T]():
622+
# These will both display the same, even though we are guaranteed to (try to) construct one of
623+
# the constraints with the typevars out of order.
624+
625+
# revealed: ty_extensions.ConstraintSet[(S@f ≤ T@f)]
626+
reveal_type(range_constraint(Never, S, T))
627+
# revealed: ty_extensions.ConstraintSet[(S@f ≤ T@f)]
628+
reveal_type(range_constraint(S, T, object))
629+
```
630+
605631
## Other simplifications
606632

607633
When displaying a constraint set, we transform the internal BDD representation into a DNF formula

crates/ty_python_semantic/src/types/constraints.rs

Lines changed: 75 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -65,7 +65,9 @@ use salsa::plumbing::AsId;
6565

6666
use crate::Db;
6767
use crate::types::generics::InferableTypeVars;
68-
use crate::types::{BoundTypeVarIdentity, IntersectionType, Type, TypeRelation, UnionType};
68+
use crate::types::{
69+
BoundTypeVarIdentity, BoundTypeVarInstance, IntersectionType, Type, TypeRelation, UnionType,
70+
};
6971

7072
/// An extension trait for building constraint sets from [`Option`] values.
7173
pub(crate) trait OptionConstraintsExtension<T> {
@@ -244,20 +246,87 @@ impl<'db> ConstraintSet<'db> {
244246
pub(crate) fn range(
245247
db: &'db dyn Db,
246248
lower: Type<'db>,
247-
typevar: BoundTypeVarIdentity<'db>,
249+
typevar: BoundTypeVarInstance<'db>,
248250
upper: Type<'db>,
249251
) -> Self {
250252
let lower = lower.bottom_materialization(db);
251253
let upper = upper.top_materialization(db);
252-
Self {
253-
node: ConstrainedTypeVar::new_node(db, lower, typevar, upper),
254-
}
254+
255+
// We have an (arbitrary) ordering for typevars. If the upper and/or lower bounds are
256+
// typevars, we have to ensure that the bounds are "earlier" according to that order than
257+
// the typevar being constrained.
258+
//
259+
// In the comments below, we use brackets to indicate which typevar is "larger", and
260+
// therefore the typevar that the constraint applies to.
261+
let node = match (lower, upper) {
262+
// A ≤ T ≤ A == (T ≤ [A] ≤ T)
263+
(Type::TypeVar(lower), Type::TypeVar(upper)) if lower == upper => {
264+
let (bound, typevar) = if lower < typevar {
265+
(lower, typevar)
266+
} else {
267+
(typevar, lower)
268+
};
269+
ConstrainedTypeVar::new_node(
270+
db,
271+
Type::TypeVar(bound),
272+
typevar.identity(db),
273+
Type::TypeVar(bound),
274+
)
275+
}
276+
277+
// A ≤ T ≤ B == ([A] ≤ T) && (T ≤ [B])
278+
(Type::TypeVar(lower), Type::TypeVar(upper)) if lower > typevar && upper > typevar => {
279+
let lower = ConstrainedTypeVar::new_node(
280+
db,
281+
Type::Never,
282+
lower.identity(db),
283+
Type::TypeVar(typevar),
284+
);
285+
let upper = ConstrainedTypeVar::new_node(
286+
db,
287+
Type::TypeVar(typevar),
288+
upper.identity(db),
289+
Type::object(),
290+
);
291+
lower.and(db, upper)
292+
}
293+
294+
// A ≤ T ≤ B == ([A] ≤ T) && ([T] ≤ B)
295+
(Type::TypeVar(lower), _) if lower > typevar => {
296+
let lower = ConstrainedTypeVar::new_node(
297+
db,
298+
Type::Never,
299+
lower.identity(db),
300+
Type::TypeVar(typevar),
301+
);
302+
let upper =
303+
ConstrainedTypeVar::new_node(db, Type::Never, typevar.identity(db), upper);
304+
lower.and(db, upper)
305+
}
306+
307+
// A ≤ T ≤ B == (A ≤ [T]) && (T ≤ [B])
308+
(_, Type::TypeVar(upper)) if upper > typevar => {
309+
let lower =
310+
ConstrainedTypeVar::new_node(db, lower, typevar.identity(db), Type::object());
311+
let upper = ConstrainedTypeVar::new_node(
312+
db,
313+
Type::TypeVar(typevar),
314+
upper.identity(db),
315+
Type::object(),
316+
);
317+
lower.and(db, upper)
318+
}
319+
320+
_ => ConstrainedTypeVar::new_node(db, lower, typevar.identity(db), upper),
321+
};
322+
323+
Self { node }
255324
}
256325

257326
pub(crate) fn negated_range(
258327
db: &'db dyn Db,
259328
lower: Type<'db>,
260-
typevar: BoundTypeVarIdentity<'db>,
329+
typevar: BoundTypeVarInstance<'db>,
261330
upper: Type<'db>,
262331
) -> Self {
263332
Self::range(db, lower, typevar, upper).negate(db)

crates/ty_python_semantic/src/types/function.rs

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1723,7 +1723,7 @@ impl KnownFunction {
17231723
return;
17241724
};
17251725

1726-
let constraints = ConstraintSet::range(db, *lower, typevar.identity(db), *upper);
1726+
let constraints = ConstraintSet::range(db, *lower, *typevar, *upper);
17271727
let tracked = TrackedConstraintSet::new(db, constraints);
17281728
overload.set_return_type(Type::KnownInstance(KnownInstanceType::ConstraintSet(
17291729
tracked,
@@ -1736,8 +1736,7 @@ impl KnownFunction {
17361736
return;
17371737
};
17381738

1739-
let constraints =
1740-
ConstraintSet::negated_range(db, *lower, typevar.identity(db), *upper);
1739+
let constraints = ConstraintSet::negated_range(db, *lower, *typevar, *upper);
17411740
let tracked = TrackedConstraintSet::new(db, constraints);
17421741
overload.set_return_type(Type::KnownInstance(KnownInstanceType::ConstraintSet(
17431742
tracked,

0 commit comments

Comments
 (0)