mirror of
https://github.com/astral-sh/ruff.git
synced 2025-09-30 13:51:16 +00:00
[ty] More constraint set simplifications via simpler constraint representation (#20423)
Previously, we used a very fine-grained representation for individual constraints: each constraint was _either_ a range constraint, a not-equivalent constraint, or an incomparable constraint. These three pieces are enough to represent all of the "real" constraints we need to create — range constraints and their negation. However, it meant that we weren't picking up as many chances to simplify constraint sets as we could. Our simplification logic depends on being able to look at _pairs_ of constraints or clauses to see if they simplify relative to each other. With our fine-grained representation, we could easily encounter situations that we should have been able to simplify, but that would require looking at three or more individual constraints. For instance, negating a range constraint would produce: ``` ¬(Base ≤ T ≤ Super) = ((T ≤ Base) ∧ (T ≠ Base)) ∨ (T ≁ Base) ∨ ((Super ≤ T) ∧ (T ≠ Super)) ∨ (T ≁ Super) ``` That is, `T` must be (strictly) less than `Base`, (strictly) greater than `Super`, or incomparable to either. If we tried to union those back together, we should get `always`, since `x ∨ ¬x` should always be true, no matter what `x` is. But instead we would get: ``` (Base ≤ T ≤ Super) ∨ ((T ≤ Base) ∧ (T ≠ Base)) ∨ (T ≁ Base) ∨ ((Super ≤ T) ∧ (T ≠ Super)) ∨ (T ≁ Super) ``` Nothing would simplify relative to each other, because we'd have to look at all five union elements to see that together they do in fact combine to `always`. The fine-grained representation was nice, because it made it easier to [work out the math](https://dcreager.net/theory/constraints/) for intersections and unions of each kind of constraint. But being able to simplify is more important, since the example above comes up immediately in #20093 when trying to handle constrained typevars. The fix in this PR is to go back to a more coarse-grained representation, where each individual constraint consists of a positive range (which might be `always` / `Never ≤ T ≤ object`), and zero or more negative ranges. The intuition is to think of a constraint as a region of the type space (representable as a range) with zero or more "holes" removed from it. With this representation, negating a range constraint produces: ``` ¬(Base ≤ T ≤ Super) = (always ∧ ¬(Base ≤ T ≤ Super)) ``` (That looks trivial, because it is! We just move the positive range to the negative side.) The math is not that much harder than before, because there are only three combinations to consider (each for intersection and union) — though the fact that there can be multiple holes in a constraint does require some nested loops. But the mdtest suite gives me confidence that this is not introducing any new issues, and it definitely removes a troublesome TODO. (As an aside, this change also means that we are back to having each clause contain no more than one individual constraint for any typevar. This turned out to be important, because part of our simplification logic was also depending on that!) --------- Co-authored-by: Carl Meyer <carl@astral.sh>
This commit is contained in:
parent
0d424d8e78
commit
1f46c18921
5 changed files with 752 additions and 999 deletions
|
@ -4058,56 +4058,26 @@ impl<'db> Type<'db> {
|
|||
)
|
||||
.into(),
|
||||
|
||||
Some(KnownFunction::RangeConstraint) => Binding::single(
|
||||
self,
|
||||
Signature::new(
|
||||
Parameters::new([
|
||||
Parameter::positional_only(Some(Name::new_static("lower_bound")))
|
||||
.type_form()
|
||||
.with_annotated_type(Type::any()),
|
||||
Parameter::positional_only(Some(Name::new_static("typevar")))
|
||||
.type_form()
|
||||
.with_annotated_type(Type::any()),
|
||||
Parameter::positional_only(Some(Name::new_static("upper_bound")))
|
||||
.type_form()
|
||||
.with_annotated_type(Type::any()),
|
||||
]),
|
||||
Some(KnownClass::ConstraintSet.to_instance(db)),
|
||||
),
|
||||
)
|
||||
.into(),
|
||||
|
||||
Some(KnownFunction::NotEquivalentConstraint) => Binding::single(
|
||||
self,
|
||||
Signature::new(
|
||||
Parameters::new([
|
||||
Parameter::positional_only(Some(Name::new_static("typevar")))
|
||||
.type_form()
|
||||
.with_annotated_type(Type::any()),
|
||||
Parameter::positional_only(Some(Name::new_static("hole")))
|
||||
.type_form()
|
||||
.with_annotated_type(Type::any()),
|
||||
]),
|
||||
Some(KnownClass::ConstraintSet.to_instance(db)),
|
||||
),
|
||||
)
|
||||
.into(),
|
||||
|
||||
Some(KnownFunction::IncomparableConstraint) => Binding::single(
|
||||
self,
|
||||
Signature::new(
|
||||
Parameters::new([
|
||||
Parameter::positional_only(Some(Name::new_static("typevar")))
|
||||
.type_form()
|
||||
.with_annotated_type(Type::any()),
|
||||
Parameter::positional_only(Some(Name::new_static("pivot")))
|
||||
.type_form()
|
||||
.with_annotated_type(Type::any()),
|
||||
]),
|
||||
Some(KnownClass::ConstraintSet.to_instance(db)),
|
||||
),
|
||||
)
|
||||
.into(),
|
||||
Some(KnownFunction::RangeConstraint | KnownFunction::NegatedRangeConstraint) => {
|
||||
Binding::single(
|
||||
self,
|
||||
Signature::new(
|
||||
Parameters::new([
|
||||
Parameter::positional_only(Some(Name::new_static("lower_bound")))
|
||||
.type_form()
|
||||
.with_annotated_type(Type::any()),
|
||||
Parameter::positional_only(Some(Name::new_static("typevar")))
|
||||
.type_form()
|
||||
.with_annotated_type(Type::any()),
|
||||
Parameter::positional_only(Some(Name::new_static("upper_bound")))
|
||||
.type_form()
|
||||
.with_annotated_type(Type::any()),
|
||||
]),
|
||||
Some(KnownClass::ConstraintSet.to_instance(db)),
|
||||
),
|
||||
)
|
||||
.into()
|
||||
}
|
||||
|
||||
Some(KnownFunction::IsSingleton | KnownFunction::IsSingleValued) => {
|
||||
Binding::single(
|
||||
|
|
File diff suppressed because it is too large
Load diff
|
@ -1259,10 +1259,8 @@ pub enum KnownFunction {
|
|||
RevealProtocolInterface,
|
||||
/// `ty_extensions.range_constraint`
|
||||
RangeConstraint,
|
||||
/// `ty_extensions.not_equivalent_constraint`
|
||||
NotEquivalentConstraint,
|
||||
/// `ty_extensions.incomparable_constraint`
|
||||
IncomparableConstraint,
|
||||
/// `ty_extensions.negated_range_constraint`
|
||||
NegatedRangeConstraint,
|
||||
}
|
||||
|
||||
impl KnownFunction {
|
||||
|
@ -1330,8 +1328,7 @@ impl KnownFunction {
|
|||
| Self::HasMember
|
||||
| Self::RevealProtocolInterface
|
||||
| Self::RangeConstraint
|
||||
| Self::NotEquivalentConstraint
|
||||
| Self::IncomparableConstraint
|
||||
| Self::NegatedRangeConstraint
|
||||
| Self::AllMembers => module.is_ty_extensions(),
|
||||
Self::ImportModule => module.is_importlib(),
|
||||
}
|
||||
|
@ -1644,61 +1641,17 @@ impl KnownFunction {
|
|||
)));
|
||||
}
|
||||
|
||||
KnownFunction::NotEquivalentConstraint => {
|
||||
let [Some(Type::NonInferableTypeVar(typevar)), Some(hole)] = parameter_types else {
|
||||
return;
|
||||
};
|
||||
|
||||
if !hole.is_equivalent_to(db, hole.top_materialization(db)) {
|
||||
if let Some(builder) =
|
||||
context.report_lint(&INVALID_ARGUMENT_TYPE, call_expression)
|
||||
{
|
||||
let mut diagnostic = builder.into_diagnostic(format_args!(
|
||||
"Not-equivalent constraint must have a fully static type"
|
||||
));
|
||||
diagnostic.annotate(
|
||||
Annotation::secondary(context.span(&call_expression.arguments.args[1]))
|
||||
.message(format_args!(
|
||||
"Type `{}` is not fully static",
|
||||
hole.display(db)
|
||||
)),
|
||||
);
|
||||
}
|
||||
return;
|
||||
}
|
||||
|
||||
let constraints = ConstraintSet::not_equivalent(db, *typevar, *hole);
|
||||
let tracked = TrackedConstraintSet::new(db, constraints);
|
||||
overload.set_return_type(Type::KnownInstance(KnownInstanceType::ConstraintSet(
|
||||
tracked,
|
||||
)));
|
||||
}
|
||||
|
||||
KnownFunction::IncomparableConstraint => {
|
||||
let [Some(Type::NonInferableTypeVar(typevar)), Some(pivot)] = parameter_types
|
||||
KnownFunction::NegatedRangeConstraint => {
|
||||
let [
|
||||
Some(lower),
|
||||
Some(Type::NonInferableTypeVar(typevar)),
|
||||
Some(upper),
|
||||
] = parameter_types
|
||||
else {
|
||||
return;
|
||||
};
|
||||
|
||||
if !pivot.is_equivalent_to(db, pivot.top_materialization(db)) {
|
||||
if let Some(builder) =
|
||||
context.report_lint(&INVALID_ARGUMENT_TYPE, call_expression)
|
||||
{
|
||||
let mut diagnostic = builder.into_diagnostic(format_args!(
|
||||
"Incomparable constraint must have a fully static type"
|
||||
));
|
||||
diagnostic.annotate(
|
||||
Annotation::secondary(context.span(&call_expression.arguments.args[1]))
|
||||
.message(format_args!(
|
||||
"Type `{}` is not fully static",
|
||||
pivot.display(db)
|
||||
)),
|
||||
);
|
||||
}
|
||||
return;
|
||||
}
|
||||
|
||||
let constraints = ConstraintSet::incomparable(db, *typevar, *pivot);
|
||||
let constraints = ConstraintSet::negated_range(db, *lower, *typevar, *upper);
|
||||
let tracked = TrackedConstraintSet::new(db, constraints);
|
||||
overload.set_return_type(Type::KnownInstance(KnownInstanceType::ConstraintSet(
|
||||
tracked,
|
||||
|
@ -1837,8 +1790,7 @@ pub(crate) mod tests {
|
|||
| KnownFunction::HasMember
|
||||
| KnownFunction::RevealProtocolInterface
|
||||
| KnownFunction::RangeConstraint
|
||||
| KnownFunction::NotEquivalentConstraint
|
||||
| KnownFunction::IncomparableConstraint
|
||||
| KnownFunction::NegatedRangeConstraint
|
||||
| KnownFunction::AllMembers => KnownModule::TyExtensions,
|
||||
|
||||
KnownFunction::ImportModule => KnownModule::ImportLib,
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue