diff options
-rw-r--r-- | docs/users_guide/exts/existential_quantification.rst | 2 | ||||
-rw-r--r-- | docs/users_guide/exts/gadt.rst | 23 | ||||
-rw-r--r-- | docs/users_guide/exts/gadt_syntax.rst | 11 | ||||
-rw-r--r-- | testsuite/tests/gadt/all.T | 1 | ||||
-rw-r--r-- | testsuite/tests/gadt/gadtSyntax002.hs | 6 |
5 files changed, 39 insertions, 4 deletions
diff --git a/docs/users_guide/exts/existential_quantification.rst b/docs/users_guide/exts/existential_quantification.rst index 42f5cbdc83..4652f2cae0 100644 --- a/docs/users_guide/exts/existential_quantification.rst +++ b/docs/users_guide/exts/existential_quantification.rst @@ -176,6 +176,8 @@ For example: :: upd4 g x = g { g2=x } -- BAD (g2's type mentions c, which is not a simple -- type-variable argument in G1's result type) +.. _existential-restrictions: + Restrictions ~~~~~~~~~~~~ diff --git a/docs/users_guide/exts/gadt.rst b/docs/users_guide/exts/gadt.rst index 3463bd63da..99902cc76d 100644 --- a/docs/users_guide/exts/gadt.rst +++ b/docs/users_guide/exts/gadt.rst @@ -80,13 +80,32 @@ also sets :extension:`GADTSyntax` and :extension:`MonoLocalBinds`. each constructor must end with ``Term ty``, but the ``ty`` need not be a type variable (e.g. the ``Lit`` constructor). +- GADT constructors can include contexts and existential variables, + generalising existential quantification (:ref:`existential-quantification`). + For example: :: + + data SomeShow where + SomeShow :: Show a => a -> SomeShow + -- `a` is existential, as it does not appear in the return type + + data G a where + MkG :: (a ~ Int) => a -> a -> G a + -- essentially the same as: + -- MkG :: Int -> Int -> G Int + - It is permitted to declare an ordinary algebraic data type using GADT-style syntax. What makes a GADT into a GADT is not the syntax, but rather the presence of data constructors whose result type is not - just ``T a b``. + just ``T a b``, or which include contexts. + +- A newtype may use GADT-style syntax, but it must declare an ordinary + data type, not a GADT. That is, the constructor must not bind + existential variables (as per :ref:`existential-quantification`) + nor include a context. - You cannot use a ``deriving`` clause for a GADT; only for an ordinary - data type. + data type (possibly using GADT-style syntax). However, you can still use a + :ref:`stand-alone-deriving` declaration. - As mentioned in :ref:`gadt-style`, record syntax is supported. For example: diff --git a/docs/users_guide/exts/gadt_syntax.rst b/docs/users_guide/exts/gadt_syntax.rst index 5b0e1631f3..c0cc6167c9 100644 --- a/docs/users_guide/exts/gadt_syntax.rst +++ b/docs/users_guide/exts/gadt_syntax.rst @@ -19,6 +19,9 @@ explicitly. For example: :: Nothing :: Maybe a Just :: a -> Maybe a + newtype Down a where + Down :: a -> Down a + The form is called a "GADT-style declaration" because Generalised Algebraic Data Types, described in :ref:`gadt`, can only be declared using this form. @@ -30,8 +33,8 @@ are equivalent: :: data Foo = forall a. MkFoo a (a -> Bool) data Foo' where { MKFoo :: a -> (a->Bool) -> Foo' } -Any data type that can be declared in standard Haskell 98 syntax can -also be declared using GADT-style syntax. The choice is largely +Any datatype (or newtype) that can be declared in standard Haskell 98 syntax, +can also be declared using GADT-style syntax. The choice is largely stylistic, but GADT-style declarations differ in one important respect: they treat class constraints on the data constructors differently. Specifically, if the constructor is given a type-class context, that @@ -103,6 +106,10 @@ implements this behaviour, odd though it is. But for GADT-style declarations, GHC's behaviour is much more useful, as well as much more intuitive. +Note that the restrictions of :ref:`existential-restrictions` are still +in place; for example, a newtype declared with ``GADTSyntax`` cannot +use existential quantification. + .. _formal-gadt-syntax: Formal syntax for GADTs diff --git a/testsuite/tests/gadt/all.T b/testsuite/tests/gadt/all.T index 3152f3561b..ce30d570f3 100644 --- a/testsuite/tests/gadt/all.T +++ b/testsuite/tests/gadt/all.T @@ -97,6 +97,7 @@ test('T3651', normal, compile_fail, ['']) test('T3638', normal, compile, ['']) test('gadtSyntax001', normal, compile, ['']) +test('gadtSyntax002', normal, compile, ['']) test('gadtSyntaxFail001', normal, compile_fail, ['']) test('gadtSyntaxFail002', normal, compile_fail, ['']) test('gadtSyntaxFail003', normal, compile_fail, ['']) diff --git a/testsuite/tests/gadt/gadtSyntax002.hs b/testsuite/tests/gadt/gadtSyntax002.hs new file mode 100644 index 0000000000..46ccfb320c --- /dev/null +++ b/testsuite/tests/gadt/gadtSyntax002.hs @@ -0,0 +1,6 @@ +{-# LANGUAGE GADTSyntax #-} + +module GADTSyntax002 where + +newtype Down a where + Down :: { getDown :: a } -> Down a |