diff --git a/crates/ty_python_semantic/resources/mdtest/annotations/self.md b/crates/ty_python_semantic/resources/mdtest/annotations/self.md
index 4d794fe6c4a49..8fc0802bac8c4 100644
--- a/crates/ty_python_semantic/resources/mdtest/annotations/self.md
+++ b/crates/ty_python_semantic/resources/mdtest/annotations/self.md
@@ -503,9 +503,11 @@ class C[T]():
     def f(self: Self):
         def b(x: Self):
             reveal_type(x)  # revealed: Self@f
-        reveal_type(generic_context(b))  # revealed: None
+        # revealed: None
+        reveal_type(generic_context(b))
 
-reveal_type(generic_context(C.f))  # revealed: tuple[Self@f]
+# revealed: ty_extensions.GenericContext[Self@f]
+reveal_type(generic_context(C.f))
 ```
 
 Even if the `Self` annotation appears first in the nested function, it is the method that binds
@@ -519,9 +521,11 @@ class C:
     def f(self: "C"):
         def b(x: Self):
             reveal_type(x)  # revealed: Self@f
-        reveal_type(generic_context(b))  # revealed: None
+        # revealed: None
+        reveal_type(generic_context(b))
 
-reveal_type(generic_context(C.f))  # revealed: None
+# revealed: None
+reveal_type(generic_context(C.f))
 ```
 
 ## Non-positional first parameters
diff --git a/crates/ty_python_semantic/resources/mdtest/generics/legacy/classes.md b/crates/ty_python_semantic/resources/mdtest/generics/legacy/classes.md
index 7ba6803ddae20..fcfa28953e182 100644
--- a/crates/ty_python_semantic/resources/mdtest/generics/legacy/classes.md
+++ b/crates/ty_python_semantic/resources/mdtest/generics/legacy/classes.md
@@ -21,14 +21,14 @@ class TypeVarAndParamSpec(Generic[P, T]): ...
 class SingleTypeVarTuple(Generic[Unpack[Ts]]): ...
 class TypeVarAndTypeVarTuple(Generic[T, Unpack[Ts]]): ...
 
-# revealed: tuple[T@SingleTypevar]
+# revealed: ty_extensions.GenericContext[T@SingleTypevar]
 reveal_type(generic_context(SingleTypevar))
-# revealed: tuple[T@MultipleTypevars, S@MultipleTypevars]
+# revealed: ty_extensions.GenericContext[T@MultipleTypevars, S@MultipleTypevars]
 reveal_type(generic_context(MultipleTypevars))
 
-# revealed: tuple[P@SingleParamSpec]
+# revealed: ty_extensions.GenericContext[P@SingleParamSpec]
 reveal_type(generic_context(SingleParamSpec))
-# revealed: tuple[P@TypeVarAndParamSpec, T@TypeVarAndParamSpec]
+# revealed: ty_extensions.GenericContext[P@TypeVarAndParamSpec, T@TypeVarAndParamSpec]
 reveal_type(generic_context(TypeVarAndParamSpec))
 
 # TODO: support `TypeVarTuple` properly (these should not reveal `None`)
@@ -66,9 +66,9 @@ class InheritedGeneric(MultipleTypevars[T, S]): ...
 class InheritedGenericPartiallySpecialized(MultipleTypevars[T, int]): ...
 class InheritedGenericFullySpecialized(MultipleTypevars[str, int]): ...
 
-# revealed: tuple[T@InheritedGeneric, S@InheritedGeneric]
+# revealed: ty_extensions.GenericContext[T@InheritedGeneric, S@InheritedGeneric]
 reveal_type(generic_context(InheritedGeneric))
-# revealed: tuple[T@InheritedGenericPartiallySpecialized]
+# revealed: ty_extensions.GenericContext[T@InheritedGenericPartiallySpecialized]
 reveal_type(generic_context(InheritedGenericPartiallySpecialized))
 # revealed: None
 reveal_type(generic_context(InheritedGenericFullySpecialized))
@@ -90,7 +90,7 @@ class OuterClass(Generic[T]):
         # revealed: None
         reveal_type(generic_context(InnerClassInMethod))
 
-# revealed: tuple[T@OuterClass]
+# revealed: ty_extensions.GenericContext[T@OuterClass]
 reveal_type(generic_context(OuterClass))
 ```
 
@@ -118,11 +118,11 @@ class ExplicitInheritedGenericPartiallySpecializedExtraTypevar(MultipleTypevars[
 # error: [invalid-generic-class] "`Generic` base class must include all type variables used in other base classes"
 class ExplicitInheritedGenericPartiallySpecializedMissingTypevar(MultipleTypevars[T, int], Generic[S]): ...
 
-# revealed: tuple[T@ExplicitInheritedGeneric, S@ExplicitInheritedGeneric]
+# revealed: ty_extensions.GenericContext[T@ExplicitInheritedGeneric, S@ExplicitInheritedGeneric]
 reveal_type(generic_context(ExplicitInheritedGeneric))
-# revealed: tuple[T@ExplicitInheritedGenericPartiallySpecialized]
+# revealed: ty_extensions.GenericContext[T@ExplicitInheritedGenericPartiallySpecialized]
 reveal_type(generic_context(ExplicitInheritedGenericPartiallySpecialized))
-# revealed: tuple[T@ExplicitInheritedGenericPartiallySpecializedExtraTypevar, S@ExplicitInheritedGenericPartiallySpecializedExtraTypevar]
+# revealed: ty_extensions.GenericContext[T@ExplicitInheritedGenericPartiallySpecializedExtraTypevar, S@ExplicitInheritedGenericPartiallySpecializedExtraTypevar]
 reveal_type(generic_context(ExplicitInheritedGenericPartiallySpecializedExtraTypevar))
 ```
 
@@ -594,18 +594,27 @@ class C(Generic[T]):
     def generic_method(self, t: T, u: U) -> U:
         return u
 
-reveal_type(generic_context(C))  # revealed: tuple[T@C]
-reveal_type(generic_context(C.method))  # revealed: tuple[Self@method]
-reveal_type(generic_context(C.generic_method))  # revealed: tuple[Self@generic_method, U@generic_method]
-reveal_type(generic_context(C[int]))  # revealed: None
-reveal_type(generic_context(C[int].method))  # revealed: tuple[Self@method]
-reveal_type(generic_context(C[int].generic_method))  # revealed: tuple[Self@generic_method, U@generic_method]
+# revealed: ty_extensions.GenericContext[T@C]
+reveal_type(generic_context(C))
+# revealed: ty_extensions.GenericContext[Self@method]
+reveal_type(generic_context(C.method))
+# revealed: ty_extensions.GenericContext[Self@generic_method, U@generic_method]
+reveal_type(generic_context(C.generic_method))
+# revealed: None
+reveal_type(generic_context(C[int]))
+# revealed: ty_extensions.GenericContext[Self@method]
+reveal_type(generic_context(C[int].method))
+# revealed: ty_extensions.GenericContext[Self@generic_method, U@generic_method]
+reveal_type(generic_context(C[int].generic_method))
 
 c: C[int] = C[int]()
 reveal_type(c.generic_method(1, "string"))  # revealed: Literal["string"]
-reveal_type(generic_context(c))  # revealed: None
-reveal_type(generic_context(c.method))  # revealed: tuple[Self@method]
-reveal_type(generic_context(c.generic_method))  # revealed: tuple[Self@generic_method, U@generic_method]
+# revealed: None
+reveal_type(generic_context(c))
+# revealed: ty_extensions.GenericContext[Self@method]
+reveal_type(generic_context(c.method))
+# revealed: ty_extensions.GenericContext[Self@generic_method, U@generic_method]
+reveal_type(generic_context(c.generic_method))
 ```
 
 ## Specializations propagate
diff --git a/crates/ty_python_semantic/resources/mdtest/generics/pep695/aliases.md b/crates/ty_python_semantic/resources/mdtest/generics/pep695/aliases.md
index 3191cf56834e2..d32029311a175 100644
--- a/crates/ty_python_semantic/resources/mdtest/generics/pep695/aliases.md
+++ b/crates/ty_python_semantic/resources/mdtest/generics/pep695/aliases.md
@@ -20,17 +20,21 @@ type TypeVarAndParamSpec[T, **P] = ...
 type SingleTypeVarTuple[*Ts] = ...
 type TypeVarAndTypeVarTuple[T, *Ts] = ...
 
-# revealed: tuple[T@SingleTypevar]
+# revealed: ty_extensions.GenericContext[T@SingleTypevar]
 reveal_type(generic_context(SingleTypevar))
-# revealed: tuple[T@MultipleTypevars, S@MultipleTypevars]
+# revealed: ty_extensions.GenericContext[T@MultipleTypevars, S@MultipleTypevars]
 reveal_type(generic_context(MultipleTypevars))
 
 # TODO: support `ParamSpec`/`TypeVarTuple` properly
 # (these should include the `ParamSpec`s and `TypeVarTuple`s in their generic contexts)
-reveal_type(generic_context(SingleParamSpec))  # revealed: tuple[()]
-reveal_type(generic_context(TypeVarAndParamSpec))  # revealed: tuple[T@TypeVarAndParamSpec]
-reveal_type(generic_context(SingleTypeVarTuple))  # revealed: tuple[()]
-reveal_type(generic_context(TypeVarAndTypeVarTuple))  # revealed: tuple[T@TypeVarAndTypeVarTuple]
+# revealed: ty_extensions.GenericContext[]
+reveal_type(generic_context(SingleParamSpec))
+# revealed: ty_extensions.GenericContext[T@TypeVarAndParamSpec]
+reveal_type(generic_context(TypeVarAndParamSpec))
+# revealed: ty_extensions.GenericContext[]
+reveal_type(generic_context(SingleTypeVarTuple))
+# revealed: ty_extensions.GenericContext[T@TypeVarAndTypeVarTuple]
+reveal_type(generic_context(TypeVarAndTypeVarTuple))
 ```
 
 You cannot use the same typevar more than once.
diff --git a/crates/ty_python_semantic/resources/mdtest/generics/pep695/classes.md b/crates/ty_python_semantic/resources/mdtest/generics/pep695/classes.md
index 5393d622f59c8..a701c0fcacc2b 100644
--- a/crates/ty_python_semantic/resources/mdtest/generics/pep695/classes.md
+++ b/crates/ty_python_semantic/resources/mdtest/generics/pep695/classes.md
@@ -20,17 +20,21 @@ class TypeVarAndParamSpec[T, **P]: ...
 class SingleTypeVarTuple[*Ts]: ...
 class TypeVarAndTypeVarTuple[T, *Ts]: ...
 
