[Git][ghc/ghc][wip/int-index/type-abs-flag] Introduce the TypeAbstractions language flag

Vladislav Zavialov (@int-index) gitlab at gitlab.haskell.org
Tue Jan 10 15:03:10 UTC 2023



Vladislav Zavialov pushed to branch wip/int-index/type-abs-flag at Glasgow Haskell Compiler / GHC


Commits:
690fbf53 by Vladislav Zavialov at 2023-01-10T18:02:54+03:00
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 changed files:

- compiler/GHC/Driver/Session.hs
- compiler/GHC/Rename/Pat.hs
- docs/users_guide/exts/gadt.rst
- + docs/users_guide/exts/type_abstractions.rst
- docs/users_guide/exts/type_applications.rst
- docs/users_guide/exts/types.rst
- libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
- testsuite/tests/driver/T4437.hs
- testsuite/tests/showIface/DocsInHiFile1.stdout
- testsuite/tests/showIface/DocsInHiFileTH.stdout
- testsuite/tests/showIface/HaddockIssue849.stdout
- testsuite/tests/showIface/HaddockOpts.stdout
- testsuite/tests/showIface/MagicHashInHaddocks.stdout
- testsuite/tests/showIface/NoExportList.stdout
- testsuite/tests/showIface/PragmaDocs.stdout
- testsuite/tests/showIface/ReExports.stdout
- testsuite/tests/typecheck/should_compile/T20443a.hs
- testsuite/tests/typecheck/should_fail/T19109.stderr


Changes:

=====================================
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,
@@ -3765,6 +3766,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
@@ -3901,6 +3903,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)


=====================================
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')


=====================================
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


=====================================
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.


=====================================
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


=====================================
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


=====================================
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


=====================================
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]


=====================================
testsuite/tests/showIface/DocsInHiFile1.stdout
=====================================
@@ -143,5 +143,6 @@ docs:
          ImportQualifiedPost
          StandaloneKindSignatures
          FieldSelectors
+         TypeAbstractions
 extensible fields:
 


=====================================
testsuite/tests/showIface/DocsInHiFileTH.stdout
=====================================
@@ -286,5 +286,6 @@ docs:
          ImportQualifiedPost
          StandaloneKindSignatures
          FieldSelectors
+         TypeAbstractions
 extensible fields:
 


=====================================
testsuite/tests/showIface/HaddockIssue849.stdout
=====================================
@@ -66,5 +66,6 @@ docs:
          ImportQualifiedPost
          StandaloneKindSignatures
          FieldSelectors
+         TypeAbstractions
 extensible fields:
 


=====================================
testsuite/tests/showIface/HaddockOpts.stdout
=====================================
@@ -58,5 +58,6 @@ docs:
          ImportQualifiedPost
          StandaloneKindSignatures
          FieldSelectors
+         TypeAbstractions
 extensible fields:
 


=====================================
testsuite/tests/showIface/MagicHashInHaddocks.stdout
=====================================
@@ -68,5 +68,6 @@ docs:
          ImportQualifiedPost
          StandaloneKindSignatures
          FieldSelectors
+         TypeAbstractions
 extensible fields:
 


=====================================
testsuite/tests/showIface/NoExportList.stdout
=====================================
@@ -94,5 +94,6 @@ docs:
          ImportQualifiedPost
          StandaloneKindSignatures
          FieldSelectors
+         TypeAbstractions
 extensible fields:
 


=====================================
testsuite/tests/showIface/PragmaDocs.stdout
=====================================
@@ -68,5 +68,6 @@ docs:
          ImportQualifiedPost
          StandaloneKindSignatures
          FieldSelectors
+         TypeAbstractions
 extensible fields:
 


=====================================
testsuite/tests/showIface/ReExports.stdout
=====================================
@@ -65,5 +65,6 @@ docs:
          ImportQualifiedPost
          StandaloneKindSignatures
          FieldSelectors
+         TypeAbstractions
 extensible fields:
 


=====================================
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) = ()


=====================================
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



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/690fbf53cca771eec58f3a345df7c33dd7f63314

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/690fbf53cca771eec58f3a345df7c33dd7f63314
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230110/4aebebd8/attachment-0001.html>


More information about the ghc-commits mailing list