diff --git a/crates/red_knot_python_semantic/resources/mdtest/import/builtins.md b/crates/red_knot_python_semantic/resources/mdtest/import/builtins.md
index 1b2305fb410c2f..7d1a3f5e0bd49a 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/import/builtins.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/import/builtins.md
@@ -7,7 +7,7 @@ Builtin symbols can be explicitly imported:
 ```py
 import builtins
 
-reveal_type(builtins.chr)  # revealed: def chr(i: int | SupportsIndex, /) -> str
+reveal_type(builtins.chr)  # revealed: def chr(i: SupportsIndex, /) -> str
 ```
 
 ## Implicit use of builtin
@@ -15,7 +15,7 @@ reveal_type(builtins.chr)  # revealed: def chr(i: int | SupportsIndex, /) -> str
 Or used implicitly:
 
 ```py
-reveal_type(chr)  # revealed: def chr(i: int | SupportsIndex, /) -> str
+reveal_type(chr)  # revealed: def chr(i: SupportsIndex, /) -> str
 reveal_type(str)  # revealed: Literal[str]
 ```
 
diff --git a/crates/red_knot_python_semantic/resources/mdtest/protocols.md b/crates/red_knot_python_semantic/resources/mdtest/protocols.md
index 0af5a8b58cdd95..5f124e0549508f 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/protocols.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/protocols.md
@@ -230,7 +230,7 @@ And it is also an error to use `Protocol` in type expressions:
 def f(
     x: Protocol,  # error: [invalid-type-form] "`typing.Protocol` is not allowed in type expressions"
     y: type[Protocol],  # TODO: should emit `[invalid-type-form]` here too
-) -> None:
+):
     reveal_type(x)  # revealed: Unknown
 
     # TODO: should be `type[Unknown]`
@@ -266,9 +266,7 @@ class Bar(typing_extensions.Protocol):
 
 static_assert(typing_extensions.is_protocol(Foo))
 static_assert(typing_extensions.is_protocol(Bar))
-
-# TODO: should pass
-static_assert(is_equivalent_to(Foo, Bar))  # error: [static-assert-error]
+static_assert(is_equivalent_to(Foo, Bar))
 ```
 
 The same goes for `typing.runtime_checkable` and `typing_extensions.runtime_checkable`:
@@ -284,9 +282,7 @@ class RuntimeCheckableBar(typing_extensions.Protocol):
 
 static_assert(typing_extensions.is_protocol(RuntimeCheckableFoo))
 static_assert(typing_extensions.is_protocol(RuntimeCheckableBar))
-
-# TODO: should pass
-static_assert(is_equivalent_to(RuntimeCheckableFoo, RuntimeCheckableBar))  # error: [static-assert-error]
+static_assert(is_equivalent_to(RuntimeCheckableFoo, RuntimeCheckableBar))
 
 # These should not error because the protocols are decorated with `@runtime_checkable`
 isinstance(object(), RuntimeCheckableFoo)
@@ -488,21 +484,20 @@ class HasX(Protocol):
 class Foo:
     x: int
 
-# TODO: these should pass
-static_assert(is_subtype_of(Foo, HasX))  # error: [static-assert-error]
-static_assert(is_assignable_to(Foo, HasX))  # error: [static-assert-error]
+static_assert(is_subtype_of(Foo, HasX))
+static_assert(is_assignable_to(Foo, HasX))
 
 class FooSub(Foo): ...
 
-# TODO: these should pass
-static_assert(is_subtype_of(FooSub, HasX))  # error: [static-assert-error]
-static_assert(is_assignable_to(FooSub, HasX))  # error: [static-assert-error]
+static_assert(is_subtype_of(FooSub, HasX))
+static_assert(is_assignable_to(FooSub, HasX))
 
 class Bar:
     x: str
 
-static_assert(not is_subtype_of(Bar, HasX))
-static_assert(not is_assignable_to(Bar, HasX))
+# TODO: these should pass
+static_assert(not is_subtype_of(Bar, HasX))  # error: [static-assert-error]
+static_assert(not is_assignable_to(Bar, HasX))  # error: [static-assert-error]
 
 class Baz:
     y: int
@@ -524,14 +519,16 @@ class A:
     def x(self) -> int:
         return 42
 
-static_assert(not is_subtype_of(A, HasX))
-static_assert(not is_assignable_to(A, HasX))
+# TODO: these should pass
+static_assert(not is_subtype_of(A, HasX))  # error: [static-assert-error]
+static_assert(not is_assignable_to(A, HasX))  # error: [static-assert-error]
 
 class B:
     x: Final = 42
 
-static_assert(not is_subtype_of(A, HasX))
-static_assert(not is_assignable_to(A, HasX))
+# TODO: these should pass
+static_assert(not is_subtype_of(A, HasX))  # error: [static-assert-error]
+static_assert(not is_assignable_to(A, HasX))  # error: [static-assert-error]
 
 class IntSub(int): ...
 
@@ -541,8 +538,10 @@ class C:
 # due to invariance, a type is only a subtype of `HasX`
 # if its `x` attribute is of type *exactly* `int`:
 # a subclass of `int` does not satisfy the interface
-static_assert(not is_subtype_of(C, HasX))
-static_assert(not is_assignable_to(C, HasX))
+#
+# TODO: these should pass
+static_assert(not is_subtype_of(C, HasX))  # error: [static-assert-error]
+static_assert(not is_assignable_to(C, HasX))  # error: [static-assert-error]
 ```
 
 All attributes on frozen dataclasses and namedtuples are immutable, so instances of these classes
@@ -556,22 +555,23 @@ from typing import NamedTuple
 class MutableDataclass:
     x: int
 
-# TODO: these should pass
-static_assert(is_subtype_of(MutableDataclass, HasX))  # error: [static-assert-error]
-static_assert(is_assignable_to(MutableDataclass, HasX))  # error: [static-assert-error]
+static_assert(is_subtype_of(MutableDataclass, HasX))
+static_assert(is_assignable_to(MutableDataclass, HasX))
 
 @dataclass(frozen=True)
 class ImmutableDataclass:
     x: int
 
-static_assert(not is_subtype_of(ImmutableDataclass, HasX))
-static_assert(not is_assignable_to(ImmutableDataclass, HasX))
+# TODO: these should pass
+static_assert(not is_subtype_of(ImmutableDataclass, HasX))  # error: [static-assert-error]
+static_assert(not is_assignable_to(ImmutableDataclass, HasX))  # error: [static-assert-error]
 
 class NamedTupleWithX(NamedTuple):
     x: int
 
-static_assert(not is_subtype_of(NamedTupleWithX, HasX))
-static_assert(not is_assignable_to(NamedTupleWithX, HasX))
+# TODO: these should pass
+static_assert(not is_subtype_of(NamedTupleWithX, HasX))  # error: [static-assert-error]
+static_assert(not is_assignable_to(NamedTupleWithX, HasX))  # error: [static-assert-error]
 ```
 
 However, a type with a read-write property `x` *does* satisfy the `HasX` protocol. The `HasX`
@@ -590,9 +590,8 @@ class XProperty:
     def x(self, x: int) -> None:
         self._x = x**2
 
-# TODO: these should pass
-static_assert(is_subtype_of(XProperty, HasX))  # error: [static-assert-error]
-static_assert(is_assignable_to(XProperty, HasX))  # error: [static-assert-error]
+static_assert(is_subtype_of(XProperty, HasX))
+static_assert(is_assignable_to(XProperty, HasX))
 ```
 
 Attribute members on protocol classes are allowed to have default values, just like instance
@@ -717,9 +716,8 @@ from typing import Protocol
 
 class UniversalSet(Protocol): ...
 
-# TODO: these should pass
-static_assert(is_assignable_to(object, UniversalSet))  # error: [static-assert-error]
-static_assert(is_subtype_of(object, UniversalSet))  # error: [static-assert-error]
+static_assert(is_assignable_to(object, UniversalSet))
+static_assert(is_subtype_of(object, UniversalSet))
 ```
 
 Which means that `UniversalSet` here is in fact an equivalent type to `object`:
@@ -727,8 +725,7 @@ Which means that `UniversalSet` here is in fact an equivalent type to `object`:
 ```py
 from knot_extensions import is_equivalent_to
 