-# revealed: tuple[T@SingleTypevar]
+# revealed: ty_extensions.GenericContext[T@SingleTypevar]
 reveal_type(generic_context(SingleTypevar))
-# revealed: tuple[T@MultipleTypevars, S@MultipleTypevars]
+# revealed: ty_extensions.GenericContext[T@MultipleTypevars, S@MultipleTypevars]
 reveal_type(generic_context(MultipleTypevars))
 
 # TODO: support `ParamSpec`/`TypeVarTuple` properly
 # (these should include the `ParamSpec`s and `TypeVarTuple`s in their generic contexts)
-reveal_type(generic_context(SingleParamSpec))  # revealed: tuple[()]
-reveal_type(generic_context(TypeVarAndParamSpec))  # revealed: tuple[T@TypeVarAndParamSpec]
-reveal_type(generic_context(SingleTypeVarTuple))  # revealed: tuple[()]
-reveal_type(generic_context(TypeVarAndTypeVarTuple))  # revealed: tuple[T@TypeVarAndTypeVarTuple]
+# revealed: ty_extensions.GenericContext[]
+reveal_type(generic_context(SingleParamSpec))
+# revealed: ty_extensions.GenericContext[T@TypeVarAndParamSpec]
+reveal_type(generic_context(TypeVarAndParamSpec))
+# revealed: ty_extensions.GenericContext[]
+reveal_type(generic_context(SingleTypeVarTuple))
+# revealed: ty_extensions.GenericContext[T@TypeVarAndTypeVarTuple]
+reveal_type(generic_context(TypeVarAndTypeVarTuple))
 ```
 
 You cannot use the same typevar more than once.
@@ -49,9 +53,9 @@ class InheritedGeneric[U, V](MultipleTypevars[U, V]): ...
 class InheritedGenericPartiallySpecialized[U](MultipleTypevars[U, int]): ...
 class InheritedGenericFullySpecialized(MultipleTypevars[str, int]): ...
 
-# revealed: tuple[U@InheritedGeneric, V@InheritedGeneric]
+# revealed: ty_extensions.GenericContext[U@InheritedGeneric, V@InheritedGeneric]
 reveal_type(generic_context(InheritedGeneric))
-# revealed: tuple[U@InheritedGenericPartiallySpecialized]
+# revealed: ty_extensions.GenericContext[U@InheritedGenericPartiallySpecialized]
 reveal_type(generic_context(InheritedGenericPartiallySpecialized))
 # revealed: None
 reveal_type(generic_context(InheritedGenericFullySpecialized))
@@ -64,7 +68,8 @@ the inheriting class generic.
 ```py
 class InheritedGenericDefaultSpecialization(MultipleTypevars): ...
 
-reveal_type(generic_context(InheritedGenericDefaultSpecialization))  # revealed: None
+# revealed: None
+reveal_type(generic_context(InheritedGenericDefaultSpecialization))
 ```
 
 You cannot use PEP-695 syntax and the legacy syntax in the same class definition.
@@ -512,18 +517,27 @@ class C[T]:
     # TODO: error
     def cannot_shadow_class_typevar[T](self, t: T): ...
 
-reveal_type(generic_context(C))  # revealed: tuple[T@C]
-reveal_type(generic_context(C.method))  # revealed: tuple[Self@method]
-reveal_type(generic_context(C.generic_method))  # revealed: tuple[Self@generic_method, U@generic_method]
-reveal_type(generic_context(C[int]))  # revealed: None
-reveal_type(generic_context(C[int].method))  # revealed: tuple[Self@method]
-reveal_type(generic_context(C[int].generic_method))  # revealed: tuple[Self@generic_method, U@generic_method]
+# revealed: ty_extensions.GenericContext[T@C]
+reveal_type(generic_context(C))
+# revealed: ty_extensions.GenericContext[Self@method]
+reveal_type(generic_context(C.method))
+# revealed: ty_extensions.GenericContext[Self@generic_method, U@generic_method]
+reveal_type(generic_context(C.generic_method))
+# revealed: None
+reveal_type(generic_context(C[int]))
+# revealed: ty_extensions.GenericContext[Self@method]
+reveal_type(generic_context(C[int].method))
+# revealed: ty_extensions.GenericContext[Self@generic_method, U@generic_method]
+reveal_type(generic_context(C[int].generic_method))
 
 c: C[int] = C[int]()
 reveal_type(c.generic_method(1, "string"))  # revealed: Literal["string"]
-reveal_type(generic_context(c))  # revealed: None
-reveal_type(generic_context(c.method))  # revealed: tuple[Self@method]
-reveal_type(generic_context(c.generic_method))  # revealed: tuple[Self@generic_method, U@generic_method]
+# revealed: None
+reveal_type(generic_context(c))
+# revealed: ty_extensions.GenericContext[Self@method]
+reveal_type(generic_context(c.method))
+# revealed: ty_extensions.GenericContext[Self@generic_method, U@generic_method]
+reveal_type(generic_context(c.generic_method))
 ```
 
 ## Specializations propagate
diff --git a/crates/ty_python_semantic/resources/mdtest/generics/scoping.md b/crates/ty_python_semantic/resources/mdtest/generics/scoping.md
index 79944b263aff3..31c04e0b37dce 100644
--- a/crates/ty_python_semantic/resources/mdtest/generics/scoping.md
+++ b/crates/ty_python_semantic/resources/mdtest/generics/scoping.md
@@ -154,8 +154,10 @@ from ty_extensions import generic_context
 
 legacy.m("string", None)  # error: [invalid-argument-type]
 reveal_type(legacy.m)  # revealed: bound method Legacy[int].m[S](x: int, y: S@m) -> S@m
