Introduce the TypeAbstractions language flag

GHC Proposals #448 "Modern scoped type variables"
and #425 "Invisible binders in type declarations"
introduce a new language extension flag: TypeAbstractions.

Part of the functionality guarded by this flag has already been
implemented, namely type abstractions in constructor patterns, but it
was guarded by a combination of TypeApplications and ScopedTypeVariables
instead of a dedicated language extension flag.

This patch does the following:

* introduces a new language extension flag TypeAbstractions
* requires TypeAbstractions for @a-syntax in constructor patterns
  instead of TypeApplications and ScopedTypeVariables
* creates a User's Guide page for TypeAbstractions and
  moves the "Type Applications in Patterns" section there

To avoid a breaking change, the new flag is implied by
ScopedTypeVariables and is retroactively added to GHC2021.

Metric Decrease:
    MultiLayerModulesTH_OneShot

18 files changed, 119 insertions, 88 deletions

diff --git a/compiler/GHC/Driver/Session.hs b/compiler/GHC/Driver/Session.hs
index 29dff3650f..57d89a15b1 100644
--- a/compiler/GHC/Driver/Session.hs
+++ b/compiler/GHC/Driver/Session.hs
@@ -1412,6 +1412,7 @@ languageExtensions (Just GHC2021)
        LangExt.PostfixOperators,
        LangExt.RankNTypes,
        LangExt.ScopedTypeVariables,
+       LangExt.TypeAbstractions,     -- implied by ScopedTypeVariables according to GHC Proposal #448 "Modern Scoped Type Variables"
        LangExt.StandaloneDeriving,
        LangExt.StandaloneKindSignatures,
        LangExt.TupleSections,
