abstract over any mention of a typevar

This commit is contained in:
Douglas Creager 2025-12-09 08:29:30 -05:00
parent 3cb4b0ecb9
commit 438de79a6b
2 changed files with 19 additions and 13 deletions

View File

@ -348,7 +348,8 @@ from ty_extensions import ConstraintSet, generic_context
def mentions[T, U]():
# (T@mentions ≤ int) ∧ (U@mentions = list[T@mentions])
constraints = ConstraintSet.range(Never, T, int) & ConstraintSet.range(list[T], U, list[T])
# revealed: ty_extensions.Specialization[T@mentions = int, U@mentions = list[int]]
# TODO: revealed: ty_extensions.Specialization[T@mentions = int, U@mentions = list[int]]
# revealed: ty_extensions.Specialization[T@mentions = int, U@mentions = Unknown]
reveal_type(generic_context(mentions).specialize_constrained(constraints))
```

View File

@ -76,7 +76,9 @@ use rustc_hash::{FxHashMap, FxHashSet};
use salsa::plumbing::AsId;
use crate::types::generics::{GenericContext, InferableTypeVars, Specialization};
use crate::types::visitor::{TypeCollector, TypeVisitor, walk_type_with_recursion_guard};
use crate::types::visitor::{
TypeCollector, TypeVisitor, any_over_type, walk_type_with_recursion_guard,
};
use crate::types::{
BoundTypeVarIdentity, BoundTypeVarInstance, IntersectionType, Type, TypeRelation,
TypeVarBoundOrConstraints, UnionType, walk_bound_type_var_type,
@ -1768,22 +1770,27 @@ impl<'db> InteriorNode<'db> {
fn exists_one(self, db: &'db dyn Db, bound_typevar: BoundTypeVarIdentity<'db>) -> Node<'db> {
let map = self.sequent_map(db);
let mut path = PathAssignments::default();
let mentions_typevar = |ty: Type<'db>| match ty {
Type::TypeVar(haystack) => haystack.identity(db) == bound_typevar,
_ => false,
};
self.abstract_one_inner(
db,
// Remove any node that constrains `bound_typevar`, or that has a lower/upper bound of
// `bound_typevar`.
// Remove any node that constrains `bound_typevar`, or that has a lower/upper bound
// that mentions `bound_typevar`.
// TODO: This will currently remove constraints that mention a typevar, but the sequent
// map is not yet propagating all derived facts about those constraints. For instance,
// removing `T` from `T ≤ int ∧ U ≤ Sequence[T]` should produce `U ≤ Sequence[int]`.
// But that requires `T ≤ int ∧ U ≤ Sequence[T] → U ≤ Sequence[int]` to exist in the
// sequent map. It doesn't, and so we currently produce `U ≤ Unknown` in this case.
&mut |constraint| {
if constraint.typevar(db).identity(db) == bound_typevar {
return true;
}
if let Type::TypeVar(lower_bound_typevar) = constraint.lower(db)
&& lower_bound_typevar.identity(db) == bound_typevar
{
if any_over_type(db, constraint.lower(db), &mentions_typevar, false) {
return true;
}
if let Type::TypeVar(upper_bound_typevar) = constraint.upper(db)
&& upper_bound_typevar.identity(db) == bound_typevar
{
if any_over_type(db, constraint.upper(db), &mentions_typevar, false) {
return true;
}
false
@ -1807,9 +1814,7 @@ impl<'db> InteriorNode<'db> {
if constraint.typevar(db).identity(db) != bound_typevar {
return true;
}
if matches!(constraint.lower(db), Type::TypeVar(_))
|| matches!(constraint.upper(db), Type::TypeVar(_))
{
if constraint.lower(db).has_typevar(db) || constraint.upper(db).has_typevar(db) {
return true;
}
false