diff --git a/crates/red_knot_ide/src/lib.rs b/crates/red_knot_ide/src/lib.rs
index 699b385d27..39e12d64a8 100644
--- a/crates/red_knot_ide/src/lib.rs
+++ b/crates/red_knot_ide/src/lib.rs
@@ -162,6 +162,17 @@ impl HasNavigationTargets for Type<'_> {
             | Type::PropertyInstance(_)
             | Type::Tuple(_) => self.to_meta_type(db.upcast()).navigation_targets(db),
 
+            Type::TypeVar(var) => {
+                let definition = var.definition(db);
+                let full_range = definition.full_range(db.upcast());
+
+                NavigationTargets::single(NavigationTarget {
+                    file: full_range.file(),
+                    focus_range: definition.focus_range(db.upcast()).range(),
+                    full_range: full_range.range(),
+                })
+            }
+
             Type::Intersection(intersection) => intersection.navigation_targets(db),
 
             Type::Dynamic(_)
diff --git a/crates/red_knot_python_semantic/resources/mdtest/generics/functions.md b/crates/red_knot_python_semantic/resources/mdtest/generics/functions.md
index 712152ba3e..32b4f1971b 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/generics/functions.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/generics/functions.md
@@ -107,8 +107,7 @@ def good_return[T: int](x: T) -> T:
     return x
 
 def bad_return[T: int](x: T) -> T:
-    # TODO: error: int is not assignable to T
-    # error: [unsupported-operator] "Operator `+` is unsupported between objects of type `T` and `Literal[1]`"
+    # error: [invalid-return-type] "Object of type `int` is not assignable to return type `T`"
     return x + 1
 ```
 
diff --git a/crates/red_knot_python_semantic/resources/mdtest/generics/pep695.md b/crates/red_knot_python_semantic/resources/mdtest/generics/pep695.md
index af60aef394..d48fd37bdd 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/generics/pep695.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/generics/pep695.md
@@ -48,4 +48,511 @@ class C[T]:
         reveal_type(x)  # revealed: T
 ```
 
