diff --git a/crates/ty_python_semantic/resources/mdtest/generics/pep695/variables.md b/crates/ty_python_semantic/resources/mdtest/generics/pep695/variables.md
index 8d3194ded2..68cce5ad3e 100644
--- a/crates/ty_python_semantic/resources/mdtest/generics/pep695/variables.md
+++ b/crates/ty_python_semantic/resources/mdtest/generics/pep695/variables.md
@@ -129,7 +129,7 @@ specialization. Thus, the typevar is a subtype of itself and of `object`, but no
 (including other typevars).
 
 ```py
-from ty_extensions import reveal_when_assignable_to, reveal_when_subtype_of
+from ty_extensions import is_assignable_to, is_subtype_of
 
 class Super: ...
 class Base(Super): ...
@@ -137,23 +137,23 @@ class Sub(Base): ...
 class Unrelated: ...
 
 def unbounded_unconstrained[T, U](t: T, u: U) -> None:
-    reveal_when_assignable_to(T, T)  # revealed: always
-    reveal_when_assignable_to(T, object)  # revealed: always
-    reveal_when_assignable_to(T, Super)  # revealed: never
-    reveal_when_assignable_to(U, U)  # revealed: always
-    reveal_when_assignable_to(U, object)  # revealed: always
-    reveal_when_assignable_to(U, Super)  # revealed: never
-    reveal_when_assignable_to(T, U)  # revealed: never
-    reveal_when_assignable_to(U, T)  # revealed: never
+    reveal_type(is_assignable_to(T, T))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(T, object))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(T, Super))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(U, U))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(U, object))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(U, Super))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(T, U))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(U, T))  # revealed: ty_extensions.ConstraintSet[never]
 
-    reveal_when_subtype_of(T, T)  # revealed: always
-    reveal_when_subtype_of(T, object)  # revealed: always
-    reveal_when_subtype_of(T, Super)  # revealed: never
-    reveal_when_subtype_of(U, U)  # revealed: always
-    reveal_when_subtype_of(U, object)  # revealed: always
-    reveal_when_subtype_of(U, Super)  # revealed: never
-    reveal_when_subtype_of(T, U)  # revealed: never
-    reveal_when_subtype_of(U, T)  # revealed: never
+    reveal_type(is_subtype_of(T, T))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_subtype_of(T, object))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_subtype_of(T, Super))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(U, U))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_subtype_of(U, object))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_subtype_of(U, Super))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(T, U))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(U, T))  # revealed: ty_extensions.ConstraintSet[never]
 ```
 
 A bounded typevar is assignable to its bound, and a bounded, fully static typevar is a subtype of
@@ -167,40 +167,40 @@ from typing import Any
 from typing_extensions import final
 
 def bounded[T: Super](t: T) -> None:
-    reveal_when_assignable_to(T, Super)  # revealed: always
-    reveal_when_assignable_to(T, Sub)  # revealed: never
-    reveal_when_assignable_to(Super, T)  # revealed: never
-    reveal_when_assignable_to(Sub, T)  # revealed: never
+    reveal_type(is_assignable_to(T, Super))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(T, Sub))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(Super, T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(Sub, T))  # revealed: ty_extensions.ConstraintSet[never]
 
-    reveal_when_subtype_of(T, Super)  # revealed: always
-    reveal_when_subtype_of(T, Sub)  # revealed: never
-    reveal_when_subtype_of(Super, T)  # revealed: never
-    reveal_when_subtype_of(Sub, T)  # revealed: never
+    reveal_type(is_subtype_of(T, Super))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_subtype_of(T, Sub))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(Super, T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(Sub, T))  # revealed: ty_extensions.ConstraintSet[never]
 
 def bounded_by_gradual[T: Any](t: T) -> None:
-    reveal_when_assignable_to(T, Any)  # revealed: always
-    reveal_when_assignable_to(Any, T)  # revealed: always
-    reveal_when_assignable_to(T, Super)  # revealed: always
-    reveal_when_assignable_to(Super, T)  # revealed: never
-    reveal_when_assignable_to(T, Sub)  # revealed: always
-    reveal_when_assignable_to(Sub, T)  # revealed: never
+    reveal_type(is_assignable_to(T, Any))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(Any, T))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(T, Super))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(Super, T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(T, Sub))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(Sub, T))  # revealed: ty_extensions.ConstraintSet[never]
 
-    reveal_when_subtype_of(T, Any)  # revealed: never
-    reveal_when_subtype_of(Any, T)  # revealed: never
-    reveal_when_subtype_of(T, Super)  # revealed: never
-    reveal_when_subtype_of(Super, T)  # revealed: never
-    reveal_when_subtype_of(T, Sub)  # revealed: never
-    reveal_when_subtype_of(Sub, T)  # revealed: never
+    reveal_type(is_subtype_of(T, Any))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(Any, T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(T, Super))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(Super, T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(T, Sub))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(Sub, T))  # revealed: ty_extensions.ConstraintSet[never]
 
 @final
 class FinalClass: ...
 
 def bounded_final[T: FinalClass](t: T) -> None:
-    reveal_when_assignable_to(T, FinalClass)  # revealed: always
-    reveal_when_assignable_to(FinalClass, T)  # revealed: never
+    reveal_type(is_assignable_to(T, FinalClass))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(FinalClass, T))  # revealed: ty_extensions.ConstraintSet[never]
 
-    reveal_when_subtype_of(T, FinalClass)  # revealed: always
-    reveal_when_subtype_of(FinalClass, T)  # revealed: never
+    reveal_type(is_subtype_of(T, FinalClass))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_subtype_of(FinalClass, T))  # revealed: ty_extensions.ConstraintSet[never]
 ```
 
 Two distinct fully static typevars are not subtypes of each other, even if they have the same
@@ -210,18 +210,18 @@ typevars to `Never` in addition to that final class.
 
 ```py
 def two_bounded[T: Super, U: Super](t: T, u: U) -> None:
-    reveal_when_assignable_to(T, U)  # revealed: never
-    reveal_when_assignable_to(U, T)  # revealed: never
+    reveal_type(is_assignable_to(T, U))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(U, T))  # revealed: ty_extensions.ConstraintSet[never]
 
-    reveal_when_subtype_of(T, U)  # revealed: never
-    reveal_when_subtype_of(U, T)  # revealed: never
+    reveal_type(is_subtype_of(T, U))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(U, T))  # revealed: ty_extensions.ConstraintSet[never]
 
 def two_final_bounded[T: FinalClass, U: FinalClass](t: T, u: U) -> None:
-    reveal_when_assignable_to(T, U)  # revealed: never
-    reveal_when_assignable_to(U, T)  # revealed: never
+    reveal_type(is_assignable_to(T, U))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(U, T))  # revealed: ty_extensions.ConstraintSet[never]
 
-    reveal_when_subtype_of(T, U)  # revealed: never
-    reveal_when_subtype_of(U, T)  # revealed: never
+    reveal_type(is_subtype_of(T, U))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(U, T))  # revealed: ty_extensions.ConstraintSet[never]
 ```
 
 A constrained fully static typevar is assignable to the union of its constraints, but not to any of
@@ -232,64 +232,64 @@ intersection of all of its constraints is a subtype of the typevar.
 from ty_extensions import Intersection
 
 def constrained[T: (Base, Unrelated)](t: T) -> None:
-    reveal_when_assignable_to(T, Super)  # revealed: never
-    reveal_when_assignable_to(T, Base)  # revealed: never
-    reveal_when_assignable_to(T, Sub)  # revealed: never
-    reveal_when_assignable_to(T, Unrelated)  # revealed: never
-    reveal_when_assignable_to(T, Super | Unrelated)  # revealed: always
-    reveal_when_assignable_to(T, Base | Unrelated)  # revealed: always
-    reveal_when_assignable_to(T, Sub | Unrelated)  # revealed: never
-    reveal_when_assignable_to(Super, T)  # revealed: never
-    reveal_when_assignable_to(Unrelated, T)  # revealed: never
-    reveal_when_assignable_to(Super | Unrelated, T)  # revealed: never
-    reveal_when_assignable_to(Intersection[Base, Unrelated], T)  # revealed: always
+    reveal_type(is_assignable_to(T, Super))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(T, Base))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(T, Sub))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(T, Unrelated))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(T, Super | Unrelated))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(T, Base | Unrelated))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(T, Sub | Unrelated))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(Super, T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(Unrelated, T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(Super | Unrelated, T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(Intersection[Base, Unrelated], T))  # revealed: ty_extensions.ConstraintSet[always]
 
-    reveal_when_subtype_of(T, Super)  # revealed: never
-    reveal_when_subtype_of(T, Base)  # revealed: never
-    reveal_when_subtype_of(T, Sub)  # revealed: never
-    reveal_when_subtype_of(T, Unrelated)  # revealed: never
-    reveal_when_subtype_of(T, Super | Unrelated)  # revealed: always
-    reveal_when_subtype_of(T, Base | Unrelated)  # revealed: always
-    reveal_when_subtype_of(T, Sub | Unrelated)  # revealed: never
-    reveal_when_subtype_of(Super, T)  # revealed: never
-    reveal_when_subtype_of(Unrelated, T)  # revealed: never
-    reveal_when_subtype_of(Super | Unrelated, T)  # revealed: never
-    reveal_when_subtype_of(Intersection[Base, Unrelated], T)  # revealed: always
+    reveal_type(is_subtype_of(T, Super))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(T, Base))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(T, Sub))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(T, Unrelated))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(T, Super | Unrelated))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_subtype_of(T, Base | Unrelated))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_subtype_of(T, Sub | Unrelated))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(Super, T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(Unrelated, T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(Super | Unrelated, T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(Intersection[Base, Unrelated], T))  # revealed: ty_extensions.ConstraintSet[always]
 
 def constrained_by_gradual[T: (Base, Any)](t: T) -> None:
-    reveal_when_assignable_to(T, Super)  # revealed: always
-    reveal_when_assignable_to(T, Base)  # revealed: always
-    reveal_when_assignable_to(T, Sub)  # revealed: never
-    reveal_when_assignable_to(T, Unrelated)  # revealed: never
-    reveal_when_assignable_to(T, Any)  # revealed: always
-    reveal_when_assignable_to(T, Super | Any)  # revealed: always
-    reveal_when_assignable_to(T, Super | Unrelated)  # revealed: always
-    reveal_when_assignable_to(Super, T)  # revealed: never
-    reveal_when_assignable_to(Base, T)  # revealed: always
-    reveal_when_assignable_to(Unrelated, T)  # revealed: never
-    reveal_when_assignable_to(Any, T)  # revealed: always
-    reveal_when_assignable_to(Super | Any, T)  # revealed: never
-    reveal_when_assignable_to(Base | Any, T)  # revealed: always
-    reveal_when_assignable_to(Super | Unrelated, T)  # revealed: never
-    reveal_when_assignable_to(Intersection[Base, Unrelated], T)  # revealed: always
-    reveal_when_assignable_to(Intersection[Base, Any], T)  # revealed: always
+    reveal_type(is_assignable_to(T, Super))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(T, Base))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(T, Sub))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(T, Unrelated))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(T, Any))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(T, Super | Any))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(T, Super | Unrelated))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(Super, T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(Base, T))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(Unrelated, T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(Any, T))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(Super | Any, T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(Base | Any, T))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(Super | Unrelated, T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(Intersection[Base, Unrelated], T))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(Intersection[Base, Any], T))  # revealed: ty_extensions.ConstraintSet[always]
 
-    reveal_when_subtype_of(T, Super)  # revealed: never
-    reveal_when_subtype_of(T, Base)  # revealed: never
-    reveal_when_subtype_of(T, Sub)  # revealed: never
-    reveal_when_subtype_of(T, Unrelated)  # revealed: never
-    reveal_when_subtype_of(T, Any)  # revealed: never
-    reveal_when_subtype_of(T, Super | Any)  # revealed: never
-    reveal_when_subtype_of(T, Super | Unrelated)  # revealed: never
-    reveal_when_subtype_of(Super, T)  # revealed: never
-    reveal_when_subtype_of(Base, T)  # revealed: never
-    reveal_when_subtype_of(Unrelated, T)  # revealed: never
-    reveal_when_subtype_of(Any, T)  # revealed: never
-    reveal_when_subtype_of(Super | Any, T)  # revealed: never
-    reveal_when_subtype_of(Base | Any, T)  # revealed: never
-    reveal_when_subtype_of(Super | Unrelated, T)  # revealed: never
-    reveal_when_subtype_of(Intersection[Base, Unrelated], T)  # revealed: never
-    reveal_when_subtype_of(Intersection[Base, Any], T)  # revealed: never
+    reveal_type(is_subtype_of(T, Super))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(T, Base))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(T, Sub))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(T, Unrelated))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(T, Any))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(T, Super | Any))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(T, Super | Unrelated))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(Super, T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(Base, T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(Unrelated, T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(Any, T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(Super | Any, T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(Base | Any, T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(Super | Unrelated, T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(Intersection[Base, Unrelated], T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(Intersection[Base, Any], T))  # revealed: ty_extensions.ConstraintSet[never]
 ```
 
 Two distinct fully static typevars are not subtypes of each other, even if they have the same
