diff options
Diffstat (limited to 'docs')
| -rw-r--r-- | docs/users_guide/8.12.1-notes.rst | 21 | ||||
| -rw-r--r-- | docs/users_guide/exts/explicit_forall.rst | 77 | ||||
| -rw-r--r-- | docs/users_guide/exts/gadt_syntax.rst | 117 |
3 files changed, 215 insertions, 0 deletions
diff --git a/docs/users_guide/8.12.1-notes.rst b/docs/users_guide/8.12.1-notes.rst index 38b20df1f8..22b9e0b571 100644 --- a/docs/users_guide/8.12.1-notes.rst +++ b/docs/users_guide/8.12.1-notes.rst @@ -103,6 +103,27 @@ Language instantiated through visible type application. More information can be found here: :ref:`Manually-defining-inferred-variables`. +* GADT constructor types now properly adhere to :ref:`forall-or-nothing`. As + a result, GHC will now reject some GADT constructors that previous versions + of GHC would accept, such as the following: :: + + data T where + MkT1 :: (forall a. a -> b -> T) + MkT2 :: (forall a. a -> T) + + ``MkT1`` and ``MkT2`` are rejected because the lack of an outermost + ``forall`` triggers implicit quantification, making the explicit ``forall``s + nested. Furthermore, GADT constructors do not permit the use of nested + ``forall``s, as explained in :ref:`formal-gadt-syntax`. + + In addition to rejecting nested ``forall``s, GHC is now more stringent about + rejecting uses of nested *contexts* in GADT constructors. For example, the + following example, which previous versions of GHC would accept, is now + rejected: + + data U a where + MkU :: (Show a => U a) + Compiler ~~~~~~~~ diff --git a/docs/users_guide/exts/explicit_forall.rst b/docs/users_guide/exts/explicit_forall.rst index 38c6e0f441..6b4fc9cef7 100644 --- a/docs/users_guide/exts/explicit_forall.rst +++ b/docs/users_guide/exts/explicit_forall.rst @@ -45,4 +45,81 @@ Notes: would warn about the unused type variable `a`. +.. _forall-or-nothing: + +The ``forall``-or-nothing rule +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +In certain forms of types, type variables obey what is known as the +"``forall``-or-nothing" rule: if a type has an outermost, explicit +``forall``, then all of the type variables in the type must be explicitly +quantified. These two examples illustrate how the rule works: :: + + f :: forall a b. a -> b -> b -- OK, `a` and `b` are explicitly bound + g :: forall a. a -> forall b. b -> b -- OK, `a` and `b` are explicitly bound + h :: forall a. a -> b -> b -- Rejected, `b` is not in scope + +The type signatures for ``f``, ``g``, and ``h`` all begin with an outermost +``forall``, so every type variable in these signatures must be explicitly +bound by a ``forall``. Both ``f`` and ``g`` obey the ``forall``-or-nothing +rule, since they explicitly quantify ``a`` and ``b``. On the other hand, +``h`` does not explicitly quantify ``b``, so GHC will reject its type +signature for being improperly scoped. + +In places where the ``forall``-or-nothing rule takes effect, if a type does +*not* have an outermost ``forall``, then any type variables that are not +explicitly bound by a ``forall`` become implicitly quantified. For example: :: + + i :: a -> b -> b -- `a` and `b` are implicitly quantified + j :: a -> forall b. b -> b -- `a` is implicitly quantified + k :: (forall a. a -> b -> b) -- `b` is implicitly quantified + +GHC will accept ``i``, ``j``, and ``k``'s type signatures. Note that: + +- ``j``'s signature is accepted despite its mixture of implicit and explicit + quantification. As long as a ``forall`` is not an outermost one, it is fine + to use it among implicitly bound type variables. +- ``k``'s signature is accepted because the outermost parentheses imply that + the ``forall`` is not an outermost ``forall``. The ``forall``-or-nothing + rule is one of the few places in GHC where the presence or absence of + parentheses can be semantically significant! + +The ``forall``-or-nothing rule takes effect in the following places: + +- Type signature declarations for functions, values, and class methods +- Expression type annotations +- Instance declarations +- :ref:`class-default-signatures` +- Type signatures in a :ref:`specialize-pragma` or + :ref:`specialize-instance-pragma` +- :ref:`standalone-kind-signatures` +- Type signatures for :ref:`gadt` constructors +- Type signatures for :ref:`pattern-synonyms` +- :ref:`data-instance-declarations`, :ref:`type-instance-declarations`, + :ref:`closed-type-families`, and :ref:`assoc-inst` +- :ref:`rewrite-rules` in which the type variables are explicitly quantified +Notes: + +- :ref:`pattern-type-sigs` are a notable example of a place where + types do *not* obey the ``forall``-or-nothing rule. For example, GHC will + accept the following: :: + + f (g :: forall a. a -> b) x = g x :: b + + Furthermore, :ref:`rewrite-rules` do not obey the ``forall``-or-nothing rule + when their type variables are not explicitly quantified: :: + + {-# RULES "f" forall (g :: forall a. a -> b) x. f g x = g x :: b #-} + +- GADT constructors are extra particular about their ``forall``s. In addition + to adhering to the ``forall``-or-nothing rule, GADT constructors also forbid + nested ``forall``s. For example, GHC would reject the following GADT: :: + + data T where + MkT :: (forall a. a -> b -> T) + + Because of the lack of an outermost ``forall`` in the type of ``MkT``, the + ``b`` would be implicitly quantified. In effect, it would be as if one had + written ``MkT :: forall b. (forall a. a -> b -> T)``, which contains nested + ``forall``s. See :ref:`formal-gadt-syntax`. diff --git a/docs/users_guide/exts/gadt_syntax.rst b/docs/users_guide/exts/gadt_syntax.rst index f89888ff3b..9b20c27ab1 100644 --- a/docs/users_guide/exts/gadt_syntax.rst +++ b/docs/users_guide/exts/gadt_syntax.rst @@ -103,6 +103,123 @@ 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. +.. _formal-gadt-syntax: + +Formal syntax for GADTs +~~~~~~~~~~~~~~~~~~~~~~~ + +To make more precise what is and what is not permitted inside of a GADT-style +constructor, we provide a BNF-style grammar for GADT below. Note that this +grammar is subject to change in the future. :: + + gadt_con ::= conids '::' opt_forall opt_ctxt gadt_body + + conids ::= conid + | conid ',' conids + + opt_forall ::= <empty> + | 'forall' tv_bndrs '.' + + tv_bndrs ::= <empty> + | tv_bndr tv_bndrs + + tv_bndr ::= tyvar + | '(' tyvar '::' ctype ')' + + opt_ctxt ::= <empty> + | btype '=>' + | '(' ctxt ')' '=>' + + ctxt ::= ctype + | ctype ',' ctxt + + gadt_body ::= prefix_gadt_body + | record_gadt_body + + prefix_gadt_body ::= '(' prefix_gadt_body ')' + | return_type + | opt_unpack btype '->' prefix_gadt_body + + record_gadt_body ::= '{' fieldtypes '}' '->' return_type + + fieldtypes ::= <empty> + | fieldnames '::' opt_unpack ctype + | fieldnames '::' opt_unpack ctype ',' fieldtypes + + fieldnames ::= fieldname + | fieldname ',' fieldnames + + opt_unpack ::= opt_bang + : {-# UNPACK #-} opt_bang + | {-# NOUNPACK #-} opt_bang + + opt_bang ::= <empty> + | '!' + | '~' + +Where: + +- ``btype`` is a type that is not allowed to have an outermost + ``forall``/``=>`` unless it is surrounded by parentheses. For example, + ``forall a. a`` and ``Eq a => a`` are not legal ``btype``s, but + ``(forall a. a)`` and ``(Eq a => a)`` are legal. +- ``ctype`` is a ``btype`` that has no restrictions on an outermost + ``forall``/``=>``, so ``forall a. a`` and ``Eq a => a`` are legal ``ctype``s. +- ``return_type`` is a type that is not allowed to have ``forall``s, ``=>``s, + or ``->``s. + +This is a simplified grammar that does not fully delve into all of the +implementation details of GHC's parser (such as the placement of Haddock +comments), but it is sufficient to attain an understanding of what is +syntactically allowed. Some further various observations about this grammar: + +- GADT constructor types are currently not permitted to have nested ``forall``s + or ``=>``s. (e.g., something like ``MkT :: Int -> forall a. a -> T`` would be + rejected.) As a result, ``gadt_sig`` puts all of its quantification and + constraints up front with ``opt_forall`` and ``opt_context``. Note that + higher-rank ``forall``s and ``=>``s are only permitted if they do not appear + directly to the right of a function arrow in a `prefix_gadt_body`. (e.g., + something like ``MkS :: Int -> (forall a. a) -> S`` is allowed, since + parentheses separate the ``forall`` from the ``->``.) +- Furthermore, GADT constructors do not permit outermost parentheses that + surround the ``opt_forall`` or ``opt_ctxt``, if at least one of them are + used. For example, ``MkU :: (forall a. a -> U)`` would be rejected, since + it would treat the ``forall`` as being nested. + + Note that it is acceptable to use parentheses in a ``prefix_gadt_body``. + For instance, ``MkV1 :: forall a. (a) -> (V1)`` is acceptable, as is + ``MkV2 :: forall a. (a -> V2)``. +- The function arrows in a ``prefix_gadt_body``, as well as the function + arrow in a ``record_gadt_body``, are required to be used infix. For + example, ``MkA :: (->) Int A`` would be rejected. +- GHC uses the function arrows in a ``prefix_gadt_body`` and + ``prefix_gadt_body`` to syntactically demarcate the function and result + types. Note that GHC does not attempt to be clever about looking through + type synonyms here. If you attempt to do this, for instance: :: + + type C = Int -> B + + data B where + MkB :: C + + Then GHC will interpret the return type of ``MkB`` to be ``C``, and since + GHC requires that the return type must be headed by ``B``, this will be + rejected. On the other hand, it is acceptable to use type synonyms within + the argument and result types themselves, so the following is permitted: :: + + type B1 = Int + type B2 = B + + data B where + MkB :: B1 -> B2 +- GHC will accept any combination of ``!``/``~`` and + ``{-# UNPACK #-}``/``{-# NOUNPACK #-}``, although GHC will ignore some + combinations. For example, GHC will produce a warning if you write + ``{-# UNPACK #-} ~Int`` and proceed as if you had written ``Int``. + +GADT syntax odds and ends +~~~~~~~~~~~~~~~~~~~~~~~~~ + The rest of this section gives further details about GADT-style data type declarations. |