diff --git a/peps/pep-0718.rst b/peps/pep-0718.rst
index 8d10e87cd..025fb8707 100644
--- a/peps/pep-0718.rst
+++ b/peps/pep-0718.rst
@@ -17,11 +17,16 @@ Abstract
 This PEP proposes making function objects subscriptable for typing purposes. Doing so
 gives developers explicit control over the types produced by the type checker where
 bi-directional inference (which allows for the types of parameters of anonymous
-functions to be inferred) and other methods than specialisation are insufficient.
+functions to be inferred) and other methods than specialisation are insufficient. It
+also brings functions in line with regular classes in their ability to be
+subscriptable.
 
 Motivation
 ----------
 
+Unknown Types
+^^^^^^^^^^^^^
+
 Currently, it is not possible to infer the type parameters to generic functions in
 certain situations:
 
@@ -62,6 +67,23 @@ If function objects were subscriptable, however, a more specific type could be g
 
    reveal_type(factory[int](lambda x: "Hello World" * x))  # type is Foo[int]
 
+Undecidable Inference
+^^^^^^^^^^^^^^^^^^^^^
+
+There are even cases where subclass relations make type inference impossible. However,
+if you can specialise the function type checkers can infer a meaningful type.
+
+.. code-block:: python
+
+   def foo[T](x: Sequence[T] | T) -> list[T]: ...
+
+   reveal_type(foo[bytes](b"hello"))
+
+Currently, type checkers do not consistently synthesise a type here.
+
+Unsolvable Type Parameters
+^^^^^^^^^^^^^^^^^^^^^^^^^^
+
 Currently, with unspecialised literals, it is not possible to determine a type for
 situations similar to:
 
@@ -93,9 +115,26 @@ Due to this, specialising the function and using it as a new factory is fine
    make_int_list = make_list[int]
    reveal_type(make_int_list())  # type is list[int]
 
+Monomorphisation and Reification
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
 This proposal also opens the door to
 `monomorphisation <https://en.wikipedia.org/wiki/Monomorphization>`_ and
-`reified types <https://en.wikipedia.org/wiki/Reification_(computer_science)>`_
+`reified types <https://en.wikipedia.org/wiki/Reification_(computer_science)>`_.
+
+This would allow for a functionality which anecdotally has been requested many times.
+
+*Please note this feature is not being proposed by the PEP, but may be implemented in
+the future.*
+
+The syntax for such a feature may look something like:
+
+.. code-block:: python
+
+   def foo[T]():
+      return T.__value__
+
+   assert foo[int]() is int
 
 Rationale
 ---------
@@ -158,7 +197,15 @@ The following code snippet would fail at runtime without this change as
    def bar[U]():
        return Foo[int]()
 
-   assert bar[str]().__orig_class__  is Foo[int]
+   assert bar[str]().__orig_class__  == Foo[int]
+
+Interactions with ``@typing.overload``
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Overloaded functions should work much the same as already, since they have no effect on
+the runtime type. The only change is that more situations will be decidable and the
+behaviour/overload can be specified by the developer rather than leaving it to ordering
+of overloads/unions.
 
 Backwards Compatibility
 -----------------------