@@ -299,43 +299,43 @@ the same type.
 
 ```py
 def two_constrained[T: (int, str), U: (int, str)](t: T, u: U) -> None:
-    reveal_when_assignable_to(T, U)  # revealed: never
-    reveal_when_assignable_to(U, T)  # revealed: never
+    reveal_type(is_assignable_to(T, U))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(U, T))  # revealed: ty_extensions.ConstraintSet[never]
 
-    reveal_when_subtype_of(T, U)  # revealed: never
-    reveal_when_subtype_of(U, T)  # revealed: never
+    reveal_type(is_subtype_of(T, U))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(U, T))  # revealed: ty_extensions.ConstraintSet[never]
 
 @final
 class AnotherFinalClass: ...
 
 def two_final_constrained[T: (FinalClass, AnotherFinalClass), U: (FinalClass, AnotherFinalClass)](t: T, u: U) -> None:
-    reveal_when_assignable_to(T, U)  # revealed: never
-    reveal_when_assignable_to(U, T)  # revealed: never
+    reveal_type(is_assignable_to(T, U))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_assignable_to(U, T))  # revealed: ty_extensions.ConstraintSet[never]
 
-    reveal_when_subtype_of(T, U)  # revealed: never
-    reveal_when_subtype_of(U, T)  # revealed: never
+    reveal_type(is_subtype_of(T, U))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(U, T))  # revealed: ty_extensions.ConstraintSet[never]
 ```
 
 A bound or constrained typevar is a subtype of itself in a union:
 
 ```py
 def union[T: Base, U: (Base, Unrelated)](t: T, u: U) -> None:
-    reveal_when_assignable_to(T, T | None)  # revealed: always
-    reveal_when_assignable_to(U, U | None)  # revealed: always
+    reveal_type(is_assignable_to(T, T | None))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(U, U | None))  # revealed: ty_extensions.ConstraintSet[always]
 
-    reveal_when_subtype_of(T, T | None)  # revealed: always
-    reveal_when_subtype_of(U, U | None)  # revealed: always
+    reveal_type(is_subtype_of(T, T | None))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_subtype_of(U, U | None))  # revealed: ty_extensions.ConstraintSet[always]
 ```
 
 A bound or constrained typevar in a union with a dynamic type is assignable to the typevar:
 
 ```py
 def union_with_dynamic[T: Base, U: (Base, Unrelated)](t: T, u: U) -> None:
-    reveal_when_assignable_to(T | Any, T)  # revealed: always
-    reveal_when_assignable_to(U | Any, U)  # revealed: always
+    reveal_type(is_assignable_to(T | Any, T))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(U | Any, U))  # revealed: ty_extensions.ConstraintSet[always]
 
-    reveal_when_subtype_of(T | Any, T)  # revealed: never
-    reveal_when_subtype_of(U | Any, U)  # revealed: never
+    reveal_type(is_subtype_of(T | Any, T))  # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(is_subtype_of(U | Any, U))  # revealed: ty_extensions.ConstraintSet[never]
 ```
 
 And an intersection of a typevar with another type is always a subtype of the TypeVar:
@@ -346,11 +346,11 @@ from ty_extensions import Intersection, Not, is_disjoint_from, static_assert
 class A: ...
 
 def inter[T: Base, U: (Base, Unrelated)](t: T, u: U) -> None:
-    reveal_when_assignable_to(Intersection[T, Unrelated], T)  # revealed: always
-    reveal_when_subtype_of(Intersection[T, Unrelated], T)  # revealed: always
+    reveal_type(is_assignable_to(Intersection[T, Unrelated], T))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_subtype_of(Intersection[T, Unrelated], T))  # revealed: ty_extensions.ConstraintSet[always]
 
-    reveal_when_assignable_to(Intersection[U, A], U)  # revealed: always
-    reveal_when_subtype_of(Intersection[U, A], U)  # revealed: always
+    reveal_type(is_assignable_to(Intersection[U, A], U))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_subtype_of(Intersection[U, A], U))  # revealed: ty_extensions.ConstraintSet[always]
 
     static_assert(is_disjoint_from(Not[T], T))
     static_assert(is_disjoint_from(T, Not[T]))
@@ -647,14 +647,14 @@ The intersection of a typevar with any other type is assignable to (and if fully
 of) itself.
 
 ```py
-from ty_extensions import reveal_when_assignable_to, reveal_when_subtype_of, Not
+from ty_extensions import is_assignable_to, is_subtype_of, Not
 
 def intersection_is_assignable[T](t: T) -> None:
-    reveal_when_assignable_to(Intersection[T, None], T)  # revealed: always
-    reveal_when_assignable_to(Intersection[T, Not[None]], T)  # revealed: always
+    reveal_type(is_assignable_to(Intersection[T, None], T))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_assignable_to(Intersection[T, Not[None]], T))  # revealed: ty_extensions.ConstraintSet[always]
 
-    reveal_when_subtype_of(Intersection[T, None], T)  # revealed: always
-    reveal_when_subtype_of(Intersection[T, Not[None]], T)  # revealed: always
+    reveal_type(is_subtype_of(Intersection[T, None], T))  # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(is_subtype_of(Intersection[T, Not[None]], T))  # revealed: ty_extensions.ConstraintSet[always]
 ```
 
 ## Narrowing
diff --git a/crates/ty_python_semantic/resources/mdtest/ty_extensions.md b/crates/ty_python_semantic/resources/mdtest/ty_extensions.md
index db29efb107..0d93d3ed2e 100644
--- a/crates/ty_python_semantic/resources/mdtest/ty_extensions.md
+++ b/crates/ty_python_semantic/resources/mdtest/ty_extensions.md
@@ -398,7 +398,7 @@ the expression `str`:
 from ty_extensions import TypeOf, is_subtype_of, static_assert
 
 # This is incorrect and therefore fails with ...
-# error: "Static assertion error: argument evaluates to `False`"
+# error: "Static assertion error: argument of type `ty_extensions.ConstraintSet[never]` is statically known to be falsy"
 static_assert(is_subtype_of(str, type[str]))
 
 # Correct, returns True:
diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md b/crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md
new file mode 100644
index 0000000000..f00f199cb1
--- /dev/null
+++ b/crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md
@@ -0,0 +1,769 @@
+# Constraints
+
+```toml
+[environment]
+python-version = "3.13"
+```
+
+For "concrete" types (which contain no type variables), type properties like assignability have
+simple answers: one type is either assignable to another type, or it isn't. (The _rules_ for
+comparing two particular concrete types can be rather complex, but the _answer_ is a simple "yes" or
+"no".)
+
+These properties are more complex when type variables are involved, because there are (usually) many
+different concrete types that a typevar can be specialized to, and the type property might hold for
+some specializations, but not for others. That means that for types that include typevars, "Is this
+type assignable to another?" no longer makes sense as a question. The better question is: "Under
+what constraints is this type assignable to another?".
+
+An individual constraint restricts the specialization of a single typevar. You can then build up
+more complex constraint sets using union, intersection, and negation operations. We use a
+disjunctive normal form (DNF) representation, just like we do for types: a _constraint set_ is the
+union of zero or more _clauses_, each of which is the intersection of zero or more _individual
+constraints_. Note that the constraint set that contains no clauses is never satisfiable
+(`⋃ {} = 0`); and the constraint set that contains a single clause, where that clause contains no
+constraints, is always satisfiable (`⋃ {⋂ {}} = 1`).
+
+## Kinds of constraints
+
+### Range
+
+A _range_ constraint requires the typevar to be within a particular lower and upper bound: the
+typevar can only specialize to a type that is a supertype of the lower bound, and a subtype of the
+upper bound.
+
+```py
+from typing import Any, final, Never, Sequence
+from ty_extensions import range_constraint
+
+class Super: ...
+class Base(Super): ...
+class Sub(Base): ...
+
+@final
+class Unrelated: ...
+
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Super)]
+    reveal_type(range_constraint(Sub, T, Super))
+```
+
+Every type is a supertype of `Never`, so a lower bound of `Never` is the same as having no lower
+bound.
+
+```py
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≤ Base)]
+    reveal_type(range_constraint(Never, T, Base))
+```
+
+Similarly, every type is a subtype of `object`, so an upper bound of `object` is the same as having
+no upper bound.
+
+```py
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[(Base ≤ T@_)]
+    reveal_type(range_constraint(Base, T, object))
+```
+
+And a range constraint with _both_ a lower bound of `Never` and an upper bound of `object` does not
+constrain the typevar at all.
+
+```py
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(range_constraint(Never, T, object))
+```
+
+If the lower bound and upper bounds are "inverted" (the upper bound is a subtype of the lower bound)
+or incomparable, then there is no type that can satisfy the constraint.
+
+```py
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(range_constraint(Super, T, Sub))
+    # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(range_constraint(Base, T, Unrelated))
+```
+
+The lower and upper bound can be the same type, in which case the typevar can only be specialized to
+that specific type.
+
+```py
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Base)]
+    reveal_type(range_constraint(Base, T, Base))
+```
+
+Constraints can only refer to fully static types, so the lower and upper bounds are transformed into
+their bottom and top materializations, respectively.
+
+```py
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[(Base ≤ T@_)]
+    reveal_type(range_constraint(Base, T, Any))
+    # revealed: ty_extensions.ConstraintSet[(Sequence[Base] ≤ T@_ ≤ Sequence[object])]
+    reveal_type(range_constraint(Sequence[Base], T, Sequence[Any]))
+
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≤ Base)]
+    reveal_type(range_constraint(Any, T, Base))
+    # revealed: ty_extensions.ConstraintSet[(Sequence[Never] ≤ T@_ ≤ Sequence[Base])]
+    reveal_type(range_constraint(Sequence[Any], T, Sequence[Base]))
+```
+
+### Not equivalent
+
+A _not-equivalent_ constraint requires the typevar to specialize to anything _other_ than a
+particular type (the "hole").
+
+```py
+from typing import Any, Never, Sequence
+from ty_extensions import not_equivalent_constraint
+
+class Base: ...
+
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base)]
+    reveal_type(not_equivalent_constraint(T, Base))
+```
+
+Unlike range constraints, `Never` and `object` are not special when used as the hole of a
+not-equivalent constraint — there are many types that are not equivalent to `Never` or `object`.
+
+```py
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≠ Never)]
+    reveal_type(not_equivalent_constraint(T, Never))
+
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≠ object)]
+    reveal_type(not_equivalent_constraint(T, object))
+```
+
+Constraints can only refer to fully static types. However, not-equivalent constraints are not
+created directly; they are only created when negating a range constraint. Since that range
+constraint will have fully static lower and upper bounds, the not-equivalent constraints that we
+create will already have a fully static hole. Therefore, we raise a diagnostic when calling the
+internal `not_equivalent_constraint` constructor with a non-fully-static type.
+
+```py
+def _[T]() -> None:
+    # error: [invalid-argument-type] "Not-equivalent constraint must have a fully static type"
+    reveal_type(not_equivalent_constraint(T, Any))  # revealed: ConstraintSet
+    # error: [invalid-argument-type] "Not-equivalent constraint must have a fully static type"
+    reveal_type(not_equivalent_constraint(T, Sequence[Any]))  # revealed: ConstraintSet
+```
+
+### Incomparable
+
+An _incomparable_ constraint requires the typevar to specialize to any type that is neither a
+subtype nor a supertype of a particular type (the "pivot").
+
+```py
+from typing import Any, Never, Sequence
+from ty_extensions import incomparable_constraint
+
+class Base: ...
+
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base)]
+    reveal_type(incomparable_constraint(T, Base))
+```
+
+Every type is comparable with `Never` and with `object`, so an incomparable constraint with either
+as a pivot cannot ever be satisfied.
+
+```py
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(incomparable_constraint(T, Never))
+
+    # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(incomparable_constraint(T, object))
+```
+
+Constraints can only refer to fully static types. However, incomparable constraints are not created
+directly; they are only created when negating a range constraint. Since that range constraint will
+have fully static lower and upper bounds, the incomparable constraints that we create will already
+have a fully static hole. Therefore, we raise a diagnostic when calling the internal
+`incomparable_constraint` constructor with a non-fully-static type.
+
+```py
+def _[T]() -> None:
+    # error: [invalid-argument-type] "Incomparable constraint must have a fully static type"
+    reveal_type(incomparable_constraint(T, Any))  # revealed: ConstraintSet
+    # error: [invalid-argument-type] "Incomparable constraint must have a fully static type"
+    reveal_type(incomparable_constraint(T, Sequence[Any]))  # revealed: ConstraintSet
+```
+
+## Intersection
+
+The intersection of two constraint sets requires that the constraints in both sets hold. In many
+cases, we can simplify the result of an intersection.
+
+### Different typevars
+
+```py
+from ty_extensions import incomparable_constraint, not_equivalent_constraint, range_constraint
+
+class Super: ...
+class Base(Super): ...
+class Sub(Base): ...
+```
+
+We cannot simplify the intersection of constraints that refer to different typevars.
+
+```py
+def _[T, U]() -> None:
+    # revealed: ty_extensions.ConstraintSet[((T@_ ≁ Base) ∧ (U@_ ≁ Base))]
+    reveal_type(incomparable_constraint(T, Base) & incomparable_constraint(U, Base))
+    # revealed: ty_extensions.ConstraintSet[((T@_ ≠ Base) ∧ (U@_ ≠ Base))]
+    reveal_type(not_equivalent_constraint(T, Base) & not_equivalent_constraint(U, Base))
+    # revealed: ty_extensions.ConstraintSet[((Sub ≤ T@_ ≤ Base) ∧ (Sub ≤ U@_ ≤ Base))]
+    reveal_type(range_constraint(Sub, T, Base) & range_constraint(Sub, U, Base))
+```
+
+Intersection is reflexive.
+
+```py
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base)]
+    reveal_type(incomparable_constraint(T, Base) & incomparable_constraint(T, Base))
+```
+
+### Intersection of two ranges
+
+The intersection of two ranges is where the ranges "overlap".
+
+```py
+from typing import final
+from ty_extensions import range_constraint
+
+class Super: ...
+class Base(Super): ...
+class Sub(Base): ...
+class SubSub(Sub): ...
+
+@final
+class Unrelated: ...
+
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base)]
+    reveal_type(range_constraint(SubSub, T, Base) & range_constraint(Sub, T, Super))
+    # revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base)]
+    reveal_type(range_constraint(SubSub, T, Super) & range_constraint(Sub, T, Base))
+    # revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Base)]
+    reveal_type(range_constraint(Sub, T, Base) & range_constraint(Base, T, Super))
+    # revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Super)]
+    reveal_type(range_constraint(Sub, T, Super) & range_constraint(Sub, T, Super))
+```
+
+If they don't overlap, the intersection is empty.
+
+```py
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(range_constraint(SubSub, T, Sub) & range_constraint(Base, T, Super))
+    # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(range_constraint(SubSub, T, Sub) & range_constraint(Unrelated, T, object))
+```
+
+### Intersection of range and not-equivalent
+
+If the hole of a not-equivalent constraint is within the lower and upper bounds of a range
+constraint, the intersection "removes" the hole from the range. The intersection cannot be
+simplified.
+
+```py
+from typing import final
+from ty_extensions import not_equivalent_constraint, range_constraint
+
+class Super: ...
+class Base(Super): ...
+class Sub(Base): ...
+
+@final
+class Unrelated: ...
+
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[((Sub ≤ T@_ ≤ Super) ∧ (T@_ ≠ Base))]
+    reveal_type(range_constraint(Sub, T, Super) & not_equivalent_constraint(T, Base))
+```
+
+If the hole is not within the lower and upper bounds (because it's a subtype of the lower bound, a
+supertype of the upper bound, or not comparable with either), then removing the hole doesn't do
+anything.
+
+```py
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Super)]
+    reveal_type(range_constraint(Base, T, Super) & not_equivalent_constraint(T, Sub))
+    # revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Super)]
+    reveal_type(range_constraint(Base, T, Super) & not_equivalent_constraint(T, Unrelated))
+    # revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base)]
+    reveal_type(range_constraint(Sub, T, Base) & not_equivalent_constraint(T, Super))
+    # revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base)]
+    reveal_type(range_constraint(Sub, T, Base) & not_equivalent_constraint(T, Unrelated))
+```
+
+If the lower and upper bounds are the same, it's actually an "equivalent" constraint. If the hole is
+also that same type, then the intersection is empty — the not-equivalent constraint removes the only
+type that satisfies the range constraint.
+
+```py
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(range_constraint(Base, T, Base) & not_equivalent_constraint(T, Base))
+```
+
+### Intersection of range and incomparable
+
+The intersection of a range constraint and an incomparable constraint cannot be satisfied if the
+pivot is a subtype of the lower bound, or a supertype of the upper bound. (If the pivot is a subtype
+of the lower bound, then by transitivity, the pivot is also a subtype of everything in the range.)
+
+```py
+from typing import final
+from ty_extensions import incomparable_constraint, range_constraint
+
+class Super: ...
+class Base(Super): ...
+class Sub(Base): ...
+
+@final
+class Unrelated: ...
+
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(range_constraint(Base, T, Super) & incomparable_constraint(T, Sub))
+    # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(range_constraint(Base, T, Super) & incomparable_constraint(T, Base))
+
+    # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(range_constraint(Sub, T, Base) & incomparable_constraint(T, Super))
+    # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(range_constraint(Sub, T, Base) & incomparable_constraint(T, Base))
+```
+
+Otherwise, the intersection cannot be simplified.
+
+```py
+from ty_extensions import is_subtype_of
+
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[((Base ≤ T@_ ≤ Super) ∧ (T@_ ≁ Unrelated))]
+    reveal_type(range_constraint(Base, T, Super) & incomparable_constraint(T, Unrelated))
+```
+
+### Intersection of two not-equivalents
+
+Intersection is reflexive, so the intersection of a not-equivalent constraint with itself is itself.
+
+```py
+from typing import final
+from ty_extensions import not_equivalent_constraint
+
+class Super: ...
+class Base(Super): ...
+class Sub(Base): ...
+
+@final
+class Unrelated: ...
+
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base)]
+    reveal_type(not_equivalent_constraint(T, Base) & not_equivalent_constraint(T, Base))
+    # revealed: ty_extensions.ConstraintSet[((T@_ ≠ Base) ∧ (T@_ ≠ Super))]
+    reveal_type(not_equivalent_constraint(T, Base) & not_equivalent_constraint(T, Super))
+    # revealed: ty_extensions.ConstraintSet[((T@_ ≠ Base) ∧ (T@_ ≠ Sub))]
+    reveal_type(not_equivalent_constraint(T, Base) & not_equivalent_constraint(T, Sub))
+    # revealed: ty_extensions.ConstraintSet[((T@_ ≠ Base) ∧ (T@_ ≠ Unrelated))]
+    reveal_type(not_equivalent_constraint(T, Base) & not_equivalent_constraint(T, Unrelated))
+```
+
+### Intersection of not-equivalent and incomparable
+
+When intersecting a not-equivalent constraint and an incomparable constraint, if the hole and pivot
+are comparable, then the incomparable constraint already excludes the hole, so removing the hole
+doesn't do anything.
+
+```py
+from typing import final
+from ty_extensions import incomparable_constraint, not_equivalent_constraint
+
+class Super: ...
+class Base(Super): ...
+class Sub(Base): ...
+
+@final
+class Unrelated: ...
+
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base)]
+    reveal_type(not_equivalent_constraint(T, Super) & incomparable_constraint(T, Base))
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base)]
+    reveal_type(not_equivalent_constraint(T, Base) & incomparable_constraint(T, Base))
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base)]
+    reveal_type(not_equivalent_constraint(T, Sub) & incomparable_constraint(T, Base))
+    # revealed: ty_extensions.ConstraintSet[((T@_ ≠ Unrelated) ∧ (T@_ ≁ Base))]
+    reveal_type(not_equivalent_constraint(T, Unrelated) & incomparable_constraint(T, Base))
+
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Super)]
+    reveal_type(not_equivalent_constraint(T, Base) & incomparable_constraint(T, Super))
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base)]
+    reveal_type(not_equivalent_constraint(T, Base) & incomparable_constraint(T, Base))
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Sub)]
+    reveal_type(not_equivalent_constraint(T, Base) & incomparable_constraint(T, Sub))
+    # revealed: ty_extensions.ConstraintSet[((T@_ ≠ Base) ∧ (T@_ ≁ Unrelated))]
+    reveal_type(not_equivalent_constraint(T, Base) & incomparable_constraint(T, Unrelated))
+```
+
+### Intersection of two incomparables
+
+We can only simplify the intersection of two incomparable constraints if they have the same pivot.
+
+```py
+from typing import final
+from ty_extensions import incomparable_constraint
+
+class Super: ...
+class Base(Super): ...
+class Sub(Base): ...
+
+@final
+class Unrelated: ...
+
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base)]
+    reveal_type(incomparable_constraint(T, Base) & incomparable_constraint(T, Base))
+    # revealed: ty_extensions.ConstraintSet[((T@_ ≁ Base) ∧ (T@_ ≁ Super))]
+    reveal_type(incomparable_constraint(T, Base) & incomparable_constraint(T, Super))
+    # revealed: ty_extensions.ConstraintSet[((T@_ ≁ Base) ∧ (T@_ ≁ Sub))]
+    reveal_type(incomparable_constraint(T, Base) & incomparable_constraint(T, Sub))
+    # revealed: ty_extensions.ConstraintSet[((T@_ ≁ Base) ∧ (T@_ ≁ Unrelated))]
+    reveal_type(incomparable_constraint(T, Base) & incomparable_constraint(T, Unrelated))
+```
+
+## Union
+
+The union of two constraint sets requires that the constraints in either set hold. In many cases, we
+can simplify the result of an union.
+
+### Different typevars
+
+```py
+from ty_extensions import incomparable_constraint, not_equivalent_constraint, range_constraint
+
+class Super: ...
+class Base(Super): ...
+class Sub(Base): ...
+```
+
+We cannot simplify the union of constraints that refer to different typevars.
+
+```py
+def _[T, U]() -> None:
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base) ∨ (U@_ ≁ Base)]
+    reveal_type(incomparable_constraint(T, Base) | incomparable_constraint(U, Base))
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base) ∨ (U@_ ≠ Base)]
+    reveal_type(not_equivalent_constraint(T, Base) | not_equivalent_constraint(U, Base))
+    # revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base) ∨ (Sub ≤ U@_ ≤ Base)]
+    reveal_type(range_constraint(Sub, T, Base) | range_constraint(Sub, U, Base))
+```
+
+Union is reflexive.
+
+```py
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base)]
+    reveal_type(incomparable_constraint(T, Base) | incomparable_constraint(T, Base))
+```
+
+### Union of two ranges
+
+When one of the bounds is entirely contained within the other, the union simplifies to the larger
+bounds.
+
+```py
+from typing import final
+from ty_extensions import range_constraint
+
+class Super: ...
+class Base(Super): ...
+class Sub(Base): ...
+class SubSub(Sub): ...
+
+@final
+class Unrelated: ...
+
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[(SubSub ≤ T@_ ≤ Super)]
+    reveal_type(range_constraint(SubSub, T, Super) | range_constraint(Sub, T, Base))
+    # revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Super)]
+    reveal_type(range_constraint(Sub, T, Super) | range_constraint(Sub, T, Super))
+```
+
+Otherwise, the union cannot be simplified.
+
+```py
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base) ∨ (Base ≤ T@_ ≤ Super)]
+    reveal_type(range_constraint(Sub, T, Base) | range_constraint(Base, T, Super))
+    # revealed: ty_extensions.ConstraintSet[(SubSub ≤ T@_ ≤ Sub) ∨ (Base ≤ T@_ ≤ Super)]
+    reveal_type(range_constraint(SubSub, T, Sub) | range_constraint(Base, T, Super))
+    # revealed: ty_extensions.ConstraintSet[(SubSub ≤ T@_ ≤ Sub) ∨ (Unrelated ≤ T@_)]
+    reveal_type(range_constraint(SubSub, T, Sub) | range_constraint(Unrelated, T, object))
+```
+
+In particular, the following does not simplify, even though it seems like it could simplify to
+`SubSub ≤ T@_ ≤ Super`. The issue is that there are types that are within the bounds of
+`SubSub ≤ T@_ ≤ Super`, but which are not comparable to `Base` or `Sub`, and which therefore should
+not be included in the union. An example would be the type that contains all instances of `Super`,
+`Base`, and `SubSub` (but _not_ including instances of `Sub`). (We don't have a way to spell that
+type at the moment, but it is a valid type.) That type is not in `SubSub ≤ T ≤ Base`, since it
+includes `Super`, which is outside the range. It's also not in `Sub ≤ T ≤ Super`, because it does
+not include `Sub`. That means it should not be in the union. Since that type _is_ in
+`SubSub ≤ T ≤ Super`, it is not correct to simplify the union in this way.
+
+```py
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[(SubSub ≤ T@_ ≤ Base) ∨ (Sub ≤ T@_ ≤ Super)]
+    reveal_type(range_constraint(SubSub, T, Base) | range_constraint(Sub, T, Super))
+```
+
+### Union of range and not-equivalent
+
+If the hole of a not-equivalent constraint is within the lower and upper bounds of a range
+constraint, the range "fills in" the hole. The resulting union can always be satisfied.
+
+```py
+from typing import final
+from ty_extensions import not_equivalent_constraint, range_constraint
+
+class Super: ...
+class Base(Super): ...
+class Sub(Base): ...
+
+@final
+class Unrelated: ...
+
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(range_constraint(Sub, T, Super) | not_equivalent_constraint(T, Base))
+```
+
+Otherwise the range constraint is subsumed by the not-equivalent constraint.
+
+```py
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≠ Super)]
+    reveal_type(range_constraint(Sub, T, Base) | not_equivalent_constraint(T, Super))
+```
+
+### Union of range and incomparable
+
+When the "pivot" of the incomparable constraint is not comparable with either bound of the range
+constraint, the incomparable constraint subsumes the range constraint.
+
+```py
+from typing import final
+from ty_extensions import incomparable_constraint, range_constraint
+
+class Super: ...
+class Base(Super): ...
+class Sub(Base): ...
+
+@final
+class Unrelated: ...
+
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Unrelated)]
+    reveal_type(range_constraint(Base, T, Super) | incomparable_constraint(T, Unrelated))
+```
+
+Otherwise, the union cannot be simplified.
+
+```py
+from ty_extensions import is_subtype_of
+
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Super) ∨ (T@_ ≁ Base)]
+    reveal_type(range_constraint(Base, T, Super) | incomparable_constraint(T, Base))
+    # revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Super) ∨ (T@_ ≁ Sub)]
+    reveal_type(range_constraint(Base, T, Super) | incomparable_constraint(T, Sub))
+    # revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Super) ∨ (T@_ ≁ Super)]
+    reveal_type(range_constraint(Base, T, Super) | incomparable_constraint(T, Super))
+```
+
+### Union of two not-equivalents
+
+Union is reflexive, so the union of a not-equivalent constraint with itself is itself. The union of
+two different not-equivalent constraints is always satisfied.
+
+```py
+from typing import final
+from ty_extensions import not_equivalent_constraint
+
+class Super: ...
+class Base(Super): ...
+class Sub(Base): ...
+
+@final
+class Unrelated: ...
+
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base)]
+    reveal_type(not_equivalent_constraint(T, Base) | not_equivalent_constraint(T, Base))
+    # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(not_equivalent_constraint(T, Base) | not_equivalent_constraint(T, Super))
+    # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(not_equivalent_constraint(T, Base) | not_equivalent_constraint(T, Sub))
+    # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(not_equivalent_constraint(T, Base) | not_equivalent_constraint(T, Unrelated))
+```
+
+### Union of not-equivalent and incomparable
+
+When the hole of the non-equivalent constraint and the pivot of the incomparable constraint are not
+comparable, then the hole is covered by the incomparable constraint, and the union is therefore
+always satisfied.
+
+```py
+from typing import final
+from ty_extensions import incomparable_constraint, not_equivalent_constraint
+
+class Super: ...
+class Base(Super): ...
+class Sub(Base): ...
+
+@final
+class Unrelated: ...
+
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(not_equivalent_constraint(T, Unrelated) | incomparable_constraint(T, Base))
+    # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(not_equivalent_constraint(T, Base) | incomparable_constraint(T, Unrelated))
+```
+
+Otherwise, the hole and pivot are comparable, and the non-equivalent constraint subsumes the
+incomparable constraint.
+
+```py
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base)]
+    reveal_type(not_equivalent_constraint(T, Base) | incomparable_constraint(T, Super))
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base)]
+    reveal_type(not_equivalent_constraint(T, Base) | incomparable_constraint(T, Base))
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base)]
+    reveal_type(not_equivalent_constraint(T, Base) | incomparable_constraint(T, Sub))
+
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≠ Super)]
+    reveal_type(not_equivalent_constraint(T, Super) | incomparable_constraint(T, Base))
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≠ Base)]
+    reveal_type(not_equivalent_constraint(T, Base) | incomparable_constraint(T, Base))
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≠ Sub)]
+    reveal_type(not_equivalent_constraint(T, Sub) | incomparable_constraint(T, Base))
+```
+
+### Union of two incomparables
+
+We can only simplify the union of two incomparable constraints if they have the same pivot.
+
+```py
+from typing import final
+from ty_extensions import incomparable_constraint
+
+class Super: ...
+class Base(Super): ...
+class Sub(Base): ...
+
+@final
+class Unrelated: ...
+
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base)]
+    reveal_type(incomparable_constraint(T, Base) | incomparable_constraint(T, Base))
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base) ∨ (T@_ ≁ Super)]
+    reveal_type(incomparable_constraint(T, Base) | incomparable_constraint(T, Super))
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base) ∨ (T@_ ≁ Sub)]
+    reveal_type(incomparable_constraint(T, Base) | incomparable_constraint(T, Sub))
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≁ Base) ∨ (T@_ ≁ Unrelated)]
+    reveal_type(incomparable_constraint(T, Base) | incomparable_constraint(T, Unrelated))
+```
+
+## Negation
+
+### Negation of a range constraint
+
+In the negation of a range constraint, the typevar must specialize to a type that is not a subtype
+of the lower bound, or is not a supertype of the upper bound. Subtyping is a partial order, so one
+type is not a subtype of another if it is a _proper_ supertype, or if they are incomparable.
+
+```py
+from typing import Never
+from ty_extensions import range_constraint
+
+class Super: ...
+class Base(Super): ...
+class Sub(Base): ...
+
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[((T@_ ≤ Sub) ∧ (T@_ ≠ Sub)) ∨ (T@_ ≁ Sub) ∨ ((Base ≤ T@_) ∧ (T@_ ≠ Base)) ∨ (T@_ ≁ Base)]
+    reveal_type(~range_constraint(Sub, T, Base))
+    # revealed: ty_extensions.ConstraintSet[((Base ≤ T@_) ∧ (T@_ ≠ Base)) ∨ (T@_ ≁ Base)]
+    reveal_type(~range_constraint(Never, T, Base))
+    # revealed: ty_extensions.ConstraintSet[((T@_ ≤ Sub) ∧ (T@_ ≠ Sub)) ∨ (T@_ ≁ Sub)]
+    reveal_type(~range_constraint(Sub, T, object))
+    # revealed: ty_extensions.ConstraintSet[never]
+    reveal_type(~range_constraint(Never, T, object))
+```
+
+### Negation of a not-equivalent constraint
+
+In the negation of a not-equivalent constrant, the typevar must specialize to a type that _is_
+equivalent to the hole. The negation does not include types that are incomparable with the hole —
+those types are not equivalent to the hole, and are therefore in the original not-equivalent
+constraint, not its negation.
+
+```py
+from typing import Never
+from ty_extensions import not_equivalent_constraint
+
+class Super: ...
+class Base(Super): ...
+class Sub(Base): ...
+
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Base)]
+    reveal_type(~not_equivalent_constraint(T, Base))
+    # revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Sub)]
+    reveal_type(~not_equivalent_constraint(T, Sub))
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≤ Never)]
+    reveal_type(~not_equivalent_constraint(T, Never))
+    # revealed: ty_extensions.ConstraintSet[(object ≤ T@_)]
+    reveal_type(~not_equivalent_constraint(T, object))
+```
+
+### Negation of an incomparable constraint
+
+In the negation of an incomparable constraint, the typevar must specialize to a type that _is_
+comparable with (either a subtype _or_ supertype of) the pivot.
+
+```py
+from typing import Never
+from ty_extensions import incomparable_constraint
+
+class Super: ...
+class Base(Super): ...
+class Sub(Base): ...
+
+def _[T]() -> None:
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≤ Base) ∨ (Base ≤ T@_)]
+    reveal_type(~incomparable_constraint(T, Base))
+    # revealed: ty_extensions.ConstraintSet[(T@_ ≤ Sub) ∨ (Sub ≤ T@_)]
+    reveal_type(~incomparable_constraint(T, Sub))
+    # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(~incomparable_constraint(T, Never))
+    # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(~incomparable_constraint(T, object))
+```
diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/is_subtype_of.md b/crates/ty_python_semantic/resources/mdtest/type_properties/is_subtype_of.md
index b3201da5e2..c5086a5003 100644
--- a/crates/ty_python_semantic/resources/mdtest/type_properties/is_subtype_of.md
+++ b/crates/ty_python_semantic/resources/mdtest/type_properties/is_subtype_of.md
@@ -1708,7 +1708,7 @@ static_assert(is_subtype_of(TypeOf[B], Callable[[], B]))
 class C: ...
 
 # TODO: This assertion should be true once we understand `Self`