-reveal_type(generic_context(Legacy))  # revealed: tuple[T@Legacy]
-reveal_type(generic_context(legacy.m))  # revealed: tuple[Self@m, S@m]
+# revealed: ty_extensions.GenericContext[T@Legacy]
+reveal_type(generic_context(Legacy))
+# revealed: ty_extensions.GenericContext[Self@m, S@m]
+reveal_type(generic_context(legacy.m))
 ```
 
 With PEP 695 syntax, it is clearer that the method uses a separate typevar:
diff --git a/crates/ty_python_semantic/resources/mdtest/generics/specialize_constrained.md b/crates/ty_python_semantic/resources/mdtest/generics/specialize_constrained.md
new file mode 100644
index 0000000000000..22210f88d2b05
--- /dev/null
+++ b/crates/ty_python_semantic/resources/mdtest/generics/specialize_constrained.md
@@ -0,0 +1,305 @@
+# Creating a specialization from a constraint set
+
+```toml
+[environment]
+python-version = "3.12"
+```
+
+We create constraint sets to describe which types a set of typevars can specialize to. We have a
+`specialize_constrained` method that creates a "best" specialization for a constraint set, which
+lets us test this logic in isolation, without having to bring in the rest of the specialization
+inference logic.
+
+## Unbounded typevars
+
+An unbounded typevar can specialize to any type. We will specialize the typevar to the least upper
+bound of all of the types that satisfy the constraint set.
+
+```py
+from typing import Never
+from ty_extensions import ConstraintSet, generic_context
+
+# fmt: off
+
+def unbounded[T]():
+    # revealed: ty_extensions.Specialization[T@unbounded = object]
+    reveal_type(generic_context(unbounded).specialize_constrained(ConstraintSet.always()))
+    # revealed: None
+    reveal_type(generic_context(unbounded).specialize_constrained(ConstraintSet.never()))
+
+    # revealed: ty_extensions.Specialization[T@unbounded = int]
+    reveal_type(generic_context(unbounded).specialize_constrained(ConstraintSet.range(Never, T, int)))
+    # revealed: ty_extensions.Specialization[T@unbounded = int]
+    reveal_type(generic_context(unbounded).specialize_constrained(ConstraintSet.range(bool, T, int)))
+
+    # revealed: ty_extensions.Specialization[T@unbounded = bool]
+    reveal_type(generic_context(unbounded).specialize_constrained(ConstraintSet.range(Never, T, int) & ConstraintSet.range(Never, T, bool)))
+    # revealed: ty_extensions.Specialization[T@unbounded = Never]
+    reveal_type(generic_context(unbounded).specialize_constrained(ConstraintSet.range(Never, T, int) & ConstraintSet.range(Never, T, str)))
+    # revealed: None
+    reveal_type(generic_context(unbounded).specialize_constrained(ConstraintSet.range(bool, T, bool) & ConstraintSet.range(Never, T, str)))
+
+    # revealed: ty_extensions.Specialization[T@unbounded = int]
+    reveal_type(generic_context(unbounded).specialize_constrained(ConstraintSet.range(Never, T, int) | ConstraintSet.range(Never, T, bool)))
+    # revealed: ty_extensions.Specialization[T@unbounded = Never]
+    reveal_type(generic_context(unbounded).specialize_constrained(ConstraintSet.range(Never, T, int) | ConstraintSet.range(Never, T, str)))
+    # revealed: None
+    reveal_type(generic_context(unbounded).specialize_constrained(ConstraintSet.range(bool, T, bool) | ConstraintSet.range(Never, T, str)))
+```
+
+## Typevar with an upper bound
+
+If a typevar has an upper bound, then it must specialize to a type that is a subtype of that bound.
+
+```py
+from typing import final, Never
+from ty_extensions import ConstraintSet, generic_context
+
+class Super: ...
+class Base(Super): ...
+class Sub(Base): ...
+
+@final
+class Unrelated: ...
+
+def bounded[T: Base]():
+    # revealed: ty_extensions.Specialization[T@bounded = Base]
+    reveal_type(generic_context(bounded).specialize_constrained(ConstraintSet.always()))
+    # revealed: None
+    reveal_type(generic_context(bounded).specialize_constrained(ConstraintSet.never()))
+
+    # revealed: ty_extensions.Specialization[T@bounded = Base]
+    reveal_type(generic_context(bounded).specialize_constrained(ConstraintSet.range(Never, T, Super)))
+    # revealed: ty_extensions.Specialization[T@bounded = Base]
+    reveal_type(generic_context(bounded).specialize_constrained(ConstraintSet.range(Never, T, Base)))
+    # revealed: ty_extensions.Specialization[T@bounded = Sub]
+    reveal_type(generic_context(bounded).specialize_constrained(ConstraintSet.range(Never, T, Sub)))
+
+    # revealed: ty_extensions.Specialization[T@bounded = Never]
+    reveal_type(generic_context(bounded).specialize_constrained(ConstraintSet.range(Never, T, Unrelated)))
+    # revealed: None
+    reveal_type(generic_context(bounded).specialize_constrained(ConstraintSet.range(Unrelated, T, Unrelated)))
+```
+
+If the upper bound is a gradual type, we are free to choose any materialization of the upper bound
+that makes the test succeed.
+
+```py
+from typing import Any
+
+def bounded_by_gradual[T: Any]():
+    # revealed: ty_extensions.Specialization[T@bounded_by_gradual = object]
+    reveal_type(generic_context(bounded_by_gradual).specialize_constrained(ConstraintSet.always()))
+    # revealed: None
+    reveal_type(generic_context(bounded_by_gradual).specialize_constrained(ConstraintSet.never()))
+
+    # revealed: ty_extensions.Specialization[T@bounded_by_gradual = Base]
+    reveal_type(generic_context(bounded_by_gradual).specialize_constrained(ConstraintSet.range(Never, T, Base)))
+
+    # revealed: ty_extensions.Specialization[T@bounded_by_gradual = Unrelated]
+    reveal_type(generic_context(bounded_by_gradual).specialize_constrained(ConstraintSet.range(Never, T, Unrelated)))
+
+def bounded_by_gradual_list[T: list[Any]]():
+    # revealed: ty_extensions.Specialization[T@bounded_by_gradual_list = Top[list[Any]]]
+    reveal_type(generic_context(bounded_by_gradual_list).specialize_constrained(ConstraintSet.always()))
+    # revealed: None
+    reveal_type(generic_context(bounded_by_gradual_list).specialize_constrained(ConstraintSet.never()))
+
+    # revealed: ty_extensions.Specialization[T@bounded_by_gradual_list = list[Base]]
+    reveal_type(generic_context(bounded_by_gradual_list).specialize_constrained(ConstraintSet.range(Never, T, list[Base])))
+
+    # revealed: ty_extensions.Specialization[T@bounded_by_gradual_list = list[Unrelated]]
+    reveal_type(generic_context(bounded_by_gradual_list).specialize_constrained(ConstraintSet.range(Never, T, list[Unrelated])))
+```
+
+## Constrained typevar
+
+If a typevar has constraints, then it must specialize to one of those specific types. (Not to a
+subtype of one of those types!)
+
+In particular, note that if a constraint set is satisfied by more than one of the typevar's
+constraints (i.e., we have no reason to prefer one over the others), then we return `None` to
+indicate an ambiguous result. We could, in theory, return _more than one_ specialization, since we
+have all of the information necessary to produce this. But it's not clear what we would do with that
+information at the moment.
+
+```py
+from typing import final, Never
+from ty_extensions import ConstraintSet, generic_context
+
+class Super: ...
+class Base(Super): ...
+class Sub(Base): ...
+
+@final
+class Unrelated: ...
+
+def constrained[T: (Base, Unrelated)]():
+    # revealed: None
+    reveal_type(generic_context(constrained).specialize_constrained(ConstraintSet.always()))
+    # revealed: None
+    reveal_type(generic_context(constrained).specialize_constrained(ConstraintSet.never()))
+
+    # revealed: ty_extensions.Specialization[T@constrained = Base]
+    reveal_type(generic_context(constrained).specialize_constrained(ConstraintSet.range(Never, T, Base)))
+    # revealed: ty_extensions.Specialization[T@constrained = Unrelated]
+    reveal_type(generic_context(constrained).specialize_constrained(ConstraintSet.range(Never, T, Unrelated)))
+
+    # revealed: ty_extensions.Specialization[T@constrained = Base]
+    reveal_type(generic_context(constrained).specialize_constrained(ConstraintSet.range(Never, T, Super)))
+    # revealed: None
+    reveal_type(generic_context(constrained).specialize_constrained(ConstraintSet.range(Super, T, Super)))
+
+    # revealed: ty_extensions.Specialization[T@constrained = Base]
+    reveal_type(generic_context(constrained).specialize_constrained(ConstraintSet.range(Sub, T, object)))
+    # revealed: None
+    reveal_type(generic_context(constrained).specialize_constrained(ConstraintSet.range(Sub, T, Sub)))
+```
+
+If any of the constraints is a gradual type, we are free to choose any materialization of that
+constraint that makes the test succeed.
+
+TODO: At the moment, we are producing a specialization that shows which particular materialization
+that we chose, but really, we should be returning the gradual constraint as the specialization.
+
+```py
+from typing import Any
+
+# fmt: off
+
+def constrained_by_gradual[T: (Base, Any)]():
+    # TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = Any]
+    # revealed: ty_extensions.Specialization[T@constrained_by_gradual = object]
+    reveal_type(generic_context(constrained_by_gradual).specialize_constrained(ConstraintSet.always()))
+    # revealed: None
+    reveal_type(generic_context(constrained_by_gradual).specialize_constrained(ConstraintSet.never()))
+
+    # revealed: ty_extensions.Specialization[T@constrained_by_gradual = Base]
+    reveal_type(generic_context(constrained_by_gradual).specialize_constrained(ConstraintSet.range(Never, T, Base)))
+    # TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = Any]
+    # revealed: ty_extensions.Specialization[T@constrained_by_gradual = Unrelated]
+    reveal_type(generic_context(constrained_by_gradual).specialize_constrained(ConstraintSet.range(Never, T, Unrelated)))
+
+    # TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = Any]
+    # revealed: ty_extensions.Specialization[T@constrained_by_gradual = Super]
+    reveal_type(generic_context(constrained_by_gradual).specialize_constrained(ConstraintSet.range(Never, T, Super)))
+    # TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = Any]
+    # revealed: ty_extensions.Specialization[T@constrained_by_gradual = Super]
+    reveal_type(generic_context(constrained_by_gradual).specialize_constrained(ConstraintSet.range(Super, T, Super)))
+
+    # TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = Any]
+    # revealed: ty_extensions.Specialization[T@constrained_by_gradual = object]
+    reveal_type(generic_context(constrained_by_gradual).specialize_constrained(ConstraintSet.range(Sub, T, object)))
+    # TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = Any]
+    # revealed: ty_extensions.Specialization[T@constrained_by_gradual = Sub]
+    reveal_type(generic_context(constrained_by_gradual).specialize_constrained(ConstraintSet.range(Sub, T, Sub)))
+
+def constrained_by_two_gradual[T: (Any, Any)]():
+    # TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = Any]
+    # revealed: ty_extensions.Specialization[T@constrained_by_two_gradual = object]
+    reveal_type(generic_context(constrained_by_two_gradual).specialize_constrained(ConstraintSet.always()))
+    # revealed: None
+    reveal_type(generic_context(constrained_by_two_gradual).specialize_constrained(ConstraintSet.never()))
+
+    # TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = Any]
+    # revealed: ty_extensions.Specialization[T@constrained_by_two_gradual = Base]
+    reveal_type(generic_context(constrained_by_two_gradual).specialize_constrained(ConstraintSet.range(Never, T, Base)))
+    # TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = Any]
+    # revealed: ty_extensions.Specialization[T@constrained_by_two_gradual = Unrelated]
+    reveal_type(generic_context(constrained_by_two_gradual).specialize_constrained(ConstraintSet.range(Never, T, Unrelated)))
+
+    # TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = Any]
+    # revealed: ty_extensions.Specialization[T@constrained_by_two_gradual = Super]
+    reveal_type(generic_context(constrained_by_two_gradual).specialize_constrained(ConstraintSet.range(Never, T, Super)))
+    # TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = Any]
+    # revealed: ty_extensions.Specialization[T@constrained_by_two_gradual = Super]
+    reveal_type(generic_context(constrained_by_two_gradual).specialize_constrained(ConstraintSet.range(Super, T, Super)))
+
+    # TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = Any]
+    # revealed: ty_extensions.Specialization[T@constrained_by_two_gradual = object]
+    reveal_type(generic_context(constrained_by_two_gradual).specialize_constrained(ConstraintSet.range(Sub, T, object)))
+    # TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = Any]
+    # revealed: ty_extensions.Specialization[T@constrained_by_two_gradual = Sub]
+    reveal_type(generic_context(constrained_by_two_gradual).specialize_constrained(ConstraintSet.range(Sub, T, Sub)))
+
+def constrained_by_gradual_list[T: (list[Base], list[Any])]():
+    # revealed: ty_extensions.Specialization[T@constrained_by_gradual_list = list[Base]]
+    reveal_type(generic_context(constrained_by_gradual_list).specialize_constrained(ConstraintSet.always()))
+    # revealed: None
+    reveal_type(generic_context(constrained_by_gradual_list).specialize_constrained(ConstraintSet.never()))
+
+    # revealed: ty_extensions.Specialization[T@constrained_by_gradual_list = list[Base]]
+    reveal_type(generic_context(constrained_by_gradual_list).specialize_constrained(ConstraintSet.range(Never, T, list[Base])))
+    # TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = list[Any]]
+    # revealed: ty_extensions.Specialization[T@constrained_by_gradual_list = list[Unrelated]]
+    reveal_type(generic_context(constrained_by_gradual_list).specialize_constrained(ConstraintSet.range(Never, T, list[Unrelated])))
+
+    # TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = list[Any]]
+    # revealed: ty_extensions.Specialization[T@constrained_by_gradual_list = list[Super]]
+    reveal_type(generic_context(constrained_by_gradual_list).specialize_constrained(ConstraintSet.range(Never, T, list[Super])))
+    # TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = list[Any]]
+    # revealed: ty_extensions.Specialization[T@constrained_by_gradual_list = list[Super]]
+    reveal_type(generic_context(constrained_by_gradual_list).specialize_constrained(ConstraintSet.range(list[Super], T, list[Super])))
+    # TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = list[Any]]
+    # revealed: ty_extensions.Specialization[T@constrained_by_gradual_list = list[Sub]]
+    reveal_type(generic_context(constrained_by_gradual_list).specialize_constrained(ConstraintSet.range(list[Sub], T, list[Sub])))
+
+def constrained_by_two_gradual_lists[T: (list[Any], list[Any])]():
+    # TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = list[Any]]
+    # revealed: ty_extensions.Specialization[T@constrained_by_two_gradual_lists = Top[list[Any]]]
+    reveal_type(generic_context(constrained_by_two_gradual_lists).specialize_constrained(ConstraintSet.always()))
+    # revealed: None
+    reveal_type(generic_context(constrained_by_two_gradual_lists).specialize_constrained(ConstraintSet.never()))
+
+    # TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = list[Any]]
+    # revealed: ty_extensions.Specialization[T@constrained_by_two_gradual_lists = list[Base]]
+    reveal_type(generic_context(constrained_by_two_gradual_lists).specialize_constrained(ConstraintSet.range(Never, T, list[Base])))
+    # TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = list[Any]]
+    # revealed: ty_extensions.Specialization[T@constrained_by_two_gradual_lists = list[Unrelated]]
+    reveal_type(generic_context(constrained_by_two_gradual_lists).specialize_constrained(ConstraintSet.range(Never, T, list[Unrelated])))
+
+    # TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = list[Any]]
+    # revealed: ty_extensions.Specialization[T@constrained_by_two_gradual_lists = list[Super]]
+    reveal_type(generic_context(constrained_by_two_gradual_lists).specialize_constrained(ConstraintSet.range(Never, T, list[Super])))
+    # TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = list[Any]]
+    # revealed: ty_extensions.Specialization[T@constrained_by_two_gradual_lists = list[Super]]
+    reveal_type(generic_context(constrained_by_two_gradual_lists).specialize_constrained(ConstraintSet.range(list[Super], T, list[Super])))
+    # TODO: revealed: ty_extensions.Specialization[T@constrained_by_gradual = list[Any]]
+    # revealed: ty_extensions.Specialization[T@constrained_by_two_gradual_lists = list[Sub]]
+    reveal_type(generic_context(constrained_by_two_gradual_lists).specialize_constrained(ConstraintSet.range(list[Sub], T, list[Sub])))
+```
+
+## Mutually constrained typevars
+
+If one typevar is constrained by another, the specialization of one can affect the specialization of
+the other.
+
+```py
+from typing import final, Never
+from ty_extensions import ConstraintSet, generic_context
+
+class Super: ...
+class Base(Super): ...
+class Sub(Base): ...
+
+@final
+class Unrelated: ...
+
+# fmt: off
+
+def mutually_bound[T: Base, U]():
+    # revealed: ty_extensions.Specialization[T@mutually_bound = Base, U@mutually_bound = object]
+    reveal_type(generic_context(mutually_bound).specialize_constrained(ConstraintSet.always()))
+    # revealed: None
+    reveal_type(generic_context(mutually_bound).specialize_constrained(ConstraintSet.never()))
+
+    # revealed: ty_extensions.Specialization[T@mutually_bound = Base, U@mutually_bound = Base]
+    reveal_type(generic_context(mutually_bound).specialize_constrained(ConstraintSet.range(Never, U, T)))
+
+    # revealed: ty_extensions.Specialization[T@mutually_bound = Sub, U@mutually_bound = object]
+    reveal_type(generic_context(mutually_bound).specialize_constrained(ConstraintSet.range(Never, T, Sub)))
+    # revealed: ty_extensions.Specialization[T@mutually_bound = Sub, U@mutually_bound = Sub]
+    reveal_type(generic_context(mutually_bound).specialize_constrained(ConstraintSet.range(Never, T, Sub) & ConstraintSet.range(Never, U, T)))
+    # revealed: ty_extensions.Specialization[T@mutually_bound = Base, U@mutually_bound = Sub]
+    reveal_type(generic_context(mutually_bound).specialize_constrained(ConstraintSet.range(Never, U, Sub) & ConstraintSet.range(Never, U, T)))
+```
diff --git a/crates/ty_python_semantic/src/types.rs b/crates/ty_python_semantic/src/types.rs
index f036090cd727e..67a598ab617e0 100644
--- a/crates/ty_python_semantic/src/types.rs
+++ b/crates/ty_python_semantic/src/types.rs
@@ -4433,6 +4433,14 @@ impl<'db> Type<'db> {
                 ))
                 .into()
             }
+            Type::KnownInstance(KnownInstanceType::GenericContext(tracked))
+                if name == "specialize_constrained" =>
+            {
+                Place::bound(Type::KnownBoundMethod(
+                    KnownBoundMethodType::GenericContextSpecializeConstrained(tracked),
+                ))
+                .into()
+            }
 
             Type::ClassLiteral(class)
                 if name == "__get__" && class.is_known(db, KnownClass::FunctionType) =>
@@ -6712,6 +6720,14 @@ impl<'db> Type<'db> {
                     invalid_expressions: smallvec::smallvec![InvalidTypeExpression::ConstraintSet],
                     fallback_type: Type::unknown(),
                 }),
+                KnownInstanceType::GenericContext(__call__) => Err(InvalidTypeExpressionError {
+                    invalid_expressions: smallvec::smallvec![InvalidTypeExpression::GenericContext],
+                    fallback_type: Type::unknown(),
+                }),
+                KnownInstanceType::Specialization(__call__) => Err(InvalidTypeExpressionError {
+                    invalid_expressions: smallvec::smallvec![InvalidTypeExpression::Specialization],
+                    fallback_type: Type::unknown(),
+                }),
                 KnownInstanceType::SubscriptedProtocol(_) => Err(InvalidTypeExpressionError {
                     invalid_expressions: smallvec::smallvec_inline![
                         InvalidTypeExpression::Protocol
@@ -7287,6 +7303,7 @@ impl<'db> Type<'db> {
                 | KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)
                 | KnownBoundMethodType::ConstraintSetSatisfies(_)
                 | KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_)
+                | KnownBoundMethodType::GenericContextSpecializeConstrained(_)
             )
             | Type::DataclassDecorator(_)
             | Type::DataclassTransformer(_)
@@ -7446,7 +7463,8 @@ impl<'db> Type<'db> {
                 | KnownBoundMethodType::ConstraintSetNever
                 | KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)
                 | KnownBoundMethodType::ConstraintSetSatisfies(_)
-                | KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_),
+                | KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_)
+                | KnownBoundMethodType::GenericContextSpecializeConstrained(_),
             )
             | Type::DataclassDecorator(_)
             | Type::DataclassTransformer(_)
@@ -7978,6 +7996,14 @@ pub enum KnownInstanceType<'db> {
     /// `ty_extensions.ConstraintSet`.
     ConstraintSet(TrackedConstraintSet<'db>),
 
+    /// A generic context, which is exposed in mdtests as an instance of
+    /// `ty_extensions.GenericContext`.
+    GenericContext(GenericContext<'db>),
+
+    /// A specialization, which is exposed in mdtests as an instance of
+    /// `ty_extensions.Specialization`.
+    Specialization(Specialization<'db>),
+
     /// A single instance of `types.UnionType`, which stores the left- and
     /// right-hand sides of a PEP 604 union.
     UnionType(InternedTypes<'db>),
@@ -8015,7 +8041,10 @@ fn walk_known_instance_type<'db, V: visitor::TypeVisitor<'db> + ?Sized>(
         KnownInstanceType::TypeAliasType(type_alias) => {
             visitor.visit_type_alias_type(db, type_alias);
         }
-        KnownInstanceType::Deprecated(_) | KnownInstanceType::ConstraintSet(_) => {
+        KnownInstanceType::Deprecated(_)
+        | KnownInstanceType::ConstraintSet(_)
+        | KnownInstanceType::GenericContext(_)
+        | KnownInstanceType::Specialization(_) => {
             // Nothing to visit
         }
         KnownInstanceType::Field(field) => {
@@ -8068,15 +8097,7 @@ impl<'db> KnownInstanceType<'db> {
             Self::TypeAliasType(type_alias) => {
                 Self::TypeAliasType(type_alias.normalized_impl(db, visitor))
             }
-            Self::Deprecated(deprecated) => {
-                // Nothing to normalize
-                Self::Deprecated(deprecated)
-            }
             Self::Field(field) => Self::Field(field.normalized_impl(db, visitor)),
-            Self::ConstraintSet(set) => {
-                // Nothing to normalize
-                Self::ConstraintSet(set)
-            }
             Self::UnionType(list) => Self::UnionType(list.normalized_impl(db, visitor)),
             Self::Literal(ty) => Self::Literal(ty.normalized_impl(db, visitor)),
             Self::Annotated(ty) => Self::Annotated(ty.normalized_impl(db, visitor)),
@@ -8086,6 +8107,13 @@ impl<'db> KnownInstanceType<'db> {
                 newtype
                     .map_base_class_type(db, |class_type| class_type.normalized_impl(db, visitor)),
             ),
+            Self::Deprecated(_)
+            | Self::ConstraintSet(_)
+            | Self::GenericContext(_)
+            | Self::Specialization(_) => {
+                // Nothing to normalize
+                self
+            }
         }
     }
 
@@ -8103,6 +8131,8 @@ impl<'db> KnownInstanceType<'db> {
             Self::Deprecated(_) => KnownClass::Deprecated,
             Self::Field(_) => KnownClass::Field,
             Self::ConstraintSet(_) => KnownClass::ConstraintSet,
+            Self::GenericContext(_) => KnownClass::GenericContext,
+            Self::Specialization(_) => KnownClass::Specialization,
             Self::UnionType(_) => KnownClass::UnionType,
             Self::Literal(_)
             | Self::Annotated(_)
@@ -8188,6 +8218,21 @@ impl<'db> KnownInstanceType<'db> {
                             constraints.display(self.db)
                         )
                     }
+                    KnownInstanceType::GenericContext(generic_context) => {
+                        write!(
+                            f,
+                            "ty_extensions.GenericContext{}",
+                            generic_context.display_full(self.db)
+                        )
+                    }
+                    KnownInstanceType::Specialization(specialization) => {
+                        // Normalize for consistent output across CI platforms
+                        write!(
+                            f,
+                            "ty_extensions.Specialization{}",
+                            specialization.normalized(self.db).display_full(self.db)
+                        )
+                    }
                     KnownInstanceType::UnionType(_) => f.write_str("types.UnionType"),
                     KnownInstanceType::Literal(_) => f.write_str("<typing.Literal special form>"),
                     KnownInstanceType::Annotated(_) => {
@@ -8434,6 +8479,10 @@ enum InvalidTypeExpression<'db> {
     Field,
     /// Same for `ty_extensions.ConstraintSet`
     ConstraintSet,
+    /// Same for `ty_extensions.GenericContext`
+    GenericContext,
+    /// Same for `ty_extensions.Specialization`
+    Specialization,
     /// Same for `typing.TypedDict`
     TypedDict,
     /// Type qualifiers are always invalid in *type expressions*,
@@ -8486,6 +8535,12 @@ impl<'db> InvalidTypeExpression<'db> {
                     InvalidTypeExpression::ConstraintSet => {
                         f.write_str("`ty_extensions.ConstraintSet` is not allowed in type expressions")
                     }
+                    InvalidTypeExpression::GenericContext => {
+                        f.write_str("`ty_extensions.GenericContext` is not allowed in type expressions")
+                    }
+                    InvalidTypeExpression::Specialization => {
+                        f.write_str("`ty_extensions.GenericContext` is not allowed in type expressions")
+                    }
                     InvalidTypeExpression::TypedDict => {
                         f.write_str(
                             "The special form `typing.TypedDict` is not allowed in type expressions. \
@@ -10941,6 +10996,9 @@ pub enum KnownBoundMethodType<'db> {
     ConstraintSetImpliesSubtypeOf(TrackedConstraintSet<'db>),
     ConstraintSetSatisfies(TrackedConstraintSet<'db>),
     ConstraintSetSatisfiedByAllTypeVars(TrackedConstraintSet<'db>),
+
+    // GenericContext methods
+    GenericContextSpecializeConstrained(GenericContext<'db>),
 }
 
 pub(super) fn walk_method_wrapper_type<'db, V: visitor::TypeVisitor<'db> + ?Sized>(
@@ -10970,7 +11028,8 @@ pub(super) fn walk_method_wrapper_type<'db, V: visitor::TypeVisitor<'db> + ?Size
         | KnownBoundMethodType::ConstraintSetNever
         | KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)
         | KnownBoundMethodType::ConstraintSetSatisfies(_)
-        | KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_) => {}
+        | KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_)
+        | KnownBoundMethodType::GenericContextSpecializeConstrained(_) => {}
     }
 }
 
@@ -11046,6 +11105,10 @@ impl<'db> KnownBoundMethodType<'db> {
             | (
                 KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_),
                 KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_),
+            )
+            | (
+                KnownBoundMethodType::GenericContextSpecializeConstrained(_),
+                KnownBoundMethodType::GenericContextSpecializeConstrained(_),
             ) => ConstraintSet::from(true),
 
             (
@@ -11060,7 +11123,8 @@ impl<'db> KnownBoundMethodType<'db> {
                 | KnownBoundMethodType::ConstraintSetNever
                 | KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)
                 | KnownBoundMethodType::ConstraintSetSatisfies(_)
-                | KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_),
+                | KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_)
+                | KnownBoundMethodType::GenericContextSpecializeConstrained(_),
                 KnownBoundMethodType::FunctionTypeDunderGet(_)
                 | KnownBoundMethodType::FunctionTypeDunderCall(_)
                 | KnownBoundMethodType::PropertyDunderGet(_)
@@ -11072,7 +11136,8 @@ impl<'db> KnownBoundMethodType<'db> {
                 | KnownBoundMethodType::ConstraintSetNever
                 | KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)
                 | KnownBoundMethodType::ConstraintSetSatisfies(_)
-                | KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_),
+                | KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_)
+                | KnownBoundMethodType::GenericContextSpecializeConstrained(_),
             ) => ConstraintSet::from(false),
         }
     }
@@ -11137,6 +11202,11 @@ impl<'db> KnownBoundMethodType<'db> {
                 .constraints(db)
                 .iff(db, right_constraints.constraints(db)),
 
+            (
+                KnownBoundMethodType::GenericContextSpecializeConstrained(left_generic_context),
+                KnownBoundMethodType::GenericContextSpecializeConstrained(right_generic_context),
+            ) => ConstraintSet::from(left_generic_context == right_generic_context),
+
             (
                 KnownBoundMethodType::FunctionTypeDunderGet(_)
                 | KnownBoundMethodType::FunctionTypeDunderCall(_)
@@ -11149,7 +11219,8 @@ impl<'db> KnownBoundMethodType<'db> {
                 | KnownBoundMethodType::ConstraintSetNever
                 | KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)
                 | KnownBoundMethodType::ConstraintSetSatisfies(_)
-                | KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_),
+                | KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_)
+                | KnownBoundMethodType::GenericContextSpecializeConstrained(_),
                 KnownBoundMethodType::FunctionTypeDunderGet(_)
                 | KnownBoundMethodType::FunctionTypeDunderCall(_)
                 | KnownBoundMethodType::PropertyDunderGet(_)
@@ -11161,7 +11232,8 @@ impl<'db> KnownBoundMethodType<'db> {
                 | KnownBoundMethodType::ConstraintSetNever
                 | KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)
                 | KnownBoundMethodType::ConstraintSetSatisfies(_)
-                | KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_),
+                | KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_)
+                | KnownBoundMethodType::GenericContextSpecializeConstrained(_),
             ) => ConstraintSet::from(false),
         }
     }
@@ -11187,7 +11259,8 @@ impl<'db> KnownBoundMethodType<'db> {
             | KnownBoundMethodType::ConstraintSetNever
             | KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)
             | KnownBoundMethodType::ConstraintSetSatisfies(_)
-            | KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_) => self,
+            | KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_)
+            | KnownBoundMethodType::GenericContextSpecializeConstrained(_) => self,
         }
     }
 
@@ -11205,7 +11278,8 @@ impl<'db> KnownBoundMethodType<'db> {
             | KnownBoundMethodType::ConstraintSetNever
             | KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)
             | KnownBoundMethodType::ConstraintSetSatisfies(_)
-            | KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_) => {
+            | KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_)
+            | KnownBoundMethodType::GenericContextSpecializeConstrained(_) => {
                 KnownClass::ConstraintSet
             }
         }
@@ -11367,6 +11441,19 @@ impl<'db> KnownBoundMethodType<'db> {
                     Some(KnownClass::Bool.to_instance(db)),
                 )))
             }
+
+            KnownBoundMethodType::GenericContextSpecializeConstrained(_) => {
+                Either::Right(std::iter::once(Signature::new(
+                    Parameters::new([Parameter::positional_only(Some(Name::new_static(
+                        "constraints",
+                    )))
+                    .with_annotated_type(KnownClass::ConstraintSet.to_instance(db))]),
+                    Some(UnionType::from_elements(
+                        db,
+                        [KnownClass::Specialization.to_instance(db), Type::none(db)],
+                    )),
+                )))
+            }
         }
     }
 }
diff --git a/crates/ty_python_semantic/src/types/call/bind.rs b/crates/ty_python_semantic/src/types/call/bind.rs
index b8376a22cac55..c4aac0bb9631a 100644
--- a/crates/ty_python_semantic/src/types/call/bind.rs
+++ b/crates/ty_python_semantic/src/types/call/bind.rs
@@ -782,6 +782,12 @@ impl<'db> Bindings<'db> {
 
                         Some(KnownFunction::GenericContext) => {
                             if let [Some(ty)] = overload.parameter_types() {
+                                let wrap_generic_context = |generic_context| {
+                                    Type::KnownInstance(KnownInstanceType::GenericContext(
+                                        generic_context,
+                                    ))
+                                };
+
                                 let function_generic_context = |function: FunctionType<'db>| {
                                     let union = UnionType::from_elements(
                                         db,
@@ -790,7 +796,7 @@ impl<'db> Bindings<'db> {
                                             .overloads
                                             .iter()
                                             .filter_map(|signature| signature.generic_context)
-                                            .map(|generic_context| generic_context.as_tuple(db)),
+                                            .map(wrap_generic_context),
                                     );
                                     if union.is_never() {
                                         Type::none(db)
@@ -804,7 +810,7 @@ impl<'db> Bindings<'db> {
                                 overload.set_return_type(match ty {
                                     Type::ClassLiteral(class) => class
                                         .generic_context(db)
-                                        .map(|generic_context| generic_context.as_tuple(db))
+                                        .map(wrap_generic_context)
                                         .unwrap_or_else(|| Type::none(db)),
 
                                     Type::FunctionLiteral(function) => {
@@ -819,7 +825,7 @@ impl<'db> Bindings<'db> {
                                         TypeAliasType::PEP695(alias),
                                     )) => alias
                                         .generic_context(db)
-                                        .map(|generic_context| generic_context.as_tuple(db))
+                                        .map(wrap_generic_context)
                                         .unwrap_or_else(|| Type::none(db)),
 
                                     _ => Type::none(db),
@@ -1268,6 +1274,28 @@ impl<'db> Bindings<'db> {
                         overload.set_return_type(Type::BooleanLiteral(result));
                     }
 
+                    Type::KnownBoundMethod(
+                        KnownBoundMethodType::GenericContextSpecializeConstrained(generic_context),
+                    ) => {
+                        let [Some(constraints)] = overload.parameter_types() else {
+                            continue;
+                        };
+                        let Type::KnownInstance(KnownInstanceType::ConstraintSet(constraints)) =
+                            constraints
+                        else {
+                            continue;
+                        };
+                        let specialization =
+                            generic_context.specialize_constrained(db, constraints.constraints(db));
+                        let result = match specialization {
+                            Ok(specialization) => Type::KnownInstance(
+                                KnownInstanceType::Specialization(specialization),
+                            ),
+                            Err(()) => Type::none(db),
+                        };
+                        overload.set_return_type(result);
+                    }
+
                     Type::ClassLiteral(class) => match class.known(db) {
                         Some(KnownClass::Bool) => match overload.parameter_types() {
                             [Some(arg)] => overload.set_return_type(arg.bool(db).into_type(db)),
diff --git a/crates/ty_python_semantic/src/types/class.rs b/crates/ty_python_semantic/src/types/class.rs
index 8ac9eca111064..720bb9e91606e 100644
--- a/crates/ty_python_semantic/src/types/class.rs
+++ b/crates/ty_python_semantic/src/types/class.rs
@@ -3957,6 +3957,8 @@ pub enum KnownClass {
     Path,
     // ty_extensions
     ConstraintSet,
+    GenericContext,
+    Specialization,
 }
 
 impl KnownClass {
@@ -4060,6 +4062,8 @@ impl KnownClass {
             | Self::NamedTupleFallback
             | Self::NamedTupleLike
             | Self::ConstraintSet
+            | Self::GenericContext
+            | Self::Specialization
             | Self::ProtocolMeta
             | Self::TypedDictFallback => Some(Truthiness::Ambiguous),
 
@@ -4143,6 +4147,8 @@ impl KnownClass {
             | KnownClass::NamedTupleFallback
             | KnownClass::NamedTupleLike
             | KnownClass::ConstraintSet
+            | KnownClass::GenericContext
+            | KnownClass::Specialization
             | KnownClass::TypedDictFallback
             | KnownClass::BuiltinFunctionType
             | KnownClass::ProtocolMeta
@@ -4226,6 +4232,8 @@ impl KnownClass {
             | KnownClass::NamedTupleFallback
             | KnownClass::NamedTupleLike
             | KnownClass::ConstraintSet
+            | KnownClass::GenericContext
+            | KnownClass::Specialization
             | KnownClass::TypedDictFallback
             | KnownClass::BuiltinFunctionType
             | KnownClass::ProtocolMeta
@@ -4309,6 +4317,8 @@ impl KnownClass {
             | KnownClass::NamedTupleLike
             | KnownClass::NamedTupleFallback
             | KnownClass::ConstraintSet
+            | KnownClass::GenericContext
+            | KnownClass::Specialization
             | KnownClass::BuiltinFunctionType
             | KnownClass::ProtocolMeta
             | KnownClass::Template
@@ -4403,6 +4413,8 @@ impl KnownClass {
             | Self::InitVar
             | Self::NamedTupleFallback
             | Self::ConstraintSet
+            | Self::GenericContext
+            | Self::Specialization
             | Self::TypedDictFallback
             | Self::BuiltinFunctionType
             | Self::ProtocolMeta
@@ -4492,6 +4504,8 @@ impl KnownClass {
             | KnownClass::Template
             | KnownClass::Path
             | KnownClass::ConstraintSet
+            | KnownClass::GenericContext
+            | KnownClass::Specialization
             | KnownClass::InitVar => false,
             KnownClass::NamedTupleFallback | KnownClass::TypedDictFallback => true,
         }
@@ -4600,6 +4614,8 @@ impl KnownClass {
             Self::NamedTupleFallback => "NamedTupleFallback",
             Self::NamedTupleLike => "NamedTupleLike",
             Self::ConstraintSet => "ConstraintSet",
+            Self::GenericContext => "GenericContext",
+            Self::Specialization => "Specialization",
             Self::TypedDictFallback => "TypedDictFallback",
             Self::Template => "Template",
             Self::Path => "Path",
@@ -4911,7 +4927,10 @@ impl KnownClass {
             | Self::OrderedDict => KnownModule::Collections,
             Self::Field | Self::KwOnly | Self::InitVar => KnownModule::Dataclasses,
             Self::NamedTupleFallback | Self::TypedDictFallback => KnownModule::TypeCheckerInternals,
-            Self::NamedTupleLike | Self::ConstraintSet => KnownModule::TyExtensions,
+            Self::NamedTupleLike
+            | Self::ConstraintSet
+            | Self::GenericContext
+            | Self::Specialization => KnownModule::TyExtensions,
             Self::Template => KnownModule::Templatelib,
             Self::Path => KnownModule::Pathlib,
         }
@@ -4994,6 +5013,8 @@ impl KnownClass {
             | Self::NamedTupleFallback
             | Self::NamedTupleLike
             | Self::ConstraintSet
+            | Self::GenericContext
+            | Self::Specialization
             | Self::TypedDictFallback
             | Self::BuiltinFunctionType
             | Self::ProtocolMeta
@@ -5082,6 +5103,8 @@ impl KnownClass {
             | Self::NamedTupleFallback
             | Self::NamedTupleLike
             | Self::ConstraintSet
+            | Self::GenericContext
+            | Self::Specialization
             | Self::TypedDictFallback
             | Self::BuiltinFunctionType
             | Self::ProtocolMeta
@@ -5185,6 +5208,8 @@ impl KnownClass {
             "NamedTupleFallback" => &[Self::NamedTupleFallback],
             "NamedTupleLike" => &[Self::NamedTupleLike],
             "ConstraintSet" => &[Self::ConstraintSet],
+            "GenericContext" => &[Self::GenericContext],
+            "Specialization" => &[Self::Specialization],
             "TypedDictFallback" => &[Self::TypedDictFallback],
             "Template" => &[Self::Template],
             "Path" => &[Self::Path],
@@ -5262,6 +5287,8 @@ impl KnownClass {
             | Self::ExtensionsTypeVar
             | Self::NamedTupleLike
             | Self::ConstraintSet
+            | Self::GenericContext
+            | Self::Specialization
             | Self::Awaitable
             | Self::Generator
             | Self::Template
diff --git a/crates/ty_python_semantic/src/types/class_base.rs b/crates/ty_python_semantic/src/types/class_base.rs
index dfc7b69000bcc..ff9aad73c4f33 100644
--- a/crates/ty_python_semantic/src/types/class_base.rs
+++ b/crates/ty_python_semantic/src/types/class_base.rs
@@ -175,6 +175,8 @@ impl<'db> ClassBase<'db> {
                 | KnownInstanceType::Field(_)
                 | KnownInstanceType::ConstraintSet(_)
                 | KnownInstanceType::Callable(_)
+                | KnownInstanceType::GenericContext(_)
+                | KnownInstanceType::Specialization(_)
                 | KnownInstanceType::UnionType(_)
                 | KnownInstanceType::Literal(_)
                 // A class inheriting from a newtype would make intuitive sense, but newtype
diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index eb09335da4053..d142a109cd667 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -64,7 +64,7 @@ use itertools::Itertools;
 use rustc_hash::{FxHashMap, FxHashSet};
 use salsa::plumbing::AsId;
 
-use crate::types::generics::InferableTypeVars;
+use crate::types::generics::{GenericContext, InferableTypeVars, Specialization};
 use crate::types::{
     BoundTypeVarIdentity, BoundTypeVarInstance, IntersectionType, Type, TypeRelation,
     TypeVarBoundOrConstraints, UnionType,
@@ -1002,17 +1002,113 @@ impl<'db> Node<'db> {
         }
     }
 
-    fn exists_one_inner(
+    /// Returns a new BDD that is the _existential abstraction_ of `self` for a set of typevars.
+    /// All typevars _other_ than the one given will be removed and abstracted away.
+    fn retain_one(self, db: &'db dyn Db, bound_typevar: BoundTypeVarIdentity<'db>) -> Self {
+        match self {
+            Node::AlwaysTrue => Node::AlwaysTrue,
+            Node::AlwaysFalse => Node::AlwaysFalse,
+            Node::Interior(interior) => interior.retain_one(db, bound_typevar),
+        }
+    }
+
+    fn abstract_one_inner(
         self,
         db: &'db dyn Db,
-        bound_typevar: BoundTypeVarIdentity<'db>,
+        should_remove: &mut dyn FnMut(ConstrainedTypeVar<'db>) -> bool,
         map: &SequentMap<'db>,
         path: &mut PathAssignments<'db>,
     ) -> Self {
         match self {
             Node::AlwaysTrue => Node::AlwaysTrue,
             Node::AlwaysFalse => Node::AlwaysFalse,
-            Node::Interior(interior) => interior.exists_one_inner(db, bound_typevar, map, path),
+            Node::Interior(interior) => interior.abstract_one_inner(db, should_remove, map, path),
+        }
+    }
+
+    /// Invokes a callback for each of the representative types of a particular typevar for this
+    /// constraint set.
+    ///
+    /// There is a representative type for each distinct path from the BDD root to the `AlwaysTrue`
+    /// terminal. Each of those paths can be viewed as the conjunction of the individual
+    /// constraints of each internal node that we traverse as we walk that path. We provide the
+    /// lower/upper bound of this conjunction to your callback, allowing you to choose any suitable
+    /// type in the range.
+    fn find_representative_types(
+        self,
+        db: &'db dyn Db,
+        bound_typevar: BoundTypeVarIdentity<'db>,
+        mut f: impl FnMut(Type<'db>, Type<'db>),
+    ) {
+        self.retain_one(db, bound_typevar)
+            .find_representative_types_inner(db, Type::Never, Type::object(), &mut f);
+    }
+
+    fn find_representative_types_inner(
+        self,
+        db: &'db dyn Db,
+        greatest_lower_bound: Type<'db>,
+        least_upper_bound: Type<'db>,
+        f: &mut dyn FnMut(Type<'db>, Type<'db>),
+    ) {
+        match self {
+            Node::AlwaysTrue => {
+                // If we reach the `true` terminal, the path we've been following represents one
+                // representative type.
+
+                // If `lower ≰ upper`, then this path somehow represents in invalid specialization.
+                // That should have been removed from the BDD domain as part of the simplification
+                // process.
+                debug_assert!(greatest_lower_bound.is_subtype_of(db, least_upper_bound));
+
+                // We've been tracking the lower and upper bound that the types for this path must
+                // satisfy. Pass those bounds along and let the caller choose a representative type
+                // from within that range.
+                f(greatest_lower_bound, least_upper_bound);
+            }
+
+            Node::AlwaysFalse => {
+                // If we reach the `false` terminal, the path we've been following represents an
+                // invalid specialization, so we skip it.
+            }
+
+            Node::Interior(interior) => {
+                // For an interior node, there are two outgoing paths: one for the `if_true`
+                // branch, and one for the `if_false` branch.
+                //
+                // For the `if_true` branch, this node's constraint places additional restrictions
+                // on the types that satisfy the current path through the BDD. So we intersect the
+                // current glb/lub with the constraint's bounds to get the new glb/lub for the
+                // recursive call.
+                let constraint = interior.constraint(db);
+                let new_greatest_lower_bound =
+                    UnionType::from_elements(db, [greatest_lower_bound, constraint.lower(db)]);
+                let new_least_upper_bound =
+                    IntersectionType::from_elements(db, [least_upper_bound, constraint.upper(db)]);
+                interior.if_true(db).find_representative_types_inner(
+                    db,
+                    new_greatest_lower_bound,
+                    new_least_upper_bound,
+                    f,
+                );
+
+                // For the `if_false` branch, then the types that satisfy the current path through
+                // the BDD do _not_ satisfy the node's constraint. Because we used `retain_one` to
+                // abstract the BDD to a single typevar, we don't need to worry about how that
+                // negative constraint affects the lower/upper bound that we're tracking. The
+                // abstraction process will have compared the negative constraint with all of the
+                // other constraints in the BDD, and added new interior nodes to handle the
+                // combination of those constraints. So we can recurse down the `if_false` branch
+                // without updating the lower/upper bounds, relying on the other constraints along
+                // the path to incorporate that negative "hole" in the set of valid types for this
+                // path.
+                interior.if_false(db).find_representative_types_inner(
+                    db,
+                    greatest_lower_bound,
+                    least_upper_bound,
+                    f,
+                );
+            }
         }
     }
 
@@ -1441,94 +1537,126 @@ impl<'db> InteriorNode<'db> {
     fn exists_one(self, db: &'db dyn Db, bound_typevar: BoundTypeVarIdentity<'db>) -> Node<'db> {
         let map = self.sequent_map(db);
         let mut path = PathAssignments::default();
-        self.exists_one_inner(db, bound_typevar, map, &mut path)
+        self.abstract_one_inner(
+            db,
+            // Remove any node that constrains `bound_typevar`, or that has a lower/upper bound of
+            // `bound_typevar`.
+            &mut |constraint| {
+                if constraint.typevar(db).identity(db) == bound_typevar {
+                    return true;
+                }
+                if let Type::TypeVar(lower_bound_typevar) = constraint.lower(db)
+                    && lower_bound_typevar.identity(db) == bound_typevar
+                {
+                    return true;
+                }
+                if let Type::TypeVar(upper_bound_typevar) = constraint.upper(db)
+                    && upper_bound_typevar.identity(db) == bound_typevar
+                {
+                    return true;
+                }
+                false
+            },
+            map,
+            &mut path,
+        )
+    }
+
+    #[salsa::tracked(heap_size=ruff_memory_usage::heap_size)]
+    fn retain_one(self, db: &'db dyn Db, bound_typevar: BoundTypeVarIdentity<'db>) -> Node<'db> {
+        let map = self.sequent_map(db);
+        let mut path = PathAssignments::default();
+        self.abstract_one_inner(
+            db,
+            // Remove any node that constrains some other typevar than `bound_typevar`, and any
+            // node that constrains `bound_typevar` with a lower/upper bound of some other typevar.
+            // (For the latter, if there are any derived facts that we can infer from the typevar
+            // bound, those will be automatically added to the result.)
+            &mut |constraint| {
+                if constraint.typevar(db).identity(db) != bound_typevar {
+                    return true;
+                }
+                if matches!(constraint.lower(db), Type::TypeVar(_))
+                    || matches!(constraint.upper(db), Type::TypeVar(_))
+                {
+                    return true;
+                }
+                false
+            },
+            map,
+            &mut path,
+        )
     }
 
-    fn exists_one_inner(
+    fn abstract_one_inner(
         self,
         db: &'db dyn Db,
-        bound_typevar: BoundTypeVarIdentity<'db>,
+        should_remove: &mut dyn FnMut(ConstrainedTypeVar<'db>) -> bool,
         map: &SequentMap<'db>,
         path: &mut PathAssignments<'db>,
     ) -> Node<'db> {
         let self_constraint = self.constraint(db);
-        let self_typevar = self_constraint.typevar(db);
-        match bound_typevar.cmp(&self_typevar.identity(db)) {
-            // If the typevar that this node checks is "later" than the typevar we're abstracting
-            // over, then we have reached a point in the BDD where the abstraction can no longer
-            // affect the result, and we can return early.
-            Ordering::Less => Node::Interior(self),
-
-            // If the typevar that this node checks _is_ the typevar we're abstracting over, then
-            // we replace this node with the OR of its if_false/if_true edges. That is, the result
-            // is true if there's any assignment of this node's constraint that is true.
+        if should_remove(self_constraint) {
+            // If we should remove constraints involving this typevar, then we replace this node
+            // with the OR of its if_false/if_true edges. That is, the result is true if there's
+            // any assignment of this node's constraint that is true.
             //
             // We also have to check if there are any derived facts that depend on the constraint
             // we're about to remove. If so, we need to "remember" them by AND-ing them in with the
             // corresponding branch.
-            Ordering::Equal => {
-                let if_true = path
-                    .walk_edge(map, self_constraint.when_true(), |path, new_range| {
-                        let branch =
-                            self.if_true(db)
-                                .exists_one_inner(db, bound_typevar, map, path);
-                        path.assignments[new_range]
-                            .iter()
-                            .filter(|assignment| {
-                                // Don't add back any derived facts if they reference the typevar
-                                // that we're trying to remove!
-                                !assignment
-                                    .constraint()
-                                    .typevar(db)
-                                    .is_same_typevar_as(db, self_typevar)
-                            })
-                            .fold(branch, |branch, assignment| {
-                                branch.and(db, Node::new_satisfied_constraint(db, *assignment))
-                            })
-                    })
-                    .unwrap_or(Node::AlwaysFalse);
-                let if_false = path
-                    .walk_edge(map, self_constraint.when_false(), |path, new_range| {
-                        let branch =
-                            self.if_false(db)
-                                .exists_one_inner(db, bound_typevar, map, path);
-                        path.assignments[new_range]
-                            .iter()
-                            .filter(|assignment| {
-                                // Don't add back any derived facts if they reference the typevar
-                                // that we're trying to remove!
-                                !assignment
-                                    .constraint()
-                                    .typevar(db)
-                                    .is_same_typevar_as(db, self_typevar)
-                            })
-                            .fold(branch, |branch, assignment| {
-                                branch.and(db, Node::new_satisfied_constraint(db, *assignment))
-                            })
-                    })
-                    .unwrap_or(Node::AlwaysFalse);
-                if_true.or(db, if_false)
-            }
-
+            let if_true = path
+                .walk_edge(map, self_constraint.when_true(), |path, new_range| {
+                    let branch = self
+                        .if_true(db)
+                        .abstract_one_inner(db, should_remove, map, path);
+                    path.assignments[new_range]
+                        .iter()
+                        .filter(|assignment| {
+                            // Don't add back any derived facts if they are ones that we would have
+                            // removed!
+                            !should_remove(assignment.constraint())
+                        })
+                        .fold(branch, |branch, assignment| {
+                            branch.and(db, Node::new_satisfied_constraint(db, *assignment))
+                        })
+                })
+                .unwrap_or(Node::AlwaysFalse);
+            let if_false = path
+                .walk_edge(map, self_constraint.when_false(), |path, new_range| {
+                    let branch = self
+                        .if_false(db)
+                        .abstract_one_inner(db, should_remove, map, path);
+                    path.assignments[new_range]
+                        .iter()
+                        .filter(|assignment| {
+                            // Don't add back any derived facts if they are ones that we would have
+                            // removed!
+                            !should_remove(assignment.constraint())
+                        })
+                        .fold(branch, |branch, assignment| {
+                            branch.and(db, Node::new_satisfied_constraint(db, *assignment))
+                        })
+                })
+                .unwrap_or(Node::AlwaysFalse);
+            if_true.or(db, if_false)
+        } else {
             // Otherwise, we abstract the if_false/if_true edges recursively.
-            Ordering::Greater => {
-                let if_true = path
-                    .walk_edge(map, self_constraint.when_true(), |path, _| {
-                        self.if_true(db)
-                            .exists_one_inner(db, bound_typevar, map, path)
-                    })
-                    .unwrap_or(Node::AlwaysFalse);
-                let if_false = path
-                    .walk_edge(map, self_constraint.when_false(), |path, _| {
-                        self.if_false(db)
-                            .exists_one_inner(db, bound_typevar, map, path)
-                    })
-                    .unwrap_or(Node::AlwaysFalse);
-                // NB: We cannot use `Node::new` here, because the recursive calls might introduce new
-                // derived constraints into the result, and those constraints might appear before this
-                // one in the BDD ordering.
-                Node::new_constraint(db, self_constraint).ite(db, if_true, if_false)
-            }
+            let if_true = path
+                .walk_edge(map, self_constraint.when_true(), |path, _| {
+                    self.if_true(db)
+                        .abstract_one_inner(db, should_remove, map, path)
+                })
+                .unwrap_or(Node::AlwaysFalse);
+            let if_false = path
+                .walk_edge(map, self_constraint.when_false(), |path, _| {
+                    self.if_false(db)
+                        .abstract_one_inner(db, should_remove, map, path)
+                })
+                .unwrap_or(Node::AlwaysFalse);
+            // NB: We cannot use `Node::new` here, because the recursive calls might introduce new
+            // derived constraints into the result, and those constraints might appear before this
+            // one in the BDD ordering.
+            Node::new_constraint(db, self_constraint).ite(db, if_true, if_false)
         }
     }
 
@@ -2792,6 +2920,72 @@ impl<'db> BoundTypeVarInstance<'db> {
     }
 }
 
+impl<'db> GenericContext<'db> {
+    pub(crate) fn specialize_constrained(
+        self,
+        db: &'db dyn Db,
+        constraints: ConstraintSet<'db>,
+    ) -> Result<Specialization<'db>, ()> {
+        // First we intersect with the valid specializations of all of the typevars. We need all of
+        // valid specializations to hold simultaneously, so we do this once before abstracting over
+        // each typevar.
+        let abstracted = self
+            .variables(db)
+            .fold(constraints.node, |constraints, bound_typevar| {
+                constraints.and(db, bound_typevar.valid_specializations(db))
+            });
+
+        // Then we find all of the "representative types" for each typevar in the constraint set.
+        let mut types = vec![Type::Never; self.len(db)];
+        for (i, bound_typevar) in self.variables(db).enumerate() {
+            // Each representative type represents one of the ways that the typevar can satisfy the
+            // constraint, expressed as a lower/upper bound on the types that the typevar can
+            // specialize to.
+            //
+            // If there are multiple paths in the BDD, they technically represent independent
+            // possible specializations. If there's a type that satisfies all of them, we will
+            // return that as the specialization. If not, then the constraint set is ambiguous.
+            // (This happens most often with constrained typevars.) We could in the future turn
+            // _each_ of the paths into separate specializations, but it's not clear what we would
+            // do with that, so instead we just report the ambiguity as a specialization failure.
+            let mut satisfied = false;
+            let mut greatest_lower_bound = Type::Never;
+            let mut least_upper_bound = Type::object();
+            abstracted.find_representative_types(
+                db,
+                bound_typevar.identity(db),
+                |lower_bound, upper_bound| {
+                    satisfied = true;
+                    greatest_lower_bound =
+                        UnionType::from_elements(db, [greatest_lower_bound, lower_bound]);
+                    least_upper_bound =
+                        IntersectionType::from_elements(db, [least_upper_bound, upper_bound]);
+                },
+            );
+
+            // If there are no satisfiable paths in the BDD, then there is no valid specialization
+            // for this constraint set.
+            if !satisfied {
+                // TODO: Construct a useful error here
+                return Err(());
+            }
+
+            // If `lower ≰ upper`, then there is no type that satisfies all of the paths in the
+            // BDD. That's an ambiguous specialization, as described above.
+            if !greatest_lower_bound.is_subtype_of(db, least_upper_bound) {
+                // TODO: Construct a useful error here
+                return Err(());
+            }
+
+            // Of all of the types that satisfy all of the paths in the BDD, we choose the
+            // "largest" one (i.e., "closest to `object`") as the specialization.
+            types[i] = least_upper_bound;
+        }
+
+        Ok(self.specialize(db, types.into_boxed_slice()))
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;
diff --git a/crates/ty_python_semantic/src/types/display.rs b/crates/ty_python_semantic/src/types/display.rs
index b8a8a05ac4ca0..063c4af0b7135 100644
--- a/crates/ty_python_semantic/src/types/display.rs
+++ b/crates/ty_python_semantic/src/types/display.rs
@@ -541,6 +541,9 @@ impl Display for DisplayRepresentation<'_> {
             Type::KnownBoundMethod(KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(
                 _,
             )) => f.write_str("bound method `ConstraintSet.satisfied_by_all_typevars`"),
+            Type::KnownBoundMethod(KnownBoundMethodType::GenericContextSpecializeConstrained(
+                _,
+            )) => f.write_str("bound method `GenericContext.specialize_constrained`"),
             Type::WrapperDescriptor(kind) => {
                 let (method, object) = match kind {
                     WrapperDescriptorKind::FunctionTypeDunderGet => ("__get__", "function"),
@@ -892,6 +895,16 @@ impl<'db> GenericContext<'db> {
     pub fn display(&'db self, db: &'db dyn Db) -> DisplayGenericContext<'db> {
         Self::display_with(self, db, DisplaySettings::default())
     }
+
+    pub fn display_full(&'db self, db: &'db dyn Db) -> DisplayGenericContext<'db> {
+        DisplayGenericContext {
+            generic_context: self,
+            db,
+            settings: DisplaySettings::default(),
+            full: true,
+        }
+    }
+
     pub fn display_with(
         &'db self,
         db: &'db dyn Db,
@@ -901,6 +914,7 @@ impl<'db> GenericContext<'db> {
             generic_context: self,
             db,
             settings,
+            full: false,
         }
     }
 }
@@ -914,12 +928,9 @@ struct DisplayOptionalGenericContext<'db> {
 impl Display for DisplayOptionalGenericContext<'_> {
     fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
         if let Some(generic_context) = self.generic_context {
-            DisplayGenericContext {
-                generic_context,
-                db: self.db,
-                settings: self.settings.clone(),
-            }
-            .fmt(f)
+            generic_context
+                .display_with(self.db, self.settings.clone())
+                .fmt(f)
         } else {
             Ok(())
         }
@@ -931,10 +942,11 @@ pub struct DisplayGenericContext<'db> {
     db: &'db dyn Db,
     #[expect(dead_code)]
     settings: DisplaySettings<'db>,
+    full: bool,
 }
 
-impl Display for DisplayGenericContext<'_> {
-    fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
+impl DisplayGenericContext<'_> {
+    fn fmt_normal(&self, f: &mut Formatter<'_>) -> fmt::Result {
         let variables = self.generic_context.variables(self.db);
 
         let non_implicit_variables: Vec<_> = variables
@@ -954,40 +966,75 @@ impl Display for DisplayGenericContext<'_> {
         }
         f.write_char(']')
     }
+
+    fn fmt_full(&self, f: &mut Formatter<'_>) -> fmt::Result {
+        let variables = self.generic_context.variables(self.db);
+        f.write_char('[')?;
+        for (idx, bound_typevar) in variables.enumerate() {
+            if idx > 0 {
+                f.write_str(", ")?;
+            }
+            bound_typevar.identity(self.db).display(self.db).fmt(f)?;
+        }
+        f.write_char(']')
+    }
+}
+
+impl Display for DisplayGenericContext<'_> {
+    fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
+        if self.full {
+            self.fmt_full(f)
+        } else {
+            self.fmt_normal(f)
+        }
+    }
 }
 
 impl<'db> Specialization<'db> {
-    pub fn display(&'db self, db: &'db dyn Db) -> DisplaySpecialization<'db> {
+    pub fn display(self, db: &'db dyn Db) -> DisplaySpecialization<'db> {
         self.display_short(db, TupleSpecialization::No, DisplaySettings::default())
     }
 
+    pub(crate) fn display_full(self, db: &'db dyn Db) -> DisplaySpecialization<'db> {
+        DisplaySpecialization {
+            specialization: self,
+            db,
+            tuple_specialization: TupleSpecialization::No,
+            settings: DisplaySettings::default(),
+            full: true,
+        }
+    }
+
     /// Renders the specialization as it would appear in a subscript expression, e.g. `[int, str]`.
     pub fn display_short(
-        &'db self,
+        self,
         db: &'db dyn Db,
         tuple_specialization: TupleSpecialization,
         settings: DisplaySettings<'db>,
     ) -> DisplaySpecialization<'db> {
         DisplaySpecialization {
-            types: self.types(db),
+            specialization: self,
             db,
             tuple_specialization,
             settings,
+            full: false,
         }
     }
 }
 
 pub struct DisplaySpecialization<'db> {
-    types: &'db [Type<'db>],
+    specialization: Specialization<'db>,
     db: &'db dyn Db,
     tuple_specialization: TupleSpecialization,
     settings: DisplaySettings<'db>,
+    full: bool,
 }
 
-impl Display for DisplaySpecialization<'_> {
-    fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
+impl DisplaySpecialization<'_> {
+    fn fmt_normal(&self, f: &mut Formatter<'_>) -> fmt::Result {
         f.write_char('[')?;
-        for (idx, ty) in self.types.iter().enumerate() {
+        let types = self.specialization.types(self.db);
+        for (idx, ty) in types.iter().enumerate() {
             if idx > 0 {
                 f.write_str(", ")?;
             }
@@ -998,6 +1045,37 @@ impl Display for DisplaySpecialization<'_> {
         }
         f.write_char(']')
     }
+
+    fn fmt_full(&self, f: &mut Formatter<'_>) -> fmt::Result {
+        f.write_char('[')?;
+        let variables = self
+            .specialization
+            .generic_context(self.db)
+            .variables(self.db);
+        let types = self.specialization.types(self.db);
+        for (idx, (bound_typevar, ty)) in variables.zip(types).enumerate() {
+            if idx > 0 {
+                f.write_str(", ")?;
+            }
+            write!(
+                f,
+                "{} = {}",
+                bound_typevar.identity(self.db).display(self.db),
+                ty.display_with(self.db, self.settings.clone()),
+            )?;
+        }
+        f.write_char(']')
+    }
+}
+
+impl Display for DisplaySpecialization<'_> {
+    fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
+        if self.full {
+            self.fmt_full(f)
+        } else {
+            self.fmt_normal(f)
+        }
+    }
 }
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
diff --git a/crates/ty_python_semantic/src/types/generics.rs b/crates/ty_python_semantic/src/types/generics.rs
index 169b69e496648..2ee21a02ba941 100644
--- a/crates/ty_python_semantic/src/types/generics.rs
+++ b/crates/ty_python_semantic/src/types/generics.rs
@@ -474,11 +474,6 @@ impl<'db> GenericContext<'db> {
         self.specialize(db, types.into())
     }
 
-    /// Returns a tuple type of the typevars introduced by this generic context.
-    pub(crate) fn as_tuple(self, db: &'db dyn Db) -> Type<'db> {
-        Type::heterogeneous_tuple(db, self.variables(db).map(Type::TypeVar))
-    }
-
     pub(crate) fn is_subset_of(self, db: &'db dyn Db, other: GenericContext<'db>) -> bool {
         let other_variables = other.variables_inner(db);
         self.variables(db)
@@ -624,7 +619,12 @@ impl std::fmt::Display for LegacyGenericBase {
 ///
 /// TODO: Handle nested specializations better, with actual parent links to the specialization of
 /// the lexically containing context.
+///
+/// # Ordering
+/// Ordering is based on the context's salsa-assigned id and not on its values.
+/// The id may change between runs, or when the context was garbage collected and recreated.
 #[salsa::interned(debug, heap_size=ruff_memory_usage::heap_size)]
+#[derive(PartialOrd, Ord)]
 pub struct Specialization<'db> {
     pub(crate) generic_context: GenericContext<'db>,
     #[returns(deref)]
@@ -1003,6 +1003,11 @@ impl<'db> Specialization<'db> {
         Specialization::new(db, self.generic_context(db), types, None, None)
     }
 
+    #[must_use]
+    pub(crate) fn normalized(self, db: &'db dyn Db) -> Self {
+        self.normalized_impl(db, &NormalizedVisitor::default())
+    }
+
     pub(crate) fn normalized_impl(self, db: &'db dyn Db, visitor: &NormalizedVisitor<'db>) -> Self {
         let types: Box<[_]> = self
             .types(db)
diff --git a/crates/ty_python_semantic/src/types/infer/builder/type_expression.rs b/crates/ty_python_semantic/src/types/infer/builder/type_expression.rs
index 6ea57af90f761..75e4e1f94a59e 100644
--- a/crates/ty_python_semantic/src/types/infer/builder/type_expression.rs
+++ b/crates/ty_python_semantic/src/types/infer/builder/type_expression.rs
@@ -783,6 +783,24 @@ impl<'db> TypeInferenceBuilder<'db, '_> {
                     }
                     Type::unknown()
                 }
+                KnownInstanceType::GenericContext(_) => {
+                    self.infer_type_expression(slice);
+                    if let Some(builder) = self.context.report_lint(&INVALID_TYPE_FORM, subscript) {
+                        builder.into_diagnostic(format_args!(
+                            "`ty_extensions.GenericContext` is not allowed in type expressions",
+                        ));
+                    }
+                    Type::unknown()
+                }
+                KnownInstanceType::Specialization(_) => {
+                    self.infer_type_expression(slice);
+                    if let Some(builder) = self.context.report_lint(&INVALID_TYPE_FORM, subscript) {
+                        builder.into_diagnostic(format_args!(
+                            "`ty_extensions.Specialization` is not allowed in type expressions",
+                        ));
+                    }
+                    Type::unknown()
+                }
                 KnownInstanceType::TypeVar(_) => {
                     self.infer_type_expression(slice);
                     todo_type!("TypeVar annotations")
diff --git a/crates/ty_vendored/ty_extensions/ty_extensions.pyi b/crates/ty_vendored/ty_extensions/ty_extensions.pyi
index 744bd5af370b7..8f45b292387d7 100644
--- a/crates/ty_vendored/ty_extensions/ty_extensions.pyi
+++ b/crates/ty_vendored/ty_extensions/ty_extensions.pyi
@@ -91,6 +91,23 @@ class ConstraintSet:
     def __or__(self, other: ConstraintSet) -> ConstraintSet: ...
     def __invert__(self) -> ConstraintSet: ...
 
+class GenericContext:
+    """
+    The set of typevars that are bound by a generic class, function, or type
+    alias.
+    """
+
+    def specialize_constrained(
+        self, constraints: ConstraintSet
+    ) -> Specialization | None:
+        """
+        Returns a specialization of this generic context that satisfies the
+        given constraints, or None if the constraints cannot be satisfied.
+        """
+
+class Specialization:
+    """A mapping of typevars to specific types"""
+
 # Predicates on types
 #
 # Ideally, these would be annotated using `TypeForm`, but that has not been
@@ -128,7 +145,7 @@ def is_single_valued(ty: Any) -> bool:
 
 # Returns the generic context of a type as a tuple of typevars, or `None` if the
 # type is not generic.
-def generic_context(ty: Any) -> Any: ...
+def generic_context(ty: Any) -> GenericContext | None: ...
 
 # Returns the `__all__` names of a module as a tuple of sorted strings, or `None` if
 # either the module does not have `__all__` or it has invalid elements.