From 31c9f7059af29732d12d29fd3e77d29d51cde897 Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Thu, 30 Oct 2025 13:46:29 -0400 Subject: [PATCH] tautology --- crates/ty_python_semantic/src/types.rs | 196 ++---------------- .../src/types/constraints.rs | 12 +- 2 files changed, 29 insertions(+), 179 deletions(-) diff --git a/crates/ty_python_semantic/src/types.rs b/crates/ty_python_semantic/src/types.rs index 4dcabd93b9..fc8a30b2a5 100644 --- a/crates/ty_python_semantic/src/types.rs +++ b/crates/ty_python_semantic/src/types.rs @@ -1726,6 +1726,29 @@ impl<'db> Type<'db> { } match (self, target) { + // Two identical typevars must always solve to the same type, so they are always + // subtypes of each other and assignable to each other. + // + // Note that this is not handled by the early return at the beginning of this method, + // since subtyping between a TypeVar and an arbitrary other type cannot be guaranteed to be reflexive. + (Type::TypeVar(lhs_bound_typevar), Type::TypeVar(rhs_bound_typevar)) + if lhs_bound_typevar.is_same_typevar_as(db, rhs_bound_typevar) => + { + ConstraintSet::from(true) + } + + // A typevar satisfies a relation when...it satisfies the relation. Yes that's a + // tautology! We're moving the caller's subtyping/assignability requirement into a + // constraint set. If the typevar has an upper bound or constraints, then the relation + // only has to hold when the typevar has a valid specialization (i.e., one that + // satisfies the upper bound/constraints). + (Type::TypeVar(bound_typevar), _) => { + ConstraintSet::constrain_typevar(db, bound_typevar, Type::Never, target, relation) + } + (_, Type::TypeVar(bound_typevar)) => { + ConstraintSet::constrain_typevar(db, bound_typevar, self, Type::object(), relation) + } + // Everything is a subtype of `object`. (_, Type::NominalInstance(instance)) if instance.is_object() => { ConstraintSet::from(true) @@ -1829,130 +1852,6 @@ impl<'db> Type<'db> { }, }), - // In general, a TypeVar `T` is not a subtype of a type `S` unless one of the two conditions is satisfied: - // 1. `T` is a bound TypeVar and `T`'s upper bound is a subtype of `S`. - // TypeVars without an explicit upper bound are treated as having an implicit upper bound of `object`. - // 2. `T` is a constrained TypeVar and all of `T`'s constraints are subtypes of `S`. - // - // However, there is one exception to this general rule: for any given typevar `T`, - // `T` will always be a subtype of any union containing `T`. - // A similar rule applies in reverse to intersection types. - (Type::TypeVar(bound_typevar), Type::Union(union)) - if !bound_typevar.is_inferable(db, inferable) - && union.elements(db).contains(&self) => - { - ConstraintSet::from(true) - } - (Type::Intersection(intersection), Type::TypeVar(bound_typevar)) - if !bound_typevar.is_inferable(db, inferable) - && intersection.positive(db).contains(&target) => - { - ConstraintSet::from(true) - } - (Type::Intersection(intersection), Type::TypeVar(bound_typevar)) - if !bound_typevar.is_inferable(db, inferable) - && intersection.negative(db).contains(&target) => - { - ConstraintSet::from(false) - } - - // Two identical typevars must always solve to the same type, so they are always - // subtypes of each other and assignable to each other. - // - // Note that this is not handled by the early return at the beginning of this method, - // since subtyping between a TypeVar and an arbitrary other type cannot be guaranteed to be reflexive. - (Type::TypeVar(lhs_bound_typevar), Type::TypeVar(rhs_bound_typevar)) - if !lhs_bound_typevar.is_inferable(db, inferable) - && lhs_bound_typevar.is_same_typevar_as(db, rhs_bound_typevar) => - { - ConstraintSet::from(true) - } - - // A fully static typevar is a subtype of its upper bound, and to something similar to - // the union of its constraints. An unbound, unconstrained, fully static typevar has an - // implicit upper bound of `object` (which is handled above). - (Type::TypeVar(bound_typevar), _) - if !bound_typevar.is_inferable(db, inferable) - && bound_typevar.typevar(db).bound_or_constraints(db).is_some() => - { - match bound_typevar.typevar(db).bound_or_constraints(db) { - None => unreachable!(), - Some(TypeVarBoundOrConstraints::UpperBound(bound)) => bound - .has_relation_to_impl( - db, - target, - inferable, - relation, - relation_visitor, - disjointness_visitor, - ), - Some(TypeVarBoundOrConstraints::Constraints(constraints)) => { - constraints.elements(db).iter().when_all(db, |constraint| { - constraint.has_relation_to_impl( - db, - target, - inferable, - relation, - relation_visitor, - disjointness_visitor, - ) - }) - } - } - } - - // If the typevar is constrained, there must be multiple constraints, and the typevar - // might be specialized to any one of them. However, the constraints do not have to be - // disjoint, which means an lhs type might be a subtype of all of the constraints. - (_, Type::TypeVar(bound_typevar)) - if !bound_typevar.is_inferable(db, inferable) - && !bound_typevar - .typevar(db) - .constraints(db) - .when_some_and(|constraints| { - constraints.iter().when_all(db, |constraint| { - self.has_relation_to_impl( - db, - *constraint, - inferable, - relation, - relation_visitor, - disjointness_visitor, - ) - }) - }) - .is_never_satisfied(db) => - { - // TODO: The repetition here isn't great, but we really need the fallthrough logic, - // where this arm only engages if it returns true (or in the world of constraints, - // not false). Once we're using real constraint sets instead of bool, we should be - // able to simplify the typevar logic. - bound_typevar - .typevar(db) - .constraints(db) - .when_some_and(|constraints| { - constraints.iter().when_all(db, |constraint| { - self.has_relation_to_impl( - db, - *constraint, - inferable, - relation, - relation_visitor, - disjointness_visitor, - ) - }) - }) - } - - (Type::TypeVar(bound_typevar), _) if bound_typevar.is_inferable(db, inferable) => { - // The implicit lower bound of a typevar is `Never`, which means - // that it is always assignable to any other type. - - // TODO: record the unification constraints - - ConstraintSet::from(true) - } - // `Never` is the bottom type, the empty set. (_, Type::Never) => ConstraintSet::from(false), @@ -2044,55 +1943,6 @@ impl<'db> Type<'db> { }) } - // Other than the special cases checked above, no other types are a subtype of a - // typevar, since there's no guarantee what type the typevar will be specialized to. - // (If the typevar is bounded, it might be specialized to a smaller type than the - // bound. This is true even if the bound is a final class, since the typevar can still - // be specialized to `Never`.) - (_, Type::TypeVar(bound_typevar)) if !bound_typevar.is_inferable(db, inferable) => { - ConstraintSet::from(false) - } - - (_, Type::TypeVar(typevar)) - if typevar.is_inferable(db, inferable) - && relation.is_assignability() - && typevar.typevar(db).upper_bound(db).is_none_or(|bound| { - !self - .has_relation_to_impl( - db, - bound, - inferable, - relation, - relation_visitor, - disjointness_visitor, - ) - .is_never_satisfied(db) - }) => - { - // TODO: record the unification constraints - - typevar.typevar(db).upper_bound(db).when_none_or(|bound| { - self.has_relation_to_impl( - db, - bound, - inferable, - relation, - relation_visitor, - disjointness_visitor, - ) - }) - } - - // TODO: Infer specializations here - (_, Type::TypeVar(bound_typevar)) if bound_typevar.is_inferable(db, inferable) => { - ConstraintSet::from(false) - } - (Type::TypeVar(bound_typevar), _) => { - // All inferable cases should have been handled above - assert!(!bound_typevar.is_inferable(db, inferable)); - ConstraintSet::from(false) - } - (Type::TypedDict(_), _) => { // TODO: Implement assignability and subtyping for TypedDict ConstraintSet::from(relation.is_assignability()) diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index 6780f47267..5efeaf573c 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -1040,7 +1040,7 @@ impl<'db> Node<'db> { // If the typevar is in inferable position, we need to verify that some valid // specialization satisfies the constraint set. let valid_specializations = typevar.valid_specializations(db); - if !some_specialization_satisfies(valid_specializations) { + if !some_specialization_satisfies(valid_specializations.node) { return false; } } else { @@ -2965,7 +2965,7 @@ impl<'db> BoundTypeVarInstance<'db> { /// Returns the valid specializations of a typevar. This is used when checking a constraint set /// when this typevar is in inferable position, where we only need _some_ specialization to /// satisfy the constraint set. - fn valid_specializations(self, db: &'db dyn Db) -> Node<'db> { + pub(crate) fn valid_specializations(self, db: &'db dyn Db) -> ConstraintSet<'db> { // For gradual upper bounds and constraints, we are free to choose any materialization that // makes the check succeed. In inferable positions, it is most helpful to choose a // materialization that is as permissive as possible, since that maximizes the number of @@ -2977,10 +2977,10 @@ impl<'db> BoundTypeVarInstance<'db> { // that _some_ valid specialization satisfies the constraint set, it's correct for us to // return the range of valid materializations that we can choose from. match self.typevar(db).bound_or_constraints(db) { - None => Node::AlwaysTrue, + None => ConstraintSet::from(true), Some(TypeVarBoundOrConstraints::UpperBound(bound)) => { let bound = bound.top_materialization(db); - ConstrainedTypeVar::new_node(db, self, Type::Never, bound) + ConstrainedTypeVar::new_node(db, self, Type::Never, bound).into() } Some(TypeVarBoundOrConstraints::Constraints(constraints)) => { let mut specializations = Node::AlwaysFalse; @@ -2992,7 +2992,7 @@ impl<'db> BoundTypeVarInstance<'db> { ConstrainedTypeVar::new_node(db, self, constraint_lower, constraint_upper), ); } - specializations + specializations.into() } } } @@ -3066,7 +3066,7 @@ impl<'db> GenericContext<'db> { let abstracted = self .variables(db) .fold(constraints.node, |constraints, bound_typevar| { - constraints.and(db, bound_typevar.valid_specializations(db)) + constraints.and(db, bound_typevar.valid_specializations(db).node) }); // Then we find all of the "representative types" for each typevar in the constraint set.