tautology

This commit is contained in:
Douglas Creager 2025-10-30 13:46:29 -04:00
parent 935abab07e
commit 31c9f7059a
2 changed files with 29 additions and 179 deletions

View File

@ -1726,6 +1726,29 @@ impl<'db> Type<'db> {
} }
match (self, target) { 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`. // Everything is a subtype of `object`.
(_, Type::NominalInstance(instance)) if instance.is_object() => { (_, Type::NominalInstance(instance)) if instance.is_object() => {
ConstraintSet::from(true) 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. // `Never` is the bottom type, the empty set.
(_, Type::Never) => ConstraintSet::from(false), (_, 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(_), _) => { (Type::TypedDict(_), _) => {
// TODO: Implement assignability and subtyping for TypedDict // TODO: Implement assignability and subtyping for TypedDict
ConstraintSet::from(relation.is_assignability()) ConstraintSet::from(relation.is_assignability())

View File

@ -1040,7 +1040,7 @@ impl<'db> Node<'db> {
// If the typevar is in inferable position, we need to verify that some valid // If the typevar is in inferable position, we need to verify that some valid
// specialization satisfies the constraint set. // specialization satisfies the constraint set.
let valid_specializations = typevar.valid_specializations(db); let valid_specializations = typevar.valid_specializations(db);
if !some_specialization_satisfies(valid_specializations) { if !some_specialization_satisfies(valid_specializations.node) {
return false; return false;
} }
} else { } else {
@ -2965,7 +2965,7 @@ impl<'db> BoundTypeVarInstance<'db> {
/// Returns the valid specializations of a typevar. This is used when checking a constraint set /// 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 /// when this typevar is in inferable position, where we only need _some_ specialization to
/// satisfy the constraint set. /// 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 // 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 // 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 // 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 // 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. // return the range of valid materializations that we can choose from.
match self.typevar(db).bound_or_constraints(db) { match self.typevar(db).bound_or_constraints(db) {
None => Node::AlwaysTrue, None => ConstraintSet::from(true),
Some(TypeVarBoundOrConstraints::UpperBound(bound)) => { Some(TypeVarBoundOrConstraints::UpperBound(bound)) => {
let bound = bound.top_materialization(db); 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)) => { Some(TypeVarBoundOrConstraints::Constraints(constraints)) => {
let mut specializations = Node::AlwaysFalse; let mut specializations = Node::AlwaysFalse;
@ -2992,7 +2992,7 @@ impl<'db> BoundTypeVarInstance<'db> {
ConstrainedTypeVar::new_node(db, self, constraint_lower, constraint_upper), ConstrainedTypeVar::new_node(db, self, constraint_lower, constraint_upper),
); );
} }
specializations specializations.into()
} }
} }
} }
@ -3066,7 +3066,7 @@ impl<'db> GenericContext<'db> {
let abstracted = self let abstracted = self
.variables(db) .variables(db)
.fold(constraints.node, |constraints, bound_typevar| { .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. // Then we find all of the "representative types" for each typevar in the constraint set.