Extension shuffling (#23291)wip/sand-witch/modern-STV-extension-shuffling

Where introduced 4 new extensions:
  - PatternSignatures
  - ExtendedForAllScope
  - MethodTypeVariables
  - ImplicitForAll

Tasks of ScopedTypeVariables extension were distributed between
PatternSignatures, ExtendedForAllScope and MethodTypeVariables according
to the proposal. Now ScopedTypeVaribles only implies these three exntesions.

Extension ImplicitForAll saves current behavior. NoImplicitForAll
disables implicit bounding of type variables in many contexts.

Was introduced one new warning option: -Wpattern-signature-binds
It warns when pattern signature binds into scope new type variable. For
example:

  f (a :: t) = ...

6 files changed, 146 insertions, 27 deletions

diff --git a/docs/users_guide/exts/explicit_forall.rst b/docs/users_guide/exts/explicit_forall.rst
index 5a6212ee4b..50e797f85d 100644
--- a/docs/users_guide/exts/explicit_forall.rst
+++ b/docs/users_guide/exts/explicit_forall.rst
@@ -114,7 +114,7 @@ The ``forall``-or-nothing rule takes effect in the following places:
 
 Notes:
 
-- :ref:`pattern-type-sigs` are a notable example of a place where
+- :extension:`PatternSignatures` are a notable example of a place where
   types do *not* obey the ``forall``-or-nothing rule. For example, GHC will
   accept the following: ::
 
diff --git a/docs/users_guide/exts/gadt.rst b/docs/users_guide/exts/gadt.rst
index 89ecf8473d..0382479104 100644
--- a/docs/users_guide/exts/gadt.rst
+++ b/docs/users_guide/exts/gadt.rst
@@ -194,7 +194,7 @@ also sets :extension:`GADTSyntax` and :extension:`MonoLocalBinds`.
 
    In the function clause for ``g``, GHC first checks ``MkF``, the outermost
    pattern, followed by the inner ``Nothing`` pattern. This outside-in order
-   can interact somewhat counterintuitively with :ref:`pattern-type-sigs`.
+   can interact somewhat counterintuitively with :extension:`PatternSignatures`.
    Consider the following variation of ``g``: ::
 
        g2 :: F a a -> a
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) = ...
diff --git a/docs/users_guide/exts/scoped_type_variables.rst b/docs/users_guide/exts/scoped_type_variables.rst
index ee6a77f32a..15972c9d08 100644
--- a/docs/users_guide/exts/scoped_type_variables.rst
+++ b/docs/users_guide/exts/scoped_type_variables.rst
@@ -6,9 +6,13 @@ Lexically scoped type variables
 ===============================
 
 .. extension:: ScopedTypeVariables
-    :shortdesc: Enable lexically-scoped type variables.
+    :shortdesc: Enable lexically-scoped type variables everywhere.
 
-    :implies: :extension:`ExplicitForAll`
+    :implies: :extension:`ExplicitForAll`,
+      :extension:`PatternSignatures`,
+      :extension:`ExtendedForAllScope`,
+      :extension:`MethodTypeVariables`,
+      :extension:`TypeAbstractions`
 
     :since: 6.8.1
 
@@ -26,7 +30,7 @@ Lexically scoped type variables
     To trigger those forms of :extension:`ScopedTypeVariables`, the ``forall`` must appear against the top-level signature (or outer expression)
     but *not* against nested signatures referring to the same type variables.
 
-    Explicit ``forall`` is not always required -- see :ref:`pattern signature equivalent <pattern-equiv-form>` for the example in this section, or :ref:`pattern-type-sigs`.
+    Explicit ``forall`` is not always required -- see :ref:`pattern signature equivalent <pattern-equiv-form>` for the example in this section, or :extension:`PatternSignatures`.
 
 GHC supports *lexically scoped type variables*, without which some type
 signatures are simply impossible to write. For example: ::
@@ -48,7 +52,7 @@ possible to do so.
 
 .. _pattern-equiv-form:
 
-An equivalent form for that example, avoiding explicit ``forall`` uses :ref:`pattern-type-sigs`: ::
+An equivalent form for that example, avoiding explicit ``forall`` uses :extension:`PatternSignatures`: ::
 
     f :: [a] -> [a]
     f (xs :: [aa]) = xs ++ ys
@@ -84,9 +88,9 @@ A *lexically scoped type variable* can be bound by:
 
 -  An expression type signature (:ref:`exp-type-sigs`)
 
--  A pattern type signature (:ref:`pattern-type-sigs`)
+-  A pattern type signature (:extension:`PatternSignatures`)
 
