diff --git a/docs/docs/reference/new-types/dependent-function-types.md b/docs/docs/reference/new-types/dependent-function-types.md
index b7003d7c66fc..a8840321e0fb 100644
--- a/docs/docs/reference/new-types/dependent-function-types.md
+++ b/docs/docs/reference/new-types/dependent-function-types.md
@@ -3,17 +3,16 @@ layout: doc-page
 title: "Dependent Function Types"
 ---
 
-A dependent function type describes functions where the result type may depend
-on the function's parameter values. Example:
+A dependent function type is a function type whose result depends
+on the function's parameters. For example:
 ```scala
 trait Entry { type Key; val key: Key }
 
 def extractKey(e: Entry): e.Key = e.key          // a dependent method
+
 val extractor: (e: Entry) => e.Key = extractKey  // a dependent function value
-//            ║   ⇓ ⇓ ⇓ ⇓ ⇓ ⇓ ⇓   ║
-//            ║     Dependent     ║
-//            ║   Function Type   ║
-//            ╚═══════════════════╝
+//             ^^^^^^^^^^^^^^^^^^^
+//             a dependent function type
 ```
 Scala already has _dependent methods_, i.e. methods where the result
 type refers to some of the parameters of the method. Method
diff --git a/docs/docs/reference/new-types/polymorphic-function-types.md b/docs/docs/reference/new-types/polymorphic-function-types.md
new file mode 100644
index 000000000000..c555a83df89d
--- /dev/null
+++ b/docs/docs/reference/new-types/polymorphic-function-types.md
@@ -0,0 +1,93 @@
+---
+layout: doc-page
+title: "Polymorphic Function Types"
+---
+
+A polymorphic function type is a function type which accepts type parameters.
+For example:
+```scala
+// A polymorphic method:
+def foo[A](xs: List[A]): List[A] = xs.reverse
+
+// A polymorphic function value:
+val bar: [A] => List[A] => List[A]
+//       ^^^^^^^^^^^^^^^^^^^^^^^^^
+//       a polymorphic function type
+       = [A] => (xs: List[A]) => foo[A](xs)
+```
+Scala already has _polymorphic methods_, i.e. methods which accepts type parameters.
+Method `foo` above is an example, accepting a type parameter `A`.
+So far, it
+was not possible to turn such methods into polymorphic function values like `bar` above,
+which can be passed as parameters to other functions, or returned as results.
+
+In Dotty this is now possible. The type of the `bar` value above is
+
+```scala
+[A] => List[A] => List[A]
+```
+
+This type describes function values which take a type `A` as a parameter,
+then take a list of type `List[A]`, and return a list of the same type `List[A]`.
+
+[More details](https://github.com/lampepfl/dotty/pull/4672)
+
+
+### Example Usage
+
+Polymorphic function type are particularly useful
+when callers of a method are required to provide a
+function which has to be polymorphic,
+meaning that it should accept arbitrary types as part of its inputs.
+
+For instance, consider the situation where we have
+a data type to represent the expressions of a simple language
+(consisting only of variables and function application)
+in a strongly-typed way:
+
+```scala
+enum Expr[A]:
+  case Var(name: String)
+  case Apply[A, B](fun: Expr[B => A], arg: Expr[B]) extends Expr[A]
+```
+
+We would like to provide a way for users to map a function
+over all immediate subexpressions of a given `Expr`.
+This requires the given function to be polymorphic,
+since each subexpression may have a different type.
+Here is how to implement this using polymorphic function types:
+
+```scala
+def mapSubexpressions[A](e: Expr[A])(f: [B] => Expr[B] => Expr[B]): Expr[A] =
+  e match
+    case Apply(fun, arg) => Apply(f(fun), f(arg))
+    case Var(n) => Var(n)
+```
+
+And here is how to use this function to _wrap_ each subexpression
+in a given expression with a call to some `wrap` function,
+defined as a variable:
+
+```scala
+val e0 = Apply(Var("f"), Var("a"))
+val e1 = mapSubexpressions(e0)(
+  [B] => (se: Expr[B]) => Apply(Var[B => B]("wrap"), se))
+println(e1) // Apply(Apply(Var(wrap),Var(f)),Apply(Var(wrap),Var(a)))
+```
+
+
+
+### Relationship With Type Lambdas
+
+Polymorphic function types are not to be confused with
+[_type lambdas_](new-types/type-lambdas.md).
+While the former describes the _type_ of a polymorphic _value_,
+the latter is an actual function value _at the type level_.
+
+A good way of understanding the difference is to notice that
+**_type lambdas are applied in types,
+whereas polymorphic functions are applied in terms_**:
+One would call the function `bar` above
+by passing it a type argument `bar[Int]` _within a method body_.
+On the other hand, given a type lambda such as `type F = [A] =>> List[A]`,
+one would call `F` _withing a type expression_, as in `type Bar = F[Int]`.
diff --git a/docs/docs/reference/overview.md b/docs/docs/reference/overview.md
index 211b34a1e7eb..86b9fd9cf22d 100644
--- a/docs/docs/reference/overview.md
+++ b/docs/docs/reference/overview.md
@@ -107,7 +107,7 @@ These are additions to the language that make it more powerful or pleasant to us
  - [Enums](enums/enums.md) provide concise syntax for enumerations and [algebraic data types](enums/adts.md).
  - [Parameter Untupling](other-new-features/parameter-untupling.md) avoids having to use `case` for tupled parameter destructuring.
  - [Dependent Function Types](new-types/dependent-function-types.md) generalize dependent methods to dependent function values and types.
- - [Polymorphic Function Types](https://github.com/lampepfl/dotty/pull/4672) generalize polymorphic methods to dependent function values and types. _Current status_: There is a proposal, and a prototype implementation, but the implementation has not been finalized or merged yet.
+ - [Polymorphic Function Types](new-types/polymorphic-function-types.md) generalize polymorphic methods to polymorphic function values and types. _Current status_: There is a proposal and a merged prototype implementation, but the implementation has not been finalized (it is notably missing type inference support).
  - [Kind Polymorphism](other-new-features/kind-polymorphism.md) allows the definition of operators working equally on types and type constructors.
  - [@targetName Annotations](other-new-features/targetName.md) make it easier to interoperate with code written in other languages and give more flexibility for avoiding name clashes.
 
diff --git a/docs/sidebar.yml b/docs/sidebar.yml
index 76124fbad574..2903457fbd50 100644
--- a/docs/sidebar.yml
+++ b/docs/sidebar.yml
@@ -35,6 +35,8 @@ sidebar:
               url: docs/reference/new-types/match-types.html
             - title: Dependent Function Types
               url: docs/reference/new-types/dependent-function-types.html
+            - title: Polymorphic Function Types
+              url: docs/reference/new-types/polymorphic-function-types.html
         - title: Enums
           subsection:
             - title: Enumerations