-# TODO: this should pass
-static_assert(is_equivalent_to(UniversalSet, object))  # error: [static-assert-error]
+static_assert(is_equivalent_to(UniversalSet, object))
 ```
 
 `object` is a subtype of certain other protocols too. Since all fully static types (whether nominal
@@ -739,17 +736,16 @@ means that these protocols are also equivalent to `UniversalSet` and `object`:
 class SupportsStr(Protocol):
     def __str__(self) -> str: ...
 
-# TODO: these should pass
-static_assert(is_equivalent_to(SupportsStr, UniversalSet))  # error: [static-assert-error]
-static_assert(is_equivalent_to(SupportsStr, object))  # error: [static-assert-error]
+static_assert(is_equivalent_to(SupportsStr, UniversalSet))
+static_assert(is_equivalent_to(SupportsStr, object))
 
 class SupportsClass(Protocol):
-    __class__: type
+    @property
+    def __class__(self) -> type: ...
 
-# TODO: these should pass
-static_assert(is_equivalent_to(SupportsClass, UniversalSet))  # error: [static-assert-error]
-static_assert(is_equivalent_to(SupportsClass, SupportsStr))  # error: [static-assert-error]
-static_assert(is_equivalent_to(SupportsClass, object))  # error: [static-assert-error]
+static_assert(is_equivalent_to(SupportsClass, UniversalSet))
+static_assert(is_equivalent_to(SupportsClass, SupportsStr))
+static_assert(is_equivalent_to(SupportsClass, object))
 ```
 
 If a protocol contains members that are not defined on `object`, then that protocol will (like all
@@ -786,8 +782,7 @@ class HasX(Protocol):
 class AlsoHasX(Protocol):
     x: int
 
-# TODO: this should pass
-static_assert(is_equivalent_to(HasX, AlsoHasX))  # error: [static-assert-error]
+static_assert(is_equivalent_to(HasX, AlsoHasX))
 ```
 
 And unions containing equivalent protocols are recognised as equivalent, even when the order is not
@@ -803,8 +798,7 @@ class AlsoHasY(Protocol):
 class A: ...
 class B: ...
 
-# TODO: this should pass
-static_assert(is_equivalent_to(A | HasX | B | HasY, B | AlsoHasY | AlsoHasX | A))  # error: [static-assert-error]
+static_assert(is_equivalent_to(A | HasX | B | HasY, B | AlsoHasY | AlsoHasX | A))
 ```
 
 ## Intersections of protocols
@@ -882,9 +876,9 @@ from knot_extensions import is_subtype_of, is_assignable_to, static_assert, Type
 class HasX(Protocol):
     x: int
 
-# TODO: these should pass
+# TODO: this should pass
 static_assert(is_subtype_of(TypeOf[module], HasX))  # error: [static-assert-error]
-static_assert(is_assignable_to(TypeOf[module], HasX))  # error: [static-assert-error]
+static_assert(is_assignable_to(TypeOf[module], HasX))
 
 class ExplicitProtocolSubtype(HasX, Protocol):
     y: int
@@ -896,9 +890,8 @@ class ImplicitProtocolSubtype(Protocol):
     x: int
     y: str
 
-# TODO: these should pass
-static_assert(is_subtype_of(ImplicitProtocolSubtype, HasX))  # error: [static-assert-error]
-static_assert(is_assignable_to(ImplicitProtocolSubtype, HasX))  # error: [static-assert-error]
+static_assert(is_subtype_of(ImplicitProtocolSubtype, HasX))
+static_assert(is_assignable_to(ImplicitProtocolSubtype, HasX))
 
 class Meta(type):
     x: int
@@ -933,23 +926,24 @@ def f(obj: ClassVarXProto):
 class InstanceAttrX:
     x: int
 
-static_assert(not is_assignable_to(InstanceAttrX, ClassVarXProto))
-static_assert(not is_subtype_of(InstanceAttrX, ClassVarXProto))
+# TODO: these should pass
+static_assert(not is_assignable_to(InstanceAttrX, ClassVarXProto))  # error: [static-assert-error]
+static_assert(not is_subtype_of(InstanceAttrX, ClassVarXProto))  # error: [static-assert-error]
 
 class PropertyX:
     @property
     def x(self) -> int:
         return 42
 
-static_assert(not is_assignable_to(PropertyX, ClassVarXProto))
-static_assert(not is_subtype_of(PropertyX, ClassVarXProto))
+# TODO: these should pass
+static_assert(not is_assignable_to(PropertyX, ClassVarXProto))  # error: [static-assert-error]
+static_assert(not is_subtype_of(PropertyX, ClassVarXProto))  # error: [static-assert-error]
 
 class ClassVarX:
     x: ClassVar[int] = 42
 
-# TODO: these should pass
-static_assert(is_assignable_to(ClassVarX, ClassVarXProto))  # error: [static-assert-error]
-static_assert(is_subtype_of(ClassVarX, ClassVarXProto))  # error: [static-assert-error]
+static_assert(is_assignable_to(ClassVarX, ClassVarXProto))
+static_assert(is_subtype_of(ClassVarX, ClassVarXProto))
 ```
 
 This is mentioned by the
@@ -976,18 +970,16 @@ class HasXProperty(Protocol):
 class XAttr:
     x: int
 
-# TODO: these should pass
-static_assert(is_subtype_of(XAttr, HasXProperty))  # error: [static-assert-error]
-static_assert(is_assignable_to(XAttr, HasXProperty))  # error: [static-assert-error]
+static_assert(is_subtype_of(XAttr, HasXProperty))
+static_assert(is_assignable_to(XAttr, HasXProperty))
 
 class XReadProperty:
     @property
     def x(self) -> int:
         return 42
 
-# TODO: these should pass
-static_assert(is_subtype_of(XReadProperty, HasXProperty))  # error: [static-assert-error]
-static_assert(is_assignable_to(XReadProperty, HasXProperty))  # error: [static-assert-error]
+static_assert(is_subtype_of(XReadProperty, HasXProperty))
+static_assert(is_assignable_to(XReadProperty, HasXProperty))
 
 class XReadWriteProperty:
     @property
@@ -997,22 +989,20 @@ class XReadWriteProperty:
     @x.setter
     def x(self, val: int) -> None: ...
 
-# TODO: these should pass
-static_assert(is_subtype_of(XReadWriteProperty, HasXProperty))  # error: [static-assert-error]
-static_assert(is_assignable_to(XReadWriteProperty, HasXProperty))  # error: [static-assert-error]
+static_assert(is_subtype_of(XReadWriteProperty, HasXProperty))
+static_assert(is_assignable_to(XReadWriteProperty, HasXProperty))
 
 class XClassVar:
     x: ClassVar[int] = 42
 
-static_assert(is_subtype_of(XClassVar, HasXProperty))  # error: [static-assert-error]
-static_assert(is_assignable_to(XClassVar, HasXProperty))  # error: [static-assert-error]
+static_assert(is_subtype_of(XClassVar, HasXProperty))
+static_assert(is_assignable_to(XClassVar, HasXProperty))
 
 class XFinal:
     x: Final = 42
 
-# TODO: these should pass
-static_assert(is_subtype_of(XFinal, HasXProperty))  # error: [static-assert-error]
-static_assert(is_assignable_to(XFinal, HasXProperty))  # error: [static-assert-error]
+static_assert(is_subtype_of(XFinal, HasXProperty))
+static_assert(is_assignable_to(XFinal, HasXProperty))
 ```
 
 A read-only property on a protocol, unlike a mutable attribute, is covariant: `XSub` in the below
@@ -1025,9 +1015,8 @@ class MyInt(int): ...
 class XSub:
     x: MyInt
 
-# TODO: these should pass
-static_assert(is_subtype_of(XSub, HasXProperty))  # error: [static-assert-error]
-static_assert(is_assignable_to(XSub, HasXProperty))  # error: [static-assert-error]
+static_assert(is_subtype_of(XSub, HasXProperty))
+static_assert(is_assignable_to(XSub, HasXProperty))
 ```
 
 A read/write property on a protocol, where the getter returns the same type that the setter takes,
@@ -1043,17 +1032,17 @@ class HasMutableXProperty(Protocol):
 class XAttr:
     x: int
 
-# TODO: these should pass
-static_assert(is_subtype_of(XAttr, HasXProperty))  # error: [static-assert-error]
-static_assert(is_assignable_to(XAttr, HasXProperty))  # error: [static-assert-error]
+static_assert(is_subtype_of(XAttr, HasXProperty))
+static_assert(is_assignable_to(XAttr, HasXProperty))
 
 class XReadProperty:
     @property
     def x(self) -> int:
         return 42
 
-static_assert(not is_subtype_of(XReadProperty, HasXProperty))
-static_assert(not is_assignable_to(XReadProperty, HasXProperty))
+# TODO: these should pass
+static_assert(not is_subtype_of(XReadProperty, HasXProperty))  # error: [static-assert-error]
+static_assert(not is_assignable_to(XReadProperty, HasXProperty))  # error: [static-assert-error]
 
 class XReadWriteProperty:
     @property
@@ -1063,15 +1052,15 @@ class XReadWriteProperty:
     @x.setter
     def x(self, val: int) -> None: ...
 
-# TODO: these should pass
-static_assert(is_subtype_of(XReadWriteProperty, HasXProperty))  # error: [static-assert-error]
-static_assert(is_assignable_to(XReadWriteProperty, HasXProperty))  # error: [static-assert-error]
+static_assert(is_subtype_of(XReadWriteProperty, HasXProperty))
+static_assert(is_assignable_to(XReadWriteProperty, HasXProperty))
 
 class XSub:
     x: MyInt
 
-static_assert(not is_subtype_of(XSub, HasXProperty))
-static_assert(not is_assignable_to(XSub, HasXProperty))
+# TODO: should pass
+static_assert(not is_subtype_of(XSub, HasXProperty))  # error: [static-assert-error]
+static_assert(not is_assignable_to(XSub, HasXProperty))  # error: [static-assert-error]
 ```
 
 A protocol with a read/write property `x` is exactly equivalent to a protocol with a mutable
@@ -1083,16 +1072,13 @@ from knot_extensions import is_equivalent_to
 class HasMutableXAttr(Protocol):
     x: int
 
-# TODO: this should pass
-static_assert(is_equivalent_to(HasMutableXAttr, HasMutableXProperty))  # error: [static-assert-error]
+static_assert(is_equivalent_to(HasMutableXAttr, HasMutableXProperty))
 
-# TODO: these should pass
-static_assert(is_subtype_of(HasMutableXAttr, HasXProperty))  # error: [static-assert-error]
-static_assert(is_assignable_to(HasMutableXAttr, HasXProperty))  # error: [static-assert-error]
+static_assert(is_subtype_of(HasMutableXAttr, HasXProperty))
+static_assert(is_assignable_to(HasMutableXAttr, HasXProperty))
 
-# TODO: these should pass
-static_assert(is_subtype_of(HasMutableXProperty, HasXProperty))  # error: [static-assert-error]
-static_assert(is_assignable_to(HasMutableXProperty, HasXProperty))  # error: [static-assert-error]
+static_assert(is_subtype_of(HasMutableXProperty, HasXProperty))
+static_assert(is_assignable_to(HasMutableXProperty, HasXProperty))
 ```
 
 A read/write property on a protocol, where the setter accepts a subtype of the type returned by the
@@ -1119,9 +1105,8 @@ class HasAsymmetricXProperty(Protocol):
 class XAttr:
     x: int
 
-# TODO: these should pass
-static_assert(is_subtype_of(XAttr, HasAsymmetricXProperty))  # error: [static-assert-error]
-static_assert(is_assignable_to(XAttr, HasAsymmetricXProperty))  # error: [static-assert-error]
+static_assert(is_subtype_of(XAttr, HasAsymmetricXProperty))
+static_assert(is_assignable_to(XAttr, HasAsymmetricXProperty))
 ```
 
 The end conclusion of this is that the getter-returned type of a property is always covariant and
@@ -1132,9 +1117,8 @@ regular mutable attribute, where the implied getter-returned and setter-accepted
 class XAttrSub:
     x: MyInt
 
-# TODO: these should pass
-static_assert(is_subtype_of(XAttrSub, HasAsymmetricXProperty))  # error: [static-assert-error]
-static_assert(is_assignable_to(XAttrSub, HasAsymmetricXProperty))  # error: [static-assert-error]
+static_assert(is_subtype_of(XAttrSub, HasAsymmetricXProperty))
+static_assert(is_assignable_to(XAttrSub, HasAsymmetricXProperty))
 
 class MyIntSub(MyInt):
     pass
@@ -1142,8 +1126,9 @@ class MyIntSub(MyInt):
 class XAttrSubSub:
     x: MyIntSub
 
-static_assert(not is_subtype_of(XAttrSubSub, HasAsymmetricXProperty))
-static_assert(not is_assignable_to(XAttrSubSub, HasAsymmetricXProperty))
+# TODO: should pass
+static_assert(not is_subtype_of(XAttrSubSub, HasAsymmetricXProperty))  # error: [static-assert-error]
+static_assert(not is_assignable_to(XAttrSubSub, HasAsymmetricXProperty))  # error: [static-assert-error]
 ```
 
 An asymmetric property on a protocol can also be satisfied by an asymmetric property on a nominal
@@ -1159,9 +1144,8 @@ class XAsymmetricProperty:
     @x.setter
     def x(self, x: int) -> None: ...
 
-# TODO: these should pass
-static_assert(is_subtype_of(XAsymmetricProperty, HasAsymmetricXProperty))  # error: [static-assert-error]
-static_assert(is_assignable_to(XAsymmetricProperty, HasAsymmetricXProperty))  # error: [static-assert-error]
+static_assert(is_subtype_of(XAsymmetricProperty, HasAsymmetricXProperty))
+static_assert(is_assignable_to(XAsymmetricProperty, HasAsymmetricXProperty))
 ```
 
 A custom descriptor attribute on the nominal class will also suffice:
@@ -1176,9 +1160,8 @@ class Descriptor:
 class XCustomDescriptor:
     x: Descriptor = Descriptor()
 
-# TODO: these should pass
-static_assert(is_subtype_of(XCustomDescriptor, HasAsymmetricXProperty))  # error: [static-assert-error]
-static_assert(is_assignable_to(XCustomDescriptor, HasAsymmetricXProperty))  # error: [static-assert-error]
+static_assert(is_subtype_of(XCustomDescriptor, HasAsymmetricXProperty))
+static_assert(is_assignable_to(XCustomDescriptor, HasAsymmetricXProperty))
 ```
 
 Moreover, a read-only property on a protocol can be satisfied by a nominal class that defines a
@@ -1191,19 +1174,20 @@ class HasGetAttr:
     def __getattr__(self, attr: str) -> int:
         return 42
 
-# TODO: these should pass
-static_assert(is_subtype_of(HasGetAttr, HasXProperty))  # error: [static-assert-error]
-static_assert(is_assignable_to(HasGetAttr, HasXProperty))  # error: [static-assert-error]
+static_assert(is_subtype_of(HasGetAttr, HasXProperty))
+static_assert(is_assignable_to(HasGetAttr, HasXProperty))
 
-static_assert(not is_subtype_of(HasGetAttr, HasMutableXAttr))
-static_assert(not is_subtype_of(HasGetAttr, HasMutableXAttr))
+# TODO: these should pass
+static_assert(not is_subtype_of(HasGetAttr, HasMutableXAttr))  # error: [static-assert-error]
+static_assert(not is_subtype_of(HasGetAttr, HasMutableXAttr))  # error: [static-assert-error]
 
 class HasGetAttrWithUnsuitableReturn:
     def __getattr__(self, attr: str) -> tuple[int, int]:
         return (1, 2)
 
-static_assert(not is_subtype_of(HasGetAttrWithUnsuitableReturn, HasXProperty))
-static_assert(not is_assignable_to(HasGetAttrWithUnsuitableReturn, HasXProperty))
+# TODO: these should pass
+static_assert(not is_subtype_of(HasGetAttrWithUnsuitableReturn, HasXProperty))  # error: [static-assert-error]
+static_assert(not is_assignable_to(HasGetAttrWithUnsuitableReturn, HasXProperty))  # error: [static-assert-error]
 
 class HasGetAttrAndSetAttr:
     def __getattr__(self, attr: str) -> MyInt:
@@ -1211,9 +1195,10 @@ class HasGetAttrAndSetAttr:
 
     def __setattr__(self, attr: str, value: int) -> None: ...
 
+static_assert(is_subtype_of(HasGetAttrAndSetAttr, HasXProperty))
+static_assert(is_assignable_to(HasGetAttrAndSetAttr, HasXProperty))
+
 # TODO: these should pass
-static_assert(is_subtype_of(HasGetAttrAndSetAttr, HasXProperty))  # error: [static-assert-error]
-static_assert(is_assignable_to(HasGetAttrAndSetAttr, HasXProperty))  # error: [static-assert-error]
 static_assert(is_subtype_of(HasGetAttrAndSetAttr, XAsymmetricProperty))  # error: [static-assert-error]
 static_assert(is_assignable_to(HasGetAttrAndSetAttr, XAsymmetricProperty))  # error: [static-assert-error]
 ```
@@ -1363,12 +1348,12 @@ from knot_extensions import is_subtype_of, is_assignable_to
 class NominalWithX:
     x: int = 42
 
-# TODO: these should pass
-static_assert(is_assignable_to(NominalWithX, FullyStatic))  # error: [static-assert-error]
-static_assert(is_assignable_to(NominalWithX, NotFullyStatic))  # error: [static-assert-error]
-static_assert(is_subtype_of(NominalWithX, FullyStatic))  # error: [static-assert-error]
+static_assert(is_assignable_to(NominalWithX, FullyStatic))
+static_assert(is_assignable_to(NominalWithX, NotFullyStatic))
+static_assert(is_subtype_of(NominalWithX, FullyStatic))
 
-static_assert(not is_subtype_of(NominalWithX, NotFullyStatic))
+# TODO: this should pass
+static_assert(not is_subtype_of(NominalWithX, NotFullyStatic))  # error: [static-assert-error]
 ```
 
 Empty protocols are fully static; this follows from the fact that an empty protocol is equivalent to
@@ -1418,30 +1403,124 @@ static_assert(not is_fully_static(NoParameterAnnotation))  # error: [static-asse
 static_assert(not is_fully_static(NoReturnAnnotation))  # error: [static-assert-error]
 ```
 
-## `typing.SupportsIndex` and `typing.Sized`
+## Callable protocols
 
-`typing.SupportsIndex` is already somewhat supported through some special-casing in red-knot.
+An instance of a protocol type is callable if the protocol defines a `__call__` method:
 
 ```py
-from typing import SupportsIndex, Literal
+from typing import Protocol
 
-def _(some_int: int, some_literal_int: Literal[1], some_indexable: SupportsIndex):
-    a: SupportsIndex = some_int
-    b: SupportsIndex = some_literal_int
-    c: SupportsIndex = some_indexable
+class CallMeMaybe(Protocol):
+    def __call__(self, x: int) -> str: ...
+
+def f(obj: CallMeMaybe):
+    reveal_type(obj(42))  # revealed: str
+    obj("bar")  # error: [invalid-argument-type]
+```
+
+An instance of a protocol like this can be assignable to a `Callable` type, but only if it has the
+right signature:
+
+```py
+from typing import Callable
+from knot_extensions import is_subtype_of, is_assignable_to, static_assert
+
+static_assert(is_subtype_of(CallMeMaybe, Callable[[int], str]))
+static_assert(is_assignable_to(CallMeMaybe, Callable[[int], str]))
+static_assert(not is_subtype_of(CallMeMaybe, Callable[[str], str]))
+static_assert(not is_assignable_to(CallMeMaybe, Callable[[str], str]))
+static_assert(not is_subtype_of(CallMeMaybe, Callable[[CallMeMaybe, int], str]))
+static_assert(not is_assignable_to(CallMeMaybe, Callable[[CallMeMaybe, int], str]))
+
+def g(obj: Callable[[int], str], obj2: CallMeMaybe, obj3: Callable[[str], str]):
+    obj = obj2
+    obj3 = obj2  # error: [invalid-assignment]
+```
+
+By the same token, a `Callable` type can also be assignable to a protocol-instance type if the
+signature implied by the `Callable` type is assignable to the signature of the `__call__` method
+specified by the protocol:
+
+```py
+class Foo(Protocol):
+    def __call__(self, x: int, /) -> str: ...
+
+# TODO: these fail because we don't yet understand that all `Callable` types have a `__call__` method,
+# and we therefore don't think that the `Callable` type is assignable to `Foo`. They should pass.
+static_assert(is_subtype_of(Callable[[int], str], Foo))  # error: [static-assert-error]
+static_assert(is_assignable_to(Callable[[int], str], Foo))  # error: [static-assert-error]
+
+static_assert(not is_subtype_of(Callable[[str], str], Foo))
+static_assert(not is_assignable_to(Callable[[str], str], Foo))
+static_assert(not is_subtype_of(Callable[[CallMeMaybe, int], str], Foo))
+static_assert(not is_assignable_to(Callable[[CallMeMaybe, int], str], Foo))
+
+def h(obj: Callable[[int], str], obj2: Foo, obj3: Callable[[str], str]):
+    # TODO: this fails because we don't yet understand that all `Callable` types have a `__call__` method,
+    # and we therefore don't think that the `Callable` type is assignable to `Foo`. It should pass.
+    obj2 = obj  # error: [invalid-assignment]
+
+    # This diagnostic is correct, however.
+    obj2 = obj3  # error: [invalid-assignment]
+```
+
+## Protocols are never singleton types, and are never single-valued types
+
+It *might* be possible to have a singleton protocol-instance type...?
+
+For example, `WeirdAndWacky` in the following snippet only has a single possible inhabitant: `None`!
+It is thus a singleton type. However, going out of our way to recognise it as such is probably not
+worth it. Such cases should anyway be exceedingly rare and/or contrived.
+
+```py
+from typing import Protocol, Callable
+from knot_extensions import is_singleton, is_single_valued
+
+class WeirdAndWacky(Protocol):
+    @property
+    def __class__(self) -> Callable[[], None]: ...
+
+reveal_type(is_singleton(WeirdAndWacky))  # revealed: Literal[False]
+reveal_type(is_single_valued(WeirdAndWacky))  # revealed: Literal[False]
 ```
 
-The same goes for `typing.Sized`:
+## Integration test: `typing.SupportsIndex` and `typing.Sized`
+
+`typing.SupportsIndex` and `typing.Sized` are two protocols that are very commonly used in the wild.
 
 ```py
-from typing import Sized
+from typing import SupportsIndex, Sized, Literal
+
+def one(some_int: int, some_literal_int: Literal[1], some_indexable: SupportsIndex):
+    a: SupportsIndex = some_int
+    b: SupportsIndex = some_literal_int
+    c: SupportsIndex = some_indexable
 
-def _(some_list: list, some_tuple: tuple[int, str], some_sized: Sized):
+def two(some_list: list, some_tuple: tuple[int, str], some_sized: Sized):
     a: Sized = some_list
     b: Sized = some_tuple
     c: Sized = some_sized
 ```
 
+## Regression test: narrowing with self-referential protocols
+
+This snippet caused us to panic on an early version of the implementation for protocols.
+
+```py
+from typing import Protocol
+
+class A(Protocol):
+    def x(self) -> "B | A": ...
+
+class B(Protocol):
+    def y(self): ...
+
+obj = something_unresolvable  # error: [unresolved-reference]
+reveal_type(obj)  # revealed: Unknown
+if isinstance(obj, (B, A)):
+    reveal_type(obj)  # revealed: (Unknown & B) | (Unknown & A)
+```
+
 ## TODO
 
 Add tests for:
diff --git a/crates/red_knot_python_semantic/resources/mdtest/scopes/builtin.md b/crates/red_knot_python_semantic/resources/mdtest/scopes/builtin.md
index 5aa4175f8e6591..fc2ca70f97bab2 100644
--- a/crates/red_knot_python_semantic/resources/mdtest/scopes/builtin.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/scopes/builtin.md
@@ -13,7 +13,7 @@ if returns_bool():
     chr: int = 1
 
 def f():
-    reveal_type(chr)  # revealed: int | (def chr(i: int | SupportsIndex, /) -> str)
+    reveal_type(chr)  # revealed: int | (def chr(i: SupportsIndex, /) -> str)
 ```
 
 ## Conditionally global or builtin, with annotation
@@ -28,5 +28,5 @@ if returns_bool():
     chr: int = 1
 
 def f():
-    reveal_type(chr)  # revealed: int | (def chr(i: int | SupportsIndex, /) -> str)
+    reveal_type(chr)  # revealed: int | (def chr(i: SupportsIndex, /) -> str)
 ```
diff --git a/crates/red_knot_python_semantic/src/symbol.rs b/crates/red_knot_python_semantic/src/symbol.rs
index 3be4ce8d02fc5f..b90103585abe63 100644
--- a/crates/red_knot_python_semantic/src/symbol.rs
+++ b/crates/red_knot_python_semantic/src/symbol.rs
@@ -1114,7 +1114,7 @@ mod tests {
     fn assert_bound_string_symbol<'db>(db: &'db dyn Db, symbol: Symbol<'db>) {
         assert!(matches!(
             symbol,
-            Symbol::Type(Type::Instance(_), Boundness::Bound)
+            Symbol::Type(Type::NominalInstance(_), Boundness::Bound)
         ));
         assert_eq!(symbol.expect_type(), KnownClass::Str.to_instance(db));
     }
diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs
index 1047e929f06b0d..826684beb100b7 100644
--- a/crates/red_knot_python_semantic/src/types.rs
+++ b/crates/red_knot_python_semantic/src/types.rs
@@ -51,7 +51,8 @@ pub(crate) use crate::types::narrow::infer_narrowing_constraint;
 use crate::types::signatures::{Parameter, ParameterForm, Parameters};
 use crate::{Db, FxOrderSet, Module, Program};
 pub(crate) use class::{ClassLiteral, ClassType, GenericAlias, KnownClass};
-pub(crate) use instance::InstanceType;
+use instance::Protocol;
+pub(crate) use instance::{NominalInstanceType, ProtocolInstanceType};
 pub(crate) use known_instance::KnownInstanceType;
 
 mod builder;
@@ -489,7 +490,10 @@ pub enum Type<'db> {
     SubclassOf(SubclassOfType<'db>),
     /// The set of Python objects with the given class in their __class__'s method resolution order.
     /// Construct this variant using the `Type::instance` constructor function.
-    Instance(InstanceType<'db>),
+    NominalInstance(NominalInstanceType<'db>),
+    /// The set of Python objects that conform to the interface described by a given protocol.
+    /// Construct this variant using the `Type::instance` constructor function.
+    ProtocolInstance(ProtocolInstanceType<'db>),
     /// A single Python object that requires special treatment in the type system
     KnownInstance(KnownInstanceType<'db>),
     /// An instance of `builtins.property`
@@ -524,7 +528,7 @@ pub enum Type<'db> {
     TypeVar(TypeVarInstance<'db>),
     // A bound super object like `super()` or `super(A, A())`
     // This type doesn't handle an unbound super object like `super(A)`; for that we just use
-    // a `Type::Instance` of `builtins.super`.
+    // a `Type::NominalInstance` of `builtins.super`.
     BoundSuper(BoundSuperType<'db>),
     // TODO protocols, overloads, generics
 }
@@ -557,17 +561,17 @@ impl<'db> Type<'db> {
     }
 
     fn is_none(&self, db: &'db dyn Db) -> bool {
-        self.into_instance()
+        self.into_nominal_instance()
             .is_some_and(|instance| instance.class().is_known(db, KnownClass::NoneType))
     }
 
     fn is_bool(&self, db: &'db dyn Db) -> bool {
-        self.into_instance()
+        self.into_nominal_instance()
             .is_some_and(|instance| instance.class().is_known(db, KnownClass::Bool))
     }
 
     pub fn is_notimplemented(&self, db: &'db dyn Db) -> bool {
-        self.into_instance().is_some_and(|instance| {
+        self.into_nominal_instance().is_some_and(|instance| {
             instance
                 .class()
                 .is_known(db, KnownClass::NotImplementedType)
@@ -575,7 +579,7 @@ impl<'db> Type<'db> {
     }
 
     pub fn is_object(&self, db: &'db dyn Db) -> bool {
-        self.into_instance()
+        self.into_nominal_instance()
             .is_some_and(|instance| instance.class().is_object(db))
     }
 
@@ -597,7 +601,7 @@ impl<'db> Type<'db> {
             | Self::BooleanLiteral(_)
             | Self::BytesLiteral(_)
             | Self::FunctionLiteral(_)
-            | Self::Instance(_)
+            | Self::NominalInstance(_)
             | Self::ModuleLiteral(_)
             | Self::ClassLiteral(_)
             | Self::KnownInstance(_)
@@ -681,6 +685,8 @@ impl<'db> Type<'db> {
                         .iter()
                         .any(|ty| ty.contains_todo(db))
             }
+
+            Self::ProtocolInstance(protocol) => protocol.contains_todo(),
         }
     }
 
@@ -894,6 +900,7 @@ impl<'db> Type<'db> {
     ///   as these are irrelevant to whether a callable type `X` is equivalent to a callable type `Y`.
     /// - Strips the types of default values from parameters in `Callable` types: only whether a parameter
     ///   *has* or *does not have* a default value is relevant to whether two `Callable` types  are equivalent.
+    /// - Converts class-based protocols into synthesized protocols
     #[must_use]
     pub fn normalized(self, db: &'db dyn Db) -> Self {
         match self {
@@ -901,8 +908,9 @@ impl<'db> Type<'db> {
             Type::Intersection(intersection) => Type::Intersection(intersection.normalized(db)),
             Type::Tuple(tuple) => Type::Tuple(tuple.normalized(db)),
             Type::Callable(callable) => Type::Callable(callable.normalized(db)),
+            Type::ProtocolInstance(protocol) => protocol.normalized(db),
             Type::LiteralString
-            | Type::Instance(_)
+            | Type::NominalInstance(_)
             | Type::PropertyInstance(_)
             | Type::AlwaysFalsy
             | Type::AlwaysTruthy
@@ -996,7 +1004,7 @@ impl<'db> Type<'db> {
             (_, Type::Never) => false,
 
             // Everything is a subtype of `object`.
-            (_, Type::Instance(instance)) if instance.class().is_object(db) => true,
+            (_, Type::NominalInstance(instance)) if instance.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
@@ -1160,6 +1168,22 @@ impl<'db> Type<'db> {
                 false
             }
 
+            (Type::NominalInstance(_) | Type::ProtocolInstance(_), Type::Callable(_)) => {
+                let call_symbol = self.member(db, "__call__").symbol;
+                match call_symbol {
+                    Symbol::Type(Type::BoundMethod(call_function), _) => call_function
+                        .into_callable_type(db)
+                        .is_subtype_of(db, target),
+                    _ => false,
+                }
+            }
+            (Type::ProtocolInstance(left), Type::ProtocolInstance(right)) => {
+                left.is_subtype_of(db, right)
+            }
+            // A protocol instance can never be a subtype of a nominal type, with the *sole* exception of `object`.
+            (Type::ProtocolInstance(_), _) => false,
+            (_, Type::ProtocolInstance(protocol)) => self.satisfies_protocol(db, protocol),
+
             (Type::Callable(_), _) => {
                 // TODO: Implement subtyping between callable types and other types like
                 // function literals, bound methods, class literals, `type[]`, etc.)
@@ -1248,7 +1272,7 @@ impl<'db> Type<'db> {
                     metaclass_instance_type.is_subtype_of(db, target)
                 }),
 
-            // For example: `Type::KnownInstance(KnownInstanceType::Type)` is a subtype of `Type::Instance(_SpecialForm)`,
+            // For example: `Type::KnownInstance(KnownInstanceType::Type)` is a subtype of `Type::NominalInstance(_SpecialForm)`,
             // because `Type::KnownInstance(KnownInstanceType::Type)` is a set with exactly one runtime value in it
             // (the symbol `typing.Type`), and that symbol is known to be an instance of `typing._SpecialForm` at runtime.
             (Type::KnownInstance(left), right) => {
@@ -1257,20 +1281,10 @@ impl<'db> Type<'db> {
 
             // `bool` is a subtype of `int`, because `bool` subclasses `int`,
             // which means that all instances of `bool` are also instances of `int`
-            (Type::Instance(self_instance), Type::Instance(target_instance)) => {
+            (Type::NominalInstance(self_instance), Type::NominalInstance(target_instance)) => {
                 self_instance.is_subtype_of(db, target_instance)
             }
 
-            (Type::Instance(_), Type::Callable(_)) => {
-                let call_symbol = self.member(db, "__call__").symbol;
-                match call_symbol {
-                    Symbol::Type(Type::BoundMethod(call_function), _) => call_function
-                        .into_callable_type(db)
-                        .is_subtype_of(db, target),
-                    _ => false,
-                }
-            }
-
             (Type::PropertyInstance(_), _) => KnownClass::Property
                 .to_instance(db)
                 .is_subtype_of(db, target),
@@ -1280,7 +1294,7 @@ impl<'db> Type<'db> {
 
             // Other than the special cases enumerated above, `Instance` types and typevars are
             // never subtypes of any other variants
-            (Type::Instance(_) | Type::TypeVar(_), _) => false,
+            (Type::NominalInstance(_) | Type::TypeVar(_), _) => false,
         }
     }
 
@@ -1302,7 +1316,7 @@ impl<'db> Type<'db> {
 
             // All types are assignable to `object`.
             // TODO this special case might be removable once the below cases are comprehensive
-            (_, Type::Instance(instance)) if instance.class().is_object(db) => true,
+            (_, Type::NominalInstance(instance)) if instance.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
@@ -1436,7 +1450,7 @@ impl<'db> Type<'db> {
             // subtypes of `type[object]` are `type[...]` types (or `Never`), and `type[Any]` can
             // materialize to any `type[...]` type (or to `type[Never]`, which is equivalent to
             // `Never`.)
-            (Type::SubclassOf(subclass_of_ty), Type::Instance(_))
+            (Type::SubclassOf(subclass_of_ty), Type::NominalInstance(_))
                 if subclass_of_ty.is_dynamic()
                     && (KnownClass::Type
                         .to_instance(db)
@@ -1448,44 +1462,14 @@ impl<'db> Type<'db> {
 
             // Any type that is assignable to `type[object]` is also assignable to `type[Any]`,
             // because `type[Any]` can materialize to `type[object]`.
-            (Type::Instance(_), Type::SubclassOf(subclass_of_ty))
+            (Type::NominalInstance(_), Type::SubclassOf(subclass_of_ty))
                 if subclass_of_ty.is_dynamic()
                     && self.is_assignable_to(db, KnownClass::Type.to_instance(db)) =>
             {
                 true
             }
 
-            // TODO: This is a workaround to avoid false positives (e.g. when checking function calls
-            // with `SupportsIndex` parameters), which should be removed when we understand protocols.
-            (lhs, Type::Instance(instance))
-                if instance.class().is_known(db, KnownClass::SupportsIndex) =>
-            {
-                match lhs {
-                    Type::Instance(instance)
-                        if matches!(
-                            instance.class().known(db),
-                            Some(KnownClass::Int | KnownClass::SupportsIndex)
-                        ) =>
-                    {
-                        true
-                    }
-                    Type::IntLiteral(_) => true,
-                    _ => false,
-                }
-            }
-
-            // TODO: ditto for avoiding false positives when checking function calls with `Sized` parameters.
-            (lhs, Type::Instance(instance)) if instance.class().is_known(db, KnownClass::Sized) => {
-                matches!(
-                    lhs.to_meta_type(db).member(db, "__len__"),
-                    SymbolAndQualifiers {
-                        symbol: Symbol::Type(..),
-                        ..
-                    }
-                )
-            }
-
-            (Type::Instance(self_instance), Type::Instance(target_instance)) => {
+            (Type::NominalInstance(self_instance), Type::NominalInstance(target_instance)) => {
                 self_instance.is_assignable_to(db, target_instance)
             }
 
@@ -1493,7 +1477,7 @@ impl<'db> Type<'db> {
                 self_callable.is_assignable_to(db, target_callable)
             }
 
-            (Type::Instance(_), Type::Callable(_)) => {
+            (Type::NominalInstance(_) | Type::ProtocolInstance(_), Type::Callable(_)) => {
                 let call_symbol = self.member(db, "__call__").symbol;
                 match call_symbol {
                     Symbol::Type(Type::BoundMethod(call_function), _) => call_function
@@ -1520,6 +1504,15 @@ impl<'db> Type<'db> {
                 .into_callable_type(db)
                 .is_assignable_to(db, target),
 
+            (Type::ProtocolInstance(left), Type::ProtocolInstance(right)) => {
+                left.is_assignable_to(db, right)
+            }
+            // Other than the dynamic types such as `Any`/`Unknown`/`Todo` handled above,
+            // a protocol instance can never be assignable to a nominal type,
+            // with the *sole* exception of `object`.
+            (Type::ProtocolInstance(_), _) => false,
+            (_, Type::ProtocolInstance(protocol)) => self.satisfies_protocol(db, protocol),
+
             // TODO other types containing gradual forms
             _ => self.is_subtype_of(db, target),
         }
@@ -1540,7 +1533,16 @@ impl<'db> Type<'db> {
             }
             (Type::Tuple(left), Type::Tuple(right)) => left.is_equivalent_to(db, right),
             (Type::Callable(left), Type::Callable(right)) => left.is_equivalent_to(db, right),
-            (Type::Instance(left), Type::Instance(right)) => left.is_equivalent_to(db, right),
+            (Type::NominalInstance(left), Type::NominalInstance(right)) => {
+                left.is_equivalent_to(db, right)
+            }
+            (Type::ProtocolInstance(left), Type::ProtocolInstance(right)) => {
+                left.is_equivalent_to(db, right)
+            }
+            (Type::ProtocolInstance(protocol), nominal @ Type::NominalInstance(n))
+            | (nominal @ Type::NominalInstance(n), Type::ProtocolInstance(protocol)) => {
+                n.class().is_object(db) && protocol.normalized(db) == nominal
+            }
             _ => self == other && self.is_fully_static(db) && other.is_fully_static(db),
         }
     }
@@ -1575,7 +1577,7 @@ impl<'db> Type<'db> {
 
             (Type::TypeVar(first), Type::TypeVar(second)) => first == second,
 
-            (Type::Instance(first), Type::Instance(second)) => {
+            (Type::NominalInstance(first), Type::NominalInstance(second)) => {
                 first.is_gradual_equivalent_to(db, second)
             }
 
@@ -1591,6 +1593,13 @@ impl<'db> Type<'db> {
                 first.is_gradual_equivalent_to(db, second)
             }
 
+            (Type::ProtocolInstance(first), Type::ProtocolInstance(second)) => {
+                first.is_gradual_equivalent_to(db, second)
+            }
+            (Type::ProtocolInstance(protocol), nominal @ Type::NominalInstance(n))
+            | (nominal @ Type::NominalInstance(n), Type::ProtocolInstance(protocol)) => {
+                n.class().is_object(db) && protocol.normalized(db) == nominal
+            }
             _ => false,
         }
     }
@@ -1791,6 +1800,68 @@ impl<'db> Type<'db> {
                 ty.bool(db).is_always_true()
             }
 
+            (Type::ProtocolInstance(left), Type::ProtocolInstance(right)) => {
+                left.is_disjoint_from(db, right)
+            }
+
+            // TODO: we could also consider `protocol` to be disjoint from `nominal` if `nominal`
+            // has the right member but the type of its member is disjoint from the type of the
+            // member on `protocol`.
+            (Type::ProtocolInstance(protocol), nominal @ Type::NominalInstance(n))
+            | (nominal @ Type::NominalInstance(n), Type::ProtocolInstance(protocol)) => {
+                n.class().is_final(db) && !nominal.satisfies_protocol(db, protocol)
+            }
+
+            (
+                ty @ (Type::LiteralString
+                | Type::StringLiteral(..)
+                | Type::BytesLiteral(..)
+                | Type::BooleanLiteral(..)
+                | Type::SliceLiteral(..)
+                | Type::ClassLiteral(..)
+                | Type::FunctionLiteral(..)
+                | Type::ModuleLiteral(..)
+                | Type::GenericAlias(..)
+                | Type::IntLiteral(..)),
+                Type::ProtocolInstance(protocol),
+            )
+            | (
+                Type::ProtocolInstance(protocol),
+                ty @ (Type::LiteralString
+                | Type::StringLiteral(..)
+                | Type::BytesLiteral(..)
+                | Type::BooleanLiteral(..)
+                | Type::SliceLiteral(..)
+                | Type::ClassLiteral(..)
+                | Type::FunctionLiteral(..)
+                | Type::ModuleLiteral(..)
+                | Type::GenericAlias(..)
+                | Type::IntLiteral(..)),
+            ) => !ty.satisfies_protocol(db, protocol),
+
+            (Type::ProtocolInstance(protocol), Type::KnownInstance(known_instance))
+            | (Type::KnownInstance(known_instance), Type::ProtocolInstance(protocol)) => {
+                !known_instance
+                    .instance_fallback(db)
+                    .satisfies_protocol(db, protocol)
+            }
+
+            (Type::Callable(_), Type::ProtocolInstance(_))
+            | (Type::ProtocolInstance(_), Type::Callable(_)) => {
+                // TODO disjointness between `Callable` and `ProtocolInstance`
+                false
+            }
+
+            (Type::Tuple(..), Type::ProtocolInstance(..))
+            | (Type::ProtocolInstance(..), Type::Tuple(..)) => {
+                // Currently we do not make any general assumptions about the disjointness of a `Tuple` type
+                // and a `ProtocolInstance` type because a `Tuple` type can be an instance of a tuple
+                // subclass.
+                //
+                // TODO when we capture the types of the protocol members, we can improve on this.
+                false
+            }
+
             // for `type[Any]`/`type[Unknown]`/`type[Todo]`, we know the type cannot be any larger than `type`,
             // so although the type is dynamic we can still determine disjointedness in some situations
             (Type::SubclassOf(subclass_of_ty), other)
@@ -1803,8 +1874,8 @@ impl<'db> Type<'db> {
                     .is_disjoint_from(db, other),
             },
 
-            (Type::KnownInstance(known_instance), Type::Instance(instance))
-            | (Type::Instance(instance), Type::KnownInstance(known_instance)) => {
+            (Type::KnownInstance(known_instance), Type::NominalInstance(instance))
+            | (Type::NominalInstance(instance), Type::KnownInstance(known_instance)) => {
                 !known_instance.is_instance_of(db, instance.class())
             }
 
@@ -1813,8 +1884,8 @@ impl<'db> Type<'db> {
                 known_instance_ty.is_disjoint_from(db, KnownClass::Tuple.to_instance(db))
             }
 
-            (Type::BooleanLiteral(..), Type::Instance(instance))
-            | (Type::Instance(instance), Type::BooleanLiteral(..)) => {
+            (Type::BooleanLiteral(..), Type::NominalInstance(instance))
+            | (Type::NominalInstance(instance), Type::BooleanLiteral(..)) => {
                 // A `Type::BooleanLiteral()` must be an instance of exactly `bool`
                 // (it cannot be an instance of a `bool` subclass)
                 !KnownClass::Bool.is_subclass_of(db, instance.class())
@@ -1822,8 +1893,8 @@ impl<'db> Type<'db> {
 
             (Type::BooleanLiteral(..), _) | (_, Type::BooleanLiteral(..)) => true,
 
-            (Type::IntLiteral(..), Type::Instance(instance))
-            | (Type::Instance(instance), Type::IntLiteral(..)) => {
+            (Type::IntLiteral(..), Type::NominalInstance(instance))
+            | (Type::NominalInstance(instance), Type::IntLiteral(..)) => {
                 // A `Type::IntLiteral()` must be an instance of exactly `int`
                 // (it cannot be an instance of an `int` subclass)
                 !KnownClass::Int.is_subclass_of(db, instance.class())
@@ -1834,8 +1905,8 @@ impl<'db> Type<'db> {
             (Type::StringLiteral(..), Type::LiteralString)
             | (Type::LiteralString, Type::StringLiteral(..)) => false,
 
-            (Type::StringLiteral(..) | Type::LiteralString, Type::Instance(instance))
-            | (Type::Instance(instance), Type::StringLiteral(..) | Type::LiteralString) => {
+            (Type::StringLiteral(..) | Type::LiteralString, Type::NominalInstance(instance))
+            | (Type::NominalInstance(instance), Type::StringLiteral(..) | Type::LiteralString) => {
                 // A `Type::StringLiteral()` or a `Type::LiteralString` must be an instance of exactly `str`
                 // (it cannot be an instance of a `str` subclass)
                 !KnownClass::Str.is_subclass_of(db, instance.class())
@@ -1844,15 +1915,15 @@ impl<'db> Type<'db> {
             (Type::LiteralString, Type::LiteralString) => false,
             (Type::LiteralString, _) | (_, Type::LiteralString) => true,
 
-            (Type::BytesLiteral(..), Type::Instance(instance))
-            | (Type::Instance(instance), Type::BytesLiteral(..)) => {
+            (Type::BytesLiteral(..), Type::NominalInstance(instance))
+            | (Type::NominalInstance(instance), Type::BytesLiteral(..)) => {
                 // A `Type::BytesLiteral()` must be an instance of exactly `bytes`
                 // (it cannot be an instance of a `bytes` subclass)
                 !KnownClass::Bytes.is_subclass_of(db, instance.class())
             }
 
-            (Type::SliceLiteral(..), Type::Instance(instance))
-            | (Type::Instance(instance), Type::SliceLiteral(..)) => {
+            (Type::SliceLiteral(..), Type::NominalInstance(instance))
+            | (Type::NominalInstance(instance), Type::SliceLiteral(..)) => {
                 // A `Type::SliceLiteral` must be an instance of exactly `slice`
                 // (it cannot be an instance of a `slice` subclass)
                 !KnownClass::Slice.is_subclass_of(db, instance.class())
@@ -1861,17 +1932,19 @@ impl<'db> Type<'db> {
             // A class-literal type `X` is always disjoint from an instance type `Y`,
             // unless the type expressing "all instances of `Z`" is a subtype of of `Y`,
             // where `Z` is `X`'s metaclass.
-            (Type::ClassLiteral(class), instance @ Type::Instance(_))
-            | (instance @ Type::Instance(_), Type::ClassLiteral(class)) => !class
-                .metaclass_instance_type(db)
-                .is_subtype_of(db, instance),
-            (Type::GenericAlias(alias), instance @ Type::Instance(_))
-            | (instance @ Type::Instance(_), Type::GenericAlias(alias)) => !ClassType::from(alias)
+            (Type::ClassLiteral(class), instance @ Type::NominalInstance(_))
+            | (instance @ Type::NominalInstance(_), Type::ClassLiteral(class)) => !class
                 .metaclass_instance_type(db)
                 .is_subtype_of(db, instance),
+            (Type::GenericAlias(alias), instance @ Type::NominalInstance(_))
+            | (instance @ Type::NominalInstance(_), Type::GenericAlias(alias)) => {
+                !ClassType::from(alias)
+                    .metaclass_instance_type(db)
+                    .is_subtype_of(db, instance)
+            }
 
-            (Type::FunctionLiteral(..), Type::Instance(instance))
-            | (Type::Instance(instance), Type::FunctionLiteral(..)) => {
+            (Type::FunctionLiteral(..), Type::NominalInstance(instance))
+            | (Type::NominalInstance(instance), Type::FunctionLiteral(..)) => {
                 // A `Type::FunctionLiteral()` must be an instance of exactly `types.FunctionType`
                 // (it cannot be an instance of a `types.FunctionType` subclass)
                 !KnownClass::FunctionType.is_subclass_of(db, instance.class())
@@ -1927,13 +2000,15 @@ impl<'db> Type<'db> {
                 false
             }
 
-            (Type::ModuleLiteral(..), other @ Type::Instance(..))
-            | (other @ Type::Instance(..), Type::ModuleLiteral(..)) => {
+            (Type::ModuleLiteral(..), other @ Type::NominalInstance(..))
+            | (other @ Type::NominalInstance(..), Type::ModuleLiteral(..)) => {
                 // Modules *can* actually be instances of `ModuleType` subclasses
                 other.is_disjoint_from(db, KnownClass::ModuleType.to_instance(db))
             }
 
-            (Type::Instance(left), Type::Instance(right)) => left.is_disjoint_from(db, right),
+            (Type::NominalInstance(left), Type::NominalInstance(right)) => {
+                left.is_disjoint_from(db, right)
+            }
 
             (Type::Tuple(tuple), Type::Tuple(other_tuple)) => {
                 let self_elements = tuple.elements(db);
@@ -1945,8 +2020,8 @@ impl<'db> Type<'db> {
                         .any(|(e1, e2)| e1.is_disjoint_from(db, *e2))
             }
 
-            (Type::Tuple(..), instance @ Type::Instance(_))
-            | (instance @ Type::Instance(_), Type::Tuple(..)) => {
+            (Type::Tuple(..), instance @ Type::NominalInstance(_))
+            | (instance @ Type::NominalInstance(_), Type::Tuple(..)) => {
                 // We cannot be sure if the tuple is disjoint from the instance because:
                 //   - 'other' might be the homogeneous arbitrary-length tuple type
                 //     tuple[T, ...] (which we don't have support for yet); if all of
@@ -1992,6 +2067,8 @@ impl<'db> Type<'db> {
             | Type::AlwaysTruthy
             | Type::PropertyInstance(_) => true,
 
+            Type::ProtocolInstance(protocol) => protocol.is_fully_static(),
+
             Type::TypeVar(typevar) => match typevar.bound_or_constraints(db) {
                 None => true,
                 Some(TypeVarBoundOrConstraints::UpperBound(bound)) => bound.is_fully_static(db),
@@ -2006,7 +2083,7 @@ impl<'db> Type<'db> {
                 !matches!(bound_super.pivot_class(db), ClassBase::Dynamic(_))
                     && !matches!(bound_super.owner(db), SuperOwnerKind::Dynamic(_))
             }
-            Type::ClassLiteral(_) | Type::GenericAlias(_) | Type::Instance(_) => {
+            Type::ClassLiteral(_) | Type::GenericAlias(_) | Type::NominalInstance(_) => {
                 // TODO: Ideally, we would iterate over the MRO of the class, check if all
                 // bases are fully static, and only return `true` if that is the case.
                 //
@@ -2057,6 +2134,26 @@ impl<'db> Type<'db> {
                 false
             }
 
+            Type::ProtocolInstance(..) => {
+                // It *might* be possible to have a singleton protocol-instance type...?
+                //
+                // E.g.:
+                //
+                // ```py
+                // from typing import Protocol, Callable
+                //
+                // class WeirdAndWacky(Protocol):
+                //     @property
+                //     def __class__(self) -> Callable[[], None]: ...
+                // ```
+                //
+                // `WeirdAndWacky` only has a single possible inhabitant: `None`!
+                // It is thus a singleton type.
+                // However, going out of our way to recognise it as such is probably not worth it.
+                // Such cases should anyway be exceedingly rare and/or contrived.
+                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`.
@@ -2112,7 +2209,7 @@ impl<'db> Type<'db> {
                 false
             }
             Type::DataclassDecorator(_) | Type::DataclassTransformer(_) => false,
-            Type::Instance(instance) => instance.is_singleton(db),
+            Type::NominalInstance(instance) => instance.is_singleton(db),
             Type::PropertyInstance(_) => false,
             Type::Tuple(..) => {
                 // The empty tuple is a singleton on CPython and PyPy, but not on other Python
@@ -2159,6 +2256,11 @@ impl<'db> Type<'db> {
             | Type::SliceLiteral(..)
             | Type::KnownInstance(..) => true,
 
+            Type::ProtocolInstance(..) => {
+                // See comment in the `Type::ProtocolInstance` branch for `Type::is_singleton`.
+                false
+            }
+
             // 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
@@ -2184,7 +2286,7 @@ impl<'db> Type<'db> {
                 .iter()
                 .all(|elem| elem.is_single_valued(db)),
 
-            Type::Instance(instance) => instance.is_single_valued(db),
+            Type::NominalInstance(instance) => instance.is_single_valued(db),
 
             Type::BoundSuper(_) => {
                 // At runtime two super instances never compare equal, even if their arguments are identical.
@@ -2322,10 +2424,11 @@ impl<'db> Type<'db> {
                 .to_class_literal(db)
                 .find_name_in_mro_with_policy(db, name, policy),
 
-            // We eagerly normalize type[object], i.e. Type::SubclassOf(object) to `type`, i.e. Type::Instance(type).
-            // So looking up a name in the MRO of `Type::Instance(type)` is equivalent to looking up the name in the
+            // We eagerly normalize type[object], i.e. Type::SubclassOf(object) to `type`,
+            // i.e. Type::NominalInstance(type). So looking up a name in the MRO of
+            // `Type::NominalInstance(type)` is equivalent to looking up the name in the
             // MRO of the class `object`.
-            Type::Instance(instance) if instance.class().is_known(db, KnownClass::Type) => {
+            Type::NominalInstance(instance) if instance.class().is_known(db, KnownClass::Type) => {
                 KnownClass::Object
                     .to_class_literal(db)
                     .find_name_in_mro_with_policy(db, name, policy)
@@ -2350,7 +2453,8 @@ impl<'db> Type<'db> {
             | Type::SliceLiteral(_)
             | Type::Tuple(_)
             | Type::TypeVar(_)
-            | Type::Instance(_)
+            | Type::NominalInstance(_)
+            | Type::ProtocolInstance(_)
             | Type::PropertyInstance(_) => None,
         }
     }
@@ -2415,7 +2519,18 @@ impl<'db> Type<'db> {
 
             Type::Dynamic(_) | Type::Never => Symbol::bound(self).into(),
 
-            Type::Instance(instance) => instance.class().instance_member(db, name),
+            Type::NominalInstance(instance) => instance.class().instance_member(db, name),
+
+            Type::ProtocolInstance(protocol) => match protocol.inner() {
+                Protocol::FromClass(class) => class.instance_member(db, name),
+                Protocol::Synthesized(synthesized) => {
+                    if synthesized.members(db).contains(name) {
+                        SymbolAndQualifiers::todo("Capture type of synthesized protocol members")
+                    } else {
+                        Symbol::Unbound.into()
+                    }
+                }
+            },
 
             Type::FunctionLiteral(_) => KnownClass::FunctionType
                 .to_instance(db)
@@ -2856,7 +2971,7 @@ impl<'db> Type<'db> {
                 .to_instance(db)
                 .member_lookup_with_policy(db, name, policy),
 
-            Type::Instance(instance)
+            Type::NominalInstance(instance)
                 if matches!(name.as_str(), "major" | "minor")
                     && instance.class().is_known(db, KnownClass::VersionInfo) =>
             {
@@ -2898,7 +3013,8 @@ impl<'db> Type<'db> {
                 policy,
             ),
 
-            Type::Instance(..)
+            Type::NominalInstance(..)
+            | Type::ProtocolInstance(..)
             | Type::BooleanLiteral(..)
             | Type::IntLiteral(..)
             | Type::StringLiteral(..)
@@ -2929,7 +3045,7 @@ impl<'db> Type<'db> {
                     // It will need a special handling, so it remember the origin type to properly
                     // resolve the attribute.
                     if matches!(
-                        self.into_instance()
+                        self.into_nominal_instance()
                             .and_then(|instance| instance.class().known(db)),
                         Some(KnownClass::ModuleType | KnownClass::GenericAlias)
                     ) {
@@ -3190,11 +3306,13 @@ impl<'db> Type<'db> {
                 }
             },
 
-            Type::Instance(instance) => match instance.class().known(db) {
+            Type::NominalInstance(instance) => match instance.class().known(db) {
                 Some(known_class) => known_class.bool(),
                 None => try_dunder_bool()?,
             },
 
+            Type::ProtocolInstance(_) => try_dunder_bool()?,
+
             Type::KnownInstance(known_instance) => known_instance.bool(),
 
             Type::PropertyInstance(_) => Truthiness::AlwaysTrue,
@@ -4006,7 +4124,7 @@ impl<'db> Type<'db> {
                 SubclassOfInner::Class(class) => Type::from(class).signatures(db),
             },
 
-            Type::Instance(_) => {
+            Type::NominalInstance(_) | Type::ProtocolInstance(_) => {
                 // Note that for objects that have a (possibly not callable!) `__call__` attribute,
                 // we will get the signature of the `__call__` attribute, but will pass in the type
                 // of the original object as the "callable type". That ensures that we get errors
@@ -4419,11 +4537,14 @@ impl<'db> Type<'db> {
                 };
                 let specialized = specialization
                     .map(|specialization| {
-                        Type::instance(ClassType::Generic(GenericAlias::new(
+                        Type::instance(
                             db,
-                            generic_origin,
-                            specialization,
-                        )))
+                            ClassType::Generic(GenericAlias::new(
+                                db,
+                                generic_origin,
+                                specialization,
+                            )),
+                        )
                     })
                     .unwrap_or(instance_ty);
                 Ok(specialized)
@@ -4454,9 +4575,9 @@ impl<'db> Type<'db> {
     pub fn to_instance(&self, db: &'db dyn Db) -> Option<Type<'db>> {
         match self {
             Type::Dynamic(_) | Type::Never => Some(*self),
-            Type::ClassLiteral(class) => Some(Type::instance(class.default_specialization(db))),
-            Type::GenericAlias(alias) => Some(Type::instance(ClassType::from(*alias))),
-            Type::SubclassOf(subclass_of_ty) => Some(subclass_of_ty.to_instance()),
+            Type::ClassLiteral(class) => Some(Type::instance(db, class.default_specialization(db))),
+            Type::GenericAlias(alias) => Some(Type::instance(db, ClassType::from(*alias))),
+            Type::SubclassOf(subclass_of_ty) => Some(subclass_of_ty.to_instance(db)),
             Type::Union(union) => {
                 let mut builder = UnionBuilder::new(db);
                 for element in union.elements(db) {
@@ -4474,7 +4595,8 @@ impl<'db> Type<'db> {
             | Type::WrapperDescriptor(_)
             | Type::DataclassDecorator(_)
             | Type::DataclassTransformer(_)
-            | Type::Instance(_)
+            | Type::NominalInstance(_)
+            | Type::ProtocolInstance(_)
             | Type::KnownInstance(_)
             | Type::PropertyInstance(_)
             | Type::ModuleLiteral(_)
@@ -4494,7 +4616,7 @@ impl<'db> Type<'db> {
     ///
     /// For example, the builtin `int` as a value expression is of type
     /// `Type::ClassLiteral(builtins.int)`, that is, it is the `int` class itself. As a type
-    /// expression, it names the type `Type::Instance(builtins.int)`, that is, all objects whose
+    /// expression, it names the type `Type::NominalInstance(builtins.int)`, that is, all objects whose
     /// `__class__` is `int`.
     pub fn in_type_expression(
         &self,
@@ -4521,11 +4643,11 @@ impl<'db> Type<'db> {
                             KnownClass::Float.to_instance(db),
                         ],
                     ),
-                    _ => Type::instance(class.default_specialization(db)),
+                    _ => Type::instance(db, class.default_specialization(db)),
                 };
                 Ok(ty)
             }
-            Type::GenericAlias(alias) => Ok(Type::instance(ClassType::from(*alias))),
+            Type::GenericAlias(alias) => Ok(Type::instance(db, ClassType::from(*alias))),
 
             Type::SubclassOf(_)
             | Type::BooleanLiteral(_)
@@ -4548,6 +4670,7 @@ impl<'db> Type<'db> {
             | Type::Never
             | Type::FunctionLiteral(_)
             | Type::BoundSuper(_)
+            | Type::ProtocolInstance(_)
             | Type::PropertyInstance(_) => Err(InvalidTypeExpressionError {
                 invalid_expressions: smallvec::smallvec![InvalidTypeExpression::InvalidType(*self)],
                 fallback_type: Type::unknown(),
@@ -4672,7 +4795,7 @@ impl<'db> Type<'db> {
 
             Type::Dynamic(_) => Ok(*self),
 
-            Type::Instance(instance) => match instance.class().known(db) {
+            Type::NominalInstance(instance) => match instance.class().known(db) {
                 Some(KnownClass::TypeVar) => Ok(todo_type!(
                     "Support for `typing.TypeVar` instances in type expressions"
                 )),
@@ -4748,7 +4871,7 @@ impl<'db> Type<'db> {
     pub fn to_meta_type(&self, db: &'db dyn Db) -> Type<'db> {
         match self {
             Type::Never => Type::Never,
-            Type::Instance(instance) => instance.to_meta_type(db),
+            Type::NominalInstance(instance) => instance.to_meta_type(db),
             Type::KnownInstance(known_instance) => known_instance.to_meta_type(db),
             Type::PropertyInstance(_) => KnownClass::Property.to_class_literal(db),
             Type::Union(union) => union.map(db, |ty| ty.to_meta_type(db)),
@@ -4796,6 +4919,7 @@ impl<'db> Type<'db> {
             ),
             Type::AlwaysTruthy | Type::AlwaysFalsy => KnownClass::Type.to_instance(db),
             Type::BoundSuper(_) => KnownClass::Super.to_class_literal(db),
+            Type::ProtocolInstance(protocol) => protocol.to_meta_type(db),
         }
     }
 
@@ -4917,9 +5041,11 @@ impl<'db> Type<'db> {
             | Type::BytesLiteral(_)
             | Type::SliceLiteral(_)
             | Type::BoundSuper(_)
-            // Instance contains a ClassType, which has already been specialized if needed, like
-            // above with BoundMethod's self_instance.
-            | Type::Instance(_)
+            // `NominalInstance` contains a ClassType, which has already been specialized if needed,
+            // like above with BoundMethod's self_instance.
+            | Type::NominalInstance(_)
+            // Same for `ProtocolInstance`
+            | Type::ProtocolInstance(_)
             | Type::KnownInstance(_) => self,
         }
     }
@@ -5006,7 +5132,8 @@ impl<'db> Type<'db> {
             | Type::BytesLiteral(_)
             | Type::SliceLiteral(_)
             | Type::BoundSuper(_)
-            | Type::Instance(_)
+            | Type::NominalInstance(_)
+            | Type::ProtocolInstance(_)
             | Type::KnownInstance(_) => {}
         }
     }
@@ -5066,7 +5193,7 @@ impl<'db> Type<'db> {
                 Some(TypeDefinition::Class(class_literal.definition(db)))
             }
             Self::GenericAlias(alias) => Some(TypeDefinition::Class(alias.definition(db))),
-            Self::Instance(instance) => {
+            Self::NominalInstance(instance) => {
                 Some(TypeDefinition::Class(instance.class().definition(db)))
             }
             Self::KnownInstance(instance) => match instance {
@@ -5100,6 +5227,11 @@ impl<'db> Type<'db> {
 
             Self::TypeVar(var) => Some(TypeDefinition::TypeVar(var.definition(db))),
 
+            Self::ProtocolInstance(protocol) => match protocol.inner() {
+                Protocol::FromClass(class) => Some(TypeDefinition::Class(class.definition(db))),
+                Protocol::Synthesized(_) => None,
+            },
+
             Self::Union(_) | Self::Intersection(_) => None,
 
             // These types have no definition
@@ -7761,7 +7893,7 @@ impl BoundSuperError<'_> {
 pub enum SuperOwnerKind<'db> {
     Dynamic(DynamicType),
     Class(ClassType<'db>),
-    Instance(InstanceType<'db>),
+    Instance(NominalInstanceType<'db>),
 }
 
 impl<'db> SuperOwnerKind<'db> {
@@ -7795,7 +7927,7 @@ impl<'db> SuperOwnerKind<'db> {
             Type::ClassLiteral(class_literal) => Some(SuperOwnerKind::Class(
                 class_literal.apply_optional_specialization(db, None),
             )),
-            Type::Instance(instance) => Some(SuperOwnerKind::Instance(instance)),
+            Type::NominalInstance(instance) => Some(SuperOwnerKind::Instance(instance)),
             Type::BooleanLiteral(_) => {
                 SuperOwnerKind::try_from_type(db, KnownClass::Bool.to_instance(db))
             }
diff --git a/crates/red_knot_python_semantic/src/types/builder.rs b/crates/red_knot_python_semantic/src/types/builder.rs
index 8f81db8d3f6dc1..3efbd2db0a93d4 100644
--- a/crates/red_knot_python_semantic/src/types/builder.rs
+++ b/crates/red_knot_python_semantic/src/types/builder.rs
@@ -591,7 +591,7 @@ impl<'db> InnerIntersectionBuilder<'db> {
             }
             _ => {
                 let known_instance = new_positive
-                    .into_instance()
+                    .into_nominal_instance()
                     .and_then(|instance| instance.class().known(db));
 
                 if known_instance == Some(KnownClass::Object) {
@@ -611,7 +611,7 @@ impl<'db> InnerIntersectionBuilder<'db> {
                         Type::AlwaysFalsy if addition_is_bool_instance => {
                             new_positive = Type::BooleanLiteral(false);
                         }
-                        Type::Instance(instance)
+                        Type::NominalInstance(instance)
                             if instance.class().is_known(db, KnownClass::Bool) =>
                         {
                             match new_positive {
@@ -705,7 +705,7 @@ impl<'db> InnerIntersectionBuilder<'db> {
         let contains_bool = || {
             self.positive
                 .iter()
-                .filter_map(|ty| ty.into_instance())
+                .filter_map(|ty| ty.into_nominal_instance())
                 .filter_map(|instance| instance.class().known(db))
                 .any(KnownClass::is_bool)
         };
@@ -722,7 +722,7 @@ impl<'db> InnerIntersectionBuilder<'db> {
             Type::Never => {
                 // Adding ~Never to an intersection is a no-op.
             }
-            Type::Instance(instance) if instance.class().is_object(db) => {
+            Type::NominalInstance(instance) if instance.class().is_object(db) => {
                 // Adding ~object to an intersection results in Never.
                 *self = Self::default();
                 self.positive.insert(Type::Never);
diff --git a/crates/red_knot_python_semantic/src/types/class.rs b/crates/red_knot_python_semantic/src/types/class.rs
index 0a4870447550ed..a2ccc66e8d3e5a 100644
--- a/crates/red_knot_python_semantic/src/types/class.rs
+++ b/crates/red_knot_python_semantic/src/types/class.rs
@@ -533,14 +533,33 @@ impl<'db> ClassLiteral<'db> {
     }
 
     /// Determine if this class is a protocol.
+    ///
+    /// This method relies on the accuracy of the [`KnownClass::is_protocol`] method,
+    /// which hardcodes knowledge about certain special-cased classes. See the docs on
+    /// that method for why we do this rather than relying on generalised logic for all
+    /// classes, including the special-cased ones that are included in the [`KnownClass`]
+    /// enum.
     pub(super) fn is_protocol(self, db: &'db dyn Db) -> bool {
-        self.explicit_bases(db).iter().rev().take(3).any(|base| {
-            matches!(
-                base,
-                Type::KnownInstance(KnownInstanceType::Protocol)
-                    | Type::Dynamic(DynamicType::SubscriptedProtocol)
-            )
-        })
+        self.known(db)
+            .map(KnownClass::is_protocol)
+            .unwrap_or_else(|| {
+                // Iterate through the last three bases of the class
+                // searching for `Protocol` or `Protocol[]` in the bases list.
+                //
+                // If `Protocol` is present in the bases list of a valid protocol class, it must either:
+                //
+                // - be the last base
+                // - OR be the last-but-one base (with the final base being `Generic[]` or `object`)
+                // - OR be the last-but-two base (with the penultimate base being `Generic[]`
+                //                                and the final base being `object`)
+                self.explicit_bases(db).iter().rev().take(3).any(|base| {
+                    matches!(
+                        base,
+                        Type::KnownInstance(KnownInstanceType::Protocol)
+                            | Type::Dynamic(DynamicType::SubscriptedProtocol)
+                    )
+                })
+            })
     }
 
     /// Return the types of the decorators on this class
@@ -1076,6 +1095,7 @@ impl<'db> ClassLiteral<'db> {
                     Parameters::new([Parameter::positional_or_keyword(Name::new_static("other"))
                         // TODO: could be `Self`.
                         .with_annotated_type(Type::instance(
+                            db,
                             self.apply_optional_specialization(db, specialization),
                         ))]),
                     Some(KnownClass::Bool.to_instance(db)),
@@ -1711,7 +1731,7 @@ impl<'db> ProtocolClassLiteral<'db> {
     /// It is illegal for a protocol class to have any instance attributes that are not declared
     /// in the protocol's class body. If any are assigned to, they are not taken into account in
     /// the protocol's list of members.
-    pub(super) fn protocol_members(self, db: &'db dyn Db) -> &'db ordermap::set::Slice<Name> {
+    pub(super) fn protocol_members(self, db: &'db dyn Db) -> &'db FxOrderSet<Name> {
         /// The list of excluded members is subject to change between Python versions,
         /// especially for dunders, but it probably doesn't matter *too* much if this
         /// list goes out of date. It's up to date as of Python commit 87b1ea016b1454b1e83b9113fa9435849b7743aa
@@ -1748,11 +1768,11 @@ impl<'db> ProtocolClassLiteral<'db> {
             )
         }
 
-        #[salsa::tracked(return_ref)]
+        #[salsa::tracked(return_ref, cycle_fn=proto_members_cycle_recover, cycle_initial=proto_members_cycle_initial)]
         fn cached_protocol_members<'db>(
             db: &'db dyn Db,
             class: ClassLiteral<'db>,
-        ) -> Box<ordermap::set::Slice<Name>> {
+        ) -> FxOrderSet<Name> {
             let mut members = FxOrderSet::default();
 
             for parent_protocol in class
@@ -1796,9 +1816,24 @@ impl<'db> ProtocolClassLiteral<'db> {
             }
 
             members.sort();
-            members.into_boxed_slice()
+            members.shrink_to_fit();
+            members
         }
 
+        fn proto_members_cycle_recover(
+            _db: &dyn Db,
+            _value: &FxOrderSet<Name>,
+            _count: u32,
+            _class: ClassLiteral,
+        ) -> salsa::CycleRecoveryAction<FxOrderSet<Name>> {
+            salsa::CycleRecoveryAction::Iterate
+        }
+
+        fn proto_members_cycle_initial(_db: &dyn Db, _class: ClassLiteral) -> FxOrderSet<Name> {
+            FxOrderSet::default()
+        }
+
+        let _span = tracing::trace_span!("protocol_members", "class='{}'", self.name(db)).entered();
         cached_protocol_members(db, *self)
     }
 
@@ -1892,8 +1927,6 @@ pub enum KnownClass {
     TypeAliasType,
     NoDefaultType,
     NewType,
-    Sized,
-    // TODO: This can probably be removed when we have support for protocols
     SupportsIndex,
     // Collections
     ChainMap,
@@ -1977,7 +2010,6 @@ impl<'db> KnownClass {
             | Self::DefaultDict
             | Self::Deque
             | Self::Float
-            | Self::Sized
             | Self::Enum
             | Self::ABCMeta
             // Evaluating `NotImplementedType` in a boolean context was deprecated in Python 3.9
@@ -1988,6 +2020,75 @@ impl<'db> KnownClass {
         }
     }
 
+    /// Return `true` if this class is a protocol class.
+    ///
+    /// In an ideal world, perhaps we wouldn't hardcode this knowledge here;
+    /// instead, we'd just look at the bases for these classes, as we do for
+    /// all other classes. However, the special casing here helps us out in
+    /// two important ways:
+    ///
+    /// 1. It helps us avoid Salsa cycles when creating types such as "instance of `str`"
+    ///    and "instance of `sys._version_info`". These types are constructed very early
+    ///    on, but it causes problems if we attempt to infer the types of their bases
+    ///    too soon.
+    /// 2. It's probably more performant.
+    const fn is_protocol(self) -> bool {
+        match self {
+            Self::SupportsIndex => true,
+
+            Self::Any
+            | Self::Bool
+            | Self::Object
+            | Self::Bytes
+            | Self::Bytearray
+            | Self::Tuple
+            | Self::Int
+            | Self::Float
+            | Self::Complex
+            | Self::FrozenSet
+            | Self::Str
+            | Self::Set
+            | Self::Dict
+            | Self::List
+            | Self::Type
+            | Self::Slice
+            | Self::Range
+            | Self::Property
+            | Self::BaseException
+            | Self::BaseExceptionGroup
+            | Self::Classmethod
+            | Self::GenericAlias
+            | Self::ModuleType
+            | Self::FunctionType
+            | Self::MethodType
+            | Self::MethodWrapperType
+            | Self::WrapperDescriptorType
+            | Self::NoneType
+            | Self::SpecialForm
+            | Self::TypeVar
+            | Self::ParamSpec
+            | Self::ParamSpecArgs
+            | Self::ParamSpecKwargs
+            | Self::TypeVarTuple
+            | Self::TypeAliasType
+            | Self::NoDefaultType
+            | Self::NewType
+            | Self::ChainMap
+            | Self::Counter
+            | Self::DefaultDict
+            | Self::Deque
+            | Self::OrderedDict
+            | Self::Enum
+            | Self::ABCMeta
+            | Self::Super
+            | Self::StdlibAlias
+            | Self::VersionInfo
+            | Self::EllipsisType
+            | Self::NotImplementedType
+            | Self::UnionType => false,
+        }
+    }
+
     pub(crate) fn name(self, db: &'db dyn Db) -> &'static str {
         match self {
             Self::Any => "Any",
@@ -2033,7 +2134,6 @@ impl<'db> KnownClass {
             Self::Counter => "Counter",
             Self::DefaultDict => "defaultdict",
             Self::Deque => "deque",
-            Self::Sized => "Sized",
             Self::OrderedDict => "OrderedDict",
             Self::Enum => "Enum",
             Self::ABCMeta => "ABCMeta",
@@ -2090,7 +2190,7 @@ impl<'db> KnownClass {
     pub(crate) fn to_instance(self, db: &'db dyn Db) -> Type<'db> {
         self.to_class_literal(db)
             .to_class_type(db)
-            .map(Type::instance)
+            .map(|class| Type::instance(db, class))
             .unwrap_or_else(Type::unknown)
     }
 
@@ -2207,8 +2307,7 @@ impl<'db> KnownClass {
             | Self::SpecialForm
             | Self::TypeVar
             | Self::StdlibAlias
-            | Self::SupportsIndex
-            | Self::Sized => KnownModule::Typing,
+            | Self::SupportsIndex => KnownModule::Typing,
             Self::TypeAliasType
             | Self::TypeVarTuple
             | Self::ParamSpec
@@ -2296,7 +2395,6 @@ impl<'db> KnownClass {
             | Self::ParamSpecArgs
             | Self::ParamSpecKwargs
             | Self::TypeVarTuple
-            | Self::Sized
             | Self::Enum
             | Self::ABCMeta
             | Self::Super
@@ -2356,7 +2454,6 @@ impl<'db> KnownClass {
             | Self::ParamSpecArgs
             | Self::ParamSpecKwargs
             | Self::TypeVarTuple
-            | Self::Sized
             | Self::Enum
             | Self::ABCMeta
             | Self::Super
@@ -2418,7 +2515,6 @@ impl<'db> KnownClass {
             "_SpecialForm" => Self::SpecialForm,
             "_NoDefaultType" => Self::NoDefaultType,
             "SupportsIndex" => Self::SupportsIndex,
-            "Sized" => Self::Sized,
             "Enum" => Self::Enum,
             "ABCMeta" => Self::ABCMeta,
             "super" => Self::Super,
@@ -2491,7 +2587,6 @@ impl<'db> KnownClass {
             | Self::ParamSpecArgs
             | Self::ParamSpecKwargs
             | Self::TypeVarTuple
-            | Self::Sized
             | Self::NewType => matches!(module, KnownModule::Typing | KnownModule::TypingExtensions),
         }
     }
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 9f480ed07eaf05..50ab0a9d78c2a5 100644
--- a/crates/red_knot_python_semantic/src/types/class_base.rs
+++ b/crates/red_knot_python_semantic/src/types/class_base.rs
@@ -78,12 +78,14 @@ impl<'db> ClassBase<'db> {
                 Self::Class(literal.default_specialization(db))
             }),
             Type::GenericAlias(generic) => Some(Self::Class(ClassType::Generic(generic))),
-            Type::Instance(instance) if instance.class().is_known(db, KnownClass::GenericAlias) => {
+            Type::NominalInstance(instance)
+                if instance.class().is_known(db, KnownClass::GenericAlias) =>
+            {
                 Self::try_from_type(db, todo_type!("GenericAlias instance"))
             }
             Type::Union(_) => None, // TODO -- forces consideration of multiple possible MROs?
             Type::Intersection(_) => None, // TODO -- probably incorrect?
-            Type::Instance(_) => None, // TODO -- handle `__mro_entries__`?
+            Type::NominalInstance(_) => None, // TODO -- handle `__mro_entries__`?
             Type::PropertyInstance(_) => None,
             Type::Never
             | Type::BooleanLiteral(_)
@@ -104,6 +106,7 @@ impl<'db> ClassBase<'db> {
             | Type::SubclassOf(_)
             | Type::TypeVar(_)
             | Type::BoundSuper(_)
+            | Type::ProtocolInstance(_)
             | 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 2633938ae9285f..c878a81539fc30 100644
--- a/crates/red_knot_python_semantic/src/types/display.rs
+++ b/crates/red_knot_python_semantic/src/types/display.rs
@@ -10,15 +10,13 @@ use crate::types::class::{ClassLiteral, ClassType, GenericAlias};
 use crate::types::generics::{GenericContext, Specialization};
 use crate::types::signatures::{Parameter, Parameters, Signature};
 use crate::types::{
-    FunctionSignature, IntersectionType, KnownClass, MethodWrapperKind, StringLiteralType,
-    SubclassOfInner, Type, TypeVarBoundOrConstraints, TypeVarInstance, UnionType,
-    WrapperDescriptorKind,
+    CallableType, FunctionSignature, IntersectionType, KnownClass, MethodWrapperKind, Protocol,
+    StringLiteralType, SubclassOfInner, Type, TypeVarBoundOrConstraints, TypeVarInstance,
+    UnionType, WrapperDescriptorKind,
 };
 use crate::Db;
 use rustc_hash::FxHashMap;
 
-use super::CallableType;
-
 impl<'db> Type<'db> {
     pub fn display(&self, db: &'db dyn Db) -> DisplayType {
         DisplayType { ty: self, db }
@@ -73,11 +71,32 @@ impl Display for DisplayRepresentation<'_> {
         match self.ty {
             Type::Dynamic(dynamic) => dynamic.fmt(f),
             Type::Never => f.write_str("Never"),
-            Type::Instance(instance) => match (instance.class(), instance.class().known(self.db)) {
-                (_, Some(KnownClass::NoneType)) => f.write_str("None"),
-                (_, Some(KnownClass::NoDefaultType)) => f.write_str("NoDefault"),
-                (ClassType::NonGeneric(class), _) => f.write_str(class.name(self.db)),
-                (ClassType::Generic(alias), _) => write!(f, "{}", alias.display(self.db)),
+            Type::NominalInstance(instance) => {
+                match (instance.class(), instance.class().known(self.db)) {
+                    (_, Some(KnownClass::NoneType)) => f.write_str("None"),
+                    (_, Some(KnownClass::NoDefaultType)) => f.write_str("NoDefault"),
+                    (ClassType::NonGeneric(class), _) => f.write_str(class.name(self.db)),
+                    (ClassType::Generic(alias), _) => write!(f, "{}", alias.display(self.db)),
+                }
+            }
+            Type::ProtocolInstance(protocol) => match protocol.inner() {
+                Protocol::FromClass(ClassType::NonGeneric(class)) => {
+                    f.write_str(class.name(self.db))
+                }
+                Protocol::FromClass(ClassType::Generic(alias)) => alias.display(self.db).fmt(f),
+                Protocol::Synthesized(synthetic) => {
+                    f.write_str("<Protocol with members ")?;
+                    let member_list = synthetic.members(self.db);
+                    let num_members = member_list.len();
+                    for (i, member) in member_list.iter().enumerate() {
+                        let is_last = i == num_members - 1;
+                        write!(f, "'{member}'")?;
+                        if !is_last {
+                            f.write_str(", ")?;
+                        }
+                    }
+                    f.write_char('>')
+                }
             },
             Type::PropertyInstance(_) => f.write_str("property"),
             Type::ModuleLiteral(module) => {
@@ -761,6 +780,7 @@ mod tests {
     use ruff_python_ast::name::Name;
 
     use crate::db::tests::setup_db;
+    use crate::symbol::typing_extensions_symbol;
     use crate::types::{
         KnownClass, Parameter, Parameters, Signature, SliceLiteralType, StringLiteralType, Type,
     };
@@ -832,6 +852,31 @@ mod tests {
         );
     }
 
+    #[test]
+    fn synthesized_protocol_display() {
+        let db = setup_db();
+
+        // Call `.normalized()` to turn the class-based protocol into a nameless synthesized one.
+        let supports_index_synthesized = KnownClass::SupportsIndex.to_instance(&db).normalized(&db);
+        assert_eq!(
+            supports_index_synthesized.display(&db).to_string(),
+            "<Protocol with members '__index__'>"
+        );
+
+        let iterator_synthesized = typing_extensions_symbol(&db, "Iterator")
+            .symbol
+            .ignore_possibly_unbound()
+            .unwrap()
+            .to_instance(&db)
+            .unwrap()
+            .normalized(&db); // Call `.normalized()` to turn the class-based protocol into a nameless synthesized one.
+
+        assert_eq!(
+            iterator_synthesized.display(&db).to_string(),
+            "<Protocol with members '__iter__', '__next__'>"
+        );
+    }
+
     fn display_signature<'db>(
         db: &dyn Db,
         parameters: impl IntoIterator<Item = Parameter<'db>>,
diff --git a/crates/red_knot_python_semantic/src/types/infer.rs b/crates/red_knot_python_semantic/src/types/infer.rs
index 6016308878674b..2e275e99924bde 100644
--- a/crates/red_knot_python_semantic/src/types/infer.rs
+++ b/crates/red_knot_python_semantic/src/types/infer.rs
@@ -1065,7 +1065,7 @@ impl<'db> TypeInferenceBuilder<'db> {
     ) -> bool {
         match left {
             Type::BooleanLiteral(_) | Type::IntLiteral(_) => {}
-            Type::Instance(instance)
+            Type::NominalInstance(instance)
                 if matches!(
                     instance.class().known(self.db()),
                     Some(KnownClass::Float | KnownClass::Int | KnownClass::Bool)
@@ -2517,7 +2517,7 @@ impl<'db> TypeInferenceBuilder<'db> {
             }
 
             // Super instances do not allow attribute assignment
-            Type::Instance(instance) if instance.class().is_known(db, KnownClass::Super) => {
+            Type::NominalInstance(instance) if instance.class().is_known(db, KnownClass::Super) => {
                 if emit_diagnostics {
                     if let Some(builder) = self.context.report_lint(&INVALID_ASSIGNMENT, target) {
                         builder.into_diagnostic(format_args!(
@@ -2542,7 +2542,8 @@ impl<'db> TypeInferenceBuilder<'db> {
 
             Type::Dynamic(..) | Type::Never => true,
 
-            Type::Instance(..)
+            Type::NominalInstance(..)
+            | Type::ProtocolInstance(_)
             | Type::BooleanLiteral(..)
             | Type::IntLiteral(..)
             | Type::StringLiteral(..)
@@ -3033,7 +3034,7 @@ impl<'db> TypeInferenceBuilder<'db> {
         }
 
         // Handle various singletons.
-        if let Type::Instance(instance) = declared_ty.inner_type() {
+        if let Type::NominalInstance(instance) = declared_ty.inner_type() {
             if instance
                 .class()
                 .is_known(self.db(), KnownClass::SpecialForm)
@@ -5125,7 +5126,8 @@ impl<'db> TypeInferenceBuilder<'db> {
                 | Type::ClassLiteral(_)
                 | Type::GenericAlias(_)
                 | Type::SubclassOf(_)
-                | Type::Instance(_)
+                | Type::NominalInstance(_)
+                | Type::ProtocolInstance(_)
                 | Type::KnownInstance(_)
                 | Type::PropertyInstance(_)
                 | Type::Union(_)
@@ -5405,7 +5407,8 @@ impl<'db> TypeInferenceBuilder<'db> {
                 | Type::ClassLiteral(_)
                 | Type::GenericAlias(_)
                 | Type::SubclassOf(_)
-                | Type::Instance(_)
+                | Type::NominalInstance(_)
+                | Type::ProtocolInstance(_)
                 | Type::KnownInstance(_)
                 | Type::PropertyInstance(_)
                 | Type::Intersection(_)
@@ -5430,7 +5433,8 @@ impl<'db> TypeInferenceBuilder<'db> {
                 | Type::ClassLiteral(_)
                 | Type::GenericAlias(_)
                 | Type::SubclassOf(_)
-                | Type::Instance(_)
+                | Type::NominalInstance(_)
+                | Type::ProtocolInstance(_)
                 | Type::KnownInstance(_)
                 | Type::PropertyInstance(_)
                 | Type::Intersection(_)
@@ -5863,13 +5867,13 @@ impl<'db> TypeInferenceBuilder<'db> {
                     right_ty: right,
                 }),
             },
-            (Type::IntLiteral(_), Type::Instance(_)) => self.infer_binary_type_comparison(
+            (Type::IntLiteral(_), Type::NominalInstance(_)) => self.infer_binary_type_comparison(
                 KnownClass::Int.to_instance(self.db()),
                 op,
                 right,
                 range,
             ),
-            (Type::Instance(_), Type::IntLiteral(_)) => self.infer_binary_type_comparison(
+            (Type::NominalInstance(_), Type::IntLiteral(_)) => self.infer_binary_type_comparison(
                 left,
                 op,
                 KnownClass::Int.to_instance(self.db()),
@@ -5995,7 +5999,7 @@ impl<'db> TypeInferenceBuilder<'db> {
                 KnownClass::Bytes.to_instance(self.db()),
                 range,
             ),
-            (Type::Tuple(_), Type::Instance(instance))
+            (Type::Tuple(_), Type::NominalInstance(instance))
                 if instance
                     .class()
                     .is_known(self.db(), KnownClass::VersionInfo) =>
@@ -6007,7 +6011,7 @@ impl<'db> TypeInferenceBuilder<'db> {
                     range,
                 )
             }
-            (Type::Instance(instance), Type::Tuple(_))
+            (Type::NominalInstance(instance), Type::Tuple(_))
                 if instance
                     .class()
                     .is_known(self.db(), KnownClass::VersionInfo) =>
@@ -6393,7 +6397,7 @@ impl<'db> TypeInferenceBuilder<'db> {
     ) -> Type<'db> {
         match (value_ty, slice_ty) {
             (
-                Type::Instance(instance),
+                Type::NominalInstance(instance),
                 Type::IntLiteral(_) | Type::BooleanLiteral(_) | Type::SliceLiteral(_),
             ) if instance
                 .class()
@@ -6699,7 +6703,7 @@ impl<'db> TypeInferenceBuilder<'db> {
                 Err(_) => SliceArg::Unsupported,
             },
             Some(Type::BooleanLiteral(b)) => SliceArg::Arg(Some(i32::from(b))),
-            Some(Type::Instance(instance))
+            Some(Type::NominalInstance(instance))
                 if instance.class().is_known(self.db(), KnownClass::NoneType) =>
             {
                 SliceArg::Arg(None)
diff --git a/crates/red_knot_python_semantic/src/types/instance.rs b/crates/red_knot_python_semantic/src/types/instance.rs
index fb1b1deb764a4f..cfd6912597abc3 100644
--- a/crates/red_knot_python_semantic/src/types/instance.rs
+++ b/crates/red_knot_python_semantic/src/types/instance.rs
@@ -1,30 +1,54 @@
 //! Instance types: both nominal and structural.
 
+use ruff_python_ast::name::Name;
+
 use super::{ClassType, KnownClass, SubclassOfType, Type};
-use crate::Db;
+use crate::{Db, FxOrderSet};
 
 impl<'db> Type<'db> {
-    pub(crate) const fn instance(class: ClassType<'db>) -> Self {
-        Self::Instance(InstanceType { class })
+    pub(crate) fn instance(db: &'db dyn Db, class: ClassType<'db>) -> Self {
+        if class.class_literal(db).0.is_protocol(db) {
+            Self::ProtocolInstance(ProtocolInstanceType(Protocol::FromClass(class)))
+        } else {
+            Self::NominalInstance(NominalInstanceType { class })
+        }
     }
 
-    pub(crate) const fn into_instance(self) -> Option<InstanceType<'db>> {
+    pub(crate) const fn into_nominal_instance(self) -> Option<NominalInstanceType<'db>> {
         match self {
-            Type::Instance(instance_type) => Some(instance_type),
+            Type::NominalInstance(instance_type) => Some(instance_type),
             _ => None,
         }
     }
+
+    /// Return `true` if `self` conforms to the interface described by `protocol`.
+    ///
+    /// TODO: we may need to split this into two methods in the future, once we start
+    /// differentiating between fully-static and non-fully-static protocols.
+    pub(super) fn satisfies_protocol(
+        self,
+        db: &'db dyn Db,
+        protocol: ProtocolInstanceType<'db>,
+    ) -> bool {
+        // TODO: this should consider the types of the protocol members
+        // as well as whether each member *exists* on `self`.
+        protocol
+            .0
+            .protocol_members(db)
+            .iter()
+            .all(|member| !self.member(db, member).symbol.is_unbound())
+    }
 }
 
 /// A type representing the set of runtime objects which are instances of a certain nominal class.
 #[derive(Copy, Clone, Debug, Eq, PartialEq, Hash, salsa::Update)]
-pub struct InstanceType<'db> {
-    // Keep this field private, so that the only way of constructing `InstanceType` instances
+pub struct NominalInstanceType<'db> {
+    // Keep this field private, so that the only way of constructing `NominalInstanceType` instances
     // is through the `Type::instance` constructor function.
     class: ClassType<'db>,
 }
 
-impl<'db> InstanceType<'db> {
+impl<'db> NominalInstanceType<'db> {
     pub(super) fn class(self) -> ClassType<'db> {
         self.class
     }
@@ -87,8 +111,152 @@ impl<'db> InstanceType<'db> {
     }
 }
 
-impl<'db> From<InstanceType<'db>> for Type<'db> {
-    fn from(value: InstanceType<'db>) -> Self {
-        Self::Instance(value)
+impl<'db> From<NominalInstanceType<'db>> for Type<'db> {
+    fn from(value: NominalInstanceType<'db>) -> Self {
+        Self::NominalInstance(value)
+    }
+}
+
+/// A `ProtocolInstanceType` represents the set of all possible runtime objects
+/// that conform to the interface described by a certain protocol.
+#[derive(Copy, Clone, Debug, Eq, PartialEq, Hash, PartialOrd, Ord, salsa::Update)]
+pub struct ProtocolInstanceType<'db>(
+    // Keep the inner field here private,
+    // so that the only way of constructing `ProtocolInstanceType` instances
+    // is through the `Type::instance` constructor function.
+    Protocol<'db>,
+);
+
+impl<'db> ProtocolInstanceType<'db> {
+    pub(super) fn inner(self) -> Protocol<'db> {
+        self.0
     }
+
+    /// Return the meta-type of this protocol-instance type.
+    pub(super) fn to_meta_type(self, db: &'db dyn Db) -> Type<'db> {
+        match self.0 {
+            Protocol::FromClass(class) => SubclassOfType::from(db, class),
+
+            // TODO: we can and should do better here.
+            //
+            // This is supported by mypy, and should be supported by us as well.
+            // We'll need to come up with a better solution for the meta-type of
+            // synthesized protocols to solve this:
+            //
+            // ```py
+            // from typing import Callable
+            //
+            // def foo(x: Callable[[], int]) -> None:
+            //     reveal_type(type(x))                 # mypy: "type[def (builtins.int) -> builtins.str]"
+            //     reveal_type(type(x).__call__)        # mypy: "def (*args: Any, **kwds: Any) -> Any"
+            // ```
+            Protocol::Synthesized(_) => KnownClass::Type.to_instance(db),
+        }
+    }
+
+    /// Return a "normalized" version of this `Protocol` type.
+    ///
+    /// See [`Type::normalized`] for more details.
+    pub(super) fn normalized(self, db: &'db dyn Db) -> Type<'db> {
+        let object = KnownClass::Object.to_instance(db);
+        if object.satisfies_protocol(db, self) {
+            return object;
+        }
+        match self.0 {
+            Protocol::FromClass(_) => Type::ProtocolInstance(Self(Protocol::Synthesized(
+                SynthesizedProtocolType::new(db, self.0.protocol_members(db)),
+            ))),
+            Protocol::Synthesized(_) => Type::ProtocolInstance(self),
+        }
+    }
+
+    /// TODO: this should return `true` if any of the members of this protocol type contain any `Todo` types.
+    #[expect(clippy::unused_self)]
+    pub(super) fn contains_todo(self) -> bool {
+        false
+    }
+
+    /// Return `true` if this protocol type is fully static.
+    ///
+    /// TODO: should not be considered fully static if any members do not have fully static types
+    #[expect(clippy::unused_self)]
+    pub(super) fn is_fully_static(self) -> bool {
+        true
+    }
+
+    /// Return `true` if this protocol type is a subtype of the protocol `other`.
+    ///
+    /// TODO: consider the types of the members as well as their existence
+    pub(super) fn is_subtype_of(self, db: &'db dyn Db, other: Self) -> bool {
+        self.0
+            .protocol_members(db)
+            .is_superset(other.0.protocol_members(db))
+    }
+
+    /// Return `true` if this protocol type is assignable to the protocol `other`.
+    ///
+    /// TODO: consider the types of the members as well as their existence
+    pub(super) fn is_assignable_to(self, db: &'db dyn Db, other: Self) -> bool {
+        self.is_subtype_of(db, other)
+    }
+
+    /// Return `true` if this protocol type is equivalent to the protocol `other`.
+    ///
+    /// TODO: consider the types of the members as well as their existence
+    pub(super) fn is_equivalent_to(self, db: &'db dyn Db, other: Self) -> bool {
+        self.normalized(db) == other.normalized(db)
+    }
+
+    /// Return `true` if this protocol type is gradually equivalent to the protocol `other`.
+    ///
+    /// TODO: consider the types of the members as well as their existence
+    pub(super) fn is_gradual_equivalent_to(self, db: &'db dyn Db, other: Self) -> bool {
+        self.is_equivalent_to(db, other)
+    }
+
+    /// Return `true` if this protocol type is disjoint from the protocol `other`.
+    ///
+    /// TODO: a protocol `X` is disjoint from a protocol `Y` if `X` and `Y`
+    /// have a member with the same name but disjoint types
+    #[expect(clippy::unused_self)]
+    pub(super) fn is_disjoint_from(self, _db: &'db dyn Db, _other: Self) -> bool {
+        false
+    }
+}
+
+/// An enumeration of the two kinds of protocol types: those that originate from a class
+/// definition in source code, and those that are synthesized from a set of members.
+#[derive(
+    Copy, Clone, Debug, Eq, PartialEq, Hash, salsa::Update, salsa::Supertype, PartialOrd, Ord,
+)]
+pub(super) enum Protocol<'db> {
+    FromClass(ClassType<'db>),
+    Synthesized(SynthesizedProtocolType<'db>),
+}
+
+impl<'db> Protocol<'db> {
+    /// Return the members of this protocol type
+    fn protocol_members(self, db: &'db dyn Db) -> &'db FxOrderSet<Name> {
+        match self {
+            Self::FromClass(class) => class
+                .class_literal(db)
+                .0
+                .into_protocol_class(db)
+                .expect("Protocol class literal should be a protocol class")
+                .protocol_members(db),
+            Self::Synthesized(synthesized) => synthesized.members(db),
+        }
+    }
+}
+
+/// A "synthesized" protocol type that is dissociated from a class definition in source code.
+///
+/// Two synthesized protocol types with the same members will share the same Salsa ID,
+/// making them easy to compare for equivalence. A synthesized protocol type is therefore
+/// returned by [`ProtocolInstanceType::normalized`] so that two protocols with the same members
+/// will be understood as equivalent even in the context of differently ordered unions or intersections.
+#[salsa::interned(debug)]
+pub(super) struct SynthesizedProtocolType<'db> {
+    #[return_ref]
+    pub(super) members: FxOrderSet<Name>,
 }
diff --git a/crates/red_knot_python_semantic/src/types/known_instance.rs b/crates/red_knot_python_semantic/src/types/known_instance.rs
index d6da1d76d42998..7a8cb2e4642ed9 100644
--- a/crates/red_knot_python_semantic/src/types/known_instance.rs
+++ b/crates/red_knot_python_semantic/src/types/known_instance.rs
@@ -1,6 +1,6 @@
 //! The `KnownInstance` type.
 //!
-//! Despite its name, this is quite a different type from [`super::InstanceType`].
+//! Despite its name, this is quite a different type from [`super::NominalInstanceType`].
 //! For the vast majority of instance-types in Python, we cannot say how many possible
 //! inhabitants there are or could be of that type at runtime. Each variant of the
 //! [`KnownInstanceType`] enum, however, represents a specific runtime symbol
@@ -260,7 +260,7 @@ impl<'db> KnownInstanceType<'db> {
     ///
     /// For example, the symbol `typing.Literal` is an instance of `typing._SpecialForm`,
     /// so `KnownInstanceType::Literal.instance_fallback(db)`
-    /// returns `Type::Instance(InstanceType { class: <typing._SpecialForm> })`.
+    /// returns `Type::NominalInstance(NominalInstanceType { class: <typing._SpecialForm> })`.
     pub(super) fn instance_fallback(self, db: &dyn Db) -> Type {
         self.class().to_instance(db)
     }
diff --git a/crates/red_knot_python_semantic/src/types/narrow.rs b/crates/red_knot_python_semantic/src/types/narrow.rs
index 19cb5c2e5d7265..a63d9d55620488 100644
--- a/crates/red_knot_python_semantic/src/types/narrow.rs
+++ b/crates/red_knot_python_semantic/src/types/narrow.rs
@@ -159,7 +159,7 @@ impl KnownConstraintFunction {
     /// union types are not yet supported. Returns `None` if the `classinfo` argument has a wrong type.
     fn generate_constraint<'db>(self, db: &'db dyn Db, classinfo: Type<'db>) -> Option<Type<'db>> {
         let constraint_fn = |class| match self {
-            KnownConstraintFunction::IsInstance => Type::instance(class),
+            KnownConstraintFunction::IsInstance => Type::instance(db, class),
             KnownConstraintFunction::IsSubclass => SubclassOfType::from(db, class),
         };
 
@@ -472,7 +472,9 @@ impl<'db> NarrowingConstraintsBuilder<'db> {
                         union.map(db, |ty| filter_to_cannot_be_equal(db, *ty, rhs_ty))
                     }
                     // Treat `bool` as `Literal[True, False]`.
-                    Type::Instance(instance) if instance.class().is_known(db, KnownClass::Bool) => {
+                    Type::NominalInstance(instance)
+                        if instance.class().is_known(db, KnownClass::Bool) =>
+                    {
                         UnionType::from_elements(
                             db,
                             [Type::BooleanLiteral(true), Type::BooleanLiteral(false)]
@@ -501,7 +503,7 @@ impl<'db> NarrowingConstraintsBuilder<'db> {
 
     fn evaluate_expr_ne(&mut self, lhs_ty: Type<'db>, rhs_ty: Type<'db>) -> Option<Type<'db>> {
         match (lhs_ty, rhs_ty) {
-            (Type::Instance(instance), Type::IntLiteral(i))
+            (Type::NominalInstance(instance), Type::IntLiteral(i))
                 if instance.class().is_known(self.db, KnownClass::Bool) =>
             {
                 if i == 0 {
@@ -682,7 +684,7 @@ impl<'db> NarrowingConstraintsBuilder<'db> {
                         let symbol = self.expect_expr_name_symbol(id);
                         constraints.insert(
                             symbol,
-                            Type::instance(rhs_class.unknown_specialization(self.db)),
+                            Type::instance(self.db, rhs_class.unknown_specialization(self.db)),
                         );
                     }
                 }
diff --git a/crates/red_knot_python_semantic/src/types/subclass_of.rs b/crates/red_knot_python_semantic/src/types/subclass_of.rs
index 52dd82aaa665ff..56bccc8b68806f 100644
--- a/crates/red_knot_python_semantic/src/types/subclass_of.rs
+++ b/crates/red_knot_python_semantic/src/types/subclass_of.rs
@@ -16,8 +16,8 @@ impl<'db> SubclassOfType<'db> {
     /// This method does not always return a [`Type::SubclassOf`] variant.
     /// If the class object is known to be a final class,
     /// this method will return a [`Type::ClassLiteral`] variant; this is a more precise type.
-    /// If the class object is `builtins.object`, `Type::Instance(<builtins.type>)` will be returned;
-    /// this is no more precise, but it is exactly equivalent to `type[object]`.
+    /// If the class object is `builtins.object`, `Type::NominalInstance(<builtins.type>)`
+    /// will be returned; this is no more precise, but it is exactly equivalent to `type[object]`.
     ///
     /// The eager normalization here means that we do not need to worry elsewhere about distinguishing
     /// between `@final` classes and other classes when dealing with [`Type::SubclassOf`] variants.
@@ -94,9 +94,9 @@ impl<'db> SubclassOfType<'db> {
         }
     }
 
-    pub(crate) fn to_instance(self) -> Type<'db> {
+    pub(crate) fn to_instance(self, db: &'db dyn Db) -> Type<'db> {
         match self.subclass_of {
-            SubclassOfInner::Class(class) => Type::instance(class),
+            SubclassOfInner::Class(class) => Type::instance(db, class),
             SubclassOfInner::Dynamic(dynamic_type) => Type::Dynamic(dynamic_type),
         }
     }
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 ba2adf6b409a7e..d62baf9b90b3ac 100644
--- a/crates/red_knot_python_semantic/src/types/type_ordering.rs
+++ b/crates/red_knot_python_semantic/src/types/type_ordering.rs
@@ -129,10 +129,18 @@ pub(super) fn union_or_intersection_elements_ordering<'db>(
 
         (Type::SubclassOf(_), _) => Ordering::Less,
         (_, Type::SubclassOf(_)) => Ordering::Greater,
-        (Type::Instance(left), Type::Instance(right)) => left.class().cmp(&right.class()),
 
-        (Type::Instance(_), _) => Ordering::Less,
-        (_, Type::Instance(_)) => Ordering::Greater,
+        (Type::NominalInstance(left), Type::NominalInstance(right)) => {
+            left.class().cmp(&right.class())
+        }
+        (Type::NominalInstance(_), _) => Ordering::Less,
+        (_, Type::NominalInstance(_)) => Ordering::Greater,
+
+        (Type::ProtocolInstance(left_proto), Type::ProtocolInstance(right_proto)) => {
+            left_proto.cmp(right_proto)
+        }
+        (Type::ProtocolInstance(_), _) => Ordering::Less,
+        (_, Type::ProtocolInstance(_)) => Ordering::Greater,
 
         (Type::TypeVar(left), Type::TypeVar(right)) => left.cmp(right),
         (Type::TypeVar(_), _) => Ordering::Less,