@@ -3766,6 +3767,7 @@ xFlagsDeps = [
   flagSpec "TraditionalRecordSyntax"          LangExt.TraditionalRecordSyntax,
   flagSpec "TransformListComp"                LangExt.TransformListComp,
   flagSpec "TupleSections"                    LangExt.TupleSections,
+  flagSpec "TypeAbstractions"                 LangExt.TypeAbstractions,
   flagSpec "TypeApplications"                 LangExt.TypeApplications,
   flagSpec "TypeData"                         LangExt.TypeData,
   depFlagSpec' "TypeInType"                   LangExt.TypeInType
@@ -3902,6 +3904,9 @@ impliedXFlags
     , (LangExt.MultiParamTypeClasses,     turnOn, LangExt.ConstrainedClassMethods)  -- c.f. #7854
     , (LangExt.TypeFamilyDependencies,    turnOn, LangExt.TypeFamilies)
 
+    -- In accordance with GHC Proposal #448 "Modern Scoped Type Variables"
+    , (LangExt.ScopedTypeVariables,       turnOn, LangExt.TypeAbstractions)
+
     , (LangExt.RebindableSyntax, turnOff, LangExt.ImplicitPrelude)      -- NB: turn off!
 
     , (LangExt.DerivingVia, turnOn, LangExt.DerivingStrategies)
diff --git a/compiler/GHC/Rename/Pat.hs b/compiler/GHC/Rename/Pat.hs
index 9c4f3dd9fb..169c2e508c 100644
--- a/compiler/GHC/Rename/Pat.hs
+++ b/compiler/GHC/Rename/Pat.hs
@@ -640,16 +640,14 @@ rnConPatAndThen mk con (PrefixCon tyargs pats)
   where
     check_lang_exts :: RnM ()
     check_lang_exts = do
-      scoped_tyvars <- xoptM LangExt.ScopedTypeVariables
-      type_app      <- xoptM LangExt.TypeApplications
-      unless (scoped_tyvars && type_app) $
+      type_abs <- xoptM LangExt.TypeAbstractions
+      unless type_abs $
         case listToMaybe tyargs of
           Nothing -> pure ()
           Just tyarg -> addErr $ mkTcRnUnknownMessage $ mkPlainError noHints $
             hang (text "Illegal visible type application in a pattern:"
                     <+> quotes (ppr tyarg))
-               2 (text "Both ScopedTypeVariables and TypeApplications are"
-                    <+> text "required to use this feature")
+               2 (text "Perhaps you intended to use TypeAbstractions")
     rnConPatTyArg (HsConPatTyArg at t) = do
       t' <- liftCpsWithCont $ rnHsPatSigTypeBindingVars HsTypeCtx t
       return (HsConPatTyArg at t')
diff --git a/docs/users_guide/exts/gadt.rst b/docs/users_guide/exts/gadt.rst
index 99902cc76d..89ecf8473d 100644
--- a/docs/users_guide/exts/gadt.rst
+++ b/docs/users_guide/exts/gadt.rst
@@ -227,7 +227,7 @@ also sets :extension:`GADTSyntax` and :extension:`MonoLocalBinds`.
          case f of
            (_ :: F (Maybe z) (Maybe z)) -> Nothing @z
 
-   Another way is to use :ref:`type-applications-in-patterns` instead of a
+   Another way is to use :ref:`type-abstractions-in-patterns` instead of a
    pattern type signature: ::
 
        g4 :: F a a -> a
diff --git a/docs/users_guide/exts/type_abstractions.rst b/docs/users_guide/exts/type_abstractions.rst
new file mode 100644
index 0000000000..02c147ed74
--- /dev/null
+++ b/docs/users_guide/exts/type_abstractions.rst
@@ -0,0 +1,95 @@
+Type abstractions
+=================
+
+.. extension:: TypeAbstractions
+    :shortdesc: Enable type abstraction syntax in patterns and type variable binders.
+
+    :since: 9.6.1
+
+    :status: Partially implemented
+
+    Allow the use of type abstraction syntax.
+
+The :extension:`TypeAbstractions` extension provides a way to explicitly bind
+scoped type or kind variables using the ``@a`` syntax. The feature is only
+partially implemented, and this text covers only the implemented parts, whereas
+the full specification can be found in GHC Proposals `#448 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0448-type-variable-scoping.rst>`__
+and `#425 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0425-decl-invis-binders.rst>`__.
+
+
+.. _type-abstractions-in-patterns:
+
+Type Abstractions in Patterns
+-----------------------------
+
+The type abstraction syntax can be used in patterns that match a data
+constructor. The syntax can't be used with record patterns or infix patterns.
+This is useful in particular to bind existential type variables associated with
+a GADT data constructor as in the following example::
+
+    {-# LANGUAGE AllowAmbiguousTypes #-}
+    {-# LANGUAGE GADTs #-}
+    {-# LANGUAGE RankNTypes #-}
+    {-# LANGUAGE TypeApplications #-}
+    import Data.Proxy
+
+    data Foo where
+      Foo :: forall a. (Show a, Num a) => Foo
+
+    test :: Foo -> String
+    test x = case x of
+      Foo @t -> show @t 0
+
+    main :: IO ()
+    main = print $ test (Foo @Float)
+
+In this example, the case in ``test``` is binding an existential variable introduced
+by ``Foo`` that otherwise could not be named and used.
+
+It's possible to bind variables to any part of the type arguments to a constructor;
+there is no need for them to be existential. In addition, it's possible to "match" against
+part of the type argument using type constructors.
+
+For a somewhat-contrived example::
+
+    foo :: (Num a) => Maybe [a] -> String
+    foo (Nothing @[t]) = show (0 :: t)
+    foo (Just @[t] xs) = show (sum xs :: t)
+
+Here, we're binding the type variable t to be the type of the elements of the list type
+which is itself the argument to Maybe.
+
+The order of the type arguments specified by the type applications in a pattern is the same
+as that for an expression: either the order as given by the user in an explicit ``forall`` in the
+definition of the data constructor, or if that is not present, the order in which the type
+variables appear in its type signature from left to right.
+
+For example if we have the following declaration in GADT syntax::
+
+    data Foo :: * -> * where
+      A :: forall s t. [(t,s)] -> Foo (t,s)
+      B :: (t,s) -> Foo (t,s)
+
+Then the type arguments to ``A`` will match first ``s`` and then ``t``, while the type arguments
+to ``B`` will match first ``t`` and then ``s``.
+
+Type arguments appearing in patterns can influence the inferred type of a definition::
+
+    foo (Nothing @Int) = 0
+    foo (Just x) = x
+
+will have inferred type::
+
+    foo :: Maybe Int -> Int
+
+which is more restricted than what it would be without the application::
+
+    foo :: Num a => Maybe a -> a
+
+For more information and detail regarding type applications in patterns, see the paper
+`Type variables in patterns <https://arxiv.org/pdf/1806.03476>`__ by Eisenberg, Breitner
+and Peyton Jones. Relative to that paper, the implementation in GHC for now at least makes one
+additional conservative restriction, that type variables occurring in patterns must not
+already be in scope, and so are always new variables that only bind whatever type is
+matched, rather than ever referring to a variable from an outer scope. Type wildcards
+``_`` may be used in any place where no new variable needs binding.
diff --git a/docs/users_guide/exts/type_applications.rst b/docs/users_guide/exts/type_applications.rst
index d2a0e4ca16..f37325d9cd 100644
--- a/docs/users_guide/exts/type_applications.rst
+++ b/docs/users_guide/exts/type_applications.rst
@@ -4,7 +4,7 @@ Visible type application
 ========================
 
 .. extension:: TypeApplications
-    :shortdesc: Enable type application syntax in terms, patterns and types.
+    :shortdesc: Enable type application syntax in terms and types.
 
     :since: 8.0.1
 
@@ -261,81 +261,4 @@ of equality over types. For example, given the following definitions: ::
   app2 g x = g x
 
 GHC will deem all of ``app1 id1``, ``app1 id2``, ``app2 id1``, and ``app2 id2``
-to be well typed.
-
-.. _type-applications-in-patterns:
-
-Type Applications in Patterns
------------------------------
-
-The type application syntax can be used in patterns that match a data
-constructor. The syntax can't be used with record patterns or infix patterns.
-This is useful in particular to bind existential type variables associated with
-a GADT data constructor as in the following example::
-
-    {-# LANGUAGE AllowAmbiguousTypes #-}
-    {-# LANGUAGE GADTs #-}
-    {-# LANGUAGE RankNTypes #-}
-    {-# LANGUAGE TypeApplications #-}
-    import Data.Proxy
-
-    data Foo where
-      Foo :: forall a. (Show a, Num a) => Foo
-
-    test :: Foo -> String
-    test x = case x of
-      Foo @t -> show @t 0
-
-    main :: IO ()
-    main = print $ test (Foo @Float)
-
-In this example, the case in ``test``` is binding an existential variable introduced
-by ``Foo`` that otherwise could not be named and used.
-
-It's possible to bind variables to any part of the type arguments to a constructor;
-there is no need for them to be existential. In addition, it's possible to "match" against
-part of the type argument using type constructors.
-
-For a somewhat-contrived example::
-
-    foo :: (Num a) => Maybe [a] -> String
-    foo (Nothing @[t]) = show (0 :: t)
-    foo (Just @[t] xs) = show (sum xs :: t)
-
-Here, we're binding the type variable t to be the type of the elements of the list type
-which is itself the argument to Maybe.
-
-The order of the type arguments specified by the type applications in a pattern is the same
-as that for an expression: either the order as given by the user in an explicit ``forall`` in the
-definition of the data constructor, or if that is not present, the order in which the type
-variables appear in its type signature from left to right.
-
-For example if we have the following declaration in GADT syntax::
-
-    data Foo :: * -> * where
-      A :: forall s t. [(t,s)] -> Foo (t,s)
-      B :: (t,s) -> Foo (t,s)
-
-Then the type arguments to ``A`` will match first ``s`` and then ``t``, while the type arguments
-to ``B`` will match first ``t`` and then ``s``.
-
-Type arguments appearing in patterns can influence the inferred type of a definition::
-
-    foo (Nothing @Int) = 0
-    foo (Just x) = x
-
-will have inferred type::
-
-    foo :: Maybe Int -> Int
-
-which is more restricted than what it would be without the application::
-
-    foo :: Num a => Maybe a -> a
-
-For more information and detail regarding type applications in patterns, see the paper
-`Type variables in patterns <https://arxiv.org/pdf/1806.03476>`__ by Eisenberg, Breitner
-and Peyton Jones. Relative to that paper, the implementation in GHC for now at least makes one
-additional conservative restriction, that type variables occurring in patterns must not
-already be in scope, and so are always new variables that only bind whatever type is
-matched, rather than ever referring to a variable from an outer scope. Type wildcards
-``_`` may be used in any place where no new variable needs binding.
+to be well typed.
\ No newline at end of file
diff --git a/docs/users_guide/exts/types.rst b/docs/users_guide/exts/types.rst
index ea85223184..8d2b6f9f90 100644
--- a/docs/users_guide/exts/types.rst
+++ b/docs/users_guide/exts/types.rst
@@ -21,6 +21,7 @@ Types
     representation_polymorphism
     type_literals
     type_applications
+    type_abstractions
     rank_polymorphism
     impredicative_types
     linear_types
diff --git a/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs b/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
index e0a1d7a2a5..532c290ba8 100644
--- a/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
+++ b/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
@@ -151,6 +151,7 @@ data Extension
    | FieldSelectors
    | OverloadedRecordDot
    | OverloadedRecordUpdate
+   | TypeAbstractions
    deriving (Eq, Enum, Show, Generic, Bounded)
 -- 'Ord' and 'Bounded' are provided for GHC API users (see discussions
 -- in https://gitlab.haskell.org/ghc/ghc/merge_requests/2707 and
diff --git a/testsuite/tests/driver/T4437.hs b/testsuite/tests/driver/T4437.hs
index c895c8da6a..3c07aa5679 100644
--- a/testsuite/tests/driver/T4437.hs
+++ b/testsuite/tests/driver/T4437.hs
@@ -37,7 +37,7 @@ check title expected got
 -- See Note [Adding a language extension] in compiler/GHC/Driver/Session.hs.
 expectedGhcOnlyExtensions :: [String]
 expectedGhcOnlyExtensions =
-    [
+    [ "TypeAbstractions"
     ]
 
 expectedCabalOnlyExtensions :: [String]
diff --git a/testsuite/tests/showIface/DocsInHiFile1.stdout b/testsuite/tests/showIface/DocsInHiFile1.stdout
index 093d07614c..b74854d941 100644
--- a/testsuite/tests/showIface/DocsInHiFile1.stdout
+++ b/testsuite/tests/showIface/DocsInHiFile1.stdout
@@ -143,5 +143,6 @@ docs:
          ImportQualifiedPost
          StandaloneKindSignatures
          FieldSelectors
+         TypeAbstractions
 extensible fields:
 
diff --git a/testsuite/tests/showIface/DocsInHiFileTH.stdout b/testsuite/tests/showIface/DocsInHiFileTH.stdout
index 1eac242a68..57ec74c37d 100644
--- a/testsuite/tests/showIface/DocsInHiFileTH.stdout
+++ b/testsuite/tests/showIface/DocsInHiFileTH.stdout
@@ -286,5 +286,6 @@ docs:
          ImportQualifiedPost
          StandaloneKindSignatures
          FieldSelectors
+         TypeAbstractions
 extensible fields:
 
diff --git a/testsuite/tests/showIface/HaddockIssue849.stdout b/testsuite/tests/showIface/HaddockIssue849.stdout
index 197f83df62..3bd32adbcc 100644
--- a/testsuite/tests/showIface/HaddockIssue849.stdout
+++ b/testsuite/tests/showIface/HaddockIssue849.stdout
@@ -66,5 +66,6 @@ docs:
          ImportQualifiedPost
          StandaloneKindSignatures
          FieldSelectors
+         TypeAbstractions
 extensible fields:
 
diff --git a/testsuite/tests/showIface/HaddockOpts.stdout b/testsuite/tests/showIface/HaddockOpts.stdout
index 60a0535457..8af1142afe 100644
--- a/testsuite/tests/showIface/HaddockOpts.stdout
+++ b/testsuite/tests/showIface/HaddockOpts.stdout
@@ -58,5 +58,6 @@ docs:
          ImportQualifiedPost
          StandaloneKindSignatures
          FieldSelectors
+         TypeAbstractions
 extensible fields:
 
diff --git a/testsuite/tests/showIface/MagicHashInHaddocks.stdout b/testsuite/tests/showIface/MagicHashInHaddocks.stdout
index 3b3d44f08d..2eb7eee959 100644
--- a/testsuite/tests/showIface/MagicHashInHaddocks.stdout
+++ b/testsuite/tests/showIface/MagicHashInHaddocks.stdout
@@ -68,5 +68,6 @@ docs:
          ImportQualifiedPost
          StandaloneKindSignatures
          FieldSelectors
+         TypeAbstractions
 extensible fields:
 
diff --git a/testsuite/tests/showIface/NoExportList.stdout b/testsuite/tests/showIface/NoExportList.stdout
index 3fec2d6c88..669774d8e4 100644
--- a/testsuite/tests/showIface/NoExportList.stdout
+++ b/testsuite/tests/showIface/NoExportList.stdout
@@ -94,5 +94,6 @@ docs:
          ImportQualifiedPost
          StandaloneKindSignatures
          FieldSelectors
+         TypeAbstractions
 extensible fields:
 
diff --git a/testsuite/tests/showIface/PragmaDocs.stdout b/testsuite/tests/showIface/PragmaDocs.stdout
index bd8ba16957..b2a9c929c6 100644
--- a/testsuite/tests/showIface/PragmaDocs.stdout
+++ b/testsuite/tests/showIface/PragmaDocs.stdout
@@ -68,5 +68,6 @@ docs:
          ImportQualifiedPost
          StandaloneKindSignatures
          FieldSelectors
+         TypeAbstractions
 extensible fields:
 
diff --git a/testsuite/tests/showIface/ReExports.stdout b/testsuite/tests/showIface/ReExports.stdout
index 31007df259..f0c1ab2c9f 100644
--- a/testsuite/tests/showIface/ReExports.stdout
+++ b/testsuite/tests/showIface/ReExports.stdout
@@ -65,5 +65,6 @@ docs:
          ImportQualifiedPost
          StandaloneKindSignatures
          FieldSelectors
+         TypeAbstractions
 extensible fields:
 
diff --git a/testsuite/tests/typecheck/should_compile/T20443a.hs b/testsuite/tests/typecheck/should_compile/T20443a.hs
index c4b552a3f2..539c0cd2f2 100644
--- a/testsuite/tests/typecheck/should_compile/T20443a.hs
+++ b/testsuite/tests/typecheck/should_compile/T20443a.hs
@@ -10,4 +10,4 @@ a :: () -> Proxy Int
 a () = Proxy @Int
 
 b :: Proxy Int -> ()
-b (Proxy @Int) = ()       -- This should compile, but doesn't
+b (Proxy @Int) = ()
diff --git a/testsuite/tests/typecheck/should_fail/T19109.stderr b/testsuite/tests/typecheck/should_fail/T19109.stderr
index 83f60680da..de40685f67 100644
--- a/testsuite/tests/typecheck/should_fail/T19109.stderr
+++ b/testsuite/tests/typecheck/should_fail/T19109.stderr
@@ -1,4 +1,4 @@
 
 T19109.hs:6:4: error:
     Illegal visible type application in a pattern: ‘@Int’
-      Both ScopedTypeVariables and TypeApplications are required to use this feature
+      Perhaps you intended to use TypeAbstractions