+## Fully static typevars
+
+We consider a typevar to be fully static unless it has a non-fully-static bound or constraint. This
+is true even though a fully static typevar might be specialized to a gradual form like `Any`. (This
+is similar to how you can assign an expression whose type is not fully static to a target whose type
+is.)
+
+```py
+from knot_extensions import is_fully_static, static_assert
+from typing import Any
+
+def unbounded_unconstrained[T](t: list[T]) -> None:
+    static_assert(is_fully_static(T))
+
+def bounded[T: int](t: list[T]) -> None:
+    static_assert(is_fully_static(T))
+
+def bounded_by_gradual[T: Any](t: list[T]) -> None:
+    static_assert(not is_fully_static(T))
+
+def constrained[T: (int, str)](t: list[T]) -> None:
+    static_assert(is_fully_static(T))
+
+def constrained_by_gradual[T: (int, Any)](t: list[T]) -> None:
+    static_assert(not is_fully_static(T))
+```
+
+## Subtyping and assignability
+
+(Note: for simplicity, all of the prose in this section refers to _subtyping_ involving fully static
+typevars. Unless otherwise noted, all of the claims also apply to _assignability_ involving gradual
+typevars.)
+
+We can make no assumption about what type an unbounded, unconstrained, fully static typevar will be
+specialized to. Properties are true of the typevar only if they are true for every valid
+specialization. Thus, the typevar is a subtype of itself and of `object`, but not of any other type
+(including other typevars).
+
+```py
+from knot_extensions import is_assignable_to, is_subtype_of, static_assert
+
+class Super: ...
+class Base(Super): ...
+class Sub(Base): ...
+class Unrelated: ...
+
+def unbounded_unconstrained[T, U](t: list[T], u: list[U]) -> None:
+    static_assert(is_assignable_to(T, T))
+    static_assert(is_assignable_to(T, object))
+    static_assert(not is_assignable_to(T, Super))
+    static_assert(is_assignable_to(U, U))
+    static_assert(is_assignable_to(U, object))
+    static_assert(not is_assignable_to(U, Super))
+    static_assert(not is_assignable_to(T, U))
+    static_assert(not is_assignable_to(U, T))
+
+    static_assert(is_subtype_of(T, T))
+    static_assert(is_subtype_of(T, object))
+    static_assert(not is_subtype_of(T, Super))
+    static_assert(is_subtype_of(U, U))
+    static_assert(is_subtype_of(U, object))
+    static_assert(not is_subtype_of(U, Super))
+    static_assert(not is_subtype_of(T, U))
+    static_assert(not is_subtype_of(U, T))
+```
+
+A bounded typevar is assignable to its bound, and a bounded, fully static typevar is a subtype of
+its bound. (A typevar with a non-fully-static bound is itself non-fully-static, and therefore does
+not participate in subtyping.) A fully static bound is not assignable to, nor a subtype of, the
+typevar, since the typevar might be specialized to a smaller type. (This is true even if the bound
+is a final class, since the typevar can still be specialized to `Never`.)
+
+```py
+from typing import Any
+from typing_extensions import final
+
+def bounded[T: Super](t: list[T]) -> None:
+    static_assert(is_assignable_to(T, Super))
+    static_assert(not is_assignable_to(T, Sub))
+    static_assert(not is_assignable_to(Super, T))
+    static_assert(not is_assignable_to(Sub, T))
+
+    static_assert(is_subtype_of(T, Super))
+    static_assert(not is_subtype_of(T, Sub))
+    static_assert(not is_subtype_of(Super, T))
+    static_assert(not is_subtype_of(Sub, T))
+
+def bounded_by_gradual[T: Any](t: list[T]) -> None:
+    static_assert(is_assignable_to(T, Any))
+    static_assert(is_assignable_to(Any, T))
+    static_assert(is_assignable_to(T, Super))
+    static_assert(not is_assignable_to(Super, T))
+    static_assert(is_assignable_to(T, Sub))
+    static_assert(not is_assignable_to(Sub, T))
+
+    static_assert(not is_subtype_of(T, Any))
+    static_assert(not is_subtype_of(Any, T))
+    static_assert(not is_subtype_of(T, Super))
+    static_assert(not is_subtype_of(Super, T))
+    static_assert(not is_subtype_of(T, Sub))
+    static_assert(not is_subtype_of(Sub, T))
+
+@final
+class FinalClass: ...
+
+def bounded_final[T: FinalClass](t: list[T]) -> None:
+    static_assert(is_assignable_to(T, FinalClass))
+    static_assert(not is_assignable_to(FinalClass, T))
+
+    static_assert(is_subtype_of(T, FinalClass))
+    static_assert(not is_subtype_of(FinalClass, T))
+```
+
+Two distinct fully static typevars are not subtypes of each other, even if they have the same
+bounds, since there is (still) no guarantee that they will be specialized to the same type. This is
+true even if both typevars are bounded by the same final class, since you can specialize the
+typevars to `Never` in addition to that final class.
+
+```py
+def two_bounded[T: Super, U: Super](t: list[T], u: list[U]) -> None:
+    static_assert(not is_assignable_to(T, U))
+    static_assert(not is_assignable_to(U, T))
+
+    static_assert(not is_subtype_of(T, U))
+    static_assert(not is_subtype_of(U, T))
+
+def two_final_bounded[T: FinalClass, U: FinalClass](t: list[T], u: list[U]) -> None:
+    static_assert(not is_assignable_to(T, U))
+    static_assert(not is_assignable_to(U, T))
+
+    static_assert(not is_subtype_of(T, U))
+    static_assert(not is_subtype_of(U, T))
+```
+
+A constrained fully static typevar is assignable to the union of its constraints, but not to any of
+the constraints individually. None of the constraints are subtypes of the typevar, though the
+intersection of all of its constraints is a subtype of the typevar.
+
+```py
+from knot_extensions import Intersection
+
+def constrained[T: (Base, Unrelated)](t: list[T]) -> None:
+    static_assert(not is_assignable_to(T, Super))
+    static_assert(not is_assignable_to(T, Base))
+    static_assert(not is_assignable_to(T, Sub))
+    static_assert(not is_assignable_to(T, Unrelated))
+    static_assert(is_assignable_to(T, Super | Unrelated))
+    static_assert(is_assignable_to(T, Base | Unrelated))
+    static_assert(not is_assignable_to(T, Sub | Unrelated))
+    static_assert(not is_assignable_to(Super, T))
+    static_assert(not is_assignable_to(Unrelated, T))
+    static_assert(not is_assignable_to(Super | Unrelated, T))
+    static_assert(is_assignable_to(Intersection[Base, Unrelated], T))
+
+    static_assert(not is_subtype_of(T, Super))
+    static_assert(not is_subtype_of(T, Base))
+    static_assert(not is_subtype_of(T, Sub))
+    static_assert(not is_subtype_of(T, Unrelated))
+    static_assert(is_subtype_of(T, Super | Unrelated))
+    static_assert(is_subtype_of(T, Base | Unrelated))
+    static_assert(not is_subtype_of(T, Sub | Unrelated))
+    static_assert(not is_subtype_of(Super, T))
+    static_assert(not is_subtype_of(Unrelated, T))
+    static_assert(not is_subtype_of(Super | Unrelated, T))
+    static_assert(is_subtype_of(Intersection[Base, Unrelated], T))
+
+def constrained_by_gradual[T: (Base, Any)](t: list[T]) -> None:
+    static_assert(is_assignable_to(T, Super))
+    static_assert(is_assignable_to(T, Base))
+    static_assert(not is_assignable_to(T, Sub))
+    static_assert(not is_assignable_to(T, Unrelated))
+    static_assert(is_assignable_to(T, Any))
+    static_assert(is_assignable_to(T, Super | Any))
+    static_assert(is_assignable_to(T, Super | Unrelated))
+    static_assert(not is_assignable_to(Super, T))
+    static_assert(is_assignable_to(Base, T))
+    static_assert(not is_assignable_to(Unrelated, T))
+    static_assert(is_assignable_to(Any, T))
+    static_assert(not is_assignable_to(Super | Any, T))
+    static_assert(is_assignable_to(Base | Any, T))
+    static_assert(not is_assignable_to(Super | Unrelated, T))
+    static_assert(is_assignable_to(Intersection[Base, Unrelated], T))
+    static_assert(is_assignable_to(Intersection[Base, Any], T))
+
+    static_assert(not is_subtype_of(T, Super))
+    static_assert(not is_subtype_of(T, Base))
+    static_assert(not is_subtype_of(T, Sub))
+    static_assert(not is_subtype_of(T, Unrelated))
+    static_assert(not is_subtype_of(T, Any))
+    static_assert(not is_subtype_of(T, Super | Any))
+    static_assert(not is_subtype_of(T, Super | Unrelated))
+    static_assert(not is_subtype_of(Super, T))
+    static_assert(not is_subtype_of(Base, T))
+    static_assert(not is_subtype_of(Unrelated, T))
+    static_assert(not is_subtype_of(Any, T))
+    static_assert(not is_subtype_of(Super | Any, T))
+    static_assert(not is_subtype_of(Base | Any, T))
+    static_assert(not is_subtype_of(Super | Unrelated, T))
+    static_assert(not is_subtype_of(Intersection[Base, Unrelated], T))
+    static_assert(not is_subtype_of(Intersection[Base, Any], T))
+```
+
+Two distinct fully static typevars are not subtypes of each other, even if they have the same
+constraints, and even if any of the constraints are final. There must always be at least two
+distinct constraints, meaning that there is (still) no guarantee that they will be specialized to
+the same type.
+
+```py
+def two_constrained[T: (int, str), U: (int, str)](t: list[T], u: list[U]) -> None:
+    static_assert(not is_assignable_to(T, U))
+    static_assert(not is_assignable_to(U, T))
+
+    static_assert(not is_subtype_of(T, U))
+    static_assert(not is_subtype_of(U, T))
+
+@final
+class AnotherFinalClass: ...
+
+def two_final_constrained[T: (FinalClass, AnotherFinalClass), U: (FinalClass, AnotherFinalClass)](t: list[T], u: list[U]) -> None:
+    static_assert(not is_assignable_to(T, U))
+    static_assert(not is_assignable_to(U, T))
+
+    static_assert(not is_subtype_of(T, U))
+    static_assert(not is_subtype_of(U, T))
+```
+
+## Singletons and single-valued types
+
+(Note: for simplicity, all of the prose in this section refers to _singleton_ types, but all of the
+claims also apply to _single-valued_ types.)
+
+An unbounded, unconstrained typevar is not a singleton, because it can be specialized to a
+non-singleton type.
+
+```py
+from knot_extensions import is_singleton, is_single_valued, static_assert
+
+def unbounded_unconstrained[T](t: list[T]) -> None:
+    static_assert(not is_singleton(T))
+    static_assert(not is_single_valued(T))
+```
+
+A bounded typevar is not a singleton, even if its bound is a singleton, since it can still be
+specialized to `Never`.
+
+```py
+def bounded[T: None](t: list[T]) -> None:
+    static_assert(not is_singleton(T))
+    static_assert(not is_single_valued(T))
+```
+
+A constrained typevar is a singleton if all of its constraints are singletons. (Note that you cannot
+specialize a constrained typevar to a subtype of a constraint.)
+
+```py
+from typing_extensions import Literal
+
+def constrained_non_singletons[T: (int, str)](t: list[T]) -> None:
+    static_assert(not is_singleton(T))
+    static_assert(not is_single_valued(T))
+
+def constrained_singletons[T: (Literal[True], Literal[False])](t: list[T]) -> None:
+    static_assert(is_singleton(T))
+
+def constrained_single_valued[T: (Literal[True], tuple[()])](t: list[T]) -> None:
+    static_assert(is_single_valued(T))
+```
+
+## Unions involving typevars
+
+The union of an unbounded unconstrained typevar with any other type cannot be simplified, since
+there is no guarantee what type the typevar will be specialized to.
+
+```py
+from typing import Any
+
+class Super: ...
+class Base(Super): ...
+class Sub(Base): ...
+class Unrelated: ...
+
+def unbounded_unconstrained[T](t: T) -> None:
+    def _(x: T | Super) -> None:
+        reveal_type(x)  # revealed: T | Super
+
+    def _(x: T | Base) -> None:
+        reveal_type(x)  # revealed: T | Base
+
+    def _(x: T | Sub) -> None:
+        reveal_type(x)  # revealed: T | Sub
+
+    def _(x: T | Unrelated) -> None:
+        reveal_type(x)  # revealed: T | Unrelated
+
+    def _(x: T | Any) -> None:
+        reveal_type(x)  # revealed: T | Any
+```
+
+The union of a bounded typevar with its bound is that bound. (The typevar is guaranteed to be
+specialized to a subtype of the bound.) The union of a bounded typevar with a subtype of its bound
+cannot be simplified. (The typevar might be specialized to a different subtype of the bound.)
+
+```py
+def bounded[T: Base](t: T) -> None:
+    def _(x: T | Super) -> None:
+        reveal_type(x)  # revealed: Super
+
+    def _(x: T | Base) -> None:
+        reveal_type(x)  # revealed: Base
+
+    def _(x: T | Sub) -> None:
+        reveal_type(x)  # revealed: T | Sub
+
+    def _(x: T | Unrelated) -> None:
+        reveal_type(x)  # revealed: T | Unrelated
+
+    def _(x: T | Any) -> None:
+        reveal_type(x)  # revealed: T | Any
+```
+
+The union of a constrained typevar with a type depends on how that type relates to the constraints.
+If all of the constraints are a subtype of that type, the union simplifies to that type. Inversely,
+if the type is a subtype of every constraint, the union simplifies to the typevar. Otherwise, the
+union cannot be simplified.
+
+```py
+def constrained[T: (Base, Sub)](t: T) -> None:
+    def _(x: T | Super) -> None:
+        reveal_type(x)  # revealed: Super
+
+    def _(x: T | Base) -> None:
+        reveal_type(x)  # revealed: Base
+
+    def _(x: T | Sub) -> None:
+        reveal_type(x)  # revealed: T
+
+    def _(x: T | Unrelated) -> None:
+        reveal_type(x)  # revealed: T | Unrelated
+
+    def _(x: T | Any) -> None:
+        reveal_type(x)  # revealed: T | Any
+```
+
+## Intersections involving typevars
+
+The intersection of an unbounded unconstrained typevar with any other type cannot be simplified,
+since there is no guarantee what type the typevar will be specialized to.
+
+```py
+from knot_extensions import Intersection
+from typing import Any
+
+class Super: ...
+class Base(Super): ...
+class Sub(Base): ...
+class Unrelated: ...
+
+def unbounded_unconstrained[T](t: T) -> None:
+    def _(x: Intersection[T, Super]) -> None:
+        reveal_type(x)  # revealed: T & Super
+
+    def _(x: Intersection[T, Base]) -> None:
+        reveal_type(x)  # revealed: T & Base
+
+    def _(x: Intersection[T, Sub]) -> None:
+        reveal_type(x)  # revealed: T & Sub
+
+    def _(x: Intersection[T, Unrelated]) -> None:
+        reveal_type(x)  # revealed: T & Unrelated
+
+    def _(x: Intersection[T, Any]) -> None:
+        reveal_type(x)  # revealed: T & Any
+```
+
+The intersection of a bounded typevar with its bound or a supertype of its bound is the typevar
+itself. (The typevar might be specialized to a subtype of the bound.) The intersection of a bounded
+typevar with a subtype of its bound cannot be simplified. (The typevar might be specialized to a
+different subtype of the bound.) The intersection of a bounded typevar with a type that is disjoint
+from its bound is `Never`.
+
+```py
+def bounded[T: Base](t: T) -> None:
+    def _(x: Intersection[T, Super]) -> None:
+        reveal_type(x)  # revealed: T
+
+    def _(x: Intersection[T, Base]) -> None:
+        reveal_type(x)  # revealed: T
+
+    def _(x: Intersection[T, Sub]) -> None:
+        reveal_type(x)  # revealed: T & Sub
+
+    def _(x: Intersection[T, None]) -> None:
+        reveal_type(x)  # revealed: Never
+
+    def _(x: Intersection[T, Any]) -> None:
+        reveal_type(x)  # revealed: T & Any
+```
+
+Constrained typevars can be modeled using a hypothetical `OneOf` connector, where the typevar must
+be specialized to _one_ of its constraints. The typevar is not the _union_ of those constraints,
+since that would allow the typevar to take on values from _multiple_ constraints simultaneously. The
+`OneOf` connector would not be a “type” according to a strict reading of the typing spec, since it
+would not represent a single set of runtime objects; it would instead represent a _set of_ sets of
+runtime objects. This is one reason we have not actually added this connector to our data model yet.
+Nevertheless, describing constrained typevars this way helps explain how we simplify intersections
+involving them.
+
+This means that when intersecting a constrained typevar with a type `T`, constraints that are
+supertypes of `T` can be simplified to `T`, since intersection distributes over `OneOf`. Moreover,
+constraints that are disjoint from `T` are no longer valid specializations of the typevar, since
+`Never` is an identity for `OneOf`. After these simplifications, if only one constraint remains, we
+can simplify the intersection as a whole to that constraint.
+
+```py
+def constrained[T: (Base, Sub, Unrelated)](t: T) -> None:
+    def _(x: Intersection[T, Base]) -> None:
+        # With OneOf this would be OneOf[Base, Sub]
+        reveal_type(x)  # revealed: T & Base
+
+    def _(x: Intersection[T, Unrelated]) -> None:
+        reveal_type(x)  # revealed: Unrelated
+
+    def _(x: Intersection[T, Sub]) -> None:
+        reveal_type(x)  # revealed: Sub
+
+    def _(x: Intersection[T, None]) -> None:
+        reveal_type(x)  # revealed: Never
+
+    def _(x: Intersection[T, Any]) -> None:
+        reveal_type(x)  # revealed: T & Any
+```
+
+We can simplify the intersection similarly when removing a type from a constrained typevar, since
+this is modeled internally as an intersection with a negation.
+
+```py
+from knot_extensions import Not
+
+def remove_constraint[T: (int, str, bool)](t: T) -> None:
+    def _(x: Intersection[T, Not[int]]) -> None:
+        reveal_type(x)  # revealed: str
+
+    def _(x: Intersection[T, Not[str]]) -> None:
+        # With OneOf this would be OneOf[int, bool]
+        reveal_type(x)  # revealed: T & ~str
+
+    def _(x: Intersection[T, Not[bool]]) -> None:
+        reveal_type(x)  # revealed: T & ~bool
+
+    def _(x: Intersection[T, Not[int], Not[str]]) -> None:
+        reveal_type(x)  # revealed: Never
+
+    def _(x: Intersection[T, Not[None]]) -> None:
+        reveal_type(x)  # revealed: T
+
+    def _(x: Intersection[T, Not[Any]]) -> None:
+        reveal_type(x)  # revealed: T & Any
+```
+
+## Narrowing
+
+We can use narrowing expressions to eliminate some of the possibilities of a constrained typevar:
+
+```py
+class P: ...
+class Q: ...
+class R: ...
+
+def f[T: (P, Q)](t: T) -> None:
+    if isinstance(t, P):
+        reveal_type(t)  # revealed: P
+        p: P = t
+    else:
+        reveal_type(t)  # revealed: Q
+        q: Q = t
+
+    if isinstance(t, Q):
+        reveal_type(t)  # revealed: Q
+        q: Q = t
+    else:
+        reveal_type(t)  # revealed: P
+        p: P = t
+
+def g[T: (P, Q, R)](t: T) -> None:
+    if isinstance(t, P):
+        reveal_type(t)  # revealed: P
+        p: P = t
+    elif isinstance(t, Q):
+        reveal_type(t)  # revealed: Q & ~P
+        q: Q = t
+    else:
+        reveal_type(t)  # revealed: R
+        r: R = t
+
+    if isinstance(t, P):
+        reveal_type(t)  # revealed: P
+        p: P = t
+    elif isinstance(t, Q):
+        reveal_type(t)  # revealed: Q & ~P
+        q: Q = t
+    elif isinstance(t, R):
+        reveal_type(t)  # revealed: R & ~P & ~Q
+        r: R = t
+    else:
+        reveal_type(t)  # revealed: Never
+```
+
 [pep 695]: https://peps.python.org/pep-0695/
diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs
index d15802b946..327f903f62 100644
--- a/crates/red_knot_python_semantic/src/types.rs
+++ b/crates/red_knot_python_semantic/src/types.rs
@@ -312,7 +312,10 @@ pub enum Type<'db> {
     /// A heterogeneous tuple type, with elements of the given types in source order.
     // TODO: Support variable length homogeneous tuple type like `tuple[int, ...]`.
     Tuple(TupleType<'db>),
-    // TODO protocols, callable types, overloads, generics, type vars
+    /// An instance of a typevar in a generic class or function. When the generic class or function
+    /// is specialized, we will replace this typevar with its specialization.
+    TypeVar(TypeVarInstance<'db>),
+    // TODO protocols, overloads, generics
 }
 
 #[salsa::tracked]
@@ -398,6 +401,15 @@ impl<'db> Type<'db> {
                 ClassBase::Class(_) => false,
             },
 
+            Self::TypeVar(typevar) => match typevar.bound_or_constraints(db) {
+                None => false,
+                Some(TypeVarBoundOrConstraints::UpperBound(bound)) => bound.contains_todo(db),
+                Some(TypeVarBoundOrConstraints::Constraints(constraints)) => constraints
+                    .elements(db)
+                    .iter()
+                    .any(|constraint| constraint.contains_todo(db)),
+            },
+
             Self::Tuple(tuple) => tuple.elements(db).iter().any(|ty| ty.contains_todo(db)),
 
             Self::Union(union) => union.elements(db).iter().any(|ty| ty.contains_todo(db)),
@@ -633,6 +645,27 @@ impl<'db> Type<'db> {
             | Type::KnownInstance(_)
             | Type::IntLiteral(_)
             | Type::SubclassOf(_) => self,
+            Type::TypeVar(typevar) => match typevar.bound_or_constraints(db) {
+                Some(TypeVarBoundOrConstraints::UpperBound(bound)) => {
+                    Type::TypeVar(TypeVarInstance::new(
+                        db,
+                        typevar.name(db).clone(),
+                        typevar.definition(db),
+                        Some(TypeVarBoundOrConstraints::UpperBound(bound.normalized(db))),
+                        typevar.default_ty(db),
+                    ))
+                }
+                Some(TypeVarBoundOrConstraints::Constraints(union)) => {
+                    Type::TypeVar(TypeVarInstance::new(
+                        db,
+                        typevar.name(db).clone(),
+                        typevar.definition(db),
+                        Some(TypeVarBoundOrConstraints::Constraints(union.normalized(db))),
+                        typevar.default_ty(db),
+                    ))
+                }
+                None => self,
+            },
         }
     }
 
