1 files changed, 76 insertions, 0 deletions
diff --git a/docs/users_guide/exts/implicit_forall.rst b/docs/users_guide/exts/implicit_forall.rst
new file mode 100644
index 0000000000..de9f77e45d
--- /dev/null
+++ b/docs/users_guide/exts/implicit_forall.rst
@@ -0,0 +1,76 @@
+Implicit ForAll
+===============
+
+.. extension:: ImplicitForAll
+    :shortdesc: Implicitly bind free type variables.
+
+    :since: 9.8.1
+
+    :status: Included in :extension:`GHC2021`
+
+    If a type signature does not have an explicit ``forall`` at the top, add an implicit one
+    that binds all the type variables mentioned in the signature that are not already in scope.
+
+
+:extension:`ImplicitForAll` creates an implicit ``forall`` in:
+
+- Type signatures for variable declarations, methods, and foreign imports and exports::
+
+    let f :: a -> a; f = ... in ...
+    -- becomes
+    let f :: forall a. a -> a; f = ... in ...
+
+- Kind signatures::
+
+    type T :: k -> Type
+    -- becomes
+    type T :: forall k. k -> Type
+
+- GADT constructor declarations::
+
+    MkG :: a -> Maybe b -> G (Either Int b)
+    -- becomes
+    MkG :: forall a b. a -> Maybe b -> G (Either Int b)
+
+- Pattern synonym signatures::
+
+    pattern P :: a -> Maybe a
+    -- becomes
+    pattern P :: forall a. a -> Maybe a
+
+- Type annotations in expressions and ``SPECIALISE`` pragmas::
+
+    Right True :: Either a Bool
+    -- becomes
+    Right True :: forall a. Either a Bool
+
+- Types in a ``deriving`` clause::
+
+    data T deriving (C a)
+    -- becomes
+    data T deriving (forall a. C a)
+
+- Instance heads, including standalone ``deriving`` instances::
+
+    instance Show a => Show (Maybe a)
+    -- becomes
+    instance forall a. Show a => Show (Maybe a)
+
+- Type and data family instances, as well as closed ``type family`` equations::
+
+    type instance F (Maybe a) = Int
+    -- becomes
+    type instance forall a. F (Maybe a) = Int
+
+- ``RULES`` pragmas::
+
+    {-# RULES "name" forall (x :: Maybe a). foo x = 5 #-}
+    -- becomes
+    {-# RULES "name" forall a. forall (x :: Maybe a). foo x = 5 #-}
+
+:extension:`ImplicitForAll` also allows binding type variables in pattern
+signatures, but there is still no explicit analogue::
+
+    f (a :: t) = ...
+    -- would be like
+    f @t (a :: t) = ...