--  Class and instance declarations (:ref:`cls-inst-scoped-tyvars`)
+-  Class and instance declarations (:extension:`MethodTypeVariables`)
 
 In Haskell, a programmer-written type signature is implicitly quantified
 over its free type variables (`Section
@@ -100,14 +104,31 @@ scope is *not* universally quantified. For example, if type variable
       (e :: b -> b)     means     (e :: forall b. b->b)
       (e :: a -> b)     means     (e :: forall b. a->b)
 
+Extended ForAll Scope
+=====================
+
+.. extension:: ExtendedForAllScope
+    :shortdesc: Enable lexically-scoped type variables in function bindings,
+                pattern synonyms and expression type signatures.
+
+    :since: 9.8.1
+
+    :implied by: :extension:`ScopedTypeVariables`
+
+    :status: Included in :extension:`GHC2021`
+
+    Enable lexical scoping of type variables explicitly introduced with
+    a ``forall`` in function bindings, pattern synonyms and expression type signatures.
+
 .. _decl-type-sigs:
 
 Declaration type signatures
 ---------------------------
 
-A declaration type signature that has *explicit* quantification (using
-``forall``) brings into scope the explicitly-quantified type variables,
-in the definition of the named function. For example: ::
+When :extension:`ExtendedForAllScope` is enabled, a declaration type signature
+that has *explicit* quantification (using ``forall``) brings into scope the
+explicitly-quantified type variables, in the definition of the named function.
+For example: ::
 
       f :: forall a. [a] -> [a]
       f (x:xs) = xs ++ [ x :: a ]
@@ -171,9 +192,9 @@ This only happens if:
 Expression type signatures
 --------------------------
 
-An expression type signature that has *explicit* quantification (using
-``forall``) brings into scope the explicitly-quantified type variables,
-in the annotated expression. For example: ::
+When :extension:`ExtendedForAllScope` is enabled, an expression type signature
+that has *explicit* quantification (using ``forall``) brings into scope the
+explicitly-quantified type variables, in the annotated expression. For example: ::
 
     f = runST ( (op >>= \(x :: STRef s Int) -> g x) :: forall s. ST s Bool )
 
@@ -181,13 +202,22 @@ Here, the type signature ``forall s. ST s Bool`` brings the type
 variable ``s`` into scope, in the annotated expression
 ``(op >>= \(x :: STRef s Int) -> g x)``.
 
-.. _pattern-type-sigs:
+Pattern Signatures
+==================
 
-Pattern type signatures
------------------------
+.. extension:: PatternSignatures
+    :shortdesc: Allow type signatures in patterns.
 
-A type signature may occur in any pattern; this is a *pattern type
-signature*. For example: ::
+    :since: 9.8.1
+
+    :implied by: :extension:`ScopedTypeVariables`
+
+    :status: Included in :extension:`GHC2021`
+
+    Allow type signatures and type variable bindings in patterns.
+
+When :extension:`PatternSignatures` is enabled, a type signature may occur
+in any pattern; this is a *pattern type signature*. For example: ::
 
     -- f and g assume that 'a' is already in scope
     f = \(x::Int, y::a) -> x
@@ -259,12 +289,22 @@ they are both legal whether or not ``a`` is already in scope.
 They differ in that *if* ``a`` is already in scope, the signature constrains
 the pattern, rather than the pattern binding the variable.
 
-.. _cls-inst-scoped-tyvars:
+Method Type Variables
+=====================
+
+.. extension:: MethodTypeVariables
+    :shortdesc: Enable lexically-scoped type variables in class and instance declarations.
+
+    :since: 9.8.1
 
-Class and instance declarations
--------------------------------
+    :implied by: :extension:`ScopedTypeVariables`
+
+    :status: Included in :extension:`GHC2021`
+
+    Enable lexical scoping of type variables explicitly introduced with
+    ``forall`` in class and instance declarations.
 
-:extension:`ScopedTypeVariables` allow the type variables bound by the top of a
+:extension:`MethodTypeVariables` allow the type variables bound by the top of a
 ``class`` or ``instance`` declaration to scope over the methods defined in the
 ``where`` part. Unlike :ref:`decl-type-sigs`, type variables from class and
 instance declarations can be lexically scoped without an explicit ``forall``
@@ -286,11 +326,11 @@ declaration; see :ref:`explicit-foralls`). For example: ::
       instance forall b. C b => C [b] where
         op xs = reverse (head (xs :: [[b]]))
 
-While :extension:`ScopedTypeVariables` is required for type variables from the
+While :extension:`MethodTypeVariables` is required for type variables from the
 top of a class or instance declaration to scope over the /bodies/ of the
 methods, it is not required for the type variables to scope over the /type
 signatures/ of the methods. For example, the following will be accepted without
-explicitly enabling :extension:`ScopedTypeVariables`: ::
+explicitly enabling :extension:`MethodTypeVariables`: ::
 
       class D a where
         m :: [a] -> a
@@ -302,11 +342,11 @@ explicitly enabling :extension:`ScopedTypeVariables`: ::
 Note that writing ``m :: [a] -> [a]`` requires the use of the
 :extension:`InstanceSigs` extension.
 
-Similarly, :extension:`ScopedTypeVariables` is not required for type variables
+Similarly, :extension:`MethodTypeVariables` is not required for type variables
 from the top of the class or instance declaration to scope over associated type
 families, which only requires the :extension:`TypeFamilies` extension. For
 instance, the following will be accepted without explicitly enabling
-:extension:`ScopedTypeVariables`: ::
+:extension:`MethodTypeVariables`: ::
 
       class E a where
         type T a
diff --git a/docs/users_guide/exts/type_abstractions.rst b/docs/users_guide/exts/type_abstractions.rst
index ca8761f405..7b109e4fad 100644
--- a/docs/users_guide/exts/type_abstractions.rst
+++ b/docs/users_guide/exts/type_abstractions.rst
@@ -6,6 +6,8 @@ Type abstractions
 
     :since: 9.8.1
 
+    :implied by: :extension:`ScopedTypeVariables`
+
     :status: Partially implemented
 
     Allow the use of type abstraction syntax.
diff --git a/docs/users_guide/exts/type_signatures.rst b/docs/users_guide/exts/type_signatures.rst
index 9d0fcdc5bb..67b1f904df 100644
--- a/docs/users_guide/exts/type_signatures.rst
+++ b/docs/users_guide/exts/type_signatures.rst
@@ -7,6 +7,7 @@ Type signatures
     :maxdepth: 1
 
     explicit_forall
+    implicit_forall
     ambiguous_types
     kind_signatures
     scoped_type_variables