@@ -680,6 +713,30 @@ impl<'db> Type<'db> {
             // Everything is a subtype of `object`.
             (_, Type::Instance(InstanceType { class })) if class.is_object(db) => true,
 
+            // A fully static typevar is always a subtype of itself, and is never a subtype of any
+            // other typevar, since there is no guarantee that they will be specialized to the same
+            // type. (This is true even if both typevars are bounded by the same final class, since
+            // you can specialize the typevars to `Never` in addition to that final class.)
+            (Type::TypeVar(self_typevar), Type::TypeVar(other_typevar)) => {
+                self_typevar == other_typevar
+            }
+
+            // A fully static typevar is a subtype of its upper bound, and to something similar to
+            // the union of its constraints. An unbound, unconstrained, fully static typevar has an
+            // implicit upper bound of `object` (which is handled above).
+            (Type::TypeVar(typevar), _) if typevar.bound_or_constraints(db).is_some() => {
+                match typevar.bound_or_constraints(db) {
+                    None => unreachable!(),
+                    Some(TypeVarBoundOrConstraints::UpperBound(bound)) => {
+                        bound.is_subtype_of(db, target)
+                    }
+                    Some(TypeVarBoundOrConstraints::Constraints(constraints)) => constraints
+                        .elements(db)
+                        .iter()
+                        .all(|constraint| constraint.is_subtype_of(db, target)),
+                }
+            }
+
             (Type::Union(union), _) => union
                 .elements(db)
                 .iter()
@@ -690,6 +747,24 @@ impl<'db> Type<'db> {
                 .iter()
                 .any(|&elem_ty| self.is_subtype_of(db, elem_ty)),
 
+            (_, Type::TypeVar(typevar)) => match typevar.bound_or_constraints(db) {
+                // No types are a subtype of a bounded typevar, or of an unbounded unconstrained
+                // typevar, since there's no guarantee what type the typevar will be specialized
+                // to. If the typevar is bounded, it might be specialized to a smaller type than
+                // the bound. (This is true even if the bound is a final class, since the typevar
+                // can still be specialized to `Never`.)
+                None => false,
+                Some(TypeVarBoundOrConstraints::UpperBound(_)) => false,
+                // If the typevar is constrained, there must be multiple constraints, and the
+                // typevar might be specialized to any one of them. However, the constraints do not
+                // have to be disjoint, which means an lhs type might be a subtype of all of the
+                // constraints.
+                Some(TypeVarBoundOrConstraints::Constraints(constraints)) => constraints
+                    .elements(db)
+                    .iter()
+                    .all(|constraint| self.is_subtype_of(db, *constraint)),
+            },
+
             // If both sides are intersections we need to handle the right side first
             // (A & B & C) is a subtype of (A & B) because the left is a subtype of both A and B,
             // but none of A, B, or C is a subtype of (A & B).
@@ -874,9 +949,9 @@ impl<'db> Type<'db> {
                 self.is_subtype_of(db, KnownClass::Property.to_instance(db))
             }
 
-            // Other than the special cases enumerated above,
-            // `Instance` types are never subtypes of any other variants
-            (Type::Instance(_), _) => false,
+            // Other than the special cases enumerated above, `Instance` types and typevars are
+            // never subtypes of any other variants
+            (Type::Instance(_) | Type::TypeVar(_), _) => false,
         }
     }
 
