From 832720c0f860e77fed3a3e7395e3d89ebc973d99 Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Wed, 18 Mar 2026 10:21:41 -0400 Subject: [PATCH 01/22] add plan --- PLAN.md | 267 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 267 insertions(+) create mode 100644 PLAN.md diff --git a/PLAN.md b/PLAN.md new file mode 100644 index 0000000000000..c71c81ba4fdd6 --- /dev/null +++ b/PLAN.md @@ -0,0 +1,267 @@ +# Plan: Propagate nested-typevar constraints through variance in the sequent map + +## Status markers + +Each step is marked with one of: + +- ⬜ Not started +- πŸ”§ In progress +- βœ… Completed + +When resuming this plan, read through the relevant files to validate status +markers before continuing. Include these instructions in the plan even though +they are also listed in the AGENTS.md file. + +## Overview + +The constraint set's `exists_one` operation removes all constraints mentioning a +bound typevar. When a typevar `T` appears *nested* inside the bound of a +constraint on a different typevar `U` (e.g., `U ≀ Sequence[T]`), we currently +lose all information about `U` because the sequent map doesn't generate derived +facts that substitute `T`'s concrete bounds into the nested occurrence. + +The fix requires teaching `add_sequents_for_pair` to recognize when one +constraint provides bounds on a typevar `T`, and the other constraint's +lower/upper bound mentions `T` nested inside a parameterized type. Using the +variance of `T`'s position in that parameterized type, we can determine what +substitution is valid: + +- **Covariant**: upper bound on `T` propagates into upper bound position; + lower bound on `T` propagates into lower bound position. (Preserves + direction.) +- **Contravariant**: upper bound on `T` propagates into lower bound + position; lower bound on `T` propagates into upper bound position. (Flips + direction.) +- **Invariant**: only an equality constraint on `T` (lower = upper) can + propagate. +- **Bivariant**: the typevar is irrelevant to the type; no implication is + needed since the constraint doesn't actually depend on the typevar. + +We implement covariance first as a complete end-to-end slice, then add +contravariance and invariance as modifications to that working foundation. + +## Steps + +### Phase 1: Helpers + +#### Step 1.1 ⬜ β€” Confirm that `variance_of` serves as our detection mechanism + +No new helper is needed. The existing `VarianceInferable` trait provides +`ty.variance_of(db, typevar)`, which returns: + +- `Bivariant` if the typevar doesn't appear in the type at all (or is genuinely + bivariant) β€” in either case, no implication is needed. +- `Covariant`, `Contravariant`, or `Invariant` if the typevar appears nested + in the type β€” telling us which substitution rule applies. + +This single call replaces both the presence check (`any_over_type`) and the +variance computation. We just call `variance_of` and skip if the result is +`Bivariant`. + +At the call site, add a prominent comment explaining this interpretation: +`Bivariant` here means "the typevar does not appear in this type (or is +genuinely bivariant, which is equivalent for our purposes β€” no implication is +needed in either case)." Note that if `Bivariant` is ever removed from the +`TypeVarVariance` enum, we would need an alternative representation for +"typevar not present" (e.g., returning `Option`). + +#### Step 1.2 ⬜ β€” Add a `Single` variant to `ApplySpecialization` + +Add a new variant to `ApplySpecialization` in `generics.rs`: + +```rust +Single(BoundTypeVarInstance<'db>, Type<'db>), +``` + +This maps a single typevar to a concrete type. The `get` method implementation +is trivial: check if `bound_typevar` matches the stored typevar and return the +mapped type if so, `None` otherwise. + +This can then be used via the existing `TypeMapping::ApplySpecialization` to +perform the substitution: `ty.apply_type_mapping(db, &TypeMapping::ApplySpecialization(ApplySpecialization::Single(typevar, replacement)))`. + +The rest of the `apply_type_mapping` infrastructure handles the recursive walk +through the type tree automatically. + +### Phase 2: Covariant nested typevar propagation (end-to-end) + +This phase implements the covariant case fully, including sequent generation, +testing, and validation. Contravariance and invariance will follow as +modifications to this working foundation. + +#### Step 2.1 ⬜ β€” Add mdtest cases for covariant propagation (red) + +Add tests to the "Transitivity" section of +`crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md`. +These follow the existing pattern: construct constraint sets with +`ConstraintSet.range(...)`, combine them with `&`, and verify implications with +`implies_subtype_of`. + +Each markdown section has its own scope, so define local `Covariant[T]` (and +later `Contravariant[T]`, `Invariant[T]`) classes in the new test sections. +Test both typevar orderings to verify BDD-ordering independence. + +Key test cases for covariant upper bound propagation: + +- `(T ≀ int) ∧ (U ≀ Covariant[T])` should imply `U ≀ Covariant[int]` + (i.e., `constraints.implies_subtype_of(U, Covariant[int])`) +- The same should NOT imply `U ≀ Covariant[bool]` (too tight) + +Key test cases for covariant lower bound propagation: + +- `(int ≀ T) ∧ (Covariant[T] ≀ U)` should imply `Covariant[int] ≀ U` + (i.e., `constraints.implies_subtype_of(Covariant[int], U)`) + +Run these tests first to verify they fail with the current logic (red phase of +TDD). Then proceed to Step 2.2 to make them pass. + +#### Step 2.2 ⬜ β€” Add sequent generation for covariant nested typevars (green) + +Currently, `add_sequents_for_pair` dispatches to +`add_mutual_sequents_for_different_typevars` when the two constraints are on +different typevars. That method only handles the case where a typevar appears as +a *direct* `Type::TypeVar(...)` in the other constraint's lower/upper bound. + +Add a new method (e.g., `add_nested_typevar_sequents`) called from +`add_mutual_sequents_for_different_typevars` (or from `add_sequents_for_pair` +directly) that handles the case where one constraint's bound *contains* the +other constraint's typevar nested inside a parameterized type. + +For the initial covariant-only implementation, the logic is: + +Given constraints `(l_B ≀ B ≀ u_B)` and `(l_C ≀ C ≀ u_C)` where `B` appears +nested in `l_C` or `u_C`: + +**Case A: `B` appears in `u_C` (upper bound of `C`)** + +- Compute `v = u_C.variance_of(db, B)`. +- If covariant: emit `(l_B ≀ B ≀ u_B) ∧ (l_C ≀ C ≀ u_C) β†’ (C ≀ u_C[B := u_B])` + (The upper bound on `B` substitutes into the upper bound of `C`.) + +**Case B: `B` appears in `l_C` (lower bound of `C`)** + +- Compute `v = l_C.variance_of(db, B)`. +- If covariant: emit `(l_B ≀ B ≀ u_B) ∧ (l_C ≀ C ≀ u_C) β†’ (l_C[B := l_B] ≀ C)` + (The lower bound on `B` substitutes into the lower bound of `C`.) + +For now, skip the contravariant, invariant, and bivariant cases β€” just return +early if the variance is not covariant. + +Note: the antecedent constraints in these sequents are the *original* +constraints from the BDD. The pair implication is valid because if both original +constraints hold, the covariant substitution certainly follows. + +The existing `add_mutual_sequents_for_different_typevars` handles direct +`Type::TypeVar(B)` references in bounds. Since a bare `Type::TypeVar` has +covariant variance in itself, the new nested logic would technically subsume it. +However, the existing code has careful handling for canonical ordering of +typevar-to-typevar constraints, so it's cleaner to keep them separate and only +check for nested references when the bound is *not* a bare `Type::TypeVar`. +Add a comment in the code explaining this relationship β€” it's a subtle point +that would be easy to miss. + +#### Step 2.3 ⬜ β€” Run the full test suite + +Run the full constraint set and ty_python_semantic test suite to check for +regressions. Fix any issues before proceeding. + +### Phase 3: Contravariant and invariant propagation + +Once covariance is working end-to-end, extend the logic to handle the remaining +variance cases. These should be fairly straightforward modifications to the +covariance logic. + +#### Step 3.1 ⬜ β€” Add mdtest cases for contravariant and invariant propagation (red) + +Add tests following the same pattern as Step 2.2, using the `Contravariant[T]` +and `Invariant[T]` classes already defined in the "Compound types" section. + +Contravariant test cases: + +- `(T ≀ int) ∧ (U ≀ Contravariant[T])` should imply + `Contravariant[int] ≀ U` (flipped direction β€” but actually this doesn't help + tighten U's upper bound). Need to think carefully about which constraints + are expressible and testable here. +- `(int ≀ T) ∧ (U ≀ Contravariant[T])` should imply + `U ≀ Contravariant[int]` (lower bound on T, flipped by contravariance, gives + upper bound on Contravariant[T]). + +Invariant test cases: + +- `(T = int) ∧ (U ≀ Invariant[T])` should imply `U ≀ Invariant[int]`. +- `(T ≀ int) ∧ (U ≀ Invariant[T])` should NOT imply `U ≀ Invariant[int]`. + +Composed variance test cases: + +- Nested generics where variances compose (e.g., `Covariant[Contravariant[T]]` + β€” net effect is contravariant). + +Run these tests first to verify they fail (red phase). + +#### Step 3.2 ⬜ β€” Add contravariant propagation + +Extend the nested typevar sequent generation: + +**`B` in `u_C` (upper bound of `C`), contravariant:** + +- Emit `(l_B ≀ B ≀ u_B) ∧ (l_C ≀ C ≀ u_C) β†’ (C ≀ u_C[B := l_B])` + (The *lower* bound on `B` substitutes into the upper bound of `C` β€” flipped.) + +**`B` in `l_C` (lower bound of `C`), contravariant:** + +- Emit `(l_B ≀ B ≀ u_B) ∧ (l_C ≀ C ≀ u_C) β†’ (l_C[B := u_B] ≀ C)` + (The *upper* bound on `B` substitutes into the lower bound of `C` β€” flipped.) + +#### Step 3.3 ⬜ β€” Add invariant propagation + +Extend the nested typevar sequent generation: + +- Only emit a derived constraint if `l_B = u_B` (equality constraint on `B`). +- If so, substitute that single type into either bound of `C`. + +#### Step 3.4 ⬜ β€” Run the full test suite + +Run the full test suite again to check for regressions. + +### Phase 4: Handle the same-typevar case with nested references + +#### Step 4.1 ⬜ β€” Extend `add_sequents_for_pair` for same-typevar with nested references + +The dispatch in `add_sequents_for_pair` currently falls through to +`add_concrete_sequents` when both constraints are on the same typevar and +neither has a typevar as a direct bound. But a constraint like `T ≀ Sequence[T]` +(recursive bound) would have `T` nested in its upper bound while also directly +constraining `T`. Check whether this case actually arises in practice, and if +so, whether it needs special handling. + +This is lower priority and may not need to be addressed initially. + +### Phase 5: Clean up + +#### Step 5.1 ⬜ β€” Remove or update the TODO comment + +Remove the TODO comment at line 2828 of `constraints.rs` once the feature is +working. Update any related comments. + +#### Step 5.2 ⬜ β€” Run `/home/dcreager/bin/jpk` + +Final pre-commit checks. We are in a jj worktree, so use `jpk` (with no +arguments) as a standin for `prek`. + +## Open questions + +1. **Performance**: The `variance_of` computation walks the type tree + recursively. Calling it inside `add_sequents_for_pair` for every pair of + constraints could be expensive. We should check if caching or early-exit + (e.g., skip if neither bound contains any typevar via `any_over_type`) is + needed. + +1. **Multiple typevar occurrences**: A single bound like `dict[T, T]` mentions + `T` twice. The `variance_of` implementation already handles this by joining + the variances of all occurrences. If one occurrence is covariant and another + contravariant, the joined variance is invariant, which correctly requires an + equality constraint. Verify that this composition works correctly for our + purposes. + +1. **Recursive bounds**: Can a constraint like `T ≀ Sequence[T]` arise? If so, + does it require special handling to avoid infinite loops during substitution? From 83596a7d058f4971f7f59e4b5bfae3e41cceed33 Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Wed, 18 Mar 2026 10:33:17 -0400 Subject: [PATCH 02/22] implement covariance case --- PLAN.md | 10 +- .../type_properties/implies_subtype_of.md | 44 +++++++ .../src/types/constraints.rs | 122 +++++++++++++++++- .../ty_python_semantic/src/types/generics.rs | 10 ++ 4 files changed, 179 insertions(+), 7 deletions(-) diff --git a/PLAN.md b/PLAN.md index c71c81ba4fdd6..17f015b4e54bb 100644 --- a/PLAN.md +++ b/PLAN.md @@ -44,7 +44,7 @@ contravariance and invariance as modifications to that working foundation. ### Phase 1: Helpers -#### Step 1.1 ⬜ β€” Confirm that `variance_of` serves as our detection mechanism +#### Step 1.1 βœ… β€” Confirm that `variance_of` serves as our detection mechanism No new helper is needed. The existing `VarianceInferable` trait provides `ty.variance_of(db, typevar)`, which returns: @@ -65,7 +65,7 @@ needed in either case)." Note that if `Bivariant` is ever removed from the `TypeVarVariance` enum, we would need an alternative representation for "typevar not present" (e.g., returning `Option`). -#### Step 1.2 ⬜ β€” Add a `Single` variant to `ApplySpecialization` +#### Step 1.2 βœ… β€” Add a `Single` variant to `ApplySpecialization` Add a new variant to `ApplySpecialization` in `generics.rs`: @@ -89,7 +89,7 @@ This phase implements the covariant case fully, including sequent generation, testing, and validation. Contravariance and invariance will follow as modifications to this working foundation. -#### Step 2.1 ⬜ β€” Add mdtest cases for covariant propagation (red) +#### Step 2.1 βœ… β€” Add mdtest cases for covariant propagation (red) Add tests to the "Transitivity" section of `crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md`. @@ -115,7 +115,7 @@ Key test cases for covariant lower bound propagation: Run these tests first to verify they fail with the current logic (red phase of TDD). Then proceed to Step 2.2 to make them pass. -#### Step 2.2 ⬜ β€” Add sequent generation for covariant nested typevars (green) +#### Step 2.2 βœ… β€” Add sequent generation for covariant nested typevars (green) Currently, `add_sequents_for_pair` dispatches to `add_mutual_sequents_for_different_typevars` when the two constraints are on @@ -160,7 +160,7 @@ check for nested references when the bound is *not* a bare `Type::TypeVar`. Add a comment in the code explaining this relationship β€” it's a subtle point that would be easy to miss. -#### Step 2.3 ⬜ β€” Run the full test suite +#### Step 2.3 βœ… β€” Run the full test suite Run the full constraint set and ty_python_semantic test suite to check for regressions. Fix any issues before proceeding. diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md b/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md index fd23c826e4b04..5762e51bd2bec 100644 --- a/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md +++ b/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md @@ -576,4 +576,48 @@ def concrete_pivot[T, U](): static_assert(not constraints.implies_subtype_of(T, U)) ``` +### Transitivity can propagate through nested covariant typevars + +When a typevar appears nested inside a covariant generic type in another constraint's bound, we can +propagate the bound "into" the generic type. + +```py +from typing import Never +from ty_extensions import ConstraintSet, static_assert + +class Covariant[T]: + def get(self) -> T: + raise ValueError + +def upper_bound[T, U](): + # If (T ≀ int) ∧ (U ≀ Covariant[T]), then by covariance, Covariant[T] ≀ Covariant[int], + # and by transitivity, U ≀ Covariant[int]. + constraints = ConstraintSet.range(Never, T, int) & ConstraintSet.range(Never, U, Covariant[T]) + static_assert(constraints.implies_subtype_of(U, Covariant[int])) + static_assert(not constraints.implies_subtype_of(U, Covariant[bool])) + static_assert(not constraints.implies_subtype_of(U, Covariant[str])) + +def lower_bound[T, U](): + # If (int ≀ T ∧ Covariant[T] ≀ U), then by covariance, Covariant[int] ≀ Covariant[T], + # and by transitivity, Covariant[int] ≀ U. Since bool ≀ int, Covariant[bool] ≀ U also holds. + constraints = ConstraintSet.range(int, T, object) & ConstraintSet.range(Covariant[T], U, object) + static_assert(constraints.implies_subtype_of(Covariant[int], U)) + static_assert(constraints.implies_subtype_of(Covariant[bool], U)) + static_assert(not constraints.implies_subtype_of(Covariant[str], U)) + +# Repeat with reversed typevar ordering to verify BDD-ordering independence. +def upper_bound[U, T](): + constraints = ConstraintSet.range(Never, T, int) & ConstraintSet.range(Never, U, Covariant[T]) + static_assert(constraints.implies_subtype_of(U, Covariant[int])) + static_assert(not constraints.implies_subtype_of(U, Covariant[bool])) + static_assert(not constraints.implies_subtype_of(U, Covariant[str])) + +def lower_bound[U, T](): + # Since bool ≀ int, Covariant[bool] ≀ U also holds. + constraints = ConstraintSet.range(int, T, object) & ConstraintSet.range(Covariant[T], U, object) + static_assert(constraints.implies_subtype_of(Covariant[int], U)) + static_assert(constraints.implies_subtype_of(Covariant[bool], U)) + static_assert(not constraints.implies_subtype_of(Covariant[str], U)) +``` + [subtyping]: https://typing.python.org/en/latest/spec/concepts.html#subtype-supertype-and-type-equivalence diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index 2250b5bf12e9f..b21b46b92f9e6 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -100,13 +100,15 @@ use rustc_hash::{FxHashMap, FxHashSet}; use smallvec::SmallVec; use crate::types::class::GenericAlias; -use crate::types::generics::InferableTypeVars; +use crate::types::generics::{ApplySpecialization, InferableTypeVars}; use crate::types::typevar::{BoundTypeVarIdentity, walk_bound_type_var_type}; +use crate::types::variance::VarianceInferable; use crate::types::visitor::{ TypeCollector, TypeVisitor, any_over_type, walk_type_with_recursion_guard, }; use crate::types::{ - BoundTypeVarInstance, IntersectionType, Type, TypeVarBoundOrConstraints, UnionType, + BoundTypeVarInstance, IntersectionType, Type, TypeContext, TypeMapping, + TypeVarBoundOrConstraints, TypeVarVariance, UnionType, }; use crate::{Db, FxIndexMap, FxIndexSet}; @@ -4287,6 +4289,7 @@ impl SequentMap { left_constraint, right_constraint, ); + self.add_nested_typevar_sequents(db, builder, left_constraint, right_constraint); } else if left_constraint_data.lower.is_type_var() || left_constraint_data.upper.is_type_var() || right_constraint_data.lower.is_type_var() @@ -4458,6 +4461,121 @@ impl SequentMap { } } + /// Adds sequents for the case where one constraint's lower or upper bound contains another + /// constraint's typevar nested inside a parameterized type (e.g., `U ≀ Covariant[T]`). + /// + /// This is distinct from `add_mutual_sequents_for_different_typevars`, which handles the case + /// where a typevar appears _directly_ as a top-level lower/upper bound (e.g., `U ≀ T`). A + /// bare `Type::TypeVar` is technically a special case of covariant nesting (since the variance + /// of `T` in `T` itself is covariant), but the existing direct-typevar logic handles it + /// separately because it requires careful canonical ordering of typevar-to-typevar constraints + /// that the generic nested-typevar logic here does not need to worry about. + fn add_nested_typevar_sequents<'db>( + &mut self, + db: &'db dyn Db, + builder: &ConstraintSetBuilder<'db>, + left_constraint: ConstraintId, + right_constraint: ConstraintId, + ) { + let mut try_one_direction = + |bound_constraint: ConstraintId, constrained_constraint: ConstraintId| { + let bound_data = builder.constraint_data(bound_constraint); + let bound_typevar = bound_data.typevar; + let constrained_data = builder.constraint_data(constrained_constraint); + let constrained_typevar = constrained_data.typevar; + + // Check the upper bound of the constrained constraint for nested occurrences of + // the bound typevar. We use `variance_of` as our combined presence + variance + // check: `Bivariant` means the typevar doesn't appear in the type (or is genuinely + // bivariant, which is semantically equivalent β€” no implication is needed in either + // case). + // + // Note: if `Bivariant` is ever removed from the `TypeVarVariance` enum, we would + // need an alternative representation for "typevar not present" + // (e.g., `Option`). + let upper_post = match constrained_data.upper.variance_of(db, bound_typevar) { + TypeVarVariance::Bivariant => None, + // Skip bare typevars β€” those are handled by + // `add_mutual_sequents_for_different_typevars`. + _ if constrained_data.upper.is_type_var() => None, + // Covariance preserves direction: upper bound on T substitutes into upper + // bound. A ≀ B β†’ G[A] ≀ G[B], so (T ≀ u_B) gives G[T] ≀ G[u_B]. + TypeVarVariance::Covariant if !bound_data.upper.is_object() => { + let new_upper = constrained_data.upper.apply_type_mapping( + db, + &TypeMapping::ApplySpecialization(ApplySpecialization::Single( + bound_typevar, + bound_data.upper, + )), + TypeContext::default(), + ); + (new_upper != constrained_data.upper).then(|| { + ConstraintId::new( + db, + builder, + constrained_typevar, + constrained_data.lower, + new_upper, + ) + }) + } + // TODO: Contravariant and Invariant cases will be added in Phase 3. + _ => None, + }; + if let Some(post) = upper_post { + self.add_pair_implication( + db, + builder, + bound_constraint, + constrained_constraint, + post, + ); + } + + // Check the lower bound of the constrained constraint for nested occurrences. + let lower_post = match constrained_data.lower.variance_of(db, bound_typevar) { + TypeVarVariance::Bivariant => None, + _ if constrained_data.lower.is_type_var() => None, + // Covariance preserves direction: lower bound on T substitutes into lower + // bound. A ≀ B β†’ G[A] ≀ G[B], so (l_B ≀ T) gives G[l_B] ≀ G[T]. + TypeVarVariance::Covariant if !bound_data.lower.is_never() => { + let new_lower = constrained_data.lower.apply_type_mapping( + db, + &TypeMapping::ApplySpecialization(ApplySpecialization::Single( + bound_typevar, + bound_data.lower, + )), + TypeContext::default(), + ); + (new_lower != constrained_data.lower).then(|| { + ConstraintId::new( + db, + builder, + constrained_typevar, + new_lower, + constrained_data.upper, + ) + }) + } + // TODO: Contravariant and Invariant cases will be added in Phase 3. + _ => None, + }; + if let Some(post) = lower_post { + self.add_pair_implication( + db, + builder, + bound_constraint, + constrained_constraint, + post, + ); + } + }; + + // Try both directions: left's typevar might be nested in right's bounds, or vice versa. + try_one_direction(left_constraint, right_constraint); + try_one_direction(right_constraint, left_constraint); + } + fn add_mutual_sequents_for_same_typevars<'db>( &mut self, db: &'db dyn Db, diff --git a/crates/ty_python_semantic/src/types/generics.rs b/crates/ty_python_semantic/src/types/generics.rs index cf8cf1ddb9bd2..e41046b0f0cff 100644 --- a/crates/ty_python_semantic/src/types/generics.rs +++ b/crates/ty_python_semantic/src/types/generics.rs @@ -1603,6 +1603,9 @@ pub enum ApplySpecialization<'a, 'db> { skip: Option, }, ReturnCallables(&'a FxIndexMap, BoundTypeVarInstance<'db>>), + /// Maps a single typevar to a concrete type. Used by the constraint set's sequent map to + /// substitute a typevar nested inside another constraint's bound. + Single(BoundTypeVarInstance<'db>, Type<'db>), } impl<'db> ApplySpecialization<'_, 'db> { @@ -1633,6 +1636,13 @@ impl<'db> ApplySpecialization<'_, 'db> { ApplySpecialization::ReturnCallables(replacements) => { replacements.get(&bound_typevar).copied().map(Type::TypeVar) } + ApplySpecialization::Single(typevar, ty) => { + if bound_typevar.is_same_typevar_as(db, *typevar) { + Some(*ty) + } else { + None + } + } } } } From 1f3c12722a51e2679c51c3386269b47fc289d89f Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Wed, 18 Mar 2026 10:55:01 -0400 Subject: [PATCH 03/22] implement contra and invariant cases --- PLAN.md | 8 +- .../type_properties/implies_subtype_of.md | 138 ++++++++++++++++++ .../src/types/constraints.rs | 124 +++++++++------- 3 files changed, 216 insertions(+), 54 deletions(-) diff --git a/PLAN.md b/PLAN.md index 17f015b4e54bb..d047313864669 100644 --- a/PLAN.md +++ b/PLAN.md @@ -171,7 +171,7 @@ Once covariance is working end-to-end, extend the logic to handle the remaining variance cases. These should be fairly straightforward modifications to the covariance logic. -#### Step 3.1 ⬜ β€” Add mdtest cases for contravariant and invariant propagation (red) +#### Step 3.1 βœ… β€” Add mdtest cases for contravariant and invariant propagation (red) Add tests following the same pattern as Step 2.2, using the `Contravariant[T]` and `Invariant[T]` classes already defined in the "Compound types" section. @@ -198,7 +198,7 @@ Composed variance test cases: Run these tests first to verify they fail (red phase). -#### Step 3.2 ⬜ β€” Add contravariant propagation +#### Step 3.2 βœ… β€” Add contravariant propagation Extend the nested typevar sequent generation: @@ -212,14 +212,14 @@ Extend the nested typevar sequent generation: - Emit `(l_B ≀ B ≀ u_B) ∧ (l_C ≀ C ≀ u_C) β†’ (l_C[B := u_B] ≀ C)` (The *upper* bound on `B` substitutes into the lower bound of `C` β€” flipped.) -#### Step 3.3 ⬜ β€” Add invariant propagation +#### Step 3.3 βœ… β€” Add invariant propagation Extend the nested typevar sequent generation: - Only emit a derived constraint if `l_B = u_B` (equality constraint on `B`). - If so, substitute that single type into either bound of `C`. -#### Step 3.4 ⬜ β€” Run the full test suite +#### Step 3.4 βœ… β€” Run the full test suite Run the full test suite again to check for regressions. diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md b/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md index 5762e51bd2bec..209fc70a43c25 100644 --- a/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md +++ b/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md @@ -620,4 +620,142 @@ def lower_bound[U, T](): static_assert(not constraints.implies_subtype_of(Covariant[str], U)) ``` +### Transitivity can propagate through nested contravariant typevars + +The previous section also works for contravariant generic types, though one of the antecedent +constraints is flipped. + +```py +from typing import Never +from ty_extensions import ConstraintSet, static_assert + +class Contravariant[T]: + def set(self, value: T): + pass + +def upper_bound[T, U](): + # If (int ≀ T ∧ U ≀ Contravariant[T]), then by contravariance, + # Contravariant[T] ≀ Contravariant[int], and by transitivity, U ≀ Contravariant[int]. + # Note: we need the *lower* bound on T (not the upper) because contravariance flips. + # Since bool ≀ int, Contravariant[int] ≀ Contravariant[bool], so U ≀ Contravariant[bool] + # also holds. + constraints = ConstraintSet.range(int, T, object) & ConstraintSet.range(Never, U, Contravariant[T]) + static_assert(constraints.implies_subtype_of(U, Contravariant[int])) + static_assert(constraints.implies_subtype_of(U, Contravariant[bool])) + static_assert(not constraints.implies_subtype_of(U, Contravariant[str])) + +def lower_bound[T, U](): + # If (T ≀ int ∧ Contravariant[T] ≀ U), then by contravariance, + # Contravariant[int] ≀ Contravariant[T], and by transitivity, Contravariant[int] ≀ U. + # Contravariant[bool] is a supertype of Contravariant[int] (since bool ≀ int), so + # Contravariant[bool] ≀ U does NOT hold. + constraints = ConstraintSet.range(Never, T, int) & ConstraintSet.range(Contravariant[T], U, object) + static_assert(constraints.implies_subtype_of(Contravariant[int], U)) + static_assert(not constraints.implies_subtype_of(Contravariant[bool], U)) + static_assert(not constraints.implies_subtype_of(Contravariant[str], U)) + +# Repeat with reversed typevar ordering to verify BDD-ordering independence. +def upper_bound[U, T](): + constraints = ConstraintSet.range(int, T, object) & ConstraintSet.range(Never, U, Contravariant[T]) + static_assert(constraints.implies_subtype_of(U, Contravariant[int])) + static_assert(constraints.implies_subtype_of(U, Contravariant[bool])) + static_assert(not constraints.implies_subtype_of(U, Contravariant[str])) + +def lower_bound[U, T](): + constraints = ConstraintSet.range(Never, T, int) & ConstraintSet.range(Contravariant[T], U, object) + static_assert(constraints.implies_subtype_of(Contravariant[int], U)) + static_assert(not constraints.implies_subtype_of(Contravariant[bool], U)) + static_assert(not constraints.implies_subtype_of(Contravariant[str], U)) +``` + +### Transitivity can propagate through nested invariant typevars + +For invariant type parameters, only an equality constraint on the typevar allows propagation. A +one-sided bound (upper or lower only) is not sufficient. + +```py +from typing import Never +from ty_extensions import ConstraintSet, static_assert + +class Invariant[T]: + def get(self) -> T: + raise ValueError + + def set(self, value: T): + pass + +def equality_constraint[T, U](): + # (T = int ∧ U ≀ Invariant[T]) should imply U ≀ Invariant[int]. + constraints = ConstraintSet.range(int, T, int) & ConstraintSet.range(Never, U, Invariant[T]) + static_assert(constraints.implies_subtype_of(U, Invariant[int])) + static_assert(not constraints.implies_subtype_of(U, Invariant[bool])) + static_assert(not constraints.implies_subtype_of(U, Invariant[str])) + +def upper_bound_only[T, U](): + # (T ≀ int ∧ U ≀ Invariant[T]) should NOT imply U ≀ Invariant[int], because T is invariant + # and we only have an upper bound, not equality. + constraints = ConstraintSet.range(Never, T, int) & ConstraintSet.range(Never, U, Invariant[T]) + static_assert(not constraints.implies_subtype_of(U, Invariant[int])) + static_assert(not constraints.implies_subtype_of(U, Invariant[bool])) + static_assert(not constraints.implies_subtype_of(U, Invariant[str])) + +def lower_bound_only[T, U](): + # (int ≀ T ∧ Invariant[T] ≀ U) should NOT imply Invariant[int] ≀ U, because T is invariant + # and we only have a lower bound, not equality. + constraints = ConstraintSet.range(int, T, object) & ConstraintSet.range(Invariant[T], U, object) + static_assert(not constraints.implies_subtype_of(Invariant[int], U)) + static_assert(not constraints.implies_subtype_of(Invariant[bool], U)) + static_assert(not constraints.implies_subtype_of(Invariant[str], U)) + +# Repeat with reversed typevar ordering. +def equality_constraint[U, T](): + constraints = ConstraintSet.range(int, T, int) & ConstraintSet.range(Never, U, Invariant[T]) + static_assert(constraints.implies_subtype_of(U, Invariant[int])) + static_assert(not constraints.implies_subtype_of(U, Invariant[bool])) + static_assert(not constraints.implies_subtype_of(U, Invariant[str])) +``` + +### Transitivity propagates through composed variance + +When a typevar is nested inside multiple layers of generics, variances compose. For instance, a +covariant type inside a contravariant type yields contravariant overall. + +```py +from typing import Never +from ty_extensions import ConstraintSet, static_assert + +class Covariant[T]: + def get(self) -> T: + raise ValueError + +class Contravariant[T]: + def set(self, value: T): + pass + +def covariant_of_contravariant[T, U](): + # Covariant[Contravariant[T]]: T is contravariant overall (covariant Γ— contravariant). + # So a lower bound on T should propagate (flipped). + constraints = ConstraintSet.range(int, T, object) & ConstraintSet.range(Never, U, Covariant[Contravariant[T]]) + static_assert(constraints.implies_subtype_of(U, Covariant[Contravariant[int]])) + static_assert(not constraints.implies_subtype_of(U, Covariant[Contravariant[str]])) + +def contravariant_of_covariant[T, U](): + # Contravariant[Covariant[T]]: T is contravariant overall (contravariant Γ— covariant). + # So a lower bound on T should propagate (flipped). + constraints = ConstraintSet.range(int, T, object) & ConstraintSet.range(Never, U, Contravariant[Covariant[T]]) + static_assert(constraints.implies_subtype_of(U, Contravariant[Covariant[int]])) + static_assert(not constraints.implies_subtype_of(U, Contravariant[Covariant[str]])) + +# Repeat with reversed typevar ordering. +def covariant_of_contravariant[U, T](): + constraints = ConstraintSet.range(int, T, object) & ConstraintSet.range(Never, U, Covariant[Contravariant[T]]) + static_assert(constraints.implies_subtype_of(U, Covariant[Contravariant[int]])) + static_assert(not constraints.implies_subtype_of(U, Covariant[Contravariant[str]])) + +def contravariant_of_covariant[U, T](): + constraints = ConstraintSet.range(int, T, object) & ConstraintSet.range(Never, U, Contravariant[Covariant[T]]) + static_assert(constraints.implies_subtype_of(U, Contravariant[Covariant[int]])) + static_assert(not constraints.implies_subtype_of(U, Contravariant[Covariant[str]])) +``` + [subtyping]: https://typing.python.org/en/latest/spec/concepts.html#subtype-supertype-and-type-equivalence diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index b21b46b92f9e6..7b58fa4d04dbe 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -4493,7 +4493,8 @@ impl SequentMap { // Note: if `Bivariant` is ever removed from the `TypeVarVariance` enum, we would // need an alternative representation for "typevar not present" // (e.g., `Option`). - let upper_post = match constrained_data.upper.variance_of(db, bound_typevar) { + let upper_replacement = match constrained_data.upper.variance_of(db, bound_typevar) + { TypeVarVariance::Bivariant => None, // Skip bare typevars β€” those are handled by // `add_mutual_sequents_for_different_typevars`. @@ -4501,73 +4502,96 @@ impl SequentMap { // Covariance preserves direction: upper bound on T substitutes into upper // bound. A ≀ B β†’ G[A] ≀ G[B], so (T ≀ u_B) gives G[T] ≀ G[u_B]. TypeVarVariance::Covariant if !bound_data.upper.is_object() => { - let new_upper = constrained_data.upper.apply_type_mapping( - db, - &TypeMapping::ApplySpecialization(ApplySpecialization::Single( - bound_typevar, - bound_data.upper, - )), - TypeContext::default(), - ); - (new_upper != constrained_data.upper).then(|| { - ConstraintId::new( - db, - builder, - constrained_typevar, - constrained_data.lower, - new_upper, - ) - }) + Some(bound_data.upper) + } + // Contravariance flips direction: lower bound on T substitutes into upper + // bound. A ≀ B β†’ G[B] ≀ G[A], so (l_B ≀ T) gives G[T] ≀ G[l_B]. + TypeVarVariance::Contravariant if !bound_data.lower.is_never() => { + Some(bound_data.lower) + } + // Invariance requires equality: only substitute if l_B = u_B. + TypeVarVariance::Invariant + if bound_data.lower == bound_data.upper && !bound_data.lower.is_never() => + { + Some(bound_data.lower) } - // TODO: Contravariant and Invariant cases will be added in Phase 3. _ => None, }; - if let Some(post) = upper_post { - self.add_pair_implication( + if let Some(replacement) = upper_replacement { + let new_upper = constrained_data.upper.apply_type_mapping( db, - builder, - bound_constraint, - constrained_constraint, - post, + &TypeMapping::ApplySpecialization(ApplySpecialization::Single( + bound_typevar, + replacement, + )), + TypeContext::default(), ); + if new_upper != constrained_data.upper { + let post = ConstraintId::new( + db, + builder, + constrained_typevar, + constrained_data.lower, + new_upper, + ); + self.add_pair_implication( + db, + builder, + bound_constraint, + constrained_constraint, + post, + ); + } } // Check the lower bound of the constrained constraint for nested occurrences. - let lower_post = match constrained_data.lower.variance_of(db, bound_typevar) { + let lower_replacement = match constrained_data.lower.variance_of(db, bound_typevar) + { TypeVarVariance::Bivariant => None, _ if constrained_data.lower.is_type_var() => None, // Covariance preserves direction: lower bound on T substitutes into lower // bound. A ≀ B β†’ G[A] ≀ G[B], so (l_B ≀ T) gives G[l_B] ≀ G[T]. TypeVarVariance::Covariant if !bound_data.lower.is_never() => { - let new_lower = constrained_data.lower.apply_type_mapping( - db, - &TypeMapping::ApplySpecialization(ApplySpecialization::Single( - bound_typevar, - bound_data.lower, - )), - TypeContext::default(), - ); - (new_lower != constrained_data.lower).then(|| { - ConstraintId::new( - db, - builder, - constrained_typevar, - new_lower, - constrained_data.upper, - ) - }) + Some(bound_data.lower) + } + // Contravariance flips direction: upper bound on T substitutes into lower + // bound. A ≀ B β†’ G[B] ≀ G[A], so (T ≀ u_B) gives G[u_B] ≀ G[T]. + TypeVarVariance::Contravariant if !bound_data.upper.is_object() => { + Some(bound_data.upper) + } + // Invariance requires equality: only substitute if l_B = u_B. + TypeVarVariance::Invariant + if bound_data.lower == bound_data.upper && !bound_data.lower.is_never() => + { + Some(bound_data.lower) } - // TODO: Contravariant and Invariant cases will be added in Phase 3. _ => None, }; - if let Some(post) = lower_post { - self.add_pair_implication( + if let Some(replacement) = lower_replacement { + let new_lower = constrained_data.lower.apply_type_mapping( db, - builder, - bound_constraint, - constrained_constraint, - post, + &TypeMapping::ApplySpecialization(ApplySpecialization::Single( + bound_typevar, + replacement, + )), + TypeContext::default(), ); + if new_lower != constrained_data.lower { + let post = ConstraintId::new( + db, + builder, + constrained_typevar, + new_lower, + constrained_data.upper, + ); + self.add_pair_implication( + db, + builder, + bound_constraint, + constrained_constraint, + post, + ); + } } }; From c39a60077d5b584b6a16caedcfc14020a4df21a7 Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Wed, 18 Mar 2026 11:00:30 -0400 Subject: [PATCH 04/22] remove stale TODO --- crates/ty_python_semantic/src/types/constraints.rs | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index 7b58fa4d04dbe..d44e8450adec4 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -2826,12 +2826,9 @@ impl InteriorNode { db, builder, // 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. + // that mentions `bound_typevar`. The sequent map ensures that derived facts are + // propagated for nested typevar references, using the variance of the typevar's + // position to determine the correct substitution. &mut |constraint| { let constraint = builder.constraint_data(constraint); if constraint.typevar.identity(db) == bound_typevar { From 658a6732d05e96fb055c0b19d2cae8f0cc0900e8 Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Wed, 18 Mar 2026 14:25:51 -0400 Subject: [PATCH 05/22] update plan with reverse checks --- PLAN.md | 220 ++++++++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 215 insertions(+), 5 deletions(-) diff --git a/PLAN.md b/PLAN.md index d047313864669..d76dff8514c1c 100644 --- a/PLAN.md +++ b/PLAN.md @@ -223,9 +223,202 @@ Extend the nested typevar sequent generation: Run the full test suite again to check for regressions. -### Phase 4: Handle the same-typevar case with nested references +### Phase 4: Reverse direction β€” decomposing matching generic bounds -#### Step 4.1 ⬜ β€” Extend `add_sequents_for_pair` for same-typevar with nested references +Phases 1–3 implemented the *forward* direction: given a concrete bound on a +typevar `T`, substitute it into a nested occurrence of `T` in another typevar's +bound. This is a cross-typevar (different-typevar) pair sequent. + +The *reverse* direction handles the case where a single constraint on a typevar +has lower and upper bounds that are both parameterizations of the same generic +type. By decomposing the generic type using variance, we can extract bounds on +the nested typevar. + +Example: the constraint `(Sequence[int] ≀ A ≀ Sequence[T])` implies +`(int ≀ T)`, because `Sequence` is covariant, so `Sequence[int] ≀ Sequence[T]` +implies `int ≀ T`. + +This combined constraint arises from two separate constraints `(Sequence[int] ≀ A)` +and `(A ≀ Sequence[T])` being combined β€” the existing `add_concrete_sequents` +logic should already produce this combined constraint as a pair implication. + +This is *part* of what's needed to make patterns like +`invoke(head_sequence, x)` work: + +```python +def invoke[A, B](c: Callable[[A], B], a: A) -> B: ... +def head_sequence[T](s: Sequence[T]) -> T: ... +def _(x: Sequence[int]): + reveal_type(invoke(head_sequence, x)) # should be int +``` + +The matching would produce constraints that combine into: + +- `Sequence[int] ≀ A ≀ Sequence[T]` (from argument + callable parameter) +- `T ≀ B` (from callable return matching) + +To derive `int ≀ T`, we need to decompose `Sequence[int] ≀ A ≀ Sequence[T]` +by recognizing that `Sequence[int] ≀ Sequence[T]` must hold, and applying +covariance. + +Note: this example will also require conjoining constraint sets across +multiple arguments (which is not yet implemented β€” tracked by the TODO in +`add_type_mappings_from_constraint_set`). The reverse decomposition is +necessary but not sufficient on its own. + +#### Where this fits + +This is a single-constraint decomposition: given a constraint +`(L ≀ A ≀ U)`, we check whether `L ≀ U` produces useful derived constraints +on the typevars mentioned in `L` and `U`. This logic belongs in +`add_sequents_for_single` (or is triggered when the combined constraint is +first created). + +#### Variance rules (same as forward, applied in reverse) + +Given a constraint `(G[l'] ≀ A ≀ G[T])` where both bounds share the same +generic base `G`: + +| Variance of T in G | Derived constraint | +| ------------------ | ------------------------------------------------ | +| Covariant | `l' ≀ T` | +| Contravariant | `T ≀ l'` | +| Invariant | `T = l'` (only if both sides match structurally) | +| Bivariant | skip | + +And symmetrically for `(G[T] ≀ A ≀ G[u'])`: + +| Variance of T in G | Derived constraint | +| ------------------ | --------------------------------------- | +| Covariant | `T ≀ u'` | +| Contravariant | `u' ≀ T` | +| Invariant | `T = u'` (only with matching structure) | +| Bivariant | skip | + +#### Approach: single implication via assignability check + +Rather than building bespoke generic-base-matching logic, we can reuse the +existing constraint set assignability machinery. Given a constraint +`(L ≀ A ≀ U)`, the constraint is only satisfiable if `L ≀ U`. If `L` and/or +`U` mention typevars, then `L ≀ U` produces a constraint set on those typevars. + +This could be triggered from `add_sequents_for_single` β€” for every constraint +`(L ≀ A ≀ U)`, compute `L.when_constraint_set_assignable_to(U)` and derive +implications from the result. No need for an upfront check on whether the +bounds mention typevars β€” just do the CSA check unconditionally and see if the +result is a non-trivial constraint set. Deeply scanning for typevars would not +be significantly cheaper than just doing the check. + +This should subsume the existing `single_implications` logic in +`add_sequents_for_single`. The current code manually propagates typevar-to- +typevar bounds (e.g., `(S ≀ T ≀ U) β†’ (S ≀ U)`), but a CSA check on `S ≀ U` +will produce that same constraint with the correct typevar ordering +automatically. The bare-typevar case does not need special treatment β€” CSA +handles canonical ordering naturally. + +Note that the existing pair sequent logic should already combine two +same-typevar constraints like `(Sequence[int] ≀ A)` and `(A ≀ Sequence[T])` +into a single combined constraint `(Sequence[int] ≀ A ≀ Sequence[T])` via +`add_concrete_sequents`. So the decomposition logic lives at the single- +constraint level. + +The result of the assignability check is a full constraint set (an arbitrary +boolean formula, not just a conjunction). The sequent map currently only +supports implications where the consequent is a single constraint. As a +pragmatic starting point, we handle only the case where the resulting +constraint set is a single conjunction β€” i.e., a single path from root to the +`always` terminal in the BDD. + +To detect this, we can take advantage of BDD reduction. Our BDDs are only +quasi-reduced, but redundant nodes where both outgoing edges lead to `never` +are still collapsed. This means if we ever encounter an interior node where +both outgoing edges (if_true and if_false) point to something other than +`never`, that node *must* have at least two paths to the `always` terminal, +and the constraint set is not a simple conjunction. So a single structural +walk of the tree suffices to check β€” no PathAssignments/SequentMap needed. + +If the constraint set is simple (single rootβ†’always path), walk it a second +time to collect the constraints along that path: + +- For each positive constraint (interior node where we take the if_true + branch): record a `single_implication` from the original constraint to the + derived constraint. +- For each negative constraint (interior node where we take the if_false + branch): record a `pair_impossibility` between the original constraint and + the derived constraint. + +For common cases (covariant/contravariant generics with a single type +parameter), the result should always be a simple conjunction, so this approach +should suffice. + +A future, more sophisticated solution could handle arbitrary constraint set +results by viewing the BDD as a DNF (disjunction of paths from root to the +`always` terminal, where each path is a conjunction). Each DNF clause could be +integrated into `PathAssignments` by recursing with resets for each path β€” a +pattern similar to what `walk_edge` already does for true/false/uncertain +branches. But this is significantly more complex and can be deferred. + +Circular dependency concern: we'd be invoking constraint set assignability +*from within* sequent map construction. We need to verify this doesn't create +cycles. A possible mitigation is to use the assignability check without +consulting the sequent map (i.e., a "raw" check that doesn't itself rely on +derived facts). + +#### Steps + +##### Step 4.1 ⬜ β€” Add mdtest cases for reverse decomposition (red) + +Add tests to the Transitivity section of `implies_subtype_of.md`. The tests +should construct the combined constraint directly using `ConstraintSet.range` +(e.g., `ConstraintSet.range(Covariant[int], A, Covariant[T])`) and verify +that the derived implications hold. + +Test cases: + +- Covariant: `(Covariant[int] ≀ A ≀ Covariant[T])` should imply `int ≀ T` +- Contravariant: `(Contravariant[int] ≀ A ≀ Contravariant[T])` should imply + `T ≀ int` (flipped) +- Invariant: `(Invariant[int] ≀ A ≀ Invariant[T])` should imply `T = int` +- Bare typevar (existing behavior, should still pass): + `(S ≀ A ≀ T)` should imply `S ≀ T` +- Test both typevar orderings for BDD-ordering independence + +##### Step 4.2 ⬜ β€” Implement reverse decomposition via CSA in `add_sequents_for_single` + +Replace (or extend) the existing single-constraint implication logic in +`add_sequents_for_single` with a CSA-based approach: + +1. For each constraint `(L ≀ A ≀ U)`, compute + `L.when_constraint_set_assignable_to(U)` to get a constraint set `C`. +1. Check if `C` is a simple conjunction (single rootβ†’always path in the BDD). + Use the structural criterion: if any interior node has both outgoing edges + pointing to something other than `never`, the result is not simple β€” bail + out. +1. If simple, walk the single path and record sequents: + - For each positive constraint (if_true branch taken): add a + `single_implication` from the original constraint to the derived one. + - For each negative constraint (if_false branch taken): add a + `pair_impossibility` between the original and derived constraints. + +This should subsume the existing `single_implications` logic in +`add_sequents_for_single`, including bare typevar-to-typevar propagation. +Variance is handled automatically by the CSA check β€” no need for explicit +variance matching or special-casing bare typevars. + +##### Step 4.3 ⬜ β€” Verify bare typevar propagation still works + +Confirm that the existing tests for typevar-to-typevar transitivity +(e.g., `(S ≀ T ≀ U) β†’ (S ≀ U)`) still pass with the new CSA-based logic. +If the new logic fully subsumes the old `single_implications` code, consider +removing the old code. + +##### Step 4.4 ⬜ β€” Run the full test suite + +Run the full test suite to check for regressions. + +### Phase 5: Handle the same-typevar case with recursive nested references + +#### Step 5.1 ⬜ β€” Extend `add_sequents_for_pair` for same-typevar with recursive nesting The dispatch in `add_sequents_for_pair` currently falls through to `add_concrete_sequents` when both constraints are on the same typevar and @@ -236,14 +429,14 @@ so, whether it needs special handling. This is lower priority and may not need to be addressed initially. -### Phase 5: Clean up +### Phase 6: Clean up -#### Step 5.1 ⬜ β€” Remove or update the TODO comment +#### Step 6.1 βœ… β€” Remove or update the TODO comment Remove the TODO comment at line 2828 of `constraints.rs` once the feature is working. Update any related comments. -#### Step 5.2 ⬜ β€” Run `/home/dcreager/bin/jpk` +#### Step 6.2 βœ… β€” Run `/home/dcreager/bin/jpk` Final pre-commit checks. We are in a jj worktree, so use `jpk` (with no arguments) as a standin for `prek`. @@ -265,3 +458,20 @@ arguments) as a standin for `prek`. 1. **Recursive bounds**: Can a constraint like `T ≀ Sequence[T]` arise? If so, does it require special handling to avoid infinite loops during substitution? + +1. **Circular dependencies in reverse decomposition**: The reverse direction + invokes constraint set assignability from within sequent map construction. + Need to verify this doesn't create cycles. May need a "raw" assignability + check that doesn't consult the sequent map. + +1. **DNF expansion for complex constraint set results**: When the assignability + check produces a non-simple constraint set (e.g., a disjunction), we could + view the BDD as a DNF and integrate each path's conjunction into + `PathAssignments` by recursing with resets. Deferred for now. + +1. **No natural Python example exercises forward direction today**: The forward + direction (Phases 1–3) is correct and tested via mdtests, but currently no + Python code path conjoins argument-level concrete bounds with callable- + matching cross-typevar constraints into a single constraint set. This will + be exercised once the specialization builder migrates to maintaining a single + constraint set (tracked by the TODO in `add_type_mappings_from_constraint_set`). From e626cff2d2734f83488ab91eee518533b8ac9c39 Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Thu, 19 Mar 2026 14:05:02 -0400 Subject: [PATCH 06/22] add reverse inference --- PLAN.md | 28 ++- .../type_properties/implies_subtype_of.md | 85 ++++++++ .../src/types/constraints.rs | 205 ++++++++++++++---- 3 files changed, 264 insertions(+), 54 deletions(-) diff --git a/PLAN.md b/PLAN.md index d76dff8514c1c..06a6b2d75e14a 100644 --- a/PLAN.md +++ b/PLAN.md @@ -383,13 +383,27 @@ Test cases: `(S ≀ A ≀ T)` should imply `S ≀ T` - Test both typevar orderings for BDD-ordering independence -##### Step 4.2 ⬜ β€” Implement reverse decomposition via CSA in `add_sequents_for_single` +##### Step 4.2 βœ… β€” Fix the disjointness check in `intersect` -Replace (or extend) the existing single-constraint implication logic in -`add_sequents_for_single` with a CSA-based approach: +The current `ConstraintId::intersect` method uses +`lower.is_constraint_set_assignable_to(db, upper)` (a universal/always check) +to determine if the intersection `(L ≀ A ≀ U)` is disjoint. When `U` contains +typevars (e.g., `Covariant[T]`), this returns false even if there exist +assignments of `T` that make `L ≀ U` hold β€” causing the combined constraint to +be pruned as unsatisfiable. + +Fix: change the check to an existential one β€” "is `L ≀ U` *ever* true?" rather +than "is `L ≀ U` *always* true?". This is +`!when_constraint_set_assignable_to(L, U).is_never_satisfied()`. If there +exists some assignment where the intersection is satisfiable, the combined +constraint should survive. + +##### Step 4.3 βœ… β€” Add CSA-based decomposition in `add_sequents_for_single` + +For each constraint `(L ≀ A ≀ U)`, compute +`L.when_constraint_set_assignable_to(U)` to get a constraint set `C` that +describes the conditions under which `L ≀ U` holds. Then: -1. For each constraint `(L ≀ A ≀ U)`, compute - `L.when_constraint_set_assignable_to(U)` to get a constraint set `C`. 1. Check if `C` is a simple conjunction (single rootβ†’always path in the BDD). Use the structural criterion: if any interior node has both outgoing edges pointing to something other than `never`, the result is not simple β€” bail @@ -405,14 +419,14 @@ This should subsume the existing `single_implications` logic in Variance is handled automatically by the CSA check β€” no need for explicit variance matching or special-casing bare typevars. -##### Step 4.3 ⬜ β€” Verify bare typevar propagation still works +##### Step 4.4 βœ… β€” Verify bare typevar propagation still works Confirm that the existing tests for typevar-to-typevar transitivity (e.g., `(S ≀ T ≀ U) β†’ (S ≀ U)`) still pass with the new CSA-based logic. If the new logic fully subsumes the old `single_implications` code, consider removing the old code. -##### Step 4.4 ⬜ β€” Run the full test suite +##### Step 4.5 βœ… β€” Run the full test suite Run the full test suite to check for regressions. diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md b/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md index 209fc70a43c25..db3021076a6ba 100644 --- a/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md +++ b/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md @@ -758,4 +758,89 @@ def contravariant_of_covariant[U, T](): static_assert(not constraints.implies_subtype_of(U, Contravariant[Covariant[str]])) ``` +### Reverse decomposition: bounds on a typevar can be decomposed via variance + +When a constraint has lower and upper bounds that are parameterizations of the same generic type, we +can decompose the bounds to extract constraints on the nested typevar. For instance, the constraint +`Covariant[int] ≀ A ≀ Covariant[T]` implies `int ≀ T`, because `Covariant` is covariant and +`Covariant[int] ≀ Covariant[T]` requires `int ≀ T`. + +```py +from typing import Never +from ty_extensions import ConstraintSet, static_assert + +class Covariant[T]: + def get(self) -> T: + raise ValueError + +class Contravariant[T]: + def set(self, value: T): + pass + +class Invariant[T]: + def get(self) -> T: + raise ValueError + + def set(self, value: T): + pass + +def covariant_decomposition[A, T](): + # Covariant[int] ≀ A ≀ Covariant[T] implies int ≀ T. + constraints = ConstraintSet.range(Covariant[int], A, Covariant[T]) + static_assert(constraints.implies_subtype_of(int, T)) + static_assert(not constraints.implies_subtype_of(str, T)) + +def contravariant_decomposition[A, T](): + # Contravariant[int] ≀ A ≀ Contravariant[T] implies T ≀ int (flipped). + # Because contravariance reverses: Contravariant[int] ≀ Contravariant[T] means T ≀ int. + constraints = ConstraintSet.range(Contravariant[int], A, Contravariant[T]) + static_assert(constraints.implies_subtype_of(T, int)) + static_assert(not constraints.implies_subtype_of(T, str)) + +def invariant_decomposition[A, T](): + # Invariant[int] ≀ A ≀ Invariant[T] implies T = int. + constraints = ConstraintSet.range(Invariant[int], A, Invariant[T]) + static_assert(constraints.implies_subtype_of(T, int)) + static_assert(constraints.implies_subtype_of(int, T)) + static_assert(not constraints.implies_subtype_of(T, str)) + +def bare_typevar_decomposition[A, S, T](): + # S ≀ A ≀ T implies S ≀ T. This is existing behavior (bare typevar transitivity) + # that should continue to work. + constraints = ConstraintSet.range(S, A, T) + static_assert(constraints.implies_subtype_of(S, T)) + +# Repeat with reversed typevar ordering. +def covariant_decomposition[T, A](): + constraints = ConstraintSet.range(Covariant[int], A, Covariant[T]) + static_assert(constraints.implies_subtype_of(int, T)) + static_assert(not constraints.implies_subtype_of(str, T)) + +def contravariant_decomposition[T, A](): + constraints = ConstraintSet.range(Contravariant[int], A, Contravariant[T]) + static_assert(constraints.implies_subtype_of(T, int)) + static_assert(not constraints.implies_subtype_of(T, str)) + +def invariant_decomposition[T, A](): + constraints = ConstraintSet.range(Invariant[int], A, Invariant[T]) + static_assert(constraints.implies_subtype_of(T, int)) + static_assert(constraints.implies_subtype_of(int, T)) + static_assert(not constraints.implies_subtype_of(T, str)) + +# The lower and upper bounds don't need to be parameterizations of the same type β€” our inference +# logic handles subtyping naturally. +class Sub(Covariant[int]): ... + +def subclass_lower_bound[A, T](): + # Sub ≀ Covariant[int], so Sub ≀ A ≀ Covariant[T] implies int ≀ T. + constraints = ConstraintSet.range(Sub, A, Covariant[T]) + static_assert(constraints.implies_subtype_of(int, T)) + static_assert(not constraints.implies_subtype_of(str, T)) + +def subclass_lower_bound[T, A](): + constraints = ConstraintSet.range(Sub, A, Covariant[T]) + static_assert(constraints.implies_subtype_of(int, T)) + static_assert(not constraints.implies_subtype_of(str, T)) +``` + [subtyping]: https://typing.python.org/en/latest/spec/concepts.html#subtype-supertype-and-type-equivalence diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index d44e8450adec4..b488938752533 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -1069,9 +1069,15 @@ impl<'db> Constraint<'db> { _ => {} } - // If `lower β‰° upper`, then the constraint cannot be satisfied, since there is no type that - // is both greater than `lower`, and less than `upper`. - if !lower.is_constraint_set_assignable_to(db, upper) { + // If `lower β‰° upper` for every possible assignment of typevars, then the constraint cannot + // be satisfied, since there is no type that is both greater than `lower`, and less than + // `upper`. We use an existential check here ("is there *some* assignment where + // `lower ≀ upper`?") rather than a universal check, because the bounds may mention + // typevars β€” e.g., `Sequence[int] ≀ A ≀ Sequence[T]` is satisfiable when `int ≀ T`. + if lower + .when_constraint_set_assignable_to(db, upper, builder, InferableTypeVars::None) + .is_never_satisfied(db) + { return ALWAYS_FALSE; } @@ -1264,9 +1270,16 @@ impl ConstraintId { let upper = IntersectionType::from_two_elements(db, self_constraint.upper, other_constraint.upper); - // If `lower β‰° upper`, then the intersection is empty, since there is no type that is both - // greater than `lower`, and less than `upper`. - if !lower.is_constraint_set_assignable_to(db, upper) { + // If `lower β‰° upper` for every possible assignment of typevars, then the intersection is + // empty, since there is no type that is both greater than `lower`, and less than `upper`. + // We use an existential check here ("is there *some* assignment where `lower ≀ upper`?") + // rather than a universal check ("is `lower ≀ upper` for *all* assignments?"), because the + // bounds may mention typevars β€” e.g., `Sequence[int] ≀ A ≀ Sequence[T]` is satisfiable + // when `int ≀ T`, even though it's not universally true for all `T`. + if lower + .when_constraint_set_assignable_to(db, upper, builder, InferableTypeVars::None) + .is_never_satisfied(db) + { return IntersectionResult::Disjoint; } @@ -1524,6 +1537,50 @@ impl NodeId { } } + /// Checks whether this BDD represents a single conjunction (of an arbitrary number of + /// positive or negative constraints). + fn is_single_conjunction(self, builder: &ConstraintSetBuilder<'_>) -> bool { + // A BDD can be viewed as an encoding of the formula's DNF representation (OR of ANDs). + // Each path from the root node to the `always` terminals represents one of the disjoints. + // The constraints that we encounter on the path represent the conjoints. That means that a + // BDD can only represent a single conjunction if there is precisely one path from the root + // node to the `always` terminal. + // + // We can take advantage of quasi-reduction. We never create an interior node with both + // outgoing edges leading to `never`; those are collapsed to `never`. That means that if we + // ever encounter a node with both outgoing edges pointing to something other than `never`, + // that node must have at least two paths to the `always` terminal. + let mut current = self.node(); + loop { + match current { + Node::AlwaysTrue => return true, + Node::AlwaysFalse => return false, + Node::Interior(interior) => { + let data = builder.interior_node_data(interior.node()); + + // If both if_true and if_false point to non-never, there are multiple paths to + // `always`, so this cannot be a simple conjunction. + if data.if_true != ALWAYS_FALSE && data.if_false != ALWAYS_FALSE { + return false; + } + + // The uncertain branch must also be never for a simple conjunction, since it + // contributes to all paths. + if data.if_uncertain != ALWAYS_FALSE { + return false; + } + + // Follow the non-never branch. + current = if data.if_true != ALWAYS_FALSE { + data.if_true.node() + } else { + data.if_false.node() + }; + } + } + } + } + fn for_each_path<'db>( self, db: &'db dyn Db, @@ -4193,58 +4250,112 @@ impl SequentMap { return; } - // If the lower or upper bound of this constraint is a typevar, we can propagate the - // constraint: + // Given a constraint `L ≀ T ≀ U`, `L ≀ U` must also hold. If those bounds contain other + // typevars, we can infer additional constraints. This is easiest to see when the bounds + // _are_ typevars: // // 1. `(S ≀ T ≀ U) β†’ (S ≀ U)` // 2. `(S ≀ T ≀ Ο„) β†’ (S ≀ Ο„)` // 3. `(Ο„ ≀ T ≀ U) β†’ (Ο„ ≀ U)` // - // Technically, (1) also allows `(S = T) β†’ (S = S)`, but the rhs of that is vacuously true, - // so we don't add a sequent for that case. + // but it also holds when the bounds _contain_ typevars: + // + // 4. `(Covariant[S] ≀ T ≀ Covariant[U]) β†’ (S ≀ U)` + // `(Covariant[S] ≀ T ≀ Covariant[Ο„]) β†’ (S ≀ Ο„)` + // `(Covariant[Ο„] ≀ T ≀ Covariant[U]) β†’ (Ο„ ≀ U)` + // + // 5. `(Contravariant[S] ≀ T ≀ Contravariant[U]) β†’ (U ≀ S)` + // `(Contravariant[S] ≀ T ≀ Contravariant[Ο„]) β†’ (Ο„ ≀ S)` + // `(Contravariant[Ο„] ≀ T ≀ Contravariant[U]) β†’ (U ≀ Ο„)` + // + // 6. `(Invariant[S] ≀ T ≀ Invariant[U]) β†’ (S = U)` + // `(Invariant[S] ≀ T ≀ Invariant[Ο„]) β†’ (S = Ο„)` + // `(Invariant[Ο„] ≀ T ≀ Invariant[U]) β†’ (Ο„ = U)` + // + // and whenever the bounds are assignable, even if they don't mention exactly the same + // types: + // + // class Sub(Covariant[int]): ... + // + // 7. `(Covariant[S] ≀ T ≀ Sub) β†’ (S ≀ int)` + // `(Sub ≀ T ≀ Covariant[U]) β†’ (int ≀ U)` + // + // To handle all of these cases, we perform a constraint set assignability check to see + // when `L ≀ U`. This gives us a constraint set, which should be the rhs of the sequent + // implication. (That is, this check directly encodes `(L ≀ T ≀ U) β†’ (L ≀ U)` as an + // implication.) - let post_constraint = match (lower, upper) { - // Case 1 - (Type::TypeVar(lower_typevar), Type::TypeVar(upper_typevar)) => { - if lower_typevar.is_same_typevar_as(db, upper_typevar) { - return; - } + // Skip trivial cases where the assignability check won't produce useful results. + if lower.is_never() || upper.is_object() { + return; + } - // We always want to propagate `lower ≀ upper`, but we must do so using a - // canonical top-level typevar ordering. - // - // Example: if we learn `(A ≀ [T] ≀ B)`, this single-constraint propagation step - // should infer `A ≀ B`. Depending on ordering, we might need to encode that as - // either `(Never ≀ [A] ≀ B)` or `(A ≀ [B] ≀ object)`. Both render as `A ≀ B`, - // but they constrain different typevars and must be created in the orientation - // allowed by `can_be_bound_for`. - if upper_typevar.can_be_bound_for(db, builder, lower_typevar) { - ConstraintId::new(db, builder, lower_typevar, Type::Never, upper) - } else { - ConstraintId::new( - db, - builder, - upper_typevar, - Type::TypeVar(lower_typevar), - Type::object(), - ) - } - } + let when = + lower.when_constraint_set_assignable_to(db, upper, builder, InferableTypeVars::None); - // Case 2 - (Type::TypeVar(lower_typevar), _) => { - ConstraintId::new(db, builder, lower_typevar, Type::Never, upper) - } + // If L is _never_ assignable to U, this constraint would violate transitivity, and should + // never have been added. + debug_assert!(!when.is_never_satisfied(db)); - // Case 3 - (_, Type::TypeVar(upper_typevar)) => { - ConstraintId::new(db, builder, upper_typevar, lower, Type::object()) - } + // Fast path: If L is trivially always assignable to U, there are no derived constraints + // that we can infer. (This would be handled correctly by the logic below, but this is a + // useful early return.) + if when.node == ALWAYS_TRUE { + return; + } - _ => return, - }; + // Technically, we've just calculated a _constraint set_ as the rhs of this implication. + // Unfortunately, our sequent map can currently only store implications where the rhs is a + // single constraint. + // + // If the constraint set that we get represents a single conjunction, we can still shoehorn + // it into this shape, since we can "break apart" a conjunction on the rhs of an + // implication: + // + // a β†’ b ∧ c ∧ d + // + // becomes + // + // a β†’ b + // a β†’ c + // a β†’ d + // + // That takes care of breaking apart the rhs conjunction: we can add each positive + // constraint as a separate single_implication. + // + // We can also handle _negative_ constraints, because those turn into impossibilities: + // + // a β†’ Β¬b + // + // becomes + // + // a ∧ b β†’ false + // + // TODO: This should handle the most common cases. In the future, we could handle arbitrary + // rhs constraint sets by moving this logic into PathAssignments::walk_path, and performing + // it once for _every_ rootβ†’always path in the BDD. (That would require resetting the + // PathAssignments state for each of those paths, which is why the logic would have to + // move.) + let mut node = when.node; + if !node.is_single_conjunction(builder) { + return; + } - self.add_single_implication(db, builder, constraint, post_constraint); + loop { + match node.node() { + Node::AlwaysTrue | Node::AlwaysFalse => break, + Node::Interior(interior) => { + let interior = builder.interior_node_data(interior.node()); + if interior.if_true != ALWAYS_FALSE { + self.add_single_implication(db, builder, constraint, interior.constraint); + node = interior.if_true; + } else { + self.add_pair_impossibility(db, builder, constraint, interior.constraint); + node = interior.if_false; + } + } + } + } } fn add_sequents_for_pair<'db>( From 50a50028782ce71e56bd578d552e0634faa6c095 Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Thu, 19 Mar 2026 17:49:33 -0400 Subject: [PATCH 07/22] update plan with half bounds --- PLAN.md | 193 +++++++++++++++++- .../type_properties/implies_subtype_of.md | 44 ++++ 2 files changed, 229 insertions(+), 8 deletions(-) diff --git a/PLAN.md b/PLAN.md index 06a6b2d75e14a..967439d3cc33e 100644 --- a/PLAN.md +++ b/PLAN.md @@ -432,16 +432,32 @@ Run the full test suite to check for regressions. ### Phase 5: Handle the same-typevar case with recursive nested references -#### Step 5.1 ⬜ β€” Extend `add_sequents_for_pair` for same-typevar with recursive nesting +#### Step 5.1 βœ… β€” Investigate same-typevar recursive nesting and concrete bound substitution -The dispatch in `add_sequents_for_pair` currently falls through to -`add_concrete_sequents` when both constraints are on the same typevar and -neither has a typevar as a direct bound. But a constraint like `T ≀ Sequence[T]` -(recursive bound) would have `T` nested in its upper bound while also directly -constraining `T`. Check whether this case actually arises in practice, and if -so, whether it needs special handling. +**Recursive nesting** (`T ≀ Covariant[T]`): Investigated and confirmed that +trivial cases (lower = Never) are handled correctly. Non-trivial cases +(`Covariant[int] ≀ T ≀ Covariant[T]`) are a pre-existing limitation β€” the +CSA decomposition derives `int ≀ T` but the pair intersection between the +original and derived constraints is flagged as disjoint, which is actually +mathematically correct (the combined constraint is unsatisfiable for most +user-defined classes). Does not arise in practice. -This is lower priority and may not need to be addressed initially. +**Concrete bound substitution** (newly identified gap): The forward direction +(Phase 2/3) substitutes B's concrete bounds into C's bounds that contain B. +The reverse direction β€” substituting B (the typevar) into C's bounds that +contain B's concrete bound β€” is not yet implemented. This is analogous to the +existing "pivot" cases in `add_mutual_sequents_for_different_typevars` but +generalized to work inside generic types. + +Examples (covariant case): + +- `(Covariant[BU] ≀ C) ∧ (B ≀ BU) β†’ (Covariant[B] ≀ C)` +- `(C ≀ Covariant[BL]) ∧ (BL ≀ B) β†’ (C ≀ Covariant[B])` + +These create cross-typevar links that are weaker than the originals but useful +for downstream inference (e.g., after `exists_one`). Test cases are written +in the mdtest file with TODO markers. Implementation deferred to a future +phase. ### Phase 6: Clean up @@ -455,6 +471,167 @@ working. Update any related comments. Final pre-commit checks. We are in a jj worktree, so use `jpk` (with no arguments) as a standin for `prek`. +### Phase 7: Typevar bound substitution into nested generic types + +Phases 2–3 implemented the *forward* direction of nested typevar propagation: +when B (a typevar) appears nested inside C's bound, substitute B's concrete +bounds for B. This phase implements a restricted *reverse* direction: when one +of B's bounds is a *bare typevar* that appears nested inside C's bound, +substitute B (the typevar) for that bound. + +This generalizes the existing top-level "pivot" cases in +`add_mutual_sequents_for_different_typevars` to work inside generic types. +The pivot cases handle: + +```text +(CL ≀ C ≀ pivot) ∧ (pivot ≀ B ≀ BU) β†’ (CL ≀ C ≀ B) +``` + +The new cases handle the same logic when the pivot appears inside a generic: + +```text +(CL ≀ C ≀ G[pivot]) ∧ (pivot ≀ B ≀ BU) β†’ (CL ≀ C ≀ G[B]) +``` + +The derived constraint is *weaker* than the original (since `B ≀ BU` means +`G[B] ≀ G[BU]` in a covariant position, so we're relaxing C's bound). But it +introduces a cross-typevar link between B and C that is useful for downstream +inference, especially after `exists_one` removes one of the typevars. + +#### Scope restriction: bare typevar bounds only + +The fully general version of this feature would handle arbitrary concrete +types nested in C's bounds β€” e.g., `Covariant[int]` where `int` matches B's +upper bound. However, detecting an arbitrary concrete type inside a nested +position requires different machinery (pattern matching on generic alias +structure, or a CSA-based approach). + +When B's bound is a bare typevar, we can reuse `variance_of` for detection, +since `variance_of` already finds typevars nested inside types. This makes +the implementation a natural extension of `add_nested_typevar_sequents`. + +For example, given `(G[S] ≀ C) ∧ (S ≀ B)` where S is a typevar: + +- `variance_of(G[S], S)` finds S in the covariant position +- We know `S ≀ B`, so `G[S] ≀ G[B]` (covariance) +- Therefore `G[S] ≀ C` implies `G[B] ≀ C` (weakening the lower bound) +- Emit pair implication: `(G[S] ≀ C) ∧ (S ≀ B) β†’ (G[B] ≀ C)` + +A TODO comment should be added noting that a future extension could handle +the case where B's bound is an arbitrary type (not just a bare typevar). + +#### Where this fits + +The existing `add_nested_typevar_sequents` handles the case where `B` (the +constraint's typevar) appears in C's bound β€” it substitutes B's concrete +bounds for B. This new logic handles the complementary case: a *different* +typevar (one of B's bounds) appears in C's bound β€” we substitute B for that +typevar, creating a weaker but useful cross-typevar constraint. + +Both are called from `add_sequents_for_pair` for different-typevar pairs. +The new logic can live in `add_nested_typevar_sequents` itself, or in a new +method called alongside it. + +#### Variance rules + +The rules mirror `add_nested_typevar_sequents` but in the *weakening* +direction rather than the *tightening* direction. We substitute B for the +found typevar only when the result weakens (relaxes) the bound. + +Given constraints `(l_C ≀ C ≀ u_C)` and `(l_B ≀ B ≀ u_B)`, and a typevar S +that is one of B's bounds: + +**S = u_B (B's upper bound is a bare typevar S) and S appears in u_C:** + +We know `B ≀ S`. By variance: + +- Covariant: `G[B] ≀ G[S]`, so `u_C[B] ≀ u_C[S]` β€” substituting B *weakens* + the upper bound β†’ emit `C ≀ u_C[S := B]` +- Contravariant: `G[S] ≀ G[B]`, so `u_C[B] β‰₯ u_C[S]` β€” substituting B + *tightens* β†’ no useful derivation +- Invariant: only if `l_B = u_B` (equality on B), then `B = S` and the + substitution is exact + +**S = l_B (B's lower bound is a bare typevar S) and S appears in l_C:** + +We know `S ≀ B`. By variance: + +- Covariant: `G[S] ≀ G[B]`, so `l_C[B] β‰₯ l_C[S]` β€” substituting B *weakens* + the lower bound β†’ emit `l_C[S := B] ≀ C` +- Contravariant: `G[B] ≀ G[S]`, so `l_C[B] ≀ l_C[S]` β€” substituting B + *tightens* β†’ no useful derivation +- Invariant: only if `l_B = u_B` (equality on B) + +**S = l_B and S appears in u_C:** + +We know `S ≀ B`. By variance: + +- Contravariant: `G[B] ≀ G[S]`, so `u_C[B] ≀ u_C[S]` β€” substituting B + *weakens* the upper bound β†’ emit `C ≀ u_C[S := B]` +- Covariant: tightens β†’ no useful derivation +- Invariant: only if `l_B = u_B` + +**S = u_B and S appears in l_C:** + +We know `B ≀ S`. By variance: + +- Contravariant: `G[S] ≀ G[B]`, so `l_C[B] β‰₯ l_C[S]` β€” substituting B + *weakens* the lower bound β†’ emit `l_C[S := B] ≀ C` +- Covariant: tightens β†’ no useful derivation +- Invariant: only if `l_B = u_B` + +#### Steps + +##### Step 7.1 ⬜ β€” Add tests for bare typevar bound substitution (red) + +Update the tests in the "Concrete bound substitution" section to use bare +typevar bounds. The existing test structure uses concrete types like `int`; +change them so B's bound is a typevar S that also appears in C's bound. + +For example: + +- `(Covariant[S] ≀ C) ∧ (S ≀ B)` should imply `Covariant[B] ≀ C` +- `(C ≀ Covariant[S]) ∧ (S ≀ B)` should imply `C ≀ Covariant[B]` +- Contravariant and invariant variants + +Keep the existing concrete-bound tests (with `int`) as TODO-commented +assertions documenting the future extension. + +Verify the tests fail before proceeding. + +##### Step 7.2 ⬜ β€” Add the typevar bound substitution logic + +Extend `add_nested_typevar_sequents` (or add a companion method called +alongside it). For each pair of constraints (C, B) on different typevars, +and for each of B's bounds that is a bare typevar S: + +1. Use `variance_of(u_C, S)` / `variance_of(l_C, S)` to check if S appears + in C's upper/lower bound and determine the variance. +1. Based on the variance and which bound of B is S, decide whether the + substitution weakens (valid) or tightens (skip). See the variance rules + above. +1. If valid, use `apply_type_mapping` with `ApplySpecialization::Single(S, B)` + to construct the new bound, and emit a pair implication. + +Skip if S is the same typevar as C (handled elsewhere) or if S equals B +(no-op substitution). + +##### Step 7.3 ⬜ β€” Run the tests (green) + +Run the test suite and verify the new tests pass. + +##### Step 7.4 ⬜ β€” Add TODO for arbitrary-type extension + +Add a TODO comment in the code noting that the current implementation only +handles the case where B's bound is a bare typevar. A future extension could +handle arbitrary types by pattern-matching on generic alias structure (checking +each type argument against B's bounds using `is_constraint_set_assignable_to`). + +##### Step 7.5 ⬜ β€” Run the full test suite and jpk + +Run the full `ty_python_semantic` test suite to check for regressions, then +run `/home/dcreager/bin/jpk` for pre-commit checks. + ## Open questions 1. **Performance**: The `variance_of` computation walks the type tree diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md b/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md index db3021076a6ba..e37aec82c3ba5 100644 --- a/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md +++ b/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md @@ -758,6 +758,50 @@ def contravariant_of_covariant[U, T](): static_assert(not constraints.implies_subtype_of(U, Contravariant[Covariant[str]])) ``` +### Concrete bound substitution into nested generic types + +When a constraint on C has a concrete type nested in a generic bound, and that concrete type matches +another typevar B's bound, we can substitute B (the typevar) for the concrete type, creating a +cross-typevar relationship. This is a weakening (the derived constraint is less restrictive), but it +introduces a useful link between the two typevars. + +For example, `(Covariant[int] ≀ C) ∧ (B ≀ int)` should derive `Covariant[B] ≀ C`, because `B ≀ int` +and covariance give `Covariant[B] ≀ Covariant[int] ≀ C`. + +```py +from typing import Never +from ty_extensions import ConstraintSet, static_assert + +class Covariant[T]: + def get(self) -> T: + raise ValueError + +def upper_bound_into_lower[B, C](): + # (Covariant[int] ≀ C) ∧ (B ≀ int) β†’ (Covariant[B] ≀ C) + # B ≀ int, so Covariant[B] ≀ Covariant[int] ≀ C. + constraints = ConstraintSet.range(Covariant[int], C, object) & ConstraintSet.range(Never, B, int) + # TODO: not yet implemented + # static_assert(constraints.implies_subtype_of(Covariant[B], C)) + +def lower_bound_into_upper[B, C](): + # (C ≀ Covariant[int]) ∧ (int ≀ B) β†’ (C ≀ Covariant[B]) + # int ≀ B, so Covariant[int] ≀ Covariant[B], and C ≀ Covariant[int] ≀ Covariant[B]. + constraints = ConstraintSet.range(Never, C, Covariant[int]) & ConstraintSet.range(int, B, object) + # TODO: not yet implemented + # static_assert(constraints.implies_subtype_of(C, Covariant[B])) + +# Repeat with reversed typevar ordering. +def upper_bound_into_lower[C, B](): + constraints = ConstraintSet.range(Covariant[int], C, object) & ConstraintSet.range(Never, B, int) + # TODO: not yet implemented + # static_assert(constraints.implies_subtype_of(Covariant[B], C)) + +def lower_bound_into_upper[C, B](): + constraints = ConstraintSet.range(Never, C, Covariant[int]) & ConstraintSet.range(int, B, object) + # TODO: not yet implemented + # static_assert(constraints.implies_subtype_of(C, Covariant[B])) +``` + ### Reverse decomposition: bounds on a typevar can be decomposed via variance When a constraint has lower and upper bounds that are parameterizations of the same generic type, we From 0a0d7afef7ae8179475f0859d2fa4bfd077d9da3 Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Thu, 19 Mar 2026 18:54:51 -0400 Subject: [PATCH 08/22] more consistent loaded ordering --- .../src/types/constraints.rs | 62 ++++++++++++------- 1 file changed, 39 insertions(+), 23 deletions(-) diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index b488938752533..7c58dcf0a4e7b 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -745,9 +745,9 @@ impl<'db> ConstraintSetBuilder<'db> { // `OwnedConstraintSet` is only used in mdtests, and not in type inference of user code. fn rebuild_node<'db>( - db: &'db dyn Db, builder: &ConstraintSetBuilder<'db>, other: &OwnedConstraintSet<'db>, + constraints: &IndexVec, cache: &mut FxHashMap, old_node: NodeId, ) -> NodeId { @@ -758,36 +758,52 @@ impl<'db> ConstraintSetBuilder<'db> { return *remapped; } - let old_interior = other.nodes[old_node]; - let old_constraint = other.constraints[old_interior.constraint]; - let condition = Constraint::new_node( - db, - builder, - old_constraint.typevar, - old_constraint.lower, - old_constraint.upper, - ); - // Absorb the uncertain branch into both true and false branches. This collapses // the TDD back to a binary structure, which is correct but loses the TDD laziness for // unions. This is acceptable since `load` is only used for `OwnedConstraintSet` in // mdtests. // TODO: A 4-arg `ite_uncertain` could preserve TDD structure if `load` ever becomes // performance-sensitive. - let if_true = rebuild_node(db, builder, other, cache, old_interior.if_true); - let if_uncertain = rebuild_node(db, builder, other, cache, old_interior.if_uncertain); - let if_false = rebuild_node(db, builder, other, cache, old_interior.if_false); + let old_interior = other.nodes[old_node]; + let if_true = rebuild_node(builder, other, constraints, cache, old_interior.if_true); + let if_uncertain = rebuild_node( + builder, + other, + constraints, + cache, + old_interior.if_uncertain, + ); + let if_false = rebuild_node(builder, other, constraints, cache, old_interior.if_false); let if_true_merged = if_true.or(builder, if_uncertain); let if_false_merged = if_false.or(builder, if_uncertain); + let condition = constraints[old_interior.constraint]; let remapped = condition.ite(builder, if_true_merged, if_false_merged); cache.insert(old_node, remapped); remapped } + // Load all of the constraints into the this builder first, to maximize the chance that the + // constraints and typevars will appear in the same order. (This is important because many + // of our mdtests try to force a particular ordering, to test that our algorithms are all + // order-independent.) + let constraints = other + .constraints + .iter() + .map(|old_constraint| { + Constraint::new_node( + db, + self, + old_constraint.typevar, + old_constraint.lower, + old_constraint.upper, + ) + }) + .collect(); + // Maps NodeIds in the OwnedConstraintSet to the corresponding NodeIds in this builder. let mut cache = FxHashMap::default(); - let node = rebuild_node(db, self, other, &mut cache, other.node); + let node = rebuild_node(self, other, &constraints, &mut cache, other.node); ConstraintSet::from_node(self, node) } @@ -5854,16 +5870,16 @@ mod tests { &builder, loaded, indoc! {r#" - <0> (T = int) 1/1 - ┑━₁ <1> (U = str) 1/1 + <0> (U = str) 1/1 + ┑━₁ <1> (T = int) 1/1 β”‚ ┑━₁ never - β”‚ β”œβ”€? never - β”‚ └─₀ always - β”œβ”€? <2> (U = str) 1/1 - β”‚ ┑━₁ always - β”‚ β”œβ”€? never + β”‚ β”œβ”€? always β”‚ └─₀ never - └─₀ never + β”œβ”€? never + └─₀ <2> (T = int) 1/1 + ┑━₁ always + β”œβ”€? never + └─₀ never "#}, ); } From 104570f3ff0654aef7911e8810a057302ffa46e3 Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Thu, 19 Mar 2026 18:19:20 -0400 Subject: [PATCH 09/22] add weakening sequents --- PLAN.md | 82 +++++----- .../type_properties/implies_subtype_of.md | 105 ++++++++++--- .../src/types/constraints.rs | 143 +++++++++++++++++- 3 files changed, 258 insertions(+), 72 deletions(-) diff --git a/PLAN.md b/PLAN.md index 967439d3cc33e..4e5e64ec4b19a 100644 --- a/PLAN.md +++ b/PLAN.md @@ -580,57 +580,51 @@ We know `B ≀ S`. By variance: - Covariant: tightens β†’ no useful derivation - Invariant: only if `l_B = u_B` -#### Steps - -##### Step 7.1 ⬜ β€” Add tests for bare typevar bound substitution (red) - -Update the tests in the "Concrete bound substitution" section to use bare -typevar bounds. The existing test structure uses concrete types like `int`; -change them so B's bound is a typevar S that also appears in C's bound. - -For example: - -- `(Covariant[S] ≀ C) ∧ (S ≀ B)` should imply `Covariant[B] ≀ C` -- `(C ≀ Covariant[S]) ∧ (S ≀ B)` should imply `C ≀ Covariant[B]` -- Contravariant and invariant variants - -Keep the existing concrete-bound tests (with `int`) as TODO-commented -assertions documenting the future extension. +#### Implementation + +Added a new method `try_reverse_nested_typevar_sequents` in the sequent map, +called from `add_nested_typevar_sequents` alongside the existing forward +direction. For each constraint pair (B, C) on different typevars: + +1. Extract B's bare typevar bounds (upper/lower bounds that are `Type::TypeVar`). +1. For each such typevar S, use `variance_of` to check if S appears nested + in C's upper/lower bounds. +1. Based on variance and which bound S is (upper vs lower), determine whether + substituting B for S *weakens* (relaxes) the bound β€” only emit in that case. +1. Construct the substituted bound via `ApplySpecialization::Single(S, B)` and + emit a pair implication. + +The variance rules for weakening: + +- **Upper bound of C** (want to make it *larger* to weaken): + - Covariant + S is B's lower bound (S ≀ B β†’ G[S] ≀ G[B]): emit + - Contravariant + S is B's upper bound (B ≀ S β†’ G[S] ≀ G[B] in contra): emit +- **Lower bound of C** (want to make it *smaller* to weaken): + - Covariant + S is B's upper bound (B ≀ S β†’ G[B] ≀ G[S]): emit + - Contravariant + S is B's lower bound (S ≀ B β†’ G[B] ≀ G[S] in contra): emit +- **Invariant**: only when B is an equality constraint (l_B = u_B). + +This was needed because the canonical constraint encoding depends on typevar +ordering in the builder: `B ≀ S` may be encoded as `(Never ≀ B ≀ S)` on B +(when S is earlier) or `(B ≀ S ≀ object)` on S (when B is earlier). The +existing forward direction in `add_nested_typevar_sequents` only handles the +second encoding. The new reverse direction handles both. -Verify the tests fail before proceeding. - -##### Step 7.2 ⬜ β€” Add the typevar bound substitution logic - -Extend `add_nested_typevar_sequents` (or add a companion method called -alongside it). For each pair of constraints (C, B) on different typevars, -and for each of B's bounds that is a bare typevar S: - -1. Use `variance_of(u_C, S)` / `variance_of(l_C, S)` to check if S appears - in C's upper/lower bound and determine the variance. -1. Based on the variance and which bound of B is S, decide whether the - substitution weakens (valid) or tightens (skip). See the variance rules - above. -1. If valid, use `apply_type_mapping` with `ApplySpecialization::Single(S, B)` - to construct the new bound, and emit a pair implication. - -Skip if S is the same typevar as C (handled elsewhere) or if S equals B -(no-op substitution). +#### Steps -##### Step 7.3 ⬜ β€” Run the tests (green) +##### Step 7.1 βœ… β€” Add tests for bare typevar bound substitution (red) -Run the test suite and verify the new tests pass. +Added tests covering covariant and contravariant cases, both typevar +orderings. All 8 assertions initially failed. -##### Step 7.4 ⬜ β€” Add TODO for arbitrary-type extension +##### Step 7.2 βœ… β€” Implement `try_reverse_nested_typevar_sequents` (green) -Add a TODO comment in the code noting that the current implementation only -handles the case where B's bound is a bare typevar. A future extension could -handle arbitrary types by pattern-matching on generic alias structure (checking -each type argument against B's bounds using `is_constraint_set_assignable_to`). +Added the reverse direction logic. All 8 assertions now pass. -##### Step 7.5 ⬜ β€” Run the full test suite and jpk +##### Step 7.3 βœ… β€” Run the full test suite and jpk -Run the full `ty_python_semantic` test suite to check for regressions, then -run `/home/dcreager/bin/jpk` for pre-commit checks. +Updated the `tdd_owned_round_trip` test to match the new `load` ordering +behavior. Full test suite (513 tests) passes. jpk passes. ## Open questions diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md b/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md index e37aec82c3ba5..1479390fd1b29 100644 --- a/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md +++ b/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md @@ -758,15 +758,83 @@ def contravariant_of_covariant[U, T](): static_assert(not constraints.implies_subtype_of(U, Contravariant[Covariant[str]])) ``` -### Concrete bound substitution into nested generic types +### Typevar bound substitution into nested generic types -When a constraint on C has a concrete type nested in a generic bound, and that concrete type matches -another typevar B's bound, we can substitute B (the typevar) for the concrete type, creating a -cross-typevar relationship. This is a weakening (the derived constraint is less restrictive), but it -introduces a useful link between the two typevars. +When a typevar B has a bare typevar S as one of its bounds, and S appears nested inside another +constraint's bound, we can substitute B for S to create a cross-typevar link. The derived constraint +is weaker (less restrictive), but introduces a useful relationship between the typevars. -For example, `(Covariant[int] ≀ C) ∧ (B ≀ int)` should derive `Covariant[B] ≀ C`, because `B ≀ int` -and covariance give `Covariant[B] ≀ Covariant[int] ≀ C`. +For example, `(Covariant[S] ≀ C) ∧ (S ≀ B)` should imply `Covariant[B] ≀ C`: we are given that +`S ≀ B`, covariance tells us that `Covariant[S] ≀ Covariant[B]`, and transitivity gives +`Covariant[B] ≀ C`. (We can infer similar weakened constraints for contravariant and invariant +typevars.) + +```py +from typing import Never +from ty_extensions import ConstraintSet, static_assert + +class Covariant[T]: + def get(self) -> T: + raise ValueError + +class Contravariant[T]: + def set(self, value: T): + pass + +class Invariant[T]: + def get(self) -> T: + raise ValueError + + def set(self, value: T): + pass + +def covariant_upper_bound_into_lower[S, B, C](): + # (Covariant[S] ≀ C) ∧ (B ≀ S) β†’ (Covariant[B] ≀ C) + # B ≀ S, so Covariant[B] ≀ Covariant[S], and Covariant[S] ≀ C gives Covariant[B] ≀ C. + constraints = ConstraintSet.range(Covariant[S], C, object) & ConstraintSet.range(Never, B, S) + static_assert(constraints.implies_subtype_of(Covariant[B], C)) + +def covariant_lower_bound_into_upper[S, B, C](): + # (C ≀ Covariant[S]) ∧ (S ≀ B) β†’ (C ≀ Covariant[B]) + # S ≀ B, so Covariant[S] ≀ Covariant[B], and C ≀ Covariant[S] ≀ Covariant[B]. + constraints = ConstraintSet.range(Never, C, Covariant[S]) & ConstraintSet.range(S, B, object) + static_assert(constraints.implies_subtype_of(C, Covariant[B])) + +def contravariant_upper_bound_into_lower[S, B, C](): + # (Contravariant[S] ≀ C) ∧ (S ≀ B) β†’ (Contravariant[B] ≀ C) + # S ≀ B gives Contravariant[B] ≀ Contravariant[S], so Contravariant[B] ≀ Contravariant[S] ≀ C. + constraints = ConstraintSet.range(Contravariant[S], C, object) & ConstraintSet.range(S, B, object) + static_assert(constraints.implies_subtype_of(Contravariant[B], C)) + +def contravariant_lower_bound_into_upper[S, B, C](): + # (C ≀ Contravariant[S]) ∧ (B ≀ S) β†’ (C ≀ Contravariant[B]) + # B ≀ S gives Contravariant[S] ≀ Contravariant[B], so C ≀ Contravariant[S] ≀ Contravariant[B]. + constraints = ConstraintSet.range(Never, C, Contravariant[S]) & ConstraintSet.range(Never, B, S) + static_assert(constraints.implies_subtype_of(C, Contravariant[B])) + +# Repeat with reversed typevar ordering. +def covariant_upper_bound_into_lower[C, B, S](): + constraints = ConstraintSet.range(Covariant[S], C, object) & ConstraintSet.range(Never, B, S) + static_assert(constraints.implies_subtype_of(Covariant[B], C)) + +def covariant_lower_bound_into_upper[C, B, S](): + constraints = ConstraintSet.range(Never, C, Covariant[S]) & ConstraintSet.range(S, B, object) + static_assert(constraints.implies_subtype_of(C, Covariant[B])) + +def contravariant_upper_bound_into_lower[C, B, S](): + constraints = ConstraintSet.range(Contravariant[S], C, object) & ConstraintSet.range(S, B, object) + static_assert(constraints.implies_subtype_of(Contravariant[B], C)) + +def contravariant_lower_bound_into_upper[C, B, S](): + constraints = ConstraintSet.range(Never, C, Contravariant[S]) & ConstraintSet.range(Never, B, S) + static_assert(constraints.implies_subtype_of(C, Contravariant[B])) +``` + +### Concrete bound substitution into nested generic types (future extension) + +When B's bound _contains_ a typevar (but is not a bare typevar), the same logic as above applies. + +TODO: This is not implemented yet, since it requires different detection machinery. ```py from typing import Never @@ -778,28 +846,17 @@ class Covariant[T]: def upper_bound_into_lower[B, C](): # (Covariant[int] ≀ C) ∧ (B ≀ int) β†’ (Covariant[B] ≀ C) - # B ≀ int, so Covariant[B] ≀ Covariant[int] ≀ C. constraints = ConstraintSet.range(Covariant[int], C, object) & ConstraintSet.range(Never, B, int) - # TODO: not yet implemented - # static_assert(constraints.implies_subtype_of(Covariant[B], C)) + # TODO: no error + # error: [static-assert-error] + static_assert(constraints.implies_subtype_of(Covariant[B], C)) def lower_bound_into_upper[B, C](): # (C ≀ Covariant[int]) ∧ (int ≀ B) β†’ (C ≀ Covariant[B]) - # int ≀ B, so Covariant[int] ≀ Covariant[B], and C ≀ Covariant[int] ≀ Covariant[B]. constraints = ConstraintSet.range(Never, C, Covariant[int]) & ConstraintSet.range(int, B, object) - # TODO: not yet implemented - # static_assert(constraints.implies_subtype_of(C, Covariant[B])) - -# Repeat with reversed typevar ordering. -def upper_bound_into_lower[C, B](): - constraints = ConstraintSet.range(Covariant[int], C, object) & ConstraintSet.range(Never, B, int) - # TODO: not yet implemented - # static_assert(constraints.implies_subtype_of(Covariant[B], C)) - -def lower_bound_into_upper[C, B](): - constraints = ConstraintSet.range(Never, C, Covariant[int]) & ConstraintSet.range(int, B, object) - # TODO: not yet implemented - # static_assert(constraints.implies_subtype_of(C, Covariant[B])) + # TODO: no error + # error: [static-assert-error] + static_assert(constraints.implies_subtype_of(C, Covariant[B])) ``` ### Reverse decomposition: bounds on a typevar can be decomposed via variance diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index 7c58dcf0a4e7b..b08887a3a890f 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -4601,7 +4601,7 @@ impl SequentMap { left_constraint: ConstraintId, right_constraint: ConstraintId, ) { - let mut try_one_direction = + let mut try_tightening = |bound_constraint: ConstraintId, constrained_constraint: ConstraintId| { let bound_data = builder.constraint_data(bound_constraint); let bound_typevar = bound_data.typevar; @@ -4719,9 +4719,144 @@ impl SequentMap { } }; - // Try both directions: left's typevar might be nested in right's bounds, or vice versa. - try_one_direction(left_constraint, right_constraint); - try_one_direction(right_constraint, left_constraint); + try_tightening(left_constraint, right_constraint); + try_tightening(right_constraint, left_constraint); + + // Additionally, check if one constraint's bare typevar *bound* appears nested in the other + // constraint's bounds. This handles the "dual" direction: instead of substituting a + // typevar's concrete bounds into another constraint (tightening), we substitute the + // typevar itself for one of its bare typevar bounds (weakening), creating a cross-typevar + // link. + // + // For example, given `(Covariant[S] ≀ C) ∧ (Never ≀ B ≀ S)`, S is B's upper bound and + // appears covariantly in C's lower bound. Since `B ≀ S`, covariance tells us that + // `Covariant[B] ≀ Covariant[S]`. Transitivity then lets us derive `Covariant[B] ≀ C`. + // + // The derived constraint is weaker than the original, but it introduces a relationship + // between B and C that we need to remember and propagate if we ever existentially quantify + // away S. + // + // TODO: This only handles the case where the bound (in this case, S) is a bare typevar. A + // future extension could handle arbitrary types by pattern-matching on generic alias + // structure. + // + // This is defined as a separate closure because it iterates over the bound constraint's + // bare typevar bounds, which is a different axis than `try_tightening`'s check on the + // bound constraint's typevar. + let mut try_weakening = + |bound_constraint: ConstraintId, constrained_constraint: ConstraintId| { + let bound_data = builder.constraint_data(bound_constraint); + let bound_typevar = bound_data.typevar; + let constrained_data = builder.constraint_data(constrained_constraint); + let constrained_typevar = constrained_data.typevar; + + let mut try_one_bound = |bound: Type<'db>, is_upper_bound: bool| { + let Some(nested_typevar) = bound.as_typevar() else { + return; + }; + + // Skip if the nested typevar is the same as the constrained typevar β€” that + // case is handled by `add_mutual_sequents_for_different_typevars`. + if nested_typevar.is_same_typevar_as(db, constrained_typevar) + || nested_typevar.is_same_typevar_as(db, bound_typevar) + { + return; + } + + let replacement = Type::TypeVar(bound_typevar); + + // Check the constrained constraint's upper bound for nested occurrences of + // nested_typevar (S). We want to *weaken* (relax) the upper bound by making it + // larger: + // - Covariant + S is B's lower bound (S ≀ B): G[S] ≀ G[B] β†’ weaker. Emit. + // - Contravariant + S is B's upper bound (B ≀ S): G[S] ≀ G[B] β†’ weaker. Emit. + // - Other combinations tighten rather than weaken. Skip. + let should_weaken_upper = + match constrained_data.upper.variance_of(db, nested_typevar) { + TypeVarVariance::Bivariant => false, + _ if constrained_data.upper.is_type_var() => false, + TypeVarVariance::Covariant => !is_upper_bound, + TypeVarVariance::Contravariant => is_upper_bound, + TypeVarVariance::Invariant => { + bound_data.lower == bound_data.upper && !bound_data.lower.is_never() + } + }; + if should_weaken_upper { + let new_upper = constrained_data.upper.apply_type_mapping( + db, + &TypeMapping::ApplySpecialization(ApplySpecialization::Single( + nested_typevar, + replacement, + )), + TypeContext::default(), + ); + if new_upper != constrained_data.upper { + let post = ConstraintId::new( + db, + builder, + constrained_typevar, + constrained_data.lower, + new_upper, + ); + self.add_pair_implication( + db, + builder, + bound_constraint, + constrained_constraint, + post, + ); + } + } + + // Ditto for the lower bound. + let should_weaken_lower = + match constrained_data.lower.variance_of(db, nested_typevar) { + TypeVarVariance::Bivariant => false, + _ if constrained_data.lower.is_type_var() => false, + TypeVarVariance::Covariant => is_upper_bound, + TypeVarVariance::Contravariant => !is_upper_bound, + TypeVarVariance::Invariant => { + bound_data.lower == bound_data.upper && !bound_data.lower.is_never() + } + }; + if should_weaken_lower { + let new_lower = constrained_data.lower.apply_type_mapping( + db, + &TypeMapping::ApplySpecialization(ApplySpecialization::Single( + nested_typevar, + replacement, + )), + TypeContext::default(), + ); + if new_lower != constrained_data.lower { + let post = ConstraintId::new( + db, + builder, + constrained_typevar, + new_lower, + constrained_data.upper, + ); + self.add_pair_implication( + db, + builder, + bound_constraint, + constrained_constraint, + post, + ); + } + } + }; + + // For each bare typevar bound S of the bound constraint, check if S appears + // nested in the constrained constraint's bounds. If so, we can substitute B + // (the bound constraint's typevar) for S, producing a weaker but useful + // constraint. + try_one_bound(bound_data.upper, true); + try_one_bound(bound_data.lower, false); + }; + + try_weakening(left_constraint, right_constraint); + try_weakening(right_constraint, left_constraint); } fn add_mutual_sequents_for_same_typevars<'db>( From cc1fb7fd63f2d3b9138d14796e480cf73f9bd015 Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Thu, 19 Mar 2026 17:43:06 -0400 Subject: [PATCH 10/22] more tests --- .../mdtest/generics/pep695/functions.md | 94 +++++++++++++++++-- 1 file changed, 85 insertions(+), 9 deletions(-) diff --git a/crates/ty_python_semantic/resources/mdtest/generics/pep695/functions.md b/crates/ty_python_semantic/resources/mdtest/generics/pep695/functions.md index 956105c723d35..7040433ea8763 100644 --- a/crates/ty_python_semantic/resources/mdtest/generics/pep695/functions.md +++ b/crates/ty_python_semantic/resources/mdtest/generics/pep695/functions.md @@ -514,22 +514,98 @@ reveal_type(g(f("a"))) # revealed: tuple[Literal["a"], int] | None ## Passing generic functions to generic functions -```py +`functions.pyi`: + +```pyi from typing import Callable -def invoke[A, B](fn: Callable[[A], B], value: A) -> B: - return fn(value) +def invoke[A, B](fn: Callable[[A], B], value: A) -> B: ... +def identity[T](x: T) -> T: ... -def identity[T](x: T) -> T: - return x +class Covariant[T]: + def get(self) -> T: + raise NotImplementedError -def head[T](xs: list[T]) -> T: - return xs[0] +def head_covariant[T](xs: Covariant[T]) -> T: ... +def lift_covariant[T](xs: T) -> Covariant[T]: ... + +class Contravariant[T]: + def receive(self, input: T): ... + +def head_contravariant[T](xs: Contravariant[T]) -> T: ... +def lift_contravariant[T](xs: T) -> Contravariant[T]: ... + +class Invariant[T]: + mutable_attribute: T + +def head_invariant[T](xs: Invariant[T]) -> T: ... +def lift_invariant[T](xs: T) -> Invariant[T]: ... +``` + +A simple function that passes through its parameter type unchanged: + +`simple.py`: + +```py +from functions import invoke, identity reveal_type(invoke(identity, 1)) # revealed: Literal[1] +``` + +When the either the parameter or the return type is a generic alias referring to the typevar, we +should still be able to propagate the specializations through. This should work regardless of the +typevar's variance in the generic alias. + +TODO: This currently only works for the `lift` functions (TODO: and only currently for the covariant +case). For the `lift` functions, the parameter type is a bare typevar, resulting in us inferring a +type mapping of `A = int, B = Class[A]`. When specializing, we can substitute the mapping of `A` +into the mapping of `B`, giving the correct return type. + +For the `head` functions, the parameter type is a generic alias, resulting in us inferring a type +mapping of `A = Class[int], A = Class[B]`. At this point, the old solver is not able to unify the +two mappings for `A`, and we have no mapping for `B`. As a result, we infer `Unknown` for the return +type. + +As part of migrating to the new solver, we will generate a single constraint set combining all of +the facts that we learn while checking the arguments. And the constraint set implementation should +be able to unify the two assignments to `A`. -# TODO: this should be `Unknown | int` -reveal_type(invoke(head, [1, 2, 3])) # revealed: Unknown +`covariant.py`: + +```py +from functions import invoke, Covariant, head_covariant, lift_covariant + +# TODO: revealed: `int` +# revealed: Unknown +reveal_type(invoke(head_covariant, Covariant[int]())) +# revealed: Covariant[Literal[1]] +reveal_type(invoke(lift_covariant, 1)) +``` + +`contravariant.py`: + +```py +from functions import invoke, Contravariant, head_contravariant, lift_contravariant + +# TODO: revealed: `int` +# revealed: Unknown +reveal_type(invoke(head_contravariant, Contravariant[int]())) +# TODO: revealed: Contravariant[int] +# revealed: Unknown +reveal_type(invoke(lift_contravariant, 1)) +``` + +`invariant.py`: + +```py +from functions import invoke, Invariant, head_invariant, lift_invariant + +# TODO: revealed: `int` +# revealed: Unknown +reveal_type(invoke(head_invariant, Invariant[int]())) +# TODO: revealed: `Invariant[int]` +# revealed: Unknown +reveal_type(invoke(lift_invariant, 1)) ``` ## Protocols as TypeVar bounds From de900ec7c8f2a50d5b135f3272abb9889072fb1a Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Fri, 20 Mar 2026 10:05:59 -0400 Subject: [PATCH 11/22] add helper for single-typevar substitution --- .../src/types/constraints.rs | 42 +++++++------------ .../ty_python_semantic/src/types/generics.rs | 18 ++++++++ 2 files changed, 33 insertions(+), 27 deletions(-) diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index b08887a3a890f..ce88a6aa3b943 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -100,15 +100,15 @@ use rustc_hash::{FxHashMap, FxHashSet}; use smallvec::SmallVec; use crate::types::class::GenericAlias; -use crate::types::generics::{ApplySpecialization, InferableTypeVars}; +use crate::types::generics::InferableTypeVars; use crate::types::typevar::{BoundTypeVarIdentity, walk_bound_type_var_type}; use crate::types::variance::VarianceInferable; use crate::types::visitor::{ TypeCollector, TypeVisitor, any_over_type, walk_type_with_recursion_guard, }; use crate::types::{ - BoundTypeVarInstance, IntersectionType, Type, TypeContext, TypeMapping, - TypeVarBoundOrConstraints, TypeVarVariance, UnionType, + BoundTypeVarInstance, IntersectionType, Type, TypeVarBoundOrConstraints, TypeVarVariance, + UnionType, }; use crate::{Db, FxIndexMap, FxIndexSet}; @@ -4642,13 +4642,10 @@ impl SequentMap { _ => None, }; if let Some(replacement) = upper_replacement { - let new_upper = constrained_data.upper.apply_type_mapping( + let new_upper = constrained_data.upper.substitute_one_typevar( db, - &TypeMapping::ApplySpecialization(ApplySpecialization::Single( - bound_typevar, - replacement, - )), - TypeContext::default(), + bound_typevar, + replacement, ); if new_upper != constrained_data.upper { let post = ConstraintId::new( @@ -4692,13 +4689,10 @@ impl SequentMap { _ => None, }; if let Some(replacement) = lower_replacement { - let new_lower = constrained_data.lower.apply_type_mapping( + let new_lower = constrained_data.lower.substitute_one_typevar( db, - &TypeMapping::ApplySpecialization(ApplySpecialization::Single( - bound_typevar, - replacement, - )), - TypeContext::default(), + bound_typevar, + replacement, ); if new_lower != constrained_data.lower { let post = ConstraintId::new( @@ -4782,13 +4776,10 @@ impl SequentMap { } }; if should_weaken_upper { - let new_upper = constrained_data.upper.apply_type_mapping( + let new_upper = constrained_data.upper.substitute_one_typevar( db, - &TypeMapping::ApplySpecialization(ApplySpecialization::Single( - nested_typevar, - replacement, - )), - TypeContext::default(), + nested_typevar, + replacement, ); if new_upper != constrained_data.upper { let post = ConstraintId::new( @@ -4820,13 +4811,10 @@ impl SequentMap { } }; if should_weaken_lower { - let new_lower = constrained_data.lower.apply_type_mapping( + let new_lower = constrained_data.lower.substitute_one_typevar( db, - &TypeMapping::ApplySpecialization(ApplySpecialization::Single( - nested_typevar, - replacement, - )), - TypeContext::default(), + nested_typevar, + replacement, ); if new_lower != constrained_data.lower { let post = ConstraintId::new( diff --git a/crates/ty_python_semantic/src/types/generics.rs b/crates/ty_python_semantic/src/types/generics.rs index e41046b0f0cff..49b0df4c07a6b 100644 --- a/crates/ty_python_semantic/src/types/generics.rs +++ b/crates/ty_python_semantic/src/types/generics.rs @@ -1647,6 +1647,24 @@ impl<'db> ApplySpecialization<'_, 'db> { } } +impl<'db> Type<'db> { + pub(crate) fn substitute_one_typevar( + self, + db: &'db dyn Db, + bound_typevar: BoundTypeVarInstance<'db>, + replacement: Type<'db>, + ) -> Type<'db> { + self.apply_type_mapping( + db, + &TypeMapping::ApplySpecialization(ApplySpecialization::Single( + bound_typevar, + replacement, + )), + TypeContext::default(), + ) + } +} + /// Performs type inference between parameter annotations and argument types, producing a /// specialization of a generic function. pub(crate) struct SpecializationBuilder<'db> { From fea48fb492864b979a95c1f19d9f2ac7a46a711c Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Fri, 20 Mar 2026 12:21:53 -0400 Subject: [PATCH 12/22] hopefully fix the timeouts --- .../ty_python_semantic/src/types/constraints.rs | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index ce88a6aa3b943..ddaa6ccfc4a92 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -4641,6 +4641,16 @@ impl SequentMap { } _ => None, }; + // If the replacement contains the bound typevar itself (e.g., the bound + // constraint is `_V ≀ G[_V]`), or the constrained typevar (e.g., the bound + // constraint is `_T ≀ G[_V]` and we're about to substitute into `_V ≀ G[_T]`), + // substituting would create a deeper nesting of the same recursive pattern + // that triggers the same substitution again ad infinitum. Skip in both cases. + let upper_replacement = upper_replacement.filter(|replacement| { + replacement.variance_of(db, bound_typevar) == TypeVarVariance::Bivariant + && replacement.variance_of(db, constrained_typevar) + == TypeVarVariance::Bivariant + }); if let Some(replacement) = upper_replacement { let new_upper = constrained_data.upper.substitute_one_typevar( db, @@ -4688,6 +4698,12 @@ impl SequentMap { } _ => None, }; + // Same recursive-type guard as above for the upper bound case. + let lower_replacement = lower_replacement.filter(|replacement| { + replacement.variance_of(db, bound_typevar) == TypeVarVariance::Bivariant + && replacement.variance_of(db, constrained_typevar) + == TypeVarVariance::Bivariant + }); if let Some(replacement) = lower_replacement { let new_lower = constrained_data.lower.substitute_one_typevar( db, From ca9d0301c912f190885f13bd56a42e8e935e6c69 Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Fri, 20 Mar 2026 16:46:53 -0400 Subject: [PATCH 13/22] add some simple filtering --- .../ty_python_semantic/src/types/constraints.rs | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index ddaa6ccfc4a92..f70f3c63294be 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -4781,10 +4781,12 @@ impl SequentMap { // - Covariant + S is B's lower bound (S ≀ B): G[S] ≀ G[B] β†’ weaker. Emit. // - Contravariant + S is B's upper bound (B ≀ S): G[S] ≀ G[B] β†’ weaker. Emit. // - Other combinations tighten rather than weaken. Skip. - let should_weaken_upper = - match constrained_data.upper.variance_of(db, nested_typevar) { + let should_weaken_upper = !constrained_data.upper.is_type_var() + && !constrained_data.upper.is_never() + && !constrained_data.upper.is_object() + && !constrained_data.upper.is_dynamic() + && match constrained_data.upper.variance_of(db, nested_typevar) { TypeVarVariance::Bivariant => false, - _ if constrained_data.upper.is_type_var() => false, TypeVarVariance::Covariant => !is_upper_bound, TypeVarVariance::Contravariant => is_upper_bound, TypeVarVariance::Invariant => { @@ -4816,10 +4818,12 @@ impl SequentMap { } // Ditto for the lower bound. - let should_weaken_lower = - match constrained_data.lower.variance_of(db, nested_typevar) { + let should_weaken_lower = !constrained_data.lower.is_type_var() + && !constrained_data.lower.is_never() + && !constrained_data.lower.is_object() + && !constrained_data.lower.is_dynamic() + && match constrained_data.lower.variance_of(db, nested_typevar) { TypeVarVariance::Bivariant => false, - _ if constrained_data.lower.is_type_var() => false, TypeVarVariance::Covariant => is_upper_bound, TypeVarVariance::Contravariant => !is_upper_bound, TypeVarVariance::Invariant => { From 19e2effbffa2bc83ec6945180e81c5425e01d813 Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Fri, 20 Mar 2026 19:08:49 -0400 Subject: [PATCH 14/22] add new regression tests --- PLAN.md | 31 +++++++-- .../type_properties/implies_subtype_of.md | 66 +++++++++++++++++++ 2 files changed, 92 insertions(+), 5 deletions(-) diff --git a/PLAN.md b/PLAN.md index 4e5e64ec4b19a..9357be9f787c1 100644 --- a/PLAN.md +++ b/PLAN.md @@ -628,11 +628,32 @@ behavior. Full test suite (513 tests) passes. jpk passes. ## Open questions -1. **Performance**: The `variance_of` computation walks the type tree - recursively. Calling it inside `add_sequents_for_pair` for every pair of - constraints could be expensive. We should check if caching or early-exit - (e.g., skip if neither bound contains any typevar via `any_over_type`) is - needed. +1. **Performance (diagnosed on 2026-03-20)**: The scipy ecosystem timeout is + not from `variance_of` itself; it is from the *upper-bound tightening* + implications in `add_nested_typevar_sequents`. + + Repro/minimization: + + - Full scipy on this branch timed out (`scipy: null`), while `main` was ~5.9s. + - Narrowed to `scipy/interpolate/tests/test_polyint.py`: + - feature branch: >20s timeout, ~1.2GB RSS + - main: ~0.59s, ~108MB RSS + - Disabling all nested-typevar sequents restores ~0.6s. + - Re-enabling only `try_weakening` stays fast. + - Re-enabling `try_tightening` regresses again. + - Within `try_tightening`, lower-bound substitutions are fine; the blowup is + upper-bound substitutions that emit pair implications. + + Candidate mitigation tested in scratch: + + - In the upper-replacement filter, skip replacements that are bare typevars + (`!replacement.is_type_var()`). + - This restores scipy to ~6.2s via `eco` and ~0.59s for `test_polyint.py`. + - `cargo nextest run -p ty_python_semantic` passes with this change. + - But this is likely too aggressive: it drops valid implications such as + `(B ≀ S) ∧ (U ≀ Covariant[B]) -> (U ≀ Covariant[S])`. + A temporary mdtest confirmed that implication fails under this filter. + So this is useful as a diagnostic, not a final fix. 1. **Multiple typevar occurrences**: A single bound like `dict[T, T]` mentions `T` twice. The `variance_of` implementation already handles this by joining diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md b/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md index 1479390fd1b29..6da5940f62fe2 100644 --- a/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md +++ b/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md @@ -859,6 +859,72 @@ def lower_bound_into_upper[B, C](): static_assert(constraints.implies_subtype_of(C, Covariant[B])) ``` +### Nested typevar propagation also works when the replacement is a bare typevar + +```py +from typing import Never +from ty_extensions import ConstraintSet, static_assert + +class Covariant[T]: + def get(self) -> T: + raise ValueError + +class Contravariant[T]: + def set(self, value: T): + pass + +class Invariant[T]: + def get(self) -> T: + raise ValueError + + def set(self, value: T): + pass + +def covariant_upper[B, S, U](): + # (B ≀ S) ∧ (U ≀ Covariant[B]) -> (U ≀ Covariant[S]) + constraints = ConstraintSet.range(Never, B, S) & ConstraintSet.range(Never, U, Covariant[B]) + static_assert(constraints.implies_subtype_of(U, Covariant[S])) + + +def covariant_lower[B, S, U](): + # (S ≀ B) ∧ (Covariant[B] ≀ U) -> (Covariant[S] ≀ U) + constraints = ConstraintSet.range(S, B, object) & ConstraintSet.range(Covariant[B], U, object) + static_assert(constraints.implies_subtype_of(Covariant[S], U)) + + +def contravariant_upper[B, S, U](): + # (S ≀ B) ∧ (U ≀ Contravariant[B]) -> (U ≀ Contravariant[S]) + constraints = ConstraintSet.range(S, B, object) & ConstraintSet.range(Never, U, Contravariant[B]) + static_assert(constraints.implies_subtype_of(U, Contravariant[S])) + + +def contravariant_lower[B, S, U](): + # (B ≀ S) ∧ (Contravariant[B] ≀ U) -> (Contravariant[S] ≀ U) + constraints = ConstraintSet.range(Never, B, S) & ConstraintSet.range(Contravariant[B], U, object) + static_assert(constraints.implies_subtype_of(Contravariant[S], U)) + + +def invariant_upper_requires_equality[B, S, U](): + # Invariant replacement only holds under equality constraints on B. + constraints = ConstraintSet.range(S, B, S) & ConstraintSet.range(Never, U, Invariant[B]) + static_assert(constraints.implies_subtype_of(U, Invariant[S])) + + +def invariant_lower_requires_equality[B, S, U](): + constraints = ConstraintSet.range(S, B, S) & ConstraintSet.range(Invariant[B], U, object) + static_assert(constraints.implies_subtype_of(Invariant[S], U)) + + +def invariant_upper_one_sided_is_not_enough[B, S, U](): + constraints = ConstraintSet.range(Never, B, S) & ConstraintSet.range(Never, U, Invariant[B]) + static_assert(not constraints.implies_subtype_of(U, Invariant[S])) + + +def invariant_lower_one_sided_is_not_enough[B, S, U](): + constraints = ConstraintSet.range(S, B, object) & ConstraintSet.range(Invariant[B], U, object) + static_assert(not constraints.implies_subtype_of(Invariant[S], U)) +``` + ### Reverse decomposition: bounds on a typevar can be decomposed via variance When a constraint has lower and upper bounds that are parameterizations of the same generic type, we From 97fc9742b943edc425f0378733ec7db4b0d78221 Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Sat, 21 Mar 2026 10:09:58 -0400 Subject: [PATCH 15/22] fix scipy perf regression --- PLAN.md | 15 +++++-- crates/ty_python_semantic/src/types.rs | 4 ++ .../src/types/constraints.rs | 43 +++++++++++++------ 3 files changed, 47 insertions(+), 15 deletions(-) diff --git a/PLAN.md b/PLAN.md index 9357be9f787c1..4e399d406b802 100644 --- a/PLAN.md +++ b/PLAN.md @@ -650,10 +650,19 @@ behavior. Full test suite (513 tests) passes. jpk passes. (`!replacement.is_type_var()`). - This restores scipy to ~6.2s via `eco` and ~0.59s for `test_polyint.py`. - `cargo nextest run -p ty_python_semantic` passes with this change. - - But this is likely too aggressive: it drops valid implications such as + - But this is too aggressive: it drops valid implications such as `(B ≀ S) ∧ (U ≀ Covariant[B]) -> (U ≀ Covariant[S])`. - A temporary mdtest confirmed that implication fails under this filter. - So this is useful as a diagnostic, not a final fix. + + Implemented mitigation: + + - Keep bare-typevar replacement support, but skip the pathological + typevarβ†’typevar replacement shape in compound bounds: + - upper bounds: skip when constrained upper bound is a union + - lower bounds (dual): skip when constrained lower bound is an intersection + - Also add a fast-path in the recursion guard for bare typevars so we avoid + tracked `variance_of` calls in that case. + - This keeps the new regression mdtests for bare typevar replacement green, + and restores scipy performance (`eco scipy` ~5.74s instead of timeout). 1. **Multiple typevar occurrences**: A single bound like `dict[T, T]` mentions `T` twice. The `variance_of` implementation already handles this by joining diff --git a/crates/ty_python_semantic/src/types.rs b/crates/ty_python_semantic/src/types.rs index c406b2e201a92..4ef6af9ae2007 100644 --- a/crates/ty_python_semantic/src/types.rs +++ b/crates/ty_python_semantic/src/types.rs @@ -1337,6 +1337,10 @@ impl<'db> Type<'db> { self.as_union().expect("Expected a Type::Union variant") } + pub(crate) const fn is_intersection(self) -> bool { + matches!(self, Type::Intersection(_)) + } + /// Returns whether this is a "real" intersection type. (Negated types are represented by an /// intersection containing a single negative branch, which this method does _not_ consider a /// "real" intersection.) diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index f70f3c63294be..adab9afc1b706 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -4608,6 +4608,21 @@ impl SequentMap { let constrained_data = builder.constraint_data(constrained_constraint); let constrained_typevar = constrained_data.typevar; + // If the replacement contains the bound typevar itself (e.g., the bound + // constraint is `_V ≀ G[_V]`), or the constrained typevar (e.g., the bound + // constraint is `_T ≀ G[_V]` and we're about to substitute into `_V ≀ G[_T]`), + // substituting would create a deeper nesting of the same recursive pattern + // that triggers the same substitution again ad infinitum. Skip in both cases. + // + // Fast-path bare typevar replacements (`Type::TypeVar`) using equality checks + // instead of calling `variance_of` on them. This avoids a large number of tiny + // tracked `variance_of` queries in hot paths. + let replacement_mentions_bound_or_constrained = |replacement: Type<'db>| { + replacement.variance_of(db, bound_typevar) != TypeVarVariance::Bivariant + || replacement.variance_of(db, constrained_typevar) + != TypeVarVariance::Bivariant + }; + // Check the upper bound of the constrained constraint for nested occurrences of // the bound typevar. We use `variance_of` as our combined presence + variance // check: `Bivariant` means the typevar doesn't appear in the type (or is genuinely @@ -4641,15 +4656,15 @@ impl SequentMap { } _ => None, }; - // If the replacement contains the bound typevar itself (e.g., the bound - // constraint is `_V ≀ G[_V]`), or the constrained typevar (e.g., the bound - // constraint is `_T ≀ G[_V]` and we're about to substitute into `_V ≀ G[_T]`), - // substituting would create a deeper nesting of the same recursive pattern - // that triggers the same substitution again ad infinitum. Skip in both cases. let upper_replacement = upper_replacement.filter(|replacement| { - replacement.variance_of(db, bound_typevar) == TypeVarVariance::Bivariant - && replacement.variance_of(db, constrained_typevar) - == TypeVarVariance::Bivariant + // Substituting one typevar for another into large unions can generate many + // very-weak derived constraints and cause severe performance regressions. + // Keep the common/non-union case enabled; skip union upper bounds for this + // specific typevar-to-typevar replacement shape. + if replacement.is_type_var() && constrained_data.upper.is_union() { + return false; + } + !replacement_mentions_bound_or_constrained(*replacement) }); if let Some(replacement) = upper_replacement { let new_upper = constrained_data.upper.substitute_one_typevar( @@ -4698,11 +4713,15 @@ impl SequentMap { } _ => None, }; - // Same recursive-type guard as above for the upper bound case. let lower_replacement = lower_replacement.filter(|replacement| { - replacement.variance_of(db, bound_typevar) == TypeVarVariance::Bivariant - && replacement.variance_of(db, constrained_typevar) - == TypeVarVariance::Bivariant + // Substituting one typevar for another into large intersections can generate + // many very-weak derived constraints and cause severe performance regressions. + // Keep the common/non-intersection case enabled; skip intersection lower + // bounds for this specific typevar-to-typevar replacement shape. + if replacement.is_type_var() && constrained_data.lower.is_intersection() { + return false; + } + !replacement_mentions_bound_or_constrained(*replacement) }); if let Some(replacement) = lower_replacement { let new_lower = constrained_data.lower.substitute_one_typevar( From b818ca9b7fbfa95cfba2837fc09ac97c152be5ea Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Wed, 18 Mar 2026 11:02:59 -0400 Subject: [PATCH 16/22] remove completed plan --- PLAN.md | 692 -------------------------------------------------------- 1 file changed, 692 deletions(-) delete mode 100644 PLAN.md diff --git a/PLAN.md b/PLAN.md deleted file mode 100644 index 4e399d406b802..0000000000000 --- a/PLAN.md +++ /dev/null @@ -1,692 +0,0 @@ -# Plan: Propagate nested-typevar constraints through variance in the sequent map - -## Status markers - -Each step is marked with one of: - -- ⬜ Not started -- πŸ”§ In progress -- βœ… Completed - -When resuming this plan, read through the relevant files to validate status -markers before continuing. Include these instructions in the plan even though -they are also listed in the AGENTS.md file. - -## Overview - -The constraint set's `exists_one` operation removes all constraints mentioning a -bound typevar. When a typevar `T` appears *nested* inside the bound of a -constraint on a different typevar `U` (e.g., `U ≀ Sequence[T]`), we currently -lose all information about `U` because the sequent map doesn't generate derived -facts that substitute `T`'s concrete bounds into the nested occurrence. - -The fix requires teaching `add_sequents_for_pair` to recognize when one -constraint provides bounds on a typevar `T`, and the other constraint's -lower/upper bound mentions `T` nested inside a parameterized type. Using the -variance of `T`'s position in that parameterized type, we can determine what -substitution is valid: - -- **Covariant**: upper bound on `T` propagates into upper bound position; - lower bound on `T` propagates into lower bound position. (Preserves - direction.) -- **Contravariant**: upper bound on `T` propagates into lower bound - position; lower bound on `T` propagates into upper bound position. (Flips - direction.) -- **Invariant**: only an equality constraint on `T` (lower = upper) can - propagate. -- **Bivariant**: the typevar is irrelevant to the type; no implication is - needed since the constraint doesn't actually depend on the typevar. - -We implement covariance first as a complete end-to-end slice, then add -contravariance and invariance as modifications to that working foundation. - -## Steps - -### Phase 1: Helpers - -#### Step 1.1 βœ… β€” Confirm that `variance_of` serves as our detection mechanism - -No new helper is needed. The existing `VarianceInferable` trait provides -`ty.variance_of(db, typevar)`, which returns: - -- `Bivariant` if the typevar doesn't appear in the type at all (or is genuinely - bivariant) β€” in either case, no implication is needed. -- `Covariant`, `Contravariant`, or `Invariant` if the typevar appears nested - in the type β€” telling us which substitution rule applies. - -This single call replaces both the presence check (`any_over_type`) and the -variance computation. We just call `variance_of` and skip if the result is -`Bivariant`. - -At the call site, add a prominent comment explaining this interpretation: -`Bivariant` here means "the typevar does not appear in this type (or is -genuinely bivariant, which is equivalent for our purposes β€” no implication is -needed in either case)." Note that if `Bivariant` is ever removed from the -`TypeVarVariance` enum, we would need an alternative representation for -"typevar not present" (e.g., returning `Option`). - -#### Step 1.2 βœ… β€” Add a `Single` variant to `ApplySpecialization` - -Add a new variant to `ApplySpecialization` in `generics.rs`: - -```rust -Single(BoundTypeVarInstance<'db>, Type<'db>), -``` - -This maps a single typevar to a concrete type. The `get` method implementation -is trivial: check if `bound_typevar` matches the stored typevar and return the -mapped type if so, `None` otherwise. - -This can then be used via the existing `TypeMapping::ApplySpecialization` to -perform the substitution: `ty.apply_type_mapping(db, &TypeMapping::ApplySpecialization(ApplySpecialization::Single(typevar, replacement)))`. - -The rest of the `apply_type_mapping` infrastructure handles the recursive walk -through the type tree automatically. - -### Phase 2: Covariant nested typevar propagation (end-to-end) - -This phase implements the covariant case fully, including sequent generation, -testing, and validation. Contravariance and invariance will follow as -modifications to this working foundation. - -#### Step 2.1 βœ… β€” Add mdtest cases for covariant propagation (red) - -Add tests to the "Transitivity" section of -`crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md`. -These follow the existing pattern: construct constraint sets with -`ConstraintSet.range(...)`, combine them with `&`, and verify implications with -`implies_subtype_of`. - -Each markdown section has its own scope, so define local `Covariant[T]` (and -later `Contravariant[T]`, `Invariant[T]`) classes in the new test sections. -Test both typevar orderings to verify BDD-ordering independence. - -Key test cases for covariant upper bound propagation: - -- `(T ≀ int) ∧ (U ≀ Covariant[T])` should imply `U ≀ Covariant[int]` - (i.e., `constraints.implies_subtype_of(U, Covariant[int])`) -- The same should NOT imply `U ≀ Covariant[bool]` (too tight) - -Key test cases for covariant lower bound propagation: - -- `(int ≀ T) ∧ (Covariant[T] ≀ U)` should imply `Covariant[int] ≀ U` - (i.e., `constraints.implies_subtype_of(Covariant[int], U)`) - -Run these tests first to verify they fail with the current logic (red phase of -TDD). Then proceed to Step 2.2 to make them pass. - -#### Step 2.2 βœ… β€” Add sequent generation for covariant nested typevars (green) - -Currently, `add_sequents_for_pair` dispatches to -`add_mutual_sequents_for_different_typevars` when the two constraints are on -different typevars. That method only handles the case where a typevar appears as -a *direct* `Type::TypeVar(...)` in the other constraint's lower/upper bound. - -Add a new method (e.g., `add_nested_typevar_sequents`) called from -`add_mutual_sequents_for_different_typevars` (or from `add_sequents_for_pair` -directly) that handles the case where one constraint's bound *contains* the -other constraint's typevar nested inside a parameterized type. - -For the initial covariant-only implementation, the logic is: - -Given constraints `(l_B ≀ B ≀ u_B)` and `(l_C ≀ C ≀ u_C)` where `B` appears -nested in `l_C` or `u_C`: - -**Case A: `B` appears in `u_C` (upper bound of `C`)** - -- Compute `v = u_C.variance_of(db, B)`. -- If covariant: emit `(l_B ≀ B ≀ u_B) ∧ (l_C ≀ C ≀ u_C) β†’ (C ≀ u_C[B := u_B])` - (The upper bound on `B` substitutes into the upper bound of `C`.) - -**Case B: `B` appears in `l_C` (lower bound of `C`)** - -- Compute `v = l_C.variance_of(db, B)`. -- If covariant: emit `(l_B ≀ B ≀ u_B) ∧ (l_C ≀ C ≀ u_C) β†’ (l_C[B := l_B] ≀ C)` - (The lower bound on `B` substitutes into the lower bound of `C`.) - -For now, skip the contravariant, invariant, and bivariant cases β€” just return -early if the variance is not covariant. - -Note: the antecedent constraints in these sequents are the *original* -constraints from the BDD. The pair implication is valid because if both original -constraints hold, the covariant substitution certainly follows. - -The existing `add_mutual_sequents_for_different_typevars` handles direct -`Type::TypeVar(B)` references in bounds. Since a bare `Type::TypeVar` has -covariant variance in itself, the new nested logic would technically subsume it. -However, the existing code has careful handling for canonical ordering of -typevar-to-typevar constraints, so it's cleaner to keep them separate and only -check for nested references when the bound is *not* a bare `Type::TypeVar`. -Add a comment in the code explaining this relationship β€” it's a subtle point -that would be easy to miss. - -#### Step 2.3 βœ… β€” Run the full test suite - -Run the full constraint set and ty_python_semantic test suite to check for -regressions. Fix any issues before proceeding. - -### Phase 3: Contravariant and invariant propagation - -Once covariance is working end-to-end, extend the logic to handle the remaining -variance cases. These should be fairly straightforward modifications to the -covariance logic. - -#### Step 3.1 βœ… β€” Add mdtest cases for contravariant and invariant propagation (red) - -Add tests following the same pattern as Step 2.2, using the `Contravariant[T]` -and `Invariant[T]` classes already defined in the "Compound types" section. - -Contravariant test cases: - -- `(T ≀ int) ∧ (U ≀ Contravariant[T])` should imply - `Contravariant[int] ≀ U` (flipped direction β€” but actually this doesn't help - tighten U's upper bound). Need to think carefully about which constraints - are expressible and testable here. -- `(int ≀ T) ∧ (U ≀ Contravariant[T])` should imply - `U ≀ Contravariant[int]` (lower bound on T, flipped by contravariance, gives - upper bound on Contravariant[T]). - -Invariant test cases: - -- `(T = int) ∧ (U ≀ Invariant[T])` should imply `U ≀ Invariant[int]`. -- `(T ≀ int) ∧ (U ≀ Invariant[T])` should NOT imply `U ≀ Invariant[int]`. - -Composed variance test cases: - -- Nested generics where variances compose (e.g., `Covariant[Contravariant[T]]` - β€” net effect is contravariant). - -Run these tests first to verify they fail (red phase). - -#### Step 3.2 βœ… β€” Add contravariant propagation - -Extend the nested typevar sequent generation: - -**`B` in `u_C` (upper bound of `C`), contravariant:** - -- Emit `(l_B ≀ B ≀ u_B) ∧ (l_C ≀ C ≀ u_C) β†’ (C ≀ u_C[B := l_B])` - (The *lower* bound on `B` substitutes into the upper bound of `C` β€” flipped.) - -**`B` in `l_C` (lower bound of `C`), contravariant:** - -- Emit `(l_B ≀ B ≀ u_B) ∧ (l_C ≀ C ≀ u_C) β†’ (l_C[B := u_B] ≀ C)` - (The *upper* bound on `B` substitutes into the lower bound of `C` β€” flipped.) - -#### Step 3.3 βœ… β€” Add invariant propagation - -Extend the nested typevar sequent generation: - -- Only emit a derived constraint if `l_B = u_B` (equality constraint on `B`). -- If so, substitute that single type into either bound of `C`. - -#### Step 3.4 βœ… β€” Run the full test suite - -Run the full test suite again to check for regressions. - -### Phase 4: Reverse direction β€” decomposing matching generic bounds - -Phases 1–3 implemented the *forward* direction: given a concrete bound on a -typevar `T`, substitute it into a nested occurrence of `T` in another typevar's -bound. This is a cross-typevar (different-typevar) pair sequent. - -The *reverse* direction handles the case where a single constraint on a typevar -has lower and upper bounds that are both parameterizations of the same generic -type. By decomposing the generic type using variance, we can extract bounds on -the nested typevar. - -Example: the constraint `(Sequence[int] ≀ A ≀ Sequence[T])` implies -`(int ≀ T)`, because `Sequence` is covariant, so `Sequence[int] ≀ Sequence[T]` -implies `int ≀ T`. - -This combined constraint arises from two separate constraints `(Sequence[int] ≀ A)` -and `(A ≀ Sequence[T])` being combined β€” the existing `add_concrete_sequents` -logic should already produce this combined constraint as a pair implication. - -This is *part* of what's needed to make patterns like -`invoke(head_sequence, x)` work: - -```python -def invoke[A, B](c: Callable[[A], B], a: A) -> B: ... -def head_sequence[T](s: Sequence[T]) -> T: ... -def _(x: Sequence[int]): - reveal_type(invoke(head_sequence, x)) # should be int -``` - -The matching would produce constraints that combine into: - -- `Sequence[int] ≀ A ≀ Sequence[T]` (from argument + callable parameter) -- `T ≀ B` (from callable return matching) - -To derive `int ≀ T`, we need to decompose `Sequence[int] ≀ A ≀ Sequence[T]` -by recognizing that `Sequence[int] ≀ Sequence[T]` must hold, and applying -covariance. - -Note: this example will also require conjoining constraint sets across -multiple arguments (which is not yet implemented β€” tracked by the TODO in -`add_type_mappings_from_constraint_set`). The reverse decomposition is -necessary but not sufficient on its own. - -#### Where this fits - -This is a single-constraint decomposition: given a constraint -`(L ≀ A ≀ U)`, we check whether `L ≀ U` produces useful derived constraints -on the typevars mentioned in `L` and `U`. This logic belongs in -`add_sequents_for_single` (or is triggered when the combined constraint is -first created). - -#### Variance rules (same as forward, applied in reverse) - -Given a constraint `(G[l'] ≀ A ≀ G[T])` where both bounds share the same -generic base `G`: - -| Variance of T in G | Derived constraint | -| ------------------ | ------------------------------------------------ | -| Covariant | `l' ≀ T` | -| Contravariant | `T ≀ l'` | -| Invariant | `T = l'` (only if both sides match structurally) | -| Bivariant | skip | - -And symmetrically for `(G[T] ≀ A ≀ G[u'])`: - -| Variance of T in G | Derived constraint | -| ------------------ | --------------------------------------- | -| Covariant | `T ≀ u'` | -| Contravariant | `u' ≀ T` | -| Invariant | `T = u'` (only with matching structure) | -| Bivariant | skip | - -#### Approach: single implication via assignability check - -Rather than building bespoke generic-base-matching logic, we can reuse the -existing constraint set assignability machinery. Given a constraint -`(L ≀ A ≀ U)`, the constraint is only satisfiable if `L ≀ U`. If `L` and/or -`U` mention typevars, then `L ≀ U` produces a constraint set on those typevars. - -This could be triggered from `add_sequents_for_single` β€” for every constraint -`(L ≀ A ≀ U)`, compute `L.when_constraint_set_assignable_to(U)` and derive -implications from the result. No need for an upfront check on whether the -bounds mention typevars β€” just do the CSA check unconditionally and see if the -result is a non-trivial constraint set. Deeply scanning for typevars would not -be significantly cheaper than just doing the check. - -This should subsume the existing `single_implications` logic in -`add_sequents_for_single`. The current code manually propagates typevar-to- -typevar bounds (e.g., `(S ≀ T ≀ U) β†’ (S ≀ U)`), but a CSA check on `S ≀ U` -will produce that same constraint with the correct typevar ordering -automatically. The bare-typevar case does not need special treatment β€” CSA -handles canonical ordering naturally. - -Note that the existing pair sequent logic should already combine two -same-typevar constraints like `(Sequence[int] ≀ A)` and `(A ≀ Sequence[T])` -into a single combined constraint `(Sequence[int] ≀ A ≀ Sequence[T])` via -`add_concrete_sequents`. So the decomposition logic lives at the single- -constraint level. - -The result of the assignability check is a full constraint set (an arbitrary -boolean formula, not just a conjunction). The sequent map currently only -supports implications where the consequent is a single constraint. As a -pragmatic starting point, we handle only the case where the resulting -constraint set is a single conjunction β€” i.e., a single path from root to the -`always` terminal in the BDD. - -To detect this, we can take advantage of BDD reduction. Our BDDs are only -quasi-reduced, but redundant nodes where both outgoing edges lead to `never` -are still collapsed. This means if we ever encounter an interior node where -both outgoing edges (if_true and if_false) point to something other than -`never`, that node *must* have at least two paths to the `always` terminal, -and the constraint set is not a simple conjunction. So a single structural -walk of the tree suffices to check β€” no PathAssignments/SequentMap needed. - -If the constraint set is simple (single rootβ†’always path), walk it a second -time to collect the constraints along that path: - -- For each positive constraint (interior node where we take the if_true - branch): record a `single_implication` from the original constraint to the - derived constraint. -- For each negative constraint (interior node where we take the if_false - branch): record a `pair_impossibility` between the original constraint and - the derived constraint. - -For common cases (covariant/contravariant generics with a single type -parameter), the result should always be a simple conjunction, so this approach -should suffice. - -A future, more sophisticated solution could handle arbitrary constraint set -results by viewing the BDD as a DNF (disjunction of paths from root to the -`always` terminal, where each path is a conjunction). Each DNF clause could be -integrated into `PathAssignments` by recursing with resets for each path β€” a -pattern similar to what `walk_edge` already does for true/false/uncertain -branches. But this is significantly more complex and can be deferred. - -Circular dependency concern: we'd be invoking constraint set assignability -*from within* sequent map construction. We need to verify this doesn't create -cycles. A possible mitigation is to use the assignability check without -consulting the sequent map (i.e., a "raw" check that doesn't itself rely on -derived facts). - -#### Steps - -##### Step 4.1 ⬜ β€” Add mdtest cases for reverse decomposition (red) - -Add tests to the Transitivity section of `implies_subtype_of.md`. The tests -should construct the combined constraint directly using `ConstraintSet.range` -(e.g., `ConstraintSet.range(Covariant[int], A, Covariant[T])`) and verify -that the derived implications hold. - -Test cases: - -- Covariant: `(Covariant[int] ≀ A ≀ Covariant[T])` should imply `int ≀ T` -- Contravariant: `(Contravariant[int] ≀ A ≀ Contravariant[T])` should imply - `T ≀ int` (flipped) -- Invariant: `(Invariant[int] ≀ A ≀ Invariant[T])` should imply `T = int` -- Bare typevar (existing behavior, should still pass): - `(S ≀ A ≀ T)` should imply `S ≀ T` -- Test both typevar orderings for BDD-ordering independence - -##### Step 4.2 βœ… β€” Fix the disjointness check in `intersect` - -The current `ConstraintId::intersect` method uses -`lower.is_constraint_set_assignable_to(db, upper)` (a universal/always check) -to determine if the intersection `(L ≀ A ≀ U)` is disjoint. When `U` contains -typevars (e.g., `Covariant[T]`), this returns false even if there exist -assignments of `T` that make `L ≀ U` hold β€” causing the combined constraint to -be pruned as unsatisfiable. - -Fix: change the check to an existential one β€” "is `L ≀ U` *ever* true?" rather -than "is `L ≀ U` *always* true?". This is -`!when_constraint_set_assignable_to(L, U).is_never_satisfied()`. If there -exists some assignment where the intersection is satisfiable, the combined -constraint should survive. - -##### Step 4.3 βœ… β€” Add CSA-based decomposition in `add_sequents_for_single` - -For each constraint `(L ≀ A ≀ U)`, compute -`L.when_constraint_set_assignable_to(U)` to get a constraint set `C` that -describes the conditions under which `L ≀ U` holds. Then: - -1. Check if `C` is a simple conjunction (single rootβ†’always path in the BDD). - Use the structural criterion: if any interior node has both outgoing edges - pointing to something other than `never`, the result is not simple β€” bail - out. -1. If simple, walk the single path and record sequents: - - For each positive constraint (if_true branch taken): add a - `single_implication` from the original constraint to the derived one. - - For each negative constraint (if_false branch taken): add a - `pair_impossibility` between the original and derived constraints. - -This should subsume the existing `single_implications` logic in -`add_sequents_for_single`, including bare typevar-to-typevar propagation. -Variance is handled automatically by the CSA check β€” no need for explicit -variance matching or special-casing bare typevars. - -##### Step 4.4 βœ… β€” Verify bare typevar propagation still works - -Confirm that the existing tests for typevar-to-typevar transitivity -(e.g., `(S ≀ T ≀ U) β†’ (S ≀ U)`) still pass with the new CSA-based logic. -If the new logic fully subsumes the old `single_implications` code, consider -removing the old code. - -##### Step 4.5 βœ… β€” Run the full test suite - -Run the full test suite to check for regressions. - -### Phase 5: Handle the same-typevar case with recursive nested references - -#### Step 5.1 βœ… β€” Investigate same-typevar recursive nesting and concrete bound substitution - -**Recursive nesting** (`T ≀ Covariant[T]`): Investigated and confirmed that -trivial cases (lower = Never) are handled correctly. Non-trivial cases -(`Covariant[int] ≀ T ≀ Covariant[T]`) are a pre-existing limitation β€” the -CSA decomposition derives `int ≀ T` but the pair intersection between the -original and derived constraints is flagged as disjoint, which is actually -mathematically correct (the combined constraint is unsatisfiable for most -user-defined classes). Does not arise in practice. - -**Concrete bound substitution** (newly identified gap): The forward direction -(Phase 2/3) substitutes B's concrete bounds into C's bounds that contain B. -The reverse direction β€” substituting B (the typevar) into C's bounds that -contain B's concrete bound β€” is not yet implemented. This is analogous to the -existing "pivot" cases in `add_mutual_sequents_for_different_typevars` but -generalized to work inside generic types. - -Examples (covariant case): - -- `(Covariant[BU] ≀ C) ∧ (B ≀ BU) β†’ (Covariant[B] ≀ C)` -- `(C ≀ Covariant[BL]) ∧ (BL ≀ B) β†’ (C ≀ Covariant[B])` - -These create cross-typevar links that are weaker than the originals but useful -for downstream inference (e.g., after `exists_one`). Test cases are written -in the mdtest file with TODO markers. Implementation deferred to a future -phase. - -### Phase 6: Clean up - -#### Step 6.1 βœ… β€” Remove or update the TODO comment - -Remove the TODO comment at line 2828 of `constraints.rs` once the feature is -working. Update any related comments. - -#### Step 6.2 βœ… β€” Run `/home/dcreager/bin/jpk` - -Final pre-commit checks. We are in a jj worktree, so use `jpk` (with no -arguments) as a standin for `prek`. - -### Phase 7: Typevar bound substitution into nested generic types - -Phases 2–3 implemented the *forward* direction of nested typevar propagation: -when B (a typevar) appears nested inside C's bound, substitute B's concrete -bounds for B. This phase implements a restricted *reverse* direction: when one -of B's bounds is a *bare typevar* that appears nested inside C's bound, -substitute B (the typevar) for that bound. - -This generalizes the existing top-level "pivot" cases in -`add_mutual_sequents_for_different_typevars` to work inside generic types. -The pivot cases handle: - -```text -(CL ≀ C ≀ pivot) ∧ (pivot ≀ B ≀ BU) β†’ (CL ≀ C ≀ B) -``` - -The new cases handle the same logic when the pivot appears inside a generic: - -```text -(CL ≀ C ≀ G[pivot]) ∧ (pivot ≀ B ≀ BU) β†’ (CL ≀ C ≀ G[B]) -``` - -The derived constraint is *weaker* than the original (since `B ≀ BU` means -`G[B] ≀ G[BU]` in a covariant position, so we're relaxing C's bound). But it -introduces a cross-typevar link between B and C that is useful for downstream -inference, especially after `exists_one` removes one of the typevars. - -#### Scope restriction: bare typevar bounds only - -The fully general version of this feature would handle arbitrary concrete -types nested in C's bounds β€” e.g., `Covariant[int]` where `int` matches B's -upper bound. However, detecting an arbitrary concrete type inside a nested -position requires different machinery (pattern matching on generic alias -structure, or a CSA-based approach). - -When B's bound is a bare typevar, we can reuse `variance_of` for detection, -since `variance_of` already finds typevars nested inside types. This makes -the implementation a natural extension of `add_nested_typevar_sequents`. - -For example, given `(G[S] ≀ C) ∧ (S ≀ B)` where S is a typevar: - -- `variance_of(G[S], S)` finds S in the covariant position -- We know `S ≀ B`, so `G[S] ≀ G[B]` (covariance) -- Therefore `G[S] ≀ C` implies `G[B] ≀ C` (weakening the lower bound) -- Emit pair implication: `(G[S] ≀ C) ∧ (S ≀ B) β†’ (G[B] ≀ C)` - -A TODO comment should be added noting that a future extension could handle -the case where B's bound is an arbitrary type (not just a bare typevar). - -#### Where this fits - -The existing `add_nested_typevar_sequents` handles the case where `B` (the -constraint's typevar) appears in C's bound β€” it substitutes B's concrete -bounds for B. This new logic handles the complementary case: a *different* -typevar (one of B's bounds) appears in C's bound β€” we substitute B for that -typevar, creating a weaker but useful cross-typevar constraint. - -Both are called from `add_sequents_for_pair` for different-typevar pairs. -The new logic can live in `add_nested_typevar_sequents` itself, or in a new -method called alongside it. - -#### Variance rules - -The rules mirror `add_nested_typevar_sequents` but in the *weakening* -direction rather than the *tightening* direction. We substitute B for the -found typevar only when the result weakens (relaxes) the bound. - -Given constraints `(l_C ≀ C ≀ u_C)` and `(l_B ≀ B ≀ u_B)`, and a typevar S -that is one of B's bounds: - -**S = u_B (B's upper bound is a bare typevar S) and S appears in u_C:** - -We know `B ≀ S`. By variance: - -- Covariant: `G[B] ≀ G[S]`, so `u_C[B] ≀ u_C[S]` β€” substituting B *weakens* - the upper bound β†’ emit `C ≀ u_C[S := B]` -- Contravariant: `G[S] ≀ G[B]`, so `u_C[B] β‰₯ u_C[S]` β€” substituting B - *tightens* β†’ no useful derivation -- Invariant: only if `l_B = u_B` (equality on B), then `B = S` and the - substitution is exact - -**S = l_B (B's lower bound is a bare typevar S) and S appears in l_C:** - -We know `S ≀ B`. By variance: - -- Covariant: `G[S] ≀ G[B]`, so `l_C[B] β‰₯ l_C[S]` β€” substituting B *weakens* - the lower bound β†’ emit `l_C[S := B] ≀ C` -- Contravariant: `G[B] ≀ G[S]`, so `l_C[B] ≀ l_C[S]` β€” substituting B - *tightens* β†’ no useful derivation -- Invariant: only if `l_B = u_B` (equality on B) - -**S = l_B and S appears in u_C:** - -We know `S ≀ B`. By variance: - -- Contravariant: `G[B] ≀ G[S]`, so `u_C[B] ≀ u_C[S]` β€” substituting B - *weakens* the upper bound β†’ emit `C ≀ u_C[S := B]` -- Covariant: tightens β†’ no useful derivation -- Invariant: only if `l_B = u_B` - -**S = u_B and S appears in l_C:** - -We know `B ≀ S`. By variance: - -- Contravariant: `G[S] ≀ G[B]`, so `l_C[B] β‰₯ l_C[S]` β€” substituting B - *weakens* the lower bound β†’ emit `l_C[S := B] ≀ C` -- Covariant: tightens β†’ no useful derivation -- Invariant: only if `l_B = u_B` - -#### Implementation - -Added a new method `try_reverse_nested_typevar_sequents` in the sequent map, -called from `add_nested_typevar_sequents` alongside the existing forward -direction. For each constraint pair (B, C) on different typevars: - -1. Extract B's bare typevar bounds (upper/lower bounds that are `Type::TypeVar`). -1. For each such typevar S, use `variance_of` to check if S appears nested - in C's upper/lower bounds. -1. Based on variance and which bound S is (upper vs lower), determine whether - substituting B for S *weakens* (relaxes) the bound β€” only emit in that case. -1. Construct the substituted bound via `ApplySpecialization::Single(S, B)` and - emit a pair implication. - -The variance rules for weakening: - -- **Upper bound of C** (want to make it *larger* to weaken): - - Covariant + S is B's lower bound (S ≀ B β†’ G[S] ≀ G[B]): emit - - Contravariant + S is B's upper bound (B ≀ S β†’ G[S] ≀ G[B] in contra): emit -- **Lower bound of C** (want to make it *smaller* to weaken): - - Covariant + S is B's upper bound (B ≀ S β†’ G[B] ≀ G[S]): emit - - Contravariant + S is B's lower bound (S ≀ B β†’ G[B] ≀ G[S] in contra): emit -- **Invariant**: only when B is an equality constraint (l_B = u_B). - -This was needed because the canonical constraint encoding depends on typevar -ordering in the builder: `B ≀ S` may be encoded as `(Never ≀ B ≀ S)` on B -(when S is earlier) or `(B ≀ S ≀ object)` on S (when B is earlier). The -existing forward direction in `add_nested_typevar_sequents` only handles the -second encoding. The new reverse direction handles both. - -#### Steps - -##### Step 7.1 βœ… β€” Add tests for bare typevar bound substitution (red) - -Added tests covering covariant and contravariant cases, both typevar -orderings. All 8 assertions initially failed. - -##### Step 7.2 βœ… β€” Implement `try_reverse_nested_typevar_sequents` (green) - -Added the reverse direction logic. All 8 assertions now pass. - -##### Step 7.3 βœ… β€” Run the full test suite and jpk - -Updated the `tdd_owned_round_trip` test to match the new `load` ordering -behavior. Full test suite (513 tests) passes. jpk passes. - -## Open questions - -1. **Performance (diagnosed on 2026-03-20)**: The scipy ecosystem timeout is - not from `variance_of` itself; it is from the *upper-bound tightening* - implications in `add_nested_typevar_sequents`. - - Repro/minimization: - - - Full scipy on this branch timed out (`scipy: null`), while `main` was ~5.9s. - - Narrowed to `scipy/interpolate/tests/test_polyint.py`: - - feature branch: >20s timeout, ~1.2GB RSS - - main: ~0.59s, ~108MB RSS - - Disabling all nested-typevar sequents restores ~0.6s. - - Re-enabling only `try_weakening` stays fast. - - Re-enabling `try_tightening` regresses again. - - Within `try_tightening`, lower-bound substitutions are fine; the blowup is - upper-bound substitutions that emit pair implications. - - Candidate mitigation tested in scratch: - - - In the upper-replacement filter, skip replacements that are bare typevars - (`!replacement.is_type_var()`). - - This restores scipy to ~6.2s via `eco` and ~0.59s for `test_polyint.py`. - - `cargo nextest run -p ty_python_semantic` passes with this change. - - But this is too aggressive: it drops valid implications such as - `(B ≀ S) ∧ (U ≀ Covariant[B]) -> (U ≀ Covariant[S])`. - - Implemented mitigation: - - - Keep bare-typevar replacement support, but skip the pathological - typevarβ†’typevar replacement shape in compound bounds: - - upper bounds: skip when constrained upper bound is a union - - lower bounds (dual): skip when constrained lower bound is an intersection - - Also add a fast-path in the recursion guard for bare typevars so we avoid - tracked `variance_of` calls in that case. - - This keeps the new regression mdtests for bare typevar replacement green, - and restores scipy performance (`eco scipy` ~5.74s instead of timeout). - -1. **Multiple typevar occurrences**: A single bound like `dict[T, T]` mentions - `T` twice. The `variance_of` implementation already handles this by joining - the variances of all occurrences. If one occurrence is covariant and another - contravariant, the joined variance is invariant, which correctly requires an - equality constraint. Verify that this composition works correctly for our - purposes. - -1. **Recursive bounds**: Can a constraint like `T ≀ Sequence[T]` arise? If so, - does it require special handling to avoid infinite loops during substitution? - -1. **Circular dependencies in reverse decomposition**: The reverse direction - invokes constraint set assignability from within sequent map construction. - Need to verify this doesn't create cycles. May need a "raw" assignability - check that doesn't consult the sequent map. - -1. **DNF expansion for complex constraint set results**: When the assignability - check produces a non-simple constraint set (e.g., a disjunction), we could - view the BDD as a DNF and integrate each path's conjunction into - `PathAssignments` by recursing with resets. Deferred for now. - -1. **No natural Python example exercises forward direction today**: The forward - direction (Phases 1–3) is correct and tested via mdtests, but currently no - Python code path conjoins argument-level concrete bounds with callable- - matching cross-typevar constraints into a single constraint set. This will - be exercised once the specialization builder migrates to maintaining a single - constraint set (tracked by the TODO in `add_type_mappings_from_constraint_set`). From 81d401f09f98b3bd49bcb13fdcb22d24ce010cfb Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Sun, 22 Mar 2026 10:38:08 -0400 Subject: [PATCH 17/22] prek!!! --- .../resources/mdtest/type_properties/implies_subtype_of.md | 7 ------- 1 file changed, 7 deletions(-) diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md b/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md index 6da5940f62fe2..94f2f7518e11f 100644 --- a/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md +++ b/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md @@ -885,41 +885,34 @@ def covariant_upper[B, S, U](): constraints = ConstraintSet.range(Never, B, S) & ConstraintSet.range(Never, U, Covariant[B]) static_assert(constraints.implies_subtype_of(U, Covariant[S])) - def covariant_lower[B, S, U](): # (S ≀ B) ∧ (Covariant[B] ≀ U) -> (Covariant[S] ≀ U) constraints = ConstraintSet.range(S, B, object) & ConstraintSet.range(Covariant[B], U, object) static_assert(constraints.implies_subtype_of(Covariant[S], U)) - def contravariant_upper[B, S, U](): # (S ≀ B) ∧ (U ≀ Contravariant[B]) -> (U ≀ Contravariant[S]) constraints = ConstraintSet.range(S, B, object) & ConstraintSet.range(Never, U, Contravariant[B]) static_assert(constraints.implies_subtype_of(U, Contravariant[S])) - def contravariant_lower[B, S, U](): # (B ≀ S) ∧ (Contravariant[B] ≀ U) -> (Contravariant[S] ≀ U) constraints = ConstraintSet.range(Never, B, S) & ConstraintSet.range(Contravariant[B], U, object) static_assert(constraints.implies_subtype_of(Contravariant[S], U)) - def invariant_upper_requires_equality[B, S, U](): # Invariant replacement only holds under equality constraints on B. constraints = ConstraintSet.range(S, B, S) & ConstraintSet.range(Never, U, Invariant[B]) static_assert(constraints.implies_subtype_of(U, Invariant[S])) - def invariant_lower_requires_equality[B, S, U](): constraints = ConstraintSet.range(S, B, S) & ConstraintSet.range(Invariant[B], U, object) static_assert(constraints.implies_subtype_of(Invariant[S], U)) - def invariant_upper_one_sided_is_not_enough[B, S, U](): constraints = ConstraintSet.range(Never, B, S) & ConstraintSet.range(Never, U, Invariant[B]) static_assert(not constraints.implies_subtype_of(U, Invariant[S])) - def invariant_lower_one_sided_is_not_enough[B, S, U](): constraints = ConstraintSet.range(S, B, object) & ConstraintSet.range(Invariant[B], U, object) static_assert(not constraints.implies_subtype_of(Invariant[S], U)) From ca9105aab3af32eb50ea46d31f0415a1027e9432 Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Mon, 23 Mar 2026 12:07:09 -0400 Subject: [PATCH 18/22] add mdtest for mypy positives --- .../resources/mdtest/bidirectional.md | 22 ++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) diff --git a/crates/ty_python_semantic/resources/mdtest/bidirectional.md b/crates/ty_python_semantic/resources/mdtest/bidirectional.md index 2cc55132621af..f6ad334c15e42 100644 --- a/crates/ty_python_semantic/resources/mdtest/bidirectional.md +++ b/crates/ty_python_semantic/resources/mdtest/bidirectional.md @@ -235,7 +235,9 @@ def _(xy: X | Y): The type context of all matching overloads are considered during argument inference: ```py -from typing import overload, TypedDict +from concurrent.futures import Future +from os.path import abspath +from typing import Awaitable, Callable, TypeVar, Union, overload, TypedDict def int_or_str() -> int | str: raise NotImplementedError @@ -330,6 +332,24 @@ def f7(y: object) -> object: # TODO: We should reveal `list[int | str]` here. x9 = f7(reveal_type(["Sheet1"])) # revealed: list[str] reveal_type(x9) # revealed: list[int | str] + +# TODO: We should not error here once call inference can conjoin constraints +# from all call arguments. +def f8(xs: tuple[str, ...]) -> tuple[str, ...]: + # error: [invalid-return-type] + return tuple(map(abspath, xs)) + +T2 = TypeVar("T2") + +def sink(func: Callable[[], Union[Awaitable[T2], T2]], future: Future[T2]) -> None: + raise NotImplementedError + +# TODO: This should not error once we conjoin constraints from all call arguments. +def f9(func: Callable[[], Union[Awaitable[T2], T2]]) -> Future[T2]: + future: Future[T2] = Future() + # error: [invalid-argument-type] + sink(func, future) + return future ``` ## Class constructor parameters From 58b656ec68b6c7bd55843b1cc232a19bfce0d201 Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Wed, 1 Apr 2026 12:22:10 -0400 Subject: [PATCH 19/22] document cheaper ALWAYS_TRUE check --- crates/ty_python_semantic/src/types/constraints.rs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index 556771c6c30e7..814d717beaabe 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -4500,8 +4500,10 @@ impl SequentMap { debug_assert!(!when.is_never_satisfied(db)); // Fast path: If L is trivially always assignable to U, there are no derived constraints - // that we can infer. (This would be handled correctly by the logic below, but this is a - // useful early return.) + // that we can infer. This would be handled correctly by the logic below, but this is a + // useful early return. Since we only use this check as an early return happy path, we can + // accept false negatives. That lets us use the simpler and cheaper check against + // ALWAYS_TRUE, rather than a more expensive is_always_satisfiable call. if when.node == ALWAYS_TRUE { return; } From aef66956c5ca151587eb71576681ef28d48ecfcb Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Wed, 1 Apr 2026 12:39:09 -0400 Subject: [PATCH 20/22] detect impossible pair implications --- .../type_properties/implies_subtype_of.md | 23 +++++++++++++++++++ .../src/types/constraints.rs | 10 ++++++++ 2 files changed, 33 insertions(+) diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md b/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md index 94f2f7518e11f..39ad0af97e5f7 100644 --- a/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md +++ b/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md @@ -1003,4 +1003,27 @@ def subclass_lower_bound[T, A](): static_assert(not constraints.implies_subtype_of(str, T)) ``` +### Transitivity should not introduce impossible constraints + +```py +from typing import Never, TypeVar, Union +from ty_extensions import ConstraintSet, static_assert + +def impossible_result[A, T, U](): + constraint_a = ConstraintSet.range(int, A, Union[T, U]) + constraint_t = ConstraintSet.range(Never, T, str) + constraint_u = ConstraintSet.range(Never, U, bytes) + + # Given (int ≀ A ≀ T | U), we can infer that (int ≀ T) ∨ (int ≀ U). If we intersect that with + # (T ≀ str), we get false ∨ (int ≀ U) β€” that is, there is no valid solution for T. Therefore A + # cannot be a subtype of T; it must be a subtype of U. + constraints = constraint_a & constraint_t + static_assert(constraints.implies_subtype_of(int, U)) + + # And if we intersect with (U ≀ bytes) as well, then there are no valid solutions for either T + # or U, and the constraint set as a whole becomes unsatisfiable. + constraints = constraint_a & constraint_t & constraint_u + static_assert(not constraints) +``` + [subtyping]: https://typing.python.org/en/latest/spec/concepts.html#subtype-supertype-and-type-equivalence diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index 814d717beaabe..8396eee5d0f8b 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -4386,6 +4386,16 @@ impl SequentMap { ante2: ConstraintId, post: ConstraintId, ) { + // If the post constraint is unsatisfiable, then the antecedents contradict each other. + let post_data = builder.constraint_data(post); + let when = post_data + .lower + .when_constraint_set_assignable_to(db, post_data.upper, builder); + if when.is_never_satisfied(db) { + self.add_pair_impossibility(db, builder, ante1, ante2); + return; + } + // If either antecedent implies the consequent on its own, this new sequent is redundant. if ante1.implies(db, builder, post) || ante2.implies(db, builder, post) { return; From ed74eac2c7f50ace9b85d3ffac6a498c4ab27d6b Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Wed, 1 Apr 2026 12:56:01 -0400 Subject: [PATCH 21/22] make specialization mapping robust to non-inferable constraint cycles --- crates/ty_python_semantic/src/types/generics.rs | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/crates/ty_python_semantic/src/types/generics.rs b/crates/ty_python_semantic/src/types/generics.rs index eae4880640996..6b93a41dff2dd 100644 --- a/crates/ty_python_semantic/src/types/generics.rs +++ b/crates/ty_python_semantic/src/types/generics.rs @@ -15,7 +15,7 @@ use crate::types::callable::walk_callable_type; use crate::types::class::ClassType; use crate::types::class_base::ClassBase; use crate::types::constraints::{ - ConstraintSet, ConstraintSetBuilder, IteratorConstraintsExtension, Solutions, + ConstraintSet, ConstraintSetBuilder, IteratorConstraintsExtension, PathBounds, Solutions, }; use crate::types::relation::{ DisjointnessChecker, HasRelationToVisitor, IsDisjointVisitor, TypeRelation, TypeRelationChecker, @@ -1760,12 +1760,19 @@ impl<'db, 'c> SpecializationBuilder<'db, 'c> { set: ConstraintSet<'db, 'c>, mut f: impl FnMut(TypeVarAssignment<'db>) -> Option>, ) -> Result<(), ()> { - let solutions = match set.solutions(self.db, self.constraints) { + let solutions = match set.solutions_with_inferable( + self.db, + self.constraints, + self.inferable, + |typevar, _variance, lower, upper| { + PathBounds::default_solve(self.db, typevar, lower, upper) + }, + ) { Solutions::Unsatisfiable => return Err(()), Solutions::Unconstrained => return Ok(()), Solutions::Constrained(solutions) => solutions, }; - for solution in solutions.iter() { + for solution in &solutions { for binding in solution { let variance = formal.variance_of(self.db, binding.bound_typevar); self.add_type_mapping(binding.bound_typevar, binding.solution, variance, &mut f); From 5354df9fedcfaa2bc1f04a6627eca2f647e5028f Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Wed, 1 Apr 2026 12:42:34 -0400 Subject: [PATCH 22/22] hoist intern_contraint_typevars call --- crates/ty_python_semantic/src/types/constraints.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index 8396eee5d0f8b..6e640bbc17743 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -1135,6 +1135,8 @@ impl<'db> Constraint<'db> { _ => {} } + builder.intern_constraint_typevars(db, typevar, lower, upper); + // If `lower β‰° upper` for every possible assignment of typevars, then the constraint cannot // be satisfied, since there is no type that is both greater than `lower`, and less than // `upper`. We use an existential check here ("is there *some* assignment where @@ -1147,8 +1149,6 @@ impl<'db> Constraint<'db> { return ALWAYS_FALSE; } - builder.intern_constraint_typevars(db, typevar, lower, upper); - // We have an (arbitrary) ordering for typevars. If the upper and/or lower bounds are // typevars, we have to ensure that the bounds are "later" according to that order than the // typevar being constrained.