.. _explicit-foralls:

Explicit universal quantification (forall)
------------------------------------------

.. extension:: ExplicitForAll
    :shortdesc: Enable explicit universal quantification.
        Implied by :extension:`ScopedTypeVariables`, :extension:`LiberalTypeSynonyms`,
        :extension:`RankNTypes` and :extension:`ExistentialQuantification`.

    :since: 6.12.1

    Allow use of the ``forall`` keyword in places where universal quantification
    is implicit.

Haskell type signatures are implicitly quantified. When the language
option :extension:`ExplicitForAll` is used, the keyword ``forall`` allows us to
say exactly what this means. For example: ::

    g :: b -> b

means this: ::

    g :: forall b. (b -> b)

The two are treated identically, except that the latter may bring type variables
into scope (see :ref:`scoped-type-variables`).

This extension also enables explicit quantification of type and kind variables
in :ref:`data-instance-declarations`, :ref:`type-instance-declarations`,
:ref:`closed-type-families`, :ref:`assoc-inst`, and :ref:`rewrite-rules`.

Notes:

- As well as in type signatures, you can also use an explicit ``forall``
  in an instance declaration: ::

      instance forall a. Eq a => Eq [a] where ...

  Note that the use of ``forall``\s in instance declarations is somewhat
  restricted in comparison to other types. For example, instance declarations
  are not allowed to contain nested ``forall``\s. See
  :ref:`formal-instance-syntax` for more information.

- If the :ghc-flag:`-Wunused-foralls` flag is enabled, a warning will be emitted
  when you write a type variable in an explicit ``forall`` statement that is
  otherwise unused. For instance: ::

    g :: forall a b. (b -> b)

  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,
invisible ``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
invisible ``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 invisible ``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
  type L :: forall a -> b -> b -- `b` is implicitly quantified

GHC will accept ``i``, ``j``, and ``k``'s type signatures, as well as ``L``'s
kind signature. 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!
- ``L``'s signature begins with an outermost ``forall``, but it is a *visible*
  ``forall``, not an invisible ``forall``, and therefore does not trigger the
  ``forall``-or-nothing rule.

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