@@ -887,6 +962,7 @@ impl<'db> Type<'db> {
         if self.is_gradual_equivalent_to(db, target) {
             return true;
         }
+
         match (self, target) {
             // Never can be assigned to any type.
             (Type::Never, _) => true,
@@ -899,6 +975,30 @@ impl<'db> Type<'db> {
             // TODO this special case might be removable once the below cases are comprehensive
             (_, Type::Instance(InstanceType { class })) if class.is_object(db) => true,
 
+            // A typevar is always assignable to itself, and is never assignable to any other
+            // typevar, since there is no guarantee that they will be specialized to the same
+            // type. (This is true even if both typevars are bounded by the same final class, since
+            // you can specialize the typevars to `Never` in addition to that final class.)
+            (Type::TypeVar(self_typevar), Type::TypeVar(other_typevar)) => {
+                self_typevar == other_typevar
+            }
+
+            // A typevar is assignable to its upper bound, and to something similar to the union of
+            // its constraints. An unbound, unconstrained typevar has an implicit upper bound of
+            // `object` (which is handled above).
+            (Type::TypeVar(typevar), _) if typevar.bound_or_constraints(db).is_some() => {
+                match typevar.bound_or_constraints(db) {
+                    None => unreachable!(),
+                    Some(TypeVarBoundOrConstraints::UpperBound(bound)) => {
+                        bound.is_assignable_to(db, target)
+                    }
+                    Some(TypeVarBoundOrConstraints::Constraints(constraints)) => constraints
+                        .elements(db)
+                        .iter()
+                        .all(|constraint| constraint.is_assignable_to(db, target)),
+                }
+            }
+
             // A union is assignable to a type T iff every element of the union is assignable to T.
             (Type::Union(union), ty) => union
                 .elements(db)
@@ -911,6 +1011,24 @@ impl<'db> Type<'db> {
                 .iter()
                 .any(|&elem_ty| ty.is_assignable_to(db, elem_ty)),
 
+            (_, Type::TypeVar(typevar)) => match typevar.bound_or_constraints(db) {
+                // No types are assignable to a bounded typevar, or to an unbounded unconstrained
+                // typevar, since there's no guarantee what type the typevar will be specialized
+                // to. If the typevar is bounded, it might be specialized to a smaller type than
+                // the bound. (This is true even if the bound is a final class, since the typevar
+                // can still be specialized to `Never`.)
+                None => false,
+                Some(TypeVarBoundOrConstraints::UpperBound(_)) => false,
+                // If the typevar is constrained, there must be multiple constraints, and the
+                // typevar might be specialized to any one of them. However, the constraints do not
+                // have to be disjoint, which means an lhs type might be assignable to all of the
+                // constraints.
+                Some(TypeVarBoundOrConstraints::Constraints(constraints)) => constraints
+                    .elements(db)
+                    .iter()
+                    .all(|constraint| self.is_assignable_to(db, *constraint)),
+            },
+
             // If both sides are intersections we need to handle the right side first
             // (A & B & C) is assignable to (A & B) because the left is assignable to both A and B,
             // but none of A, B, or C is assignable to (A & B).
@@ -1115,6 +1233,8 @@ impl<'db> Type<'db> {
                 }
             }
 
+            (Type::TypeVar(first), Type::TypeVar(second)) => first == second,
+
             (Type::Tuple(first), Type::Tuple(second)) => first.is_gradual_equivalent_to(db, second),
 
             (Type::Union(first), Type::Union(second)) => first.is_gradual_equivalent_to(db, second),
@@ -1141,6 +1261,33 @@ impl<'db> Type<'db> {
 
             (Type::Dynamic(_), _) | (_, Type::Dynamic(_)) => false,
 
+            // A typevar is never disjoint from itself, since all occurrences of the typevar must
+            // be specialized to the same type. (This is an important difference between typevars
+            // and `Any`!) Different typevars might be disjoint, depending on their bounds and
+            // constraints, which are handled below.
+            (Type::TypeVar(self_typevar), Type::TypeVar(other_typevar))
+                if self_typevar == other_typevar =>
+            {
+                false
+            }
+
+            // An unbounded typevar is never disjoint from any other type, since it might be
+            // specialized to any type. A bounded typevar is not disjoint from its bound, and is
+            // only disjoint from other types if its bound is. A constrained typevar is disjoint
+            // from a type if all of its constraints are.
+            (Type::TypeVar(typevar), other) | (other, Type::TypeVar(typevar)) => {
+                match typevar.bound_or_constraints(db) {
+                    None => false,
+                    Some(TypeVarBoundOrConstraints::UpperBound(bound)) => {
+                        bound.is_disjoint_from(db, other)
+                    }
+                    Some(TypeVarBoundOrConstraints::Constraints(constraints)) => constraints
+                        .elements(db)
+                        .iter()
+                        .all(|constraint| constraint.is_disjoint_from(db, other)),
+                }
+            }
+
             (Type::Union(union), other) | (other, Type::Union(union)) => union
                 .elements(db)
                 .iter()
@@ -1482,6 +1629,16 @@ impl<'db> Type<'db> {
             | Type::AlwaysFalsy
             | Type::AlwaysTruthy
             | Type::PropertyInstance(_) => true,
+
+            Type::TypeVar(typevar) => match typevar.bound_or_constraints(db) {
+                None => true,
+                Some(TypeVarBoundOrConstraints::UpperBound(bound)) => bound.is_fully_static(db),
+                Some(TypeVarBoundOrConstraints::Constraints(constraints)) => constraints
+                    .elements(db)
+                    .iter()
+                    .all(|constraint| constraint.is_fully_static(db)),
+            },
+
             Type::SubclassOf(subclass_of_ty) => subclass_of_ty.is_fully_static(),
             Type::ClassLiteral(_) | Type::Instance(_) => {
                 // TODO: Ideally, we would iterate over the MRO of the class, check if all
@@ -1533,6 +1690,21 @@ impl<'db> Type<'db> {
                 // are both of type Literal[345], for example.
                 false
             }
+
+            // An unbounded, unconstrained typevar is not a singleton, because it can be
+            // specialized to a non-singleton type. A bounded typevar is not a singleton, even if
+            // the bound is a final singleton class, since it can still be specialized to `Never`.
+            // A constrained typevar is a singleton if all of its constraints are singletons. (Note
+            // that you cannot specialize a constrained typevar to a subtype of a constraint.)
+            Type::TypeVar(typevar) => match typevar.bound_or_constraints(db) {
+                None => false,
+                Some(TypeVarBoundOrConstraints::UpperBound(_)) => false,
+                Some(TypeVarBoundOrConstraints::Constraints(constraints)) => constraints
+                    .elements(db)
+                    .iter()
+                    .all(|constraint| constraint.is_singleton(db)),
+            },
+
             // We eagerly transform `SubclassOf` to `ClassLiteral` for final types, so `SubclassOf` is never a singleton.
             Type::SubclassOf(..) => false,
             Type::BooleanLiteral(_)
@@ -1611,6 +1783,21 @@ impl<'db> Type<'db> {
             | Type::SliceLiteral(..)
             | Type::KnownInstance(..) => true,
 
+            // An unbounded, unconstrained typevar is not single-valued, because it can be
+            // specialized to a multiple-valued type. A bounded typevar is not single-valued, even
+            // if the bound is a final single-valued class, since it can still be specialized to
+            // `Never`. A constrained typevar is single-valued if all of its constraints are
+            // single-valued. (Note that you cannot specialize a constrained typevar to a subtype
+            // of a constraint.)
+            Type::TypeVar(typevar) => match typevar.bound_or_constraints(db) {
+                None => false,
+                Some(TypeVarBoundOrConstraints::UpperBound(_)) => false,
+                Some(TypeVarBoundOrConstraints::Constraints(constraints)) => constraints
+                    .elements(db)
+                    .iter()
+                    .all(|constraint| constraint.is_single_valued(db)),
+            },
+
             Type::SubclassOf(..) => {
                 // TODO: Same comment as above for `is_singleton`
                 false
@@ -1758,6 +1945,7 @@ impl<'db> Type<'db> {
             | Type::BytesLiteral(_)
             | Type::SliceLiteral(_)
             | Type::Tuple(_)
+            | Type::TypeVar(_)
             | Type::Instance(_)
             | Type::PropertyInstance(_) => None,
         }
@@ -1829,6 +2017,17 @@ impl<'db> Type<'db> {
                 .instance_member(db, name),
             Type::Callable(_) => KnownClass::Object.to_instance(db).instance_member(db, name),
 
+            Type::TypeVar(typevar) => match typevar.bound_or_constraints(db) {
+                None => KnownClass::Object.to_instance(db).instance_member(db, name),
+                Some(TypeVarBoundOrConstraints::UpperBound(bound)) => {
+                    bound.instance_member(db, name)
+                }
+                Some(TypeVarBoundOrConstraints::Constraints(constraints)) => constraints
+                    .map_with_boundness_and_qualifiers(db, |constraint| {
+                        constraint.instance_member(db, name)
+                    }),
+            },
+
             Type::IntLiteral(_) => KnownClass::Int.to_instance(db).instance_member(db, name),
             Type::BooleanLiteral(_) => KnownClass::Bool.to_instance(db).instance_member(db, name),
             Type::StringLiteral(_) | Type::LiteralString => {
@@ -2265,6 +2464,7 @@ impl<'db> Type<'db> {
             | Type::LiteralString
             | Type::SliceLiteral(..)
             | Type::Tuple(..)
+            | Type::TypeVar(..)
             | Type::KnownInstance(..)
             | Type::PropertyInstance(..)
             | Type::FunctionLiteral(..) => {
@@ -2384,6 +2584,108 @@ impl<'db> Type<'db> {
         db: &'db dyn Db,
         allow_short_circuit: bool,
     ) -> Result<Truthiness, BoolError<'db>> {
+        let type_to_truthiness = |ty| {
+            if let Type::BooleanLiteral(bool_val) = ty {
+                Truthiness::from(bool_val)
+            } else {
+                Truthiness::Ambiguous
+            }
+        };
+
+        let try_dunder_bool = || {
+            // We only check the `__bool__` method for truth testing, even though at
+            // runtime there is a fallback to `__len__`, since `__bool__` takes precedence
+            // and a subclass could add a `__bool__` method.
+
+            match self.try_call_dunder(db, "__bool__", CallArgumentTypes::none()) {
+                Ok(outcome) => {
+                    let return_type = outcome.return_type(db);
+                    if !return_type.is_assignable_to(db, KnownClass::Bool.to_instance(db)) {
+                        // The type has a `__bool__` method, but it doesn't return a
+                        // boolean.
+                        return Err(BoolError::IncorrectReturnType {
+                            return_type,
+                            not_boolable_type: *self,
+                        });
+                    }
+                    Ok(type_to_truthiness(return_type))
+                }
+
+                Err(CallDunderError::PossiblyUnbound(outcome)) => {
+                    let return_type = outcome.return_type(db);
+                    if !return_type.is_assignable_to(db, KnownClass::Bool.to_instance(db)) {
+                        // The type has a `__bool__` method, but it doesn't return a
+                        // boolean.
+                        return Err(BoolError::IncorrectReturnType {
+                            return_type: outcome.return_type(db),
+                            not_boolable_type: *self,
+                        });
+                    }
+
+                    // Don't trust possibly unbound `__bool__` method.
+                    Ok(Truthiness::Ambiguous)
+                }
+
+                Err(CallDunderError::MethodNotAvailable) => Ok(Truthiness::Ambiguous),
+                Err(CallDunderError::CallError(CallErrorKind::BindingError, bindings)) => {
+                    Err(BoolError::IncorrectArguments {
+                        truthiness: type_to_truthiness(bindings.return_type(db)),
+                        not_boolable_type: *self,
+                    })
+                }
+                Err(CallDunderError::CallError(CallErrorKind::NotCallable, _)) => {
+                    Err(BoolError::NotCallable {
+                        not_boolable_type: *self,
+                    })
+                }
+                Err(CallDunderError::CallError(CallErrorKind::PossiblyNotCallable, _)) => {
+                    Err(BoolError::Other {
+                        not_boolable_type: *self,
+                    })
+                }
+            }
+        };
+
+        let try_union = |union: UnionType<'db>| {
+            let mut truthiness = None;
+            let mut all_not_callable = true;
+            let mut has_errors = false;
+
+            for element in union.elements(db) {
+                let element_truthiness = match element.try_bool_impl(db, allow_short_circuit) {
+                    Ok(truthiness) => truthiness,
+                    Err(err) => {
+                        has_errors = true;
+                        all_not_callable &= matches!(err, BoolError::NotCallable { .. });
+                        err.fallback_truthiness()
+                    }
+                };
+
+                truthiness.get_or_insert(element_truthiness);
+
+                if Some(element_truthiness) != truthiness {
+                    truthiness = Some(Truthiness::Ambiguous);
+
+                    if allow_short_circuit {
+                        return Ok(Truthiness::Ambiguous);
+                    }
+                }
+            }
+
+            if has_errors {
+                if all_not_callable {
+                    return Err(BoolError::NotCallable {
+                        not_boolable_type: *self,
+                    });
+                }
+                return Err(BoolError::Union {
+                    union,
+                    truthiness: truthiness.unwrap_or(Truthiness::Ambiguous),
+                });
+            }
+            Ok(truthiness.unwrap_or(Truthiness::Ambiguous))
+        };
+
         let truthiness = match self {
             Type::Dynamic(_) | Type::Never | Type::Callable(_) | Type::LiteralString => {
                 Truthiness::Ambiguous
@@ -2410,114 +2712,26 @@ impl<'db> Type<'db> {
                 }
             },
 
-            instance_ty @ Type::Instance(InstanceType { class }) => match class.known(db) {
-                Some(known_class) => known_class.bool(),
-                None => {
-                    // We only check the `__bool__` method for truth testing, even though at
-                    // runtime there is a fallback to `__len__`, since `__bool__` takes precedence
-                    // and a subclass could add a `__bool__` method.
-
-                    let type_to_truthiness = |ty| {
-                        if let Type::BooleanLiteral(bool_val) = ty {
-                            Truthiness::from(bool_val)
-                        } else {
-                            Truthiness::Ambiguous
-                        }
-                    };
-
-                    match self.try_call_dunder(db, "__bool__", CallArgumentTypes::none()) {
-                        Ok(outcome) => {
-                            let return_type = outcome.return_type(db);
-                            if !return_type.is_assignable_to(db, KnownClass::Bool.to_instance(db)) {
-                                // The type has a `__bool__` method, but it doesn't return a
-                                // boolean.
-                                return Err(BoolError::IncorrectReturnType {
-                                    return_type,
-                                    not_boolable_type: *instance_ty,
-                                });
-                            }
-                            type_to_truthiness(return_type)
-                        }
-
-                        Err(CallDunderError::PossiblyUnbound(outcome)) => {
-                            let return_type = outcome.return_type(db);
-                            if !return_type.is_assignable_to(db, KnownClass::Bool.to_instance(db)) {
-                                // The type has a `__bool__` method, but it doesn't return a
-                                // boolean.
-                                return Err(BoolError::IncorrectReturnType {
-                                    return_type: outcome.return_type(db),
-                                    not_boolable_type: *instance_ty,
-                                });
-                            }
-
-                            // Don't trust possibly unbound `__bool__` method.
-                            Truthiness::Ambiguous
-                        }
-
-                        Err(CallDunderError::MethodNotAvailable) => Truthiness::Ambiguous,
-                        Err(CallDunderError::CallError(CallErrorKind::BindingError, bindings)) => {
-                            return Err(BoolError::IncorrectArguments {
-                                truthiness: type_to_truthiness(bindings.return_type(db)),
-                                not_boolable_type: *instance_ty,
-                            });
-                        }
-                        Err(CallDunderError::CallError(CallErrorKind::NotCallable, _)) => {
-                            return Err(BoolError::NotCallable {
-                                not_boolable_type: *instance_ty,
-                            });
-                        }
-                        Err(CallDunderError::CallError(CallErrorKind::PossiblyNotCallable, _)) => {
-                            return Err(BoolError::Other {
-                                not_boolable_type: *self,
-                            })
-                        }
-                    }
+            Type::TypeVar(typevar) => match typevar.bound_or_constraints(db) {
+                None => Truthiness::Ambiguous,
+                Some(TypeVarBoundOrConstraints::UpperBound(bound)) => {
+                    bound.try_bool_impl(db, allow_short_circuit)?
                 }
+                Some(TypeVarBoundOrConstraints::Constraints(constraints)) => {
+                    try_union(constraints)?
+                }
+            },
+
+            Type::Instance(InstanceType { class }) => match class.known(db) {
+                Some(known_class) => known_class.bool(),
+                None => try_dunder_bool()?,
             },
 
             Type::KnownInstance(known_instance) => known_instance.bool(),
 
             Type::PropertyInstance(_) => Truthiness::AlwaysTrue,
 
-            Type::Union(union) => {
-                let mut truthiness = None;
-                let mut all_not_callable = true;
-                let mut has_errors = false;
-
-                for element in union.elements(db) {
-                    let element_truthiness = match element.try_bool_impl(db, allow_short_circuit) {
-                        Ok(truthiness) => truthiness,
-                        Err(err) => {
-                            has_errors = true;
-                            all_not_callable &= matches!(err, BoolError::NotCallable { .. });
-                            err.fallback_truthiness()
-                        }
-                    };
-
-                    truthiness.get_or_insert(element_truthiness);
-
-                    if Some(element_truthiness) != truthiness {
-                        truthiness = Some(Truthiness::Ambiguous);
-
-                        if allow_short_circuit {
-                            return Ok(Truthiness::Ambiguous);
-                        }
-                    }
-                }
-
-                if has_errors {
-                    if all_not_callable {
-                        return Err(BoolError::NotCallable {
-                            not_boolable_type: *self,
-                        });
-                    }
-                    return Err(BoolError::Union {
-                        union: *union,
-                        truthiness: truthiness.unwrap_or(Truthiness::Ambiguous),
-                    });
-                }
-                truthiness.unwrap_or(Truthiness::Ambiguous)
-            }
+            Type::Union(union) => try_union(*union)?,
 
             Type::Intersection(_) => {
                 // TODO
@@ -3274,6 +3488,7 @@ impl<'db> Type<'db> {
             | Type::StringLiteral(_)
             | Type::SliceLiteral(_)
             | Type::Tuple(_)
+            | Type::TypeVar(_)
             | Type::LiteralString
             | Type::AlwaysTruthy
             | Type::AlwaysFalsy => None,
@@ -3327,6 +3542,7 @@ impl<'db> Type<'db> {
             | Type::ModuleLiteral(_)
             | Type::StringLiteral(_)
             | Type::Tuple(_)
+            | Type::TypeVar(_)
             | Type::Callable(_)
             | Type::BoundMethod(_)
             | Type::WrapperDescriptor(_)
@@ -3362,8 +3578,7 @@ impl<'db> Type<'db> {
                 KnownInstanceType::Deque => Ok(KnownClass::Deque.to_instance(db)),
                 KnownInstanceType::OrderedDict => Ok(KnownClass::OrderedDict.to_instance(db)),
 
-                // TODO map this to a new `Type::TypeVar` variant
-                KnownInstanceType::TypeVar(_) => Ok(*self),
+                KnownInstanceType::TypeVar(typevar) => Ok(Type::TypeVar(*typevar)),
 
                 // TODO: Use an opt-in rule for a bare `Callable`
                 KnownInstanceType::Callable => Ok(Type::Callable(CallableType::unknown(db))),
@@ -3541,6 +3756,17 @@ impl<'db> Type<'db> {
             Type::Callable(_) => KnownClass::Type.to_instance(db),
             Type::ModuleLiteral(_) => KnownClass::ModuleType.to_class_literal(db),
             Type::Tuple(_) => KnownClass::Tuple.to_class_literal(db),
+
+            Type::TypeVar(typevar) => match typevar.bound_or_constraints(db) {
+                None => KnownClass::Object.to_class_literal(db),
+                Some(TypeVarBoundOrConstraints::UpperBound(bound)) => bound.to_meta_type(db),
+                Some(TypeVarBoundOrConstraints::Constraints(constraints)) => {
+                    // TODO: If we add a proper `OneOf` connector, we should use that here instead
+                    // of union. (Using a union here doesn't break anything, but it is imprecise.)
+                    constraints.map(db, |constraint| constraint.to_meta_type(db))
+                }
+            },
+
             Type::ClassLiteral(ClassLiteralType { class }) => class.metaclass(db),
             Type::SubclassOf(subclass_of_ty) => match subclass_of_ty.subclass_of() {
                 ClassBase::Dynamic(_) => *self,
@@ -3809,10 +4035,10 @@ impl<'db> InvalidTypeExpression<'db> {
 /// Data regarding a single type variable.
 ///
 /// This is referenced by `KnownInstanceType::TypeVar` (to represent the singleton type of the
-/// runtime `typing.TypeVar` object itself). In the future, it will also be referenced also by a
-/// new `Type` variant to represent the type that this typevar represents as an annotation: that
-/// is, an unknown set of objects, constrained by the upper-bound/constraints on this type var,
-/// defaulting to the default type of this type var when not otherwise bound to a type.
+/// runtime `typing.TypeVar` object itself), and by `Type::TypeVar` to represent the type that this
+/// typevar represents as an annotation: that is, an unknown set of objects, constrained by the
+/// upper-bound/constraints on this type var, defaulting to the default type of this type var when
+/// not otherwise bound to a type.
 ///
 /// This must be a tracked struct, not an interned one, because typevar equivalence is by identity,
 /// not by value. Two typevars that have the same name, bound/constraints, and default, are still
@@ -3856,7 +4082,7 @@ impl<'db> TypeVarInstance<'db> {
 #[derive(Clone, Debug, Hash, PartialEq, Eq, salsa::Update)]
 pub enum TypeVarBoundOrConstraints<'db> {
     UpperBound(Type<'db>),
-    Constraints(TupleType<'db>),
+    Constraints(UnionType<'db>),
 }
 
 /// Error returned if a type is not (or may not be) a context manager.
diff --git a/crates/red_knot_python_semantic/src/types/builder.rs b/crates/red_knot_python_semantic/src/types/builder.rs
index 23b9f83807..ff03e4453a 100644
--- a/crates/red_knot_python_semantic/src/types/builder.rs
+++ b/crates/red_knot_python_semantic/src/types/builder.rs
@@ -26,7 +26,7 @@
 //!     eliminate the supertype from the intersection).
 //!   * An intersection containing two non-overlapping types should simplify to [`Type::Never`].
 
-use crate::types::{IntersectionType, KnownClass, Type, UnionType};
+use crate::types::{IntersectionType, KnownClass, Type, TypeVarBoundOrConstraints, UnionType};
 use crate::{Db, FxOrderSet};
 use smallvec::SmallVec;
 
@@ -485,7 +485,109 @@ impl<'db> InnerIntersectionBuilder<'db> {
         }
     }
 
+    /// Tries to simplify any constrained typevars in the intersection:
+    ///
+    /// - If the intersection contains a positive entry for exactly one of the constraints, we can
+    ///   remove the typevar (effectively replacing it with that one positive constraint).
+    ///
+    /// - If the intersection contains negative entries for all but one of the constraints, we can
+    ///   remove the negative constraints and replace the typevar with the remaining positive
+    ///   constraint.
+    ///
+    /// - If the intersection contains negative entries for all of the constraints, the overall
+    ///   intersection is `Never`.
+    fn simplify_constrained_typevars(&mut self, db: &'db dyn Db) {
+        let mut to_add = SmallVec::<[Type<'db>; 1]>::new();
+        let mut positive_to_remove = SmallVec::<[usize; 1]>::new();
+        let mut negative_to_remove = Vec::new();
+
+        for (typevar_index, ty) in self.positive.iter().enumerate() {
+            let Type::TypeVar(typevar) = ty else {
+                continue;
+            };
+            let Some(TypeVarBoundOrConstraints::Constraints(constraints)) =
+                typevar.bound_or_constraints(db)
+            else {
+                continue;
+            };
+
+            // Determine which constraints appear as positive entries in the intersection. Note
+            // that we shouldn't have duplicate entries in the positive or negative lists, so we
+            // don't need to worry about finding any particular constraint more than once.
+            let constraints = constraints.elements(db);
+            let mut positive_constraint_count = 0;
+            for positive in &self.positive {
+                // This linear search should be fine as long as we don't encounter typevars with
+                // thousands of constraints.
+                positive_constraint_count += constraints
+                    .iter()
+                    .filter(|c| c.is_subtype_of(db, *positive))
+                    .count();
+            }
+
+            // If precisely one constraint appears as a positive element, we can replace the
+            // typevar with that positive constraint.
+            if positive_constraint_count == 1 {
+                positive_to_remove.push(typevar_index);
+                continue;
+            }
+
+            // Determine which constraints appear as negative entries in the intersection.
+            let mut to_remove = Vec::with_capacity(constraints.len());
+            let mut remaining_constraints: Vec<_> = constraints.iter().copied().map(Some).collect();
+            for (negative_index, negative) in self.negative.iter().enumerate() {
+                // This linear search should be fine as long as we don't encounter typevars with
+                // thousands of constraints.
+                let matching_constraints = constraints
+                    .iter()
+                    .enumerate()
+                    .filter(|(_, c)| c.is_subtype_of(db, *negative));
+                for (constraint_index, _) in matching_constraints {
+                    to_remove.push(negative_index);
+                    remaining_constraints[constraint_index] = None;
+                }
+            }
+
+            let mut iter = remaining_constraints.into_iter().flatten();
+            let Some(remaining_constraint) = iter.next() else {
+                // All of the typevar constraints have been removed, so the entire intersection is
+                // `Never`.
+                *self = Self::default();
+                self.positive.insert(Type::Never);
+                return;
+            };
+
+            let more_than_one_remaining_constraint = iter.next().is_some();
+            if more_than_one_remaining_constraint {
+                // This typevar cannot be simplified.
+                continue;
+            }
+
+            // Only one typevar constraint remains. Remove all of the negative constraints, and
+            // replace the typevar itself with the remaining positive constraint.
+            to_add.push(remaining_constraint);
+            positive_to_remove.push(typevar_index);
+            negative_to_remove.extend(to_remove);
+        }
+
+        // We don't need to sort the positive list, since we only append to it in increasing order.
+        for index in positive_to_remove.into_iter().rev() {
+            self.positive.swap_remove_index(index);
+        }
+
+        negative_to_remove.sort_unstable();
+        negative_to_remove.dedup();
+        for index in negative_to_remove.into_iter().rev() {
+            self.negative.swap_remove_index(index);
+        }
+
+        for remaining_constraint in to_add {
+            self.add_positive(db, remaining_constraint);
+        }
+    }
+
     fn build(mut self, db: &'db dyn Db) -> Type<'db> {
+        self.simplify_constrained_typevars(db);
         match (self.positive.len(), self.negative.len()) {
             (0, 0) => Type::object(db),
             (1, 0) => self.positive[0],
diff --git a/crates/red_knot_python_semantic/src/types/class_base.rs b/crates/red_knot_python_semantic/src/types/class_base.rs
index 6309d6fb83..db9dbc671b 100644
--- a/crates/red_knot_python_semantic/src/types/class_base.rs
+++ b/crates/red_knot_python_semantic/src/types/class_base.rs
@@ -85,6 +85,7 @@ impl<'db> ClassBase<'db> {
             | Type::SliceLiteral(_)
             | Type::ModuleLiteral(_)
             | Type::SubclassOf(_)
+            | Type::TypeVar(_)
             | Type::AlwaysFalsy
             | Type::AlwaysTruthy => None,
             Type::KnownInstance(known_instance) => match known_instance {
diff --git a/crates/red_knot_python_semantic/src/types/display.rs b/crates/red_knot_python_semantic/src/types/display.rs
index ceeed236c6..7c5fac3c98 100644
--- a/crates/red_knot_python_semantic/src/types/display.rs
+++ b/crates/red_knot_python_semantic/src/types/display.rs
@@ -165,6 +165,9 @@ impl Display for DisplayRepresentation<'_> {
                 }
                 f.write_str("]")
             }
+            Type::TypeVar(typevar) => {
+                write!(f, "{}", typevar.name(self.db))
+            }
             Type::AlwaysTruthy => f.write_str("AlwaysTruthy"),
             Type::AlwaysFalsy => f.write_str("AlwaysFalsy"),
         }
diff --git a/crates/red_knot_python_semantic/src/types/infer.rs b/crates/red_knot_python_semantic/src/types/infer.rs
index 0bc051b850..60571aca6b 100644
--- a/crates/red_knot_python_semantic/src/types/infer.rs
+++ b/crates/red_knot_python_semantic/src/types/infer.rs
@@ -1997,14 +1997,25 @@ impl<'db> TypeInferenceBuilder<'db> {
                     self.infer_expression(expr);
                     None
                 } else {
-                    let tuple = TupleType::new(
+                    // We don't use UnionType::from_elements or UnionBuilder here, because we don't
+                    // want to simplify the list of constraints like we do with the elements of an
+                    // actual union type.
+                    // TODO: Consider using a new `OneOfType` connective here instead, since that
+                    // more accurately represents the actual semantics of typevar constraints.
+                    let elements = UnionType::new(
                         self.db(),
                         elts.iter()
                             .map(|expr| self.infer_type_expression(expr))
-                            .collect::<Box<_>>(),
+                            .collect::<Box<[_]>>(),
+                    );
+                    let constraints = TypeVarBoundOrConstraints::Constraints(elements);
+                    // But when we construct an actual union type for the constraint expression as
+                    // a whole, we do use UnionType::from_elements to maintain the invariant that
+                    // all union types are simplified.
+                    self.store_expression_type(
+                        expr,
+                        UnionType::from_elements(self.db(), elements.elements(self.db())),
                     );
-                    let constraints = TypeVarBoundOrConstraints::Constraints(tuple);
-                    self.store_expression_type(expr, Type::Tuple(tuple));
                     Some(constraints)
                 }
             }
@@ -2344,6 +2355,7 @@ impl<'db> TypeInferenceBuilder<'db> {
             | Type::BoundMethod(_)
             | Type::MethodWrapper(_)
             | Type::WrapperDescriptor(_)
+            | Type::TypeVar(..)
             | Type::AlwaysTruthy
             | Type::AlwaysFalsy => match object_ty.class_member(db, attribute.into()) {
                 meta_attr @ SymbolAndQualifiers { .. } if meta_attr.is_class_var() => {
@@ -4462,7 +4474,8 @@ impl<'db> TypeInferenceBuilder<'db> {
                 | Type::LiteralString
                 | Type::BytesLiteral(_)
                 | Type::SliceLiteral(_)
-                | Type::Tuple(_),
+                | Type::Tuple(_)
+                | Type::TypeVar(_),
             ) => {
                 let unary_dunder_method = match op {
                     ast::UnaryOp::Invert => "__invert__",
@@ -4737,7 +4750,8 @@ impl<'db> TypeInferenceBuilder<'db> {
                 | Type::LiteralString
                 | Type::BytesLiteral(_)
                 | Type::SliceLiteral(_)
-                | Type::Tuple(_),
+                | Type::Tuple(_)
+                | Type::TypeVar(_),
                 Type::FunctionLiteral(_)
                 | Type::Callable(..)
                 | Type::BoundMethod(_)
@@ -4757,7 +4771,8 @@ impl<'db> TypeInferenceBuilder<'db> {
                 | Type::LiteralString
                 | Type::BytesLiteral(_)
                 | Type::SliceLiteral(_)
-                | Type::Tuple(_),
+                | Type::Tuple(_)
+                | Type::TypeVar(_),
                 op,
             ) => {
                 // We either want to call lhs.__op__ or rhs.__rop__. The full decision tree from
diff --git a/crates/red_knot_python_semantic/src/types/type_ordering.rs b/crates/red_knot_python_semantic/src/types/type_ordering.rs
index e7f199aa9a..71252ebb25 100644
--- a/crates/red_knot_python_semantic/src/types/type_ordering.rs
+++ b/crates/red_knot_python_semantic/src/types/type_ordering.rs
@@ -121,6 +121,10 @@ pub(super) fn union_or_intersection_elements_ordering<'db>(
         (Type::Instance(_), _) => Ordering::Less,
         (_, Type::Instance(_)) => Ordering::Greater,
 
+        (Type::TypeVar(left), Type::TypeVar(right)) => left.cmp(right),
+        (Type::TypeVar(_), _) => Ordering::Less,
+        (_, Type::TypeVar(_)) => Ordering::Greater,
+
         (Type::AlwaysTruthy, _) => Ordering::Less,
         (_, Type::AlwaysTruthy) => Ordering::Greater,