[Git][ghc/ghc][master] Introduce the TypeAbstractions language flag
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Wed Jan 11 05:58:24 UTC 2023
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
bc125775 by Vladislav Zavialov at 2023-01-11T00:58:03-05: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,
@@ -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)
=====================================
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/bc1257750f507218059ac6bad05d9c96a8b88d67
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/bc1257750f507218059ac6bad05d9c96a8b88d67
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/20230111/57a82adb/attachment-0001.html>
More information about the ghc-commits
mailing list