-# error: [static-assert-error] "Static assertion error: argument evaluates to `False`"
+# error: [static-assert-error] "Static assertion error: argument of type `ty_extensions.ConstraintSet[never]` is statically known to be falsy"
 static_assert(is_subtype_of(TypeOf[C], Callable[[], C]))
 
 class D[T]:
@@ -1865,7 +1865,7 @@ static_assert(not is_subtype_of(TypeOf[a.f], Callable[[float], int]))
 static_assert(not is_subtype_of(TypeOf[A.g], Callable[[], int]))
 
 # TODO: This assertion should be true
-# error: [static-assert-error] "Static assertion error: argument evaluates to `False`"
+# error: [static-assert-error] "Static assertion error: argument of type `ty_extensions.ConstraintSet[never]` is statically known to be falsy"
 static_assert(is_subtype_of(TypeOf[A.f], Callable[[A, int], int]))
 ```
 
diff --git a/crates/ty_python_semantic/src/types.rs b/crates/ty_python_semantic/src/types.rs
index ccf4a9f2f1..e3623f48d2 100644
--- a/crates/ty_python_semantic/src/types.rs
+++ b/crates/ty_python_semantic/src/types.rs
@@ -3838,6 +3838,11 @@ impl<'db> Type<'db> {
                 Truthiness::Ambiguous
             }
 
+            Type::KnownInstance(KnownInstanceType::ConstraintSet(tracked_set)) => {
+                let constraints = tracked_set.constraints(db);
+                Truthiness::from(constraints.is_always_satisfied(db))
+            }
+
             Type::FunctionLiteral(_)
             | Type::BoundMethod(_)
             | Type::WrapperDescriptor(_)
@@ -4186,8 +4191,8 @@ impl<'db> Type<'db> {
             Type::FunctionLiteral(function_type) => match function_type.known(db) {
                 Some(
                     KnownFunction::IsEquivalentTo
-                    | KnownFunction::IsSubtypeOf
                     | KnownFunction::IsAssignableTo
+                    | KnownFunction::IsSubtypeOf
                     | KnownFunction::IsDisjointFrom,
                 ) => Binding::single(
                     self,
@@ -4200,25 +4205,58 @@ impl<'db> Type<'db> {
                                 .type_form()
                                 .with_annotated_type(Type::any()),
                         ]),
-                        Some(KnownClass::Bool.to_instance(db)),
+                        Some(KnownClass::ConstraintSet.to_instance(db)),
                     ),
                 )
                 .into(),
 
-                Some(
-                    KnownFunction::RevealWhenAssignableTo | KnownFunction::RevealWhenSubtypeOf,
-                ) => Binding::single(
+                Some(KnownFunction::RangeConstraint) => Binding::single(
                     self,
                     Signature::new(
                         Parameters::new([
-                            Parameter::positional_only(Some(Name::new_static("a")))
+                            Parameter::positional_only(Some(Name::new_static("lower_bound")))
                                 .type_form()
                                 .with_annotated_type(Type::any()),
-                            Parameter::positional_only(Some(Name::new_static("b")))
+                            Parameter::positional_only(Some(Name::new_static("typevar")))
+                                .type_form()
+                                .with_annotated_type(Type::any()),
+                            Parameter::positional_only(Some(Name::new_static("upper_bound")))
                                 .type_form()
                                 .with_annotated_type(Type::any()),
                         ]),
-                        Some(KnownClass::NoneType.to_instance(db)),
+                        Some(KnownClass::ConstraintSet.to_instance(db)),
+                    ),
+                )
+                .into(),
+
+                Some(KnownFunction::NotEquivalentConstraint) => Binding::single(
+                    self,
+                    Signature::new(
+                        Parameters::new([
+                            Parameter::positional_only(Some(Name::new_static("typevar")))
+                                .type_form()
+                                .with_annotated_type(Type::any()),
+                            Parameter::positional_only(Some(Name::new_static("hole")))
+                                .type_form()
+                                .with_annotated_type(Type::any()),
+                        ]),
+                        Some(KnownClass::ConstraintSet.to_instance(db)),
+                    ),
+                )
+                .into(),
+
+                Some(KnownFunction::IncomparableConstraint) => Binding::single(
+                    self,
+                    Signature::new(
+                        Parameters::new([
+                            Parameter::positional_only(Some(Name::new_static("typevar")))
+                                .type_form()
+                                .with_annotated_type(Type::any()),
+                            Parameter::positional_only(Some(Name::new_static("pivot")))
+                                .type_form()
+                                .with_annotated_type(Type::any()),
+                        ]),
+                        Some(KnownClass::ConstraintSet.to_instance(db)),
                     ),
                 )
                 .into(),
@@ -5702,6 +5740,10 @@ impl<'db> Type<'db> {
                     invalid_expressions: smallvec::smallvec![InvalidTypeExpression::Field],
                     fallback_type: Type::unknown(),
                 }),
+                KnownInstanceType::ConstraintSet(__call__) => Err(InvalidTypeExpressionError {
+                    invalid_expressions: smallvec::smallvec![InvalidTypeExpression::ConstraintSet],
+                    fallback_type: Type::unknown(),
+                }),
                 KnownInstanceType::SubscriptedProtocol(_) => Err(InvalidTypeExpressionError {
                     invalid_expressions: smallvec::smallvec_inline![
                         InvalidTypeExpression::Protocol
@@ -6851,6 +6893,20 @@ impl<'db> TypeMapping<'_, 'db> {
     }
 }
 
+/// A Salsa-tracked constraint set. This is only needed to have something appropriately small to
+/// put in a [`KnownInstance::ConstraintSet`]. We don't actually manipulate these as part of using
+/// constraint sets to check things like assignability; they're only used as a debugging aid in
+/// mdtests. That means there's no need for this to be interned; being tracked is sufficient.
+#[salsa::tracked(debug, heap_size=ruff_memory_usage::heap_size)]
+#[derive(PartialOrd, Ord)]
+pub struct TrackedConstraintSet<'db> {
+    #[returns(ref)]
+    constraints: ConstraintSet<'db>,
+}
+
+// The Salsa heap is tracked separately.
+impl get_size2::GetSize for TrackedConstraintSet<'_> {}
+
 /// Singleton types that are heavily special-cased by ty. Despite its name,
 /// quite a different type to [`NominalInstanceType`].
 ///
@@ -6893,6 +6949,10 @@ pub enum KnownInstanceType<'db> {
 
     /// A single instance of `dataclasses.Field`
     Field(FieldInstance<'db>),
+
+    /// A constraint set, which is exposed in mdtests as an instance of
+    /// `ty_extensions.ConstraintSet`.
+    ConstraintSet(TrackedConstraintSet<'db>),
 }
 
 fn walk_known_instance_type<'db, V: visitor::TypeVisitor<'db> + ?Sized>(
@@ -6911,7 +6971,7 @@ 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::Deprecated(_) | KnownInstanceType::ConstraintSet(_) => {
             // Nothing to visit
         }
         KnownInstanceType::Field(field) => {
@@ -6938,6 +6998,10 @@ impl<'db> KnownInstanceType<'db> {
                 Self::Deprecated(deprecated)
             }
             Self::Field(field) => Self::Field(field.normalized_impl(db, visitor)),
+            Self::ConstraintSet(set) => {
+                // Nothing to normalize
+                Self::ConstraintSet(set)
+            }
         }
     }
 
@@ -6951,6 +7015,7 @@ impl<'db> KnownInstanceType<'db> {
             Self::TypeAliasType(_) => KnownClass::TypeAliasType,
             Self::Deprecated(_) => KnownClass::Deprecated,
             Self::Field(_) => KnownClass::Field,
+            Self::ConstraintSet(_) => KnownClass::ConstraintSet,
         }
     }
 
@@ -7010,6 +7075,20 @@ impl<'db> KnownInstanceType<'db> {
                         field.default_type(self.db).display(self.db).fmt(f)?;
                         f.write_str("]")
                     }
+                    KnownInstanceType::ConstraintSet(tracked_set) => {
+                        let constraints = tracked_set.constraints(self.db);
+                        if constraints.is_always_satisfied(self.db) {
+                            f.write_str("ty_extensions.ConstraintSet[always]")
+                        } else if constraints.is_never_satisfied(self.db) {
+                            f.write_str("ty_extensions.ConstraintSet[never]")
+                        } else {
+                            write!(
+                                f,
+                                "ty_extensions.ConstraintSet[{}]",
+                                constraints.display(self.db)
+                            )
+                        }
+                    }
                 }
             }
         }
@@ -7249,6 +7328,8 @@ enum InvalidTypeExpression<'db> {
     Deprecated,
     /// Same for `dataclasses.Field`
     Field,
+    /// Same for `ty_extensions.ConstraintSet`
+    ConstraintSet,
     /// Same for `typing.TypedDict`
     TypedDict,
     /// Type qualifiers are always invalid in *type expressions*,
@@ -7298,6 +7379,9 @@ impl<'db> InvalidTypeExpression<'db> {
                     InvalidTypeExpression::Field => {
                         f.write_str("`dataclasses.Field` is not allowed in type expressions")
                     }
+                    InvalidTypeExpression::ConstraintSet => {
+                        f.write_str("`ty_extensions.ConstraintSet` is not allowed in type expressions")
+                    }
                     InvalidTypeExpression::TypedDict => {
                         f.write_str(
                             "The special form `typing.TypedDict` is not allowed in type expressions. \
diff --git a/crates/ty_python_semantic/src/types/call/bind.rs b/crates/ty_python_semantic/src/types/call/bind.rs
index 25fdce5e09..d79493ff81 100644
--- a/crates/ty_python_semantic/src/types/call/bind.rs
+++ b/crates/ty_python_semantic/src/types/call/bind.rs
@@ -32,8 +32,8 @@ use crate::types::signatures::{Parameter, ParameterForm, Parameters};
 use crate::types::tuple::{Tuple, TupleLength, TupleType};
 use crate::types::{
     BoundMethodType, ClassLiteral, DataclassParams, FieldInstance, KnownBoundMethodType,
-    KnownClass, KnownInstanceType, PropertyInstanceType, SpecialFormType, TypeAliasType,
-    TypeMapping, UnionType, WrapperDescriptorKind, enums, ide_support, todo_type,
+    KnownClass, KnownInstanceType, PropertyInstanceType, SpecialFormType, TrackedConstraintSet,
+    TypeAliasType, TypeMapping, UnionType, WrapperDescriptorKind, enums, ide_support, todo_type,
 };
 use ruff_db::diagnostic::{Annotation, Diagnostic, SubDiagnostic, SubDiagnosticSeverity};
 use ruff_python_ast::{self as ast, PythonVersion};
@@ -586,32 +586,43 @@ impl<'db> Bindings<'db> {
                     Type::FunctionLiteral(function_type) => match function_type.known(db) {
                         Some(KnownFunction::IsEquivalentTo) => {
                             if let [Some(ty_a), Some(ty_b)] = overload.parameter_types() {
-                                overload.set_return_type(Type::BooleanLiteral(
-                                    ty_a.is_equivalent_to(db, *ty_b),
+                                let constraints =
+                                    ty_a.when_equivalent_to::<ConstraintSet>(db, *ty_b);
+                                let tracked = TrackedConstraintSet::new(db, constraints);
+                                overload.set_return_type(Type::KnownInstance(
+                                    KnownInstanceType::ConstraintSet(tracked),
                                 ));
                             }
                         }
 
                         Some(KnownFunction::IsSubtypeOf) => {
                             if let [Some(ty_a), Some(ty_b)] = overload.parameter_types() {
-                                overload.set_return_type(Type::BooleanLiteral(
-                                    ty_a.is_subtype_of(db, *ty_b),
+                                let constraints = ty_a.when_subtype_of::<ConstraintSet>(db, *ty_b);
+                                let tracked = TrackedConstraintSet::new(db, constraints);
+                                overload.set_return_type(Type::KnownInstance(
+                                    KnownInstanceType::ConstraintSet(tracked),
                                 ));
                             }
                         }
 
                         Some(KnownFunction::IsAssignableTo) => {
                             if let [Some(ty_a), Some(ty_b)] = overload.parameter_types() {
-                                overload.set_return_type(Type::BooleanLiteral(
-                                    ty_a.is_assignable_to(db, *ty_b),
+                                let constraints =
+                                    ty_a.when_assignable_to::<ConstraintSet>(db, *ty_b);
+                                let tracked = TrackedConstraintSet::new(db, constraints);
+                                overload.set_return_type(Type::KnownInstance(
+                                    KnownInstanceType::ConstraintSet(tracked),
                                 ));
                             }
                         }
 
                         Some(KnownFunction::IsDisjointFrom) => {
                             if let [Some(ty_a), Some(ty_b)] = overload.parameter_types() {
-                                overload.set_return_type(Type::BooleanLiteral(
-                                    ty_a.is_disjoint_from(db, *ty_b),
+                                let constraints =
+                                    ty_a.when_disjoint_from::<ConstraintSet>(db, *ty_b);
+                                let tracked = TrackedConstraintSet::new(db, constraints);
+                                overload.set_return_type(Type::KnownInstance(
+                                    KnownInstanceType::ConstraintSet(tracked),
                                 ));
                             }
                         }
diff --git a/crates/ty_python_semantic/src/types/class.rs b/crates/ty_python_semantic/src/types/class.rs
index fef907fe10..8284f5b7c7 100644
--- a/crates/ty_python_semantic/src/types/class.rs
+++ b/crates/ty_python_semantic/src/types/class.rs
@@ -3652,6 +3652,8 @@ pub enum KnownClass {
     TypedDictFallback,
     // string.templatelib
     Template,
+    // ty_extensions
+    ConstraintSet,
 }
 
 impl KnownClass {
@@ -3751,6 +3753,7 @@ impl KnownClass {
             | Self::InitVar
             | Self::NamedTupleFallback
             | Self::NamedTupleLike
+            | Self::ConstraintSet
             | Self::TypedDictFallback => Some(Truthiness::Ambiguous),
 
             Self::Tuple => None,
@@ -3830,6 +3833,7 @@ impl KnownClass {
             | KnownClass::InitVar
             | KnownClass::NamedTupleFallback
             | KnownClass::NamedTupleLike
+            | KnownClass::ConstraintSet
             | KnownClass::TypedDictFallback
             | KnownClass::BuiltinFunctionType
             | KnownClass::Template => false,
@@ -3908,6 +3912,7 @@ impl KnownClass {
             | KnownClass::InitVar
             | KnownClass::NamedTupleFallback
             | KnownClass::NamedTupleLike
+            | KnownClass::ConstraintSet
             | KnownClass::TypedDictFallback
             | KnownClass::BuiltinFunctionType
             | KnownClass::Template => false,
@@ -3986,6 +3991,7 @@ impl KnownClass {
             | KnownClass::TypedDictFallback
             | KnownClass::NamedTupleLike
             | KnownClass::NamedTupleFallback
+            | KnownClass::ConstraintSet
             | KnownClass::BuiltinFunctionType
             | KnownClass::Template => false,
         }
@@ -4075,6 +4081,7 @@ impl KnownClass {
             | Self::KwOnly
             | Self::InitVar
             | Self::NamedTupleFallback
+            | Self::ConstraintSet
             | Self::TypedDictFallback
             | Self::BuiltinFunctionType
             | Self::Template => false,
@@ -4173,6 +4180,7 @@ impl KnownClass {
             Self::InitVar => "InitVar",
             Self::NamedTupleFallback => "NamedTupleFallback",
             Self::NamedTupleLike => "NamedTupleLike",
+            Self::ConstraintSet => "ConstraintSet",
             Self::TypedDictFallback => "TypedDictFallback",
             Self::Template => "Template",
         }
@@ -4439,7 +4447,7 @@ impl KnownClass {
             | Self::OrderedDict => KnownModule::Collections,
             Self::Field | Self::KwOnly | Self::InitVar => KnownModule::Dataclasses,
             Self::NamedTupleFallback | Self::TypedDictFallback => KnownModule::TypeCheckerInternals,
-            Self::NamedTupleLike => KnownModule::TyExtensions,
+            Self::NamedTupleLike | Self::ConstraintSet => KnownModule::TyExtensions,
             Self::Template => KnownModule::Templatelib,
         }
     }
@@ -4518,6 +4526,7 @@ impl KnownClass {
             | Self::Iterator
             | Self::NamedTupleFallback
             | Self::NamedTupleLike
+            | Self::ConstraintSet
             | Self::TypedDictFallback
             | Self::BuiltinFunctionType
             | Self::Template => Some(false),
@@ -4601,6 +4610,7 @@ impl KnownClass {
             | Self::Iterator
             | Self::NamedTupleFallback
             | Self::NamedTupleLike
+            | Self::ConstraintSet
             | Self::TypedDictFallback
             | Self::BuiltinFunctionType
             | Self::Template => false,
@@ -4693,6 +4703,7 @@ impl KnownClass {
             "InitVar" => Self::InitVar,
             "NamedTupleFallback" => Self::NamedTupleFallback,
             "NamedTupleLike" => Self::NamedTupleLike,
+            "ConstraintSet" => Self::ConstraintSet,
             "TypedDictFallback" => Self::TypedDictFallback,
             "Template" => Self::Template,
             _ => return None,
@@ -4761,6 +4772,7 @@ impl KnownClass {
             | Self::NamedTupleFallback
             | Self::TypedDictFallback
             | Self::NamedTupleLike
+            | Self::ConstraintSet
             | Self::Awaitable
             | Self::Generator
             | Self::Template => module == self.canonical_module(db),
diff --git a/crates/ty_python_semantic/src/types/class_base.rs b/crates/ty_python_semantic/src/types/class_base.rs
index 1bcf448218..1306651c5c 100644
--- a/crates/ty_python_semantic/src/types/class_base.rs
+++ b/crates/ty_python_semantic/src/types/class_base.rs
@@ -166,7 +166,8 @@ impl<'db> ClassBase<'db> {
                 KnownInstanceType::TypeAliasType(_)
                 | KnownInstanceType::TypeVar(_)
                 | KnownInstanceType::Deprecated(_)
-                | KnownInstanceType::Field(_) => None,
+                | KnownInstanceType::Field(_)
+                | KnownInstanceType::ConstraintSet(_) => None,
             },
 
             Type::SpecialForm(special_form) => match special_form {
diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index e02be31257..f475b78b08 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -102,8 +102,12 @@ use smallvec::{SmallVec, smallvec};
 use crate::Db;
 use crate::types::{BoundTypeVarInstance, IntersectionType, Type, UnionType};
 
+fn comparable<'db>(db: &'db dyn Db, left: Type<'db>, right: Type<'db>) -> bool {
+    left.is_subtype_of(db, right) || right.is_subtype_of(db, left)
+}
+
 fn incomparable<'db>(db: &'db dyn Db, left: Type<'db>, right: Type<'db>) -> bool {
-    !left.is_subtype_of(db, right) && !right.is_subtype_of(db, left)
+    !comparable(db, left, right)
 }
 
 /// Encodes the constraints under which a type property (e.g. assignability) holds.
@@ -246,8 +250,8 @@ where
 ///   be simplified into a single clause.
 ///
 /// [POPL2015]: https://doi.org/10.1145/2676726.2676991
-#[derive(Clone, Debug)]
-pub(crate) struct ConstraintSet<'db> {
+#[derive(Clone, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)]
+pub struct ConstraintSet<'db> {
     // NOTE: We use 2 here because there are a couple of places where we create unions of 2 clauses
     // as temporary values — in particular when negating a constraint — and this lets us avoid
     // spilling the temporary value to the heap.
@@ -269,6 +273,42 @@ impl<'db> ConstraintSet<'db> {
         }
     }
 
+    pub(crate) fn range(
+        db: &'db dyn Db,
+        lower: Type<'db>,
+        typevar: BoundTypeVarInstance<'db>,
+        upper: Type<'db>,
+    ) -> Self {
+        let lower = lower.bottom_materialization(db);
+        let upper = upper.top_materialization(db);
+        let constraint = Constraint::range(db, lower, upper).constrain(typevar);
+        let mut result = Self::never();
+        result.union_constraint(db, constraint);
+        result
+    }
+
+    pub(crate) fn not_equivalent(
+        db: &'db dyn Db,
+        typevar: BoundTypeVarInstance<'db>,
+        hole: Type<'db>,
+    ) -> Self {
+        let constraint = Constraint::not_equivalent(db, hole).constrain(typevar);
+        let mut result = Self::never();
+        result.union_constraint(db, constraint);
+        result
+    }
+
+    pub(crate) fn incomparable(
+        db: &'db dyn Db,
+        typevar: BoundTypeVarInstance<'db>,
+        pivot: Type<'db>,
+    ) -> Self {
+        let constraint = Constraint::incomparable(db, pivot).constrain(typevar);
+        let mut result = Self::never();
+        result.union_constraint(db, constraint);
+        result
+    }
+
     /// Updates this set to be the union of itself and a constraint.
     fn union_constraint(
         &mut self,
@@ -429,7 +469,7 @@ impl<'db> Constraints<'db> for ConstraintSet<'db> {
 /// This is called a "constraint set", and denoted _C_, in [[POPL2015][]].
 ///
 /// [POPL2015]: https://doi.org/10.1145/2676726.2676991
-#[derive(Clone, Debug)]
+#[derive(Clone, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)]
 pub(crate) struct ConstraintClause<'db> {
     // NOTE: We use 1 here because most clauses only mention a single typevar.
     constraints: SmallVec<[ConstrainedTypeVar<'db>; 1]>,
@@ -810,7 +850,7 @@ impl<'db> ConstraintClause<'db> {
     }
 }
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+#[derive(Clone, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)]
 pub(crate) struct ConstrainedTypeVar<'db> {
     typevar: BoundTypeVarInstance<'db>,
     constraint: Constraint<'db>,
@@ -857,7 +897,7 @@ impl<'db> ConstrainedTypeVar<'db> {
     }
 }
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+#[derive(Clone, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)]
 pub(crate) enum Constraint<'db> {
     Range(RangeConstraint<'db>),
     NotEquivalent(NotEquivalentConstraint<'db>),
@@ -980,7 +1020,7 @@ impl<'db> Satisfiable<Constraint<'db>> {
     }
 }
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+#[derive(Clone, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)]
 pub(crate) struct RangeConstraint<'db> {
     lower: Type<'db>,
     upper: Type<'db>,
@@ -1054,7 +1094,7 @@ impl<'db> RangeConstraint<'db> {
         db: &'db dyn Db,
         other: &IncomparableConstraint<'db>,
     ) -> Simplifiable<Constraint<'db>> {
-        if other.ty.is_subtype_of(db, other.ty) || self.upper.is_subtype_of(db, other.ty) {
+        if other.ty.is_subtype_of(db, self.lower) || self.upper.is_subtype_of(db, other.ty) {
             return Simplifiable::NeverSatisfiable;
         }
 
@@ -1189,7 +1229,7 @@ impl<'db> RangeConstraint<'db> {
     }
 }
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+#[derive(Clone, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)]
 pub(crate) struct NotEquivalentConstraint<'db> {
     ty: Type<'db>,
 }
@@ -1224,8 +1264,9 @@ impl<'db> NotEquivalentConstraint<'db> {
         db: &'db dyn Db,
         other: &IncomparableConstraint<'db>,
     ) -> Simplifiable<Constraint<'db>> {
-        // (α ≠ t) ∧ (a ≁ t) = a ≁ t
-        if self.ty.is_equivalent_to(db, other.ty) {
+        // If the hole and pivot are comparable, then removing the hole from the incomparable
+        // constraint doesn't do anything.
+        if comparable(db, self.ty, other.ty) {
             return Simplifiable::Simplified(Constraint::Incomparable(other.clone()));
         }
         Simplifiable::NotSimplified(
@@ -1302,7 +1343,7 @@ impl<'db> NotEquivalentConstraint<'db> {
     }
 }
 
-#[derive(Clone, Debug, Eq, PartialEq)]
+#[derive(Clone, Debug, Eq, Hash, PartialEq, get_size2::GetSize, salsa::Update)]
 pub(crate) struct IncomparableConstraint<'db> {
     ty: Type<'db>,
 }
diff --git a/crates/ty_python_semantic/src/types/function.rs b/crates/ty_python_semantic/src/types/function.rs
index 8a3d4406d5..4d8bf36e58 100644
--- a/crates/ty_python_semantic/src/types/function.rs
+++ b/crates/ty_python_semantic/src/types/function.rs
@@ -79,8 +79,9 @@ use crate::types::visitor::any_over_type;
 use crate::types::{
     BoundMethodType, BoundTypeVarInstance, CallableType, ClassBase, ClassLiteral, ClassType,
     DeprecatedInstance, DynamicType, FindLegacyTypeVarsVisitor, HasRelationToVisitor,
-    IsEquivalentVisitor, KnownClass, NormalizedVisitor, SpecialFormType, Truthiness, Type,
-    TypeMapping, TypeRelation, UnionBuilder, all_members, binding_type, walk_type_mapping,
+    IsEquivalentVisitor, KnownClass, KnownInstanceType, NormalizedVisitor, SpecialFormType,
+    TrackedConstraintSet, Truthiness, Type, TypeMapping, TypeRelation, UnionBuilder, all_members,
+    binding_type, walk_type_mapping,
 };
 use crate::{Db, FxOrderSet, ModuleName, resolve_module};
 
@@ -1255,10 +1256,12 @@ pub enum KnownFunction {
     HasMember,
     /// `ty_extensions.reveal_protocol_interface`
     RevealProtocolInterface,
-    /// `ty_extensions.reveal_when_assignable_to`
-    RevealWhenAssignableTo,
-    /// `ty_extensions.reveal_when_subtype_of`
-    RevealWhenSubtypeOf,
+    /// `ty_extensions.range_constraint`
+    RangeConstraint,
+    /// `ty_extensions.not_equivalent_constraint`
+    NotEquivalentConstraint,
+    /// `ty_extensions.incomparable_constraint`
+    IncomparableConstraint,
 }
 
 impl KnownFunction {
@@ -1324,8 +1327,9 @@ impl KnownFunction {
             | Self::StaticAssert
             | Self::HasMember
             | Self::RevealProtocolInterface
-            | Self::RevealWhenAssignableTo
-            | Self::RevealWhenSubtypeOf
+            | Self::RangeConstraint
+            | Self::NotEquivalentConstraint
+            | Self::IncomparableConstraint
             | Self::AllMembers => module.is_ty_extensions(),
             Self::ImportModule => module.is_importlib(),
         }
@@ -1621,52 +1625,82 @@ impl KnownFunction {
                 overload.set_return_type(Type::module_literal(db, file, module));
             }
 
-            KnownFunction::RevealWhenAssignableTo => {
-                let [Some(ty_a), Some(ty_b)] = overload.parameter_types() else {
-                    return;
-                };
-                let constraints = ty_a.when_assignable_to::<ConstraintSet>(db, *ty_b);
-                let Some(builder) =
-                    context.report_diagnostic(DiagnosticId::RevealedType, Severity::Info)
+            KnownFunction::RangeConstraint => {
+                let [
+                    Some(lower),
+                    Some(Type::NonInferableTypeVar(typevar)),
+                    Some(upper),
+                ] = parameter_types
                 else {
                     return;
                 };
-                let mut diag = builder.into_diagnostic("Assignability holds");
-                let span = context.span(call_expression);
-                if constraints.is_always_satisfied(db) {
-                    diag.annotate(Annotation::primary(span).message("always"));
-                } else if constraints.is_never_satisfied(db) {
-                    diag.annotate(Annotation::primary(span).message("never"));
-                } else {
-                    diag.annotate(
-                        Annotation::primary(span)
-                            .message(format_args!("when {}", constraints.display(db))),
-                    );
-                }
+
+                let constraints = ConstraintSet::range(db, *lower, *typevar, *upper);
+                let tracked = TrackedConstraintSet::new(db, constraints);
+                overload.set_return_type(Type::KnownInstance(KnownInstanceType::ConstraintSet(
+                    tracked,
+                )));
             }
 
-            KnownFunction::RevealWhenSubtypeOf => {
-                let [Some(ty_a), Some(ty_b)] = overload.parameter_types() else {
+            KnownFunction::NotEquivalentConstraint => {
+                let [Some(Type::NonInferableTypeVar(typevar)), Some(hole)] = parameter_types else {
                     return;
                 };
-                let constraints = ty_a.when_subtype_of::<ConstraintSet>(db, *ty_b);
-                let Some(builder) =
-                    context.report_diagnostic(DiagnosticId::RevealedType, Severity::Info)
+
+                if !hole.is_equivalent_to(db, hole.top_materialization(db)) {
+                    if let Some(builder) =
+                        context.report_lint(&INVALID_ARGUMENT_TYPE, call_expression)
+                    {
+                        let mut diagnostic = builder.into_diagnostic(format_args!(
+                            "Not-equivalent constraint must have a fully static type"
+                        ));
+                        diagnostic.annotate(
+                            Annotation::secondary(context.span(&call_expression.arguments.args[1]))
+                                .message(format_args!(
+                                    "Type `{}` is not fully static",
+                                    hole.display(db)
+                                )),
+                        );
+                    }
+                    return;
+                }
+
+                let constraints = ConstraintSet::not_equivalent(db, *typevar, *hole);
+                let tracked = TrackedConstraintSet::new(db, constraints);
+                overload.set_return_type(Type::KnownInstance(KnownInstanceType::ConstraintSet(
+                    tracked,
+                )));
+            }
+
+            KnownFunction::IncomparableConstraint => {
+                let [Some(Type::NonInferableTypeVar(typevar)), Some(pivot)] = parameter_types
                 else {
                     return;
                 };
-                let mut diag = builder.into_diagnostic("Subtyping holds");
-                let span = context.span(call_expression);
-                if constraints.is_always_satisfied(db) {
-                    diag.annotate(Annotation::primary(span).message("always"));
-                } else if constraints.is_never_satisfied(db) {
-                    diag.annotate(Annotation::primary(span).message("never"));
-                } else {
-                    diag.annotate(
-                        Annotation::primary(span)
-                            .message(format_args!("when {}", constraints.display(db))),
-                    );
+
+                if !pivot.is_equivalent_to(db, pivot.top_materialization(db)) {
+                    if let Some(builder) =
+                        context.report_lint(&INVALID_ARGUMENT_TYPE, call_expression)
+                    {
+                        let mut diagnostic = builder.into_diagnostic(format_args!(
+                            "Incomparable constraint must have a fully static type"
+                        ));
+                        diagnostic.annotate(
+                            Annotation::secondary(context.span(&call_expression.arguments.args[1]))
+                                .message(format_args!(
+                                    "Type `{}` is not fully static",
+                                    pivot.display(db)
+                                )),
+                        );
+                    }
+                    return;
                 }
+
+                let constraints = ConstraintSet::incomparable(db, *typevar, *pivot);
+                let tracked = TrackedConstraintSet::new(db, constraints);
+                overload.set_return_type(Type::KnownInstance(KnownInstanceType::ConstraintSet(
+                    tracked,
+                )));
             }
 
             _ => {}
@@ -1729,8 +1763,9 @@ pub(crate) mod tests {
                 | KnownFunction::IsEquivalentTo
                 | KnownFunction::HasMember
                 | KnownFunction::RevealProtocolInterface
-                | KnownFunction::RevealWhenAssignableTo
-                | KnownFunction::RevealWhenSubtypeOf
+                | KnownFunction::RangeConstraint
+                | KnownFunction::NotEquivalentConstraint
+                | KnownFunction::IncomparableConstraint
                 | KnownFunction::AllMembers => KnownModule::TyExtensions,
 
                 KnownFunction::ImportModule => KnownModule::ImportLib,
diff --git a/crates/ty_python_semantic/src/types/infer.rs b/crates/ty_python_semantic/src/types/infer.rs
index e7aca51cfb..439b3cf1b8 100644
--- a/crates/ty_python_semantic/src/types/infer.rs
+++ b/crates/ty_python_semantic/src/types/infer.rs
@@ -93,6 +93,7 @@ use crate::semantic_index::{
 };
 use crate::types::call::{Binding, Bindings, CallArguments, CallError, CallErrorKind};
 use crate::types::class::{CodeGeneratorKind, FieldKind, MetaclassErrorKind, MethodDecorator};
+use crate::types::constraints::Constraints;
 use crate::types::diagnostic::{
     self, CALL_NON_CALLABLE, CONFLICTING_DECLARATIONS, CONFLICTING_METACLASS,
     CYCLIC_CLASS_DEFINITION, DIVISION_BY_ZERO, DUPLICATE_KW_ONLY, INCONSISTENT_MRO,
@@ -130,10 +131,10 @@ use crate::types::{
     CallDunderError, CallableType, ClassLiteral, ClassType, DataclassParams, DynamicType,
     IntersectionBuilder, IntersectionType, KnownClass, KnownInstanceType, LintDiagnosticGuard,
     MemberLookupPolicy, MetaclassCandidate, PEP695TypeAliasType, Parameter, ParameterForm,
-    Parameters, SpecialFormType, SubclassOfType, Truthiness, Type, TypeAliasType,
-    TypeAndQualifiers, TypeIsType, TypeQualifiers, TypeVarBoundOrConstraintsEvaluation,
-    TypeVarDefaultEvaluation, TypeVarInstance, TypeVarKind, UnionBuilder, UnionType, binding_type,
-    todo_type,
+    Parameters, SpecialFormType, SubclassOfType, TrackedConstraintSet, Truthiness, Type,
+    TypeAliasType, TypeAndQualifiers, TypeIsType, TypeQualifiers,
+    TypeVarBoundOrConstraintsEvaluation, TypeVarDefaultEvaluation, TypeVarInstance, TypeVarKind,
+    UnionBuilder, UnionType, binding_type, todo_type,
 };
 use crate::unpack::{EvaluationMode, Unpack, UnpackPosition};
 use crate::util::diagnostics::format_enumeration;
@@ -7375,6 +7376,18 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
                 Type::IntLiteral(!i64::from(bool))
             }
 
+            (
+                ast::UnaryOp::Invert,
+                Type::KnownInstance(KnownInstanceType::ConstraintSet(constraints)),
+            ) => {
+                let constraints = constraints.constraints(self.db()).clone();
+                let result = constraints.negate(self.db());
+                Type::KnownInstance(KnownInstanceType::ConstraintSet(TrackedConstraintSet::new(
+                    self.db(),
+                    result,
+                )))
+            }
+
             (ast::UnaryOp::Not, ty) => ty
                 .try_bool(self.db())
                 .unwrap_or_else(|err| {
@@ -7726,6 +7739,32 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
                     op,
                 ),
 
+            (
+                Type::KnownInstance(KnownInstanceType::ConstraintSet(left)),
+                Type::KnownInstance(KnownInstanceType::ConstraintSet(right)),
+                ast::Operator::BitAnd,
+            ) => {
+                let left = left.constraints(self.db()).clone();
+                let right = right.constraints(self.db()).clone();
+                let result = left.and(self.db(), || right);
+                Some(Type::KnownInstance(KnownInstanceType::ConstraintSet(
+                    TrackedConstraintSet::new(self.db(), result),
+                )))
+            }
+
+            (
+                Type::KnownInstance(KnownInstanceType::ConstraintSet(left)),
+                Type::KnownInstance(KnownInstanceType::ConstraintSet(right)),
+                ast::Operator::BitOr,
+            ) => {
+                let left = left.constraints(self.db()).clone();
+                let right = right.constraints(self.db()).clone();
+                let result = left.or(self.db(), || right);
+                Some(Type::KnownInstance(KnownInstanceType::ConstraintSet(
+                    TrackedConstraintSet::new(self.db(), result),
+                )))
+            }
+
             // We've handled all of the special cases that we support for literals, so we need to
             // fall back on looking for dunder methods on one of the operand types.
             (
@@ -10594,6 +10633,15 @@ impl<'db> TypeInferenceBuilder<'db, '_> {
                     }
                     Type::unknown()
                 }
+                KnownInstanceType::ConstraintSet(_) => {
+                    self.infer_type_expression(&subscript.slice);
+                    if let Some(builder) = self.context.report_lint(&INVALID_TYPE_FORM, subscript) {
+                        builder.into_diagnostic(format_args!(
+                            "`ty_extensions.ConstraintSet` is not allowed in type expressions",
+                        ));
+                    }
+                    Type::unknown()
+                }
                 KnownInstanceType::TypeVar(_) => {
                     self.infer_type_expression(&subscript.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 a9c733fba2..6b09ce0b97 100644
--- a/crates/ty_vendored/ty_extensions/ty_extensions.pyi
+++ b/crates/ty_vendored/ty_extensions/ty_extensions.pyi
@@ -40,23 +40,30 @@ Bottom: _SpecialForm
 type JustFloat = TypeOf[1.0]
 type JustComplex = TypeOf[1.0j]
 
+# Constraints
+class ConstraintSet:
+    def __bool__(self) -> bool: ...
+    def __and__(self, other: ConstraintSet) -> ConstraintSet: ...
+    def __or__(self, other: ConstraintSet) -> ConstraintSet: ...
+    def __invert__(self) -> ConstraintSet: ...
+
+def range_constraint(
+    lower_bound: Any, typevar: Any, upper_bound: Any
+) -> ConstraintSet: ...
+def not_equivalent_constraint(typevar: Any, hole: Any) -> ConstraintSet: ...
+def incomparable_constraint(typevar: Any, pivot: Any) -> ConstraintSet: ...
+
 # Predicates on types
 #
 # Ideally, these would be annotated using `TypeForm`, but that has not been
 # standardized yet (https://peps.python.org/pep-0747).
-def is_equivalent_to(type_a: Any, type_b: Any) -> bool: ...
-def is_subtype_of(type_a: Any, type_b: Any) -> bool: ...
-def is_assignable_to(type_a: Any, type_b: Any) -> bool: ...
-def is_disjoint_from(type_a: Any, type_b: Any) -> bool: ...
+def is_equivalent_to(type_a: Any, type_b: Any) -> ConstraintSet: ...
+def is_subtype_of(type_a: Any, type_b: Any) -> ConstraintSet: ...
+def is_assignable_to(type_a: Any, type_b: Any) -> ConstraintSet: ...
+def is_disjoint_from(type_a: Any, type_b: Any) -> ConstraintSet: ...
 def is_singleton(ty: Any) -> bool: ...
 def is_single_valued(ty: Any) -> bool: ...
 
-# These are the same as above, but instead of returning _whether_ the property
-# holds, it shows a diagnostic that describes under what constraints the
-# property holds.
-def reveal_when_assignable_to(type_a: Any, type_b: Any) -> None: ...
-def reveal_when_subtype_of(type_a: Any, type_b: Any) -> None: ...
-
 # 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: ...