User's Guide: forall is a keyword nowadays
[ghc.git] / docs / users_guide / glasgow_exts.rst
index 1963503..eae0283 100644 (file)
@@ -743,7 +743,7 @@ follows:
       view pattern expression are in scope. For example: ::
 
           example :: Maybe ((String -> Integer,Integer), String) -> Bool
-          example Just ((f,_), f -> 4) = True
+          example (Just ((f,_), f -> 4)) = True
 
       Additionally, in function definitions, variables bound by matching
       earlier curried arguments may be used in view pattern expressions
@@ -1642,9 +1642,12 @@ not the Prelude versions:
 -  An integer literal ``368`` means "``fromInteger (368::Integer)``",
    rather than "``Prelude.fromInteger (368::Integer)``".
 
--  Fractional literals are handed in just the same way, except that the
+-  Fractional literals are handled in just the same way, except that the
    translation is ``fromRational (3.68::Rational)``.
 
+-  String literals are also handled the same way, except that the
+   translation is ``fromString ("368"::String)``.
+
 -  The equality test in an overloaded numeric pattern uses whatever
    ``(==)`` is in scope.
 
@@ -2233,9 +2236,10 @@ The following syntax is stolen:
     .. index::
        single: forall
 
-    Stolen (in types) by: :extension:`ExplicitForAll`, and hence by
-    :extension:`ScopedTypeVariables`, :extension:`LiberalTypeSynonyms`,
-    :extension:`RankNTypes`, :extension:`ExistentialQuantification`
+    Stolen (in types) by default (see :ref:`infelicities-lexical`). ``forall`` is
+    a reserved keyword and never a type variable, in accordance with `GHC Proposal #43
+    <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0043-forall-keyword.rst>`__.
+
 
 ``mdo``
     .. index::
@@ -5876,8 +5880,7 @@ The superclasses of a class declaration
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 .. extension:: FlexibleContexts
-    :shortdesc: Enable flexible contexts. Implied by
-        :extension:`ImplicitParams`.
+    :shortdesc: Enable flexible contexts.
 
     :since: 6.8.1
 
@@ -6461,7 +6464,6 @@ Relaxed rules for the instance head
 .. extension:: FlexibleInstances
     :shortdesc: Enable flexible instances.
         Implies :extension:`TypeSynonymInstances`.
-        Implied by :extension:`ImplicitParams`.
 
     :implies: :extension:`TypeSynonymInstances`
     :since: 6.8.1
@@ -7574,13 +7576,13 @@ can be any number.
 
 When :extension:`ExplicitForAll` is enabled, type or kind variables used on
 the left hand side can be explicitly bound. For example: ::
-  
+
     data instance forall a (b :: Proxy a). F (Proxy b) = FProxy Bool
 
-When an explicit ``forall`` is present, all *type* variables mentioned must
-be bound by the ``forall``. Kind variables will be implicitly bound if
-necessary, for example: ::
-  
+When an explicit ``forall`` is present, all *type* variables mentioned which
+are not already in scope must be bound by the ``forall``. Kind variables will
+be implicitly bound if necessary, for example: ::
+
     data instance forall (a :: k). F a = FOtherwise
 
 When the flag :ghc-flag:`-Wunused-type-patterns` is enabled, type
@@ -8099,13 +8101,13 @@ Note the following points:
    cannot give any *subsequent* instances for ``(GMap Flob ...)``, this
    facility is most useful when the free indexed parameter is of a kind
    with a finite number of alternatives (unlike ``Type``).
-   
+
 -  When :extension:`ExplicitForAll` is enabled, type and kind variables can be
    explicily bound in associated data or type family instances in the same way
    (and with the same restrictions) as :ref:`data-instance-declarations` or
    :ref:`type-instance-declarations`. For example, adapting the above, the
    following is accepted: ::
-     
+
      instance Eq (Elem [e]) => Collects [e] where
        type forall e. Elem [e] = e
 
@@ -8144,7 +8146,7 @@ Note the following points:
    variables that are explicitly bound on the left hand side. This restriction
    is relaxed for *kind* variables, however, as the right hand side is allowed
    to mention kind variables that are implicitly bound on the left hand side.
-   
+
    Because of this, unlike :ref:`assoc-inst`, explicit binding of type/kind
    variables in default declarations is not permitted by
    :extension:`ExplicitForAll`.
@@ -8785,8 +8787,9 @@ Kind polymorphism
     :implies: :extension:`PolyKinds`, :extension:`DataKinds`, :extension:`KindSignatures`
     :since: 8.0.1
 
-    In the past this extension used to enable advanced type-level programming
-    techniques. Now it's a shorthand for a couple of other extensions.
+    The extension :extension:`TypeInType` is now deprecated: its sole effect is
+    to switch on :extension:`PolyKinds`
+    (and hence :extension:`KindSignatures`) and :extension:`DataKinds`.
 
 .. extension:: PolyKinds
     :shortdesc: Enable kind polymorphism.
@@ -8879,18 +8882,18 @@ using kind signatures: ::
 
 The general principle is this:
 
--  *When there is a right-hand side, GHC infers the most polymorphic
-   kind consistent with the right-hand side.* Examples: ordinary data
+-  When there is a right-hand side, GHC infers the most polymorphic
+   kind consistent with the right-hand side. Examples: ordinary data
    type and GADT declarations, class declarations. In the case of a
    class declaration the role of "right hand side" is played by the
    class method signatures.
 
--  *When there is no right hand side, GHC defaults argument and result
-   kinds to ``Type``, except when directed otherwise by a kind signature*.
+-  When there is no right hand side, GHC defaults argument and result
+   kinds to ``Type``, except when directed otherwise by a kind signature.
    Examples: data and open type family declarations.
 
 This rule has occasionally-surprising consequences (see
-:ghc-ticket:`10132`. ::
+:ghc-ticket:`10132`). ::
 
     class C a where    -- Class declarations are generalised
                        -- so C :: forall k. k -> Constraint
@@ -8904,6 +8907,78 @@ This rule has occasionally-surprising consequences (see
 The kind-polymorphism from the class declaration makes ``D1``
 kind-polymorphic, but not so ``D2``; and similarly ``F1``, ``F1``.
 
+.. _inferring-variable-order:
+
+Inferring the order of variables in a type/class declaration
+------------------------------------------------------------
+
+It is possible to get intricate dependencies among the type variables
+introduced in a type or class declaration. Here is an example::
+
+  data T a (b :: k) c = MkT (a c)
+
+After analysing this declaration, GHC will discover that ``a`` and
+``c`` can be kind-polymorphic, with ``a :: k2 -> Type`` and
+``c :: k2``. We thus infer the following kind::
+
+  T :: forall {k2 :: Type} (k :: Type). (k2 -> Type) -> k -> k2 -> Type
+
+Note that ``k2`` is placed *before* ``k``, and that ``k`` is placed *before*
+``a``. Also, note that ``k2`` is written here in braces. As explained with
+:extension:`TypeApplications` (:ref:`inferred-vs-specified`),
+type and kind variables that GHC generalises
+over, but not written in the original program, are not available for visible
+type application. (These are called *inferred* variables.)
+Such variables are written in braces with
+:ghc-flag:`-fprint-explicit-foralls` enabled.
+
+The general principle is this:
+
+  * Variables not available for type application come first.
+
+  * Then come variables the user has written, implicitly brought into scope
+    in a type variable's kind.
+
+  * Lastly come the normal type variables of a declaration.
+
+  * Variables not given an explicit ordering by the user are sorted according
+    to ScopedSort (:ref:`ScopedSort`).
+
+With the ``T`` example above, we could bind ``k`` *after* ``a``; doing so
+would not violate dependency concerns. However, it would violate our general
+principle, and so ``k`` comes first.
+
+Sometimes, this ordering does not respect dependency. For example::
+
+  data T2 k (a :: k) (c :: Proxy '[a, b])
+
+It must be that ``a`` and ``b`` have the same kind. Note also that ``b``
+is implicitly declared in ``c``\'s kind. Thus, according to our general
+principle, ``b`` must come *before* ``k``. However, ``b`` *depends on*
+``k``. We thus reject ``T2`` with a suitable error message.
+
+In associated types, we order the type variables as if the type family was a
+top-level declaration, ignoring the visibilities of the class's type variable
+binders. Here is an example: ::
+
+  class C (a :: k) b where
+    type F (c :: j) (d :: Proxy m) a b
+
+We infer these kinds::
+
+  C :: forall {k1 :: Type} (k :: Type). k -> k1 -> Constraint
+  F :: forall {k1 :: Type} {k2 :: Type} {k3 :: Type} j (m :: k1).
+       j -> Proxy m -> k2 -> k3 -> Type
+
+Note that the kind of ``a`` is specified in the kind of ``C`` but inferred in
+the kind of ``F``.
+
+The "general principle" described here is meant to make all this more
+predictable for users. It would not be hard to extend GHC to relax
+this principle. If you should want a change here, consider writing
+a `proposal <https://github.com/ghc-proposals/ghc-proposals/>`_ to
+do so.
+
 .. index::
    single: CUSK
    single: complete user-supplied kind signature
@@ -9205,9 +9280,8 @@ distinction). GHC does not consider ``forall k. k -> Type`` and
 Constraints in kinds
 --------------------
 
-As kinds and types are the same, kinds can (with :extension:`PolyKinds`)
-contain type constraints. Only equality constraints are currently supported,
-however. We expect this to extend to other constraints in the future.
+As kinds and types are the same, kinds can (with :extension:`TypeInType`)
+contain type constraints. However, only equality constraints are supported.
 
 Here is an example of a constrained kind: ::
 
@@ -9360,8 +9434,8 @@ Here are the key definitions, all available from ``GHC.Exts``: ::
   data RuntimeRep = LiftedRep     -- for things like `Int`
                   | UnliftedRep   -- for things like `Array#`
                   | IntRep        -- for `Int#`
-                 | TupleRep [RuntimeRep]  -- unboxed tuples, indexed by the representations of the elements
-                 | SumRep [RuntimeRep]    -- unboxed sums, indexed by the representations of the disjuncts
+                  | TupleRep [RuntimeRep]  -- unboxed tuples, indexed by the representations of the elements
+                  | SumRep [RuntimeRep]    -- unboxed sums, indexed by the representations of the disjuncts
                   | ...
 
   type Type = TYPE LiftedRep    -- Type is just an ordinary type synonym
@@ -9653,7 +9727,7 @@ denotes representational equality between ``t1`` and ``t2`` in the sense
 of Roles (:ref:`roles`). It is exported by :base-ref:`Data.Coerce.`, which also
 contains the documentation. More details and discussion can be found in the
 paper
-`"Safe Coercions" <http://www.cis.upenn.edu/~eir/papers/2014/coercible/coercible.pdf>`__.
+`"Safe Coercions" <https://www.microsoft.com/en-us/research/uploads/prod/2018/05/coercible-JFP.pdf>`__.
 
 .. _constraint-kind:
 
@@ -10032,9 +10106,6 @@ in :ref:`data-instance-declarations`, :ref:`type-instance-declarations`,
 
 Notes:
 
-- With :extension:`ExplicitForAll`, ``forall`` becomes a keyword; you can't use ``forall`` as a
-  type variable any more!
-
 - As well in type signatures, you can also use an explicit ``forall``
   in an instance declaration: ::
 
@@ -10633,7 +10704,7 @@ Visible type application
 ========================
 
 .. extension:: TypeApplications
-    :shortdesc: Enable type application syntax.
+    :shortdesc: Enable type application syntax in terms and types.
 
     :since: 8.0.1
 
@@ -10654,14 +10725,112 @@ is an identifier (the common case), its type is considered known only when
 the identifier has been given a type signature. If the identifier does
 not have a type signature, visible type application cannot be used.
 
-Here are the details:
+GHC also permits visible kind application, where users can declare the kind
+arguments to be instantiated in kind-polymorphic cases. Its usage parallels
+visible type application in the term level, as specified above.
+
+.. _inferred-vs-specified:
 
-- If an identifier's type signature does not include an
-  explicit ``forall``, the type variable arguments appear
-  in the left-to-right order in which the variables appear in the type.
-  So, ``foo :: Monad m => a b -> m (a c)``
-  will have its type variables
-  ordered as ``m, a, b, c``.
+Inferred vs. specified type variables
+-------------------------------------
+
+.. index::
+   single: type variable; inferred vs. specified
+
+GHC tracks a distinction between what we call *inferred* and *specified*
+type variables. Only specified type variables are available for instantiation
+with visible type application. An example illustrates this well::
+
+  f :: (Eq b, Eq a) => a -> b -> Bool
+  f x y = (x == x) && (y == y)
+
+  g x y = (x == x) && (y == y)
+
+The functions ``f`` and ``g`` have the same body, but only ``f`` is given
+a type signature. When GHC is figuring out how to process a visible type application,
+it must know what variable to instantiate. It thus must be able to provide
+an ordering to the type variables in a function's type.
+
+If the user has supplied a type signature, as in ``f``, then this is easy:
+we just take the ordering from the type signature, going left to right and
+using the first occurrence of a variable to choose its position within the
+ordering. Thus, the variables in ``f`` will be ``b``, then ``a``.
+
+In contrast, there is no reliable way to do this for ``g``; we will not know
+whether ``Eq a`` or ``Eq b`` will be listed first in the constraint in ``g``\'s
+type. In order to have visible type application be robust between releases of
+GHC, we thus forbid its use with ``g``.
+
+We say that the type variables in ``f`` are *specified*, while those in
+``g`` are *inferred*. The general rule is this: if the user has written
+a type variable in the source program, it is *specified*; if not, it is
+*inferred*.
+
+Thus rule applies in datatype declarations, too. For example, if we have
+``data Proxy a = Proxy`` (and :extension:`PolyKinds` is enabled), then
+``a`` will be assigned kind ``k``, where ``k`` is a fresh kind variable.
+Because ``k`` was not written by the user, it will be unavailable for
+type application in the type of the constructor ``Proxy``; only the ``a``
+will be available.
+
+When :ghc-flag:`-fprint-explicit-foralls` is enabled, inferred variables
+are printed in braces. Thus, the type of the data constructor ``Proxy``
+from the previous example would be ``forall {k} (a :: k). Proxy a``.
+We can observe this behavior in a GHCi session: ::
+
+  > :set -XTypeApplications -fprint-explicit-foralls
+  > let myLength1 :: Foldable f => f a -> Int; myLength1 = length
+  > :type +v myLength1
+  myLength1 :: forall (f :: * -> *) a. Foldable f => f a -> Int
+  > let myLength2 = length
+  > :type +v myLength2
+  myLength2 :: forall {a} {t :: * -> *}. Foldable t => t a -> Int
+  > :type +v myLength2 @[]
+
+  <interactive>:1:1: error:
+      • Cannot apply expression of type ‘t0 a0 -> Int’
+        to a visible type argument ‘[]’
+      • In the expression: myLength2 @[]
+
+Notice that since ``myLength1`` was defined with an explicit type signature,
+:ghci-cmd:`:type +v` reports that all of its type variables are available
+for type application. On the other hand, ``myLength2`` was not given a type
+signature. As a result, all of its type variables are surrounded with braces,
+and trying to use visible type application with ``myLength2`` fails.
+
+Also note the use of :ghci-cmd:`:type +v` in the GHCi session above instead
+of :ghci-cmd:`:type`. This is because :ghci-cmd:`:type` gives you the type
+that would be inferred for a variable assigned to the expression provided
+(that is, the type of ``x`` in ``let x = <expr>``). As we saw above with
+``myLength2``, this type will have no variables available to visible type
+application. On the other hand, :ghci-cmd:`:type +v` gives you the actual
+type of the expression provided. To illustrate this: ::
+
+  > :type myLength1
+  myLength1 :: forall {a} {f :: * -> *}. Foldable f => f a -> Int
+  > :type myLength2
+  myLength2 :: forall {a} {t :: * -> *}. Foldable t => t a -> Int
+
+Using :ghci-cmd:`:type` might lead one to conclude that none of the type
+variables in ``myLength1``'s type signature are available for type
+application. This isn't true, however! Be sure to use :ghci-cmd:`:type +v`
+if you want the most accurate information with respect to visible type
+application properties.
+
+.. index::
+   single: ScopedSort
+
+.. _ScopedSort:
+
+Ordering of specified variables
+-------------------------------
+
+In the simple case of the previous section, we can say that specified variables
+appear in left-to-right order. However, not all cases are so simple. Here are
+the rules in the subtler cases:
+
+- If an identifier's type has a ``forall``, then the order of type variables
+  as written in the ``forall`` is retained.
 
 - If the type signature includes any kind annotations (either on variable
   binders or as annotations on types), any variables used in kind
@@ -10680,7 +10849,7 @@ Here are the details:
   of the variables are *kind* variables), the variables are reordered
   so that kind variables come before type variables, preserving the
   left-to-right order as much as possible. That is, GHC performs a
-  stable topological sort on the variables. Examples::
+  stable topological sort on the variables. Example::
 
     h :: Proxy (a :: (j, k)) -> Proxy (b :: Proxy a) -> ()
       -- as if h :: forall j k a b. ...
@@ -10693,10 +10862,12 @@ Here are the details:
   are not reordered with respect to each other, even though doing so would
   not violate dependency conditions.
 
-- Visible type application is available to instantiate only user-specified
-  type variables. This means that in ``data Proxy a = Proxy``, the unmentioned
-  kind variable used in ``a``'s kind is *not* available for visible type
-  application.
+  A "stable topological sort" here, we mean that we perform this algorithm
+  (which we call *ScopedSort*):
+
+  * Work left-to-right through the input list of type variables, with a cursor.
+  * If variable ``v`` at the cursor is depended on by any earlier variable ``w``,
+    move ``v`` immediately before the leftmost such ``w``.
 
 - Class methods' type arguments include the class type
   variables, followed by any variables an individual method is polymorphic
@@ -10715,75 +10886,12 @@ Here are the details:
   application. If you want to specify only the second type argument to
   ``wurble``, then you can say ``wurble @_ @Int``.
   The first argument is a wildcard, just like in a partial type signature.
-  However, if used in a visible type application, it is *not*
-  necessary to specify :extension:`PartialTypeSignatures` and your
+  However, if used in a visible type application/visible kind application,
+  it is *not* necessary to specify :extension:`PartialTypeSignatures` and your
   code will not generate a warning informing you of the omitted type.
 
-- When printing types with :ghc-flag:`-fprint-explicit-foralls` enabled,
-  type variables not available for visible type application are printed
-  in braces. We can observe this behavior in a GHCi session: ::
-
-    > :set -XTypeApplications -fprint-explicit-foralls
-    > let myLength1 :: Foldable f => f a -> Int; myLength1 = length
-    > :type +v myLength1
-    myLength1 :: forall (f :: * -> *) a. Foldable f => f a -> Int
-    > let myLength2 = length
-    > :type +v myLength2
-    myLength2 :: forall {a} {t :: * -> *}. Foldable t => t a -> Int
-    > :type +v myLength2 @[]
-
-    <interactive>:1:1: error:
-        • Cannot apply expression of type ‘t0 a0 -> Int’
-          to a visible type argument ‘[]’
-        • In the expression: myLength2 @[]
-
-  Notice that since ``myLength1`` was defined with an explicit type signature,
-  :ghci-cmd:`:type +v` reports that all of its type variables are available
-  for type application. On the other hand, ``myLength2`` was not given a type
-  signature. As a result, all of its type variables are surrounded with braces,
-  and trying to use visible type application with ``myLength2`` fails.
-
-  Also note the use of :ghci-cmd:`:type +v` in the GHCi session above instead
-  of :ghci-cmd:`:type`. This is because :ghci-cmd:`:type` gives you the type
-  that would be inferred for a variable assigned to the expression provided
-  (that is, the type of ``x`` in ``let x = <expr>``). As we saw above with
-  ``myLength2``, this type will have no variables available to visible type
-  application. On the other hand, :ghci-cmd:`:type +v` gives you the actual
-  type of the expression provided. To illustrate this: ::
-
-    > :type myLength1
-    myLength1 :: forall {a} {f :: * -> *}. Foldable f => f a -> Int
-    > :type myLength2
-    myLength2 :: forall {a} {t :: * -> *}. Foldable t => t a -> Int
-
-  Using :ghci-cmd:`:type` might lead one to conclude that none of the type
-  variables in ``myLength1``'s type signature are available for type
-  application. This isn't true, however! Be sure to use :ghci-cmd:`:type +v`
-  if you want the most accurate information with respect to visible type
-  application properties.
-
-- Although GHC supports visible *type* applications, it does not yet support
-  visible *kind* applications. However, GHC does follow similar rules for
-  quantifying variables in kind signatures as it does for quantifying type
-  signatures. For instance: ::
-
-    type family F (a :: j) (b :: k) :: l
-      -- F :: forall j k l. j -> k -> l
-
-  In the kind of ``F``, the left-to-right ordering of ``j``, ``k``, and ``l``
-  is preserved.
-
-  If a family declaration is associated with a class, then class-bound
-  variables always come first in the kind of the family. For instance: ::
-
-    class C (a :: Type) where
-      type T (x :: f a)
-      -- T :: forall a f. f a -> Type
-
-  Contrast this with the kind of the following top-level family declaration: ::
-
-    type family T2 (x :: f a)
-    -- T2 :: forall f a. f a -> Type
+The section in this manual on kind polymorphism describes how variables
+in type and class declarations are ordered (:ref:`inferring-variable-order`).
 
 .. _implicit-parameters:
 
@@ -10792,7 +10900,6 @@ Implicit parameters
 
 .. extension:: ImplicitParams
     :shortdesc: Enable Implicit Parameters.
-        Implies :extension:`FlexibleContexts` and :extension:`FlexibleInstances`.
 
     :since: 6.8.1
 
@@ -11793,7 +11900,7 @@ fixing the hole, this can help users understand what options they have.
 
 .. ghc-flag:: -fabstract-refinement-hole-fits
     :shortdesc: *default: off.* Toggles whether refinements where one or more
-         or more of the holes are abstract are reported.
+         of the holes are abstract are reported.
     :type: dynamic
     :reverse: -fno-abstract-refinement-hole-fits
     :category: verbosity
@@ -12165,10 +12272,10 @@ Anonymous and named wildcards *can* occur on the left hand side of a
 type or data instance declaration;
 see :ref:`type-wildcards-lhs`.
 
-Anonymous wildcards are also allowed in visible type applications
-(:ref:`visible-type-application`). If you want to specify only the second type
-argument to ``wurble``, then you can say ``wurble @_ @Int`` where the first
-argument is a wildcard.
+Anonymous wildcards are also allowed in visible type applications/ visible kind
+applications (:ref:`visible-type-application`). If you want to specify only the
+second type argument to ``wurble``, then you can say ``wurble @_ @Int`` where
+the first argument is a wildcard.
 
 Standalone ``deriving`` declarations permit the use of a single,
 extra-constraints wildcard, like so: ::
@@ -14256,9 +14363,11 @@ Certain pragmas are *file-header pragmas*:
 ``LANGUAGE`` pragma
 -------------------
 
-.. index::
-   single: LANGUAGE; pragma
-   single: pragma; LANGUAGE
+.. pragma:: LANGUAGE ⟨ext⟩, ⟨ext⟩, ...
+
+    :where: file header
+
+    Enable or disable a set of language extensions.
 
 The ``LANGUAGE`` pragma allows language extensions to be enabled in a
 portable way. It is the intention that all Haskell compilers support the
@@ -14288,9 +14397,9 @@ if any of the requested extensions are not supported.
 ``OPTIONS_GHC`` pragma
 ----------------------
 
-.. index::
-   single: OPTIONS_GHC
-   single: pragma; OPTIONS_GHC
+.. pragma:: OPTIONS_GHC ⟨flags⟩
+
+    :where: file header
 
 The ``OPTIONS_GHC`` pragma is used to specify additional options that
 are given to the compiler when compiling this source file. See
@@ -14316,14 +14425,21 @@ other compilers.
 ``WARNING`` and ``DEPRECATED`` pragmas
 --------------------------------------
 
-.. index::
-   single: WARNING
-   single: DEPRECATED
+.. pragma:: WARNING
+
+    :where: declaration
+
+    The ``WARNING`` pragma allows you to attach an arbitrary warning to a
+    particular function, class, or type.
 
-The ``WARNING`` pragma allows you to attach an arbitrary warning to a
-particular function, class, or type. A ``DEPRECATED`` pragma lets you
-specify that a particular function, class, or type is deprecated. There
-are two ways of using these pragmas.
+.. pragma:: DEPRECATED
+
+    :where: declaration
+
+    A ``DEPRECATED`` pragma lets you specify that a particular function, class,
+    or type is deprecated.
+
+There are two ways of using these pragmas.
 
 -  You can work on an entire module thus: ::
 
@@ -14374,9 +14490,11 @@ You can suppress the warnings with the flag
 ``MINIMAL`` pragma
 ------------------
 
-.. index::
-   single: MINIMAL
-   single: pragma; MINIMAL
+.. pragma:: MINIMAL ⟨name⟩ | ⟨name⟩ , ...
+
+    :where: in class body
+
+    Define the methods needed for a minimal complete instance of a class.
 
 The ``MINIMAL`` pragma is used to specify the minimal complete definition of
 a class, i.e. specify which methods must be implemented by all
@@ -14425,9 +14543,11 @@ These pragmas control the inlining of function definitions.
 ``INLINE`` pragma
 ~~~~~~~~~~~~~~~~~
 
-.. index::
-   single: INLINE
-   single: pragma; INLINE
+.. pragma:: INLINE ⟨name⟩
+
+    :where: top-level
+
+    Force GHC to inline a value.
 
 GHC (with :ghc-flag:`-O`, as always) tries to inline (or "unfold")
 functions/values that are "small enough," thus avoiding the call
@@ -14491,7 +14611,7 @@ has a number of other effects:
    which will optimise better than the corresponding use of ``comp2``.
 
 -  It is useful for GHC to optimise the definition of an INLINE function
-   ``f`` just like any other non-INLINE function, in case the
+   ``f`` just like any other non-``INLINE`` function, in case the
    non-inlined version of ``f`` is ultimately called. But we don't want
    to inline the *optimised* version of ``f``; a major reason for ``INLINE``
    pragmas is to expose functions in ``f``\'s RHS that have rewrite
@@ -14504,7 +14624,7 @@ has a number of other effects:
    usual. For externally-visible functions the inline-RHS (not the
    optimised RHS) is recorded in the interface file.
 
--  An INLINE function is not worker/wrappered by strictness analysis.
+-  An ``INLINE`` function is not worker/wrappered by strictness analysis.
    It's going to be inlined wholesale instead.
 
 GHC ensures that inlining cannot go on forever: every mutually-recursive
@@ -14535,6 +14655,12 @@ See also the ``NOINLINE`` (:ref:`noinline-pragma`) and ``INLINABLE``
 ``INLINABLE`` pragma
 ~~~~~~~~~~~~~~~~~~~~
 
+.. pragma:: INLINABLE ⟨name⟩
+
+    :where: top-level
+
+    Suggest that the compiler always consider inlining ``name``.
+
 An ``{-# INLINABLE f #-}`` pragma on a function ``f`` has the following
 behaviour:
 
@@ -14574,10 +14700,15 @@ The alternative spelling ``INLINEABLE`` is also accepted by GHC.
 ~~~~~~~~~~~~~~~~~~~
 
 .. index::
-   single: NOINLINE
    single: NOTINLINE
 
-The ``NOINLINE`` pragma does exactly what you'd expect: it stops the
+.. pragma:: NOINLINE ⟨name⟩
+
+    :where: top-level
+
+    Instructs the compiler not to inline a value.
+
+The :pragma:`NOINLINE` pragma does exactly what you'd expect: it stops the
 named function from being inlined by the compiler. You shouldn't ever
 need to do this, unless you're very cautious about code size.
 
@@ -14590,23 +14721,26 @@ used if you want your code to be portable).
 ``CONLIKE`` modifier
 ~~~~~~~~~~~~~~~~~~~~
 
-.. index::
-   single: CONLIKE
+.. pragma:: CONLINE
+
+    :where: modifies :pragma:`INLINE` or :pragma:`NOINLINE` pragma
 
-An ``INLINE`` or ``NOINLINE`` pragma may have a ``CONLIKE`` modifier, which affects
-matching in RULEs (only). See :ref:`conlike`.
+    Instructs GHC to consider a value to be especially cheap to inline.
+
+An :pragma:`INLINE` or :pragma:`NOINLINE` pragma may have a :pragma:`CONLIKE` modifier, which affects
+matching in :pragma:`RULE`\s (only). See :ref:`conlike`.
 
 .. _phase-control:
 
 Phase control
 ~~~~~~~~~~~~~
 
-Sometimes you want to control exactly when in GHC's pipeline the ``INLINE``
+Sometimes you want to control exactly when in GHC's pipeline the :pragma:`INLINE`
 pragma is switched on. Inlining happens only during runs of the
 *simplifier*. Each run of the simplifier has a different *phase number*;
 the phase number decreases towards zero. If you use
-``-dverbose-core2core`` you'll see the sequence of phase numbers for
-successive runs of the simplifier. In an ``INLINE`` pragma you can
+:ghc-flag:`-dverbose-core2core` you will see the sequence of phase numbers for
+successive runs of the simplifier. In an :pragma:`INLINE` pragma you can
 optionally specify a phase number, thus:
 
 -  "``INLINE[k] f``" means: do not inline ``f`` until phase ``k``, but
@@ -14624,7 +14758,7 @@ optionally specify a phase number, thus:
 
 The same information is summarised here:
 
-::
+.. code-block:: none
 
                                -- Before phase 2     Phase 2 and later
       {-# INLINE   [2]  f #-}  --      No                 Yes
@@ -14639,14 +14773,14 @@ By "Maybe" we mean that the usual heuristic inlining rules apply (if the
 function body is small, or it is applied to interesting-looking
 arguments etc). Another way to understand the semantics is this:
 
--  For both ``INLINE`` and ``NOINLINE``, the phase number says when inlining is
-   allowed at all.
+-  For both :pragma:`INLINE` and :pragma:`NOINLINE`, the phase number says when
+   inlining is allowed at all.
 
--  The ``INLINE`` pragma has the additional effect of making the function
+-  The :pragma:`INLINE` pragma has the additional effect of making the function
    body look small, so that when inlining is allowed it is very likely
    to happen.
 
-The same phase-numbering control is available for RULES
+The same phase-numbering control is available for :pragma:`RULE`\s
 (:ref:`rewrite-rules`).
 
 .. _line-pragma:
@@ -14654,9 +14788,12 @@ The same phase-numbering control is available for RULES
 ``LINE`` pragma
 ---------------
 
-.. index::
-   single: LINE; pragma
-   single: pragma; LINE
+.. pragma:: LINE ⟨lineno⟩ "⟨file⟩"
+
+    :where: anywhere
+
+    Generated by preprocessors to convey source line numbers of the original
+    source.
 
 This pragma is similar to C's ``#line`` pragma, and is mainly for use in
 automatically generated Haskell code. It lets you specify the line
@@ -14704,7 +14841,7 @@ diagnostics and does not change the syntax of the code itself.
 ``RULES`` pragma
 ----------------
 
-The ``RULES`` pragma lets you specify rewrite rules. It is described in
+The :pragma:`RULES` pragma lets you specify rewrite rules. It is described in
 :ref:`rewrite-rules`.
 
 .. _specialize-pragma:
@@ -14717,8 +14854,12 @@ The ``RULES`` pragma lets you specify rewrite rules. It is described in
    single: pragma, SPECIALIZE
    single: overloading, death to
 
+.. pragma:: SPECIALIZE ⟨name⟩ :: ⟨type⟩
+
+    Ask that GHC specialize a polymorphic value to a particular type.
+
 (UK spelling also accepted.) For key overloaded functions, you can
-create extra versions (NB: more code space) specialised to particular
+create extra versions (NB: at the cost of larger code) specialised to particular
 types. Thus, if you have an overloaded function:
 
 ::
@@ -14815,6 +14956,10 @@ specialise it as follows:
 ``SPECIALIZE INLINE``
 ~~~~~~~~~~~~~~~~~~~~~
 
+.. pragma:: SPECIALIZE INLINE ⟨name⟩ :: ⟨type⟩
+
+    :where: top-level
+
 A ``SPECIALIZE`` pragma can optionally be followed with a ``INLINE`` or
 ``NOINLINE`` pragma, optionally followed by a phase, as described in
 :ref:`inline-noinline-pragma`. The ``INLINE`` pragma affects the
@@ -14840,9 +14985,9 @@ fire the first specialisation, whose body is also inlined. The result is
 a type-based unrolling of the indexing function.
 
 You can add explicit phase control (:ref:`phase-control`) to
-``SPECIALISE INLINE`` pragma, just like on an ``INLINE`` pragma; if you
-do so, the same phase is used for the rewrite rule and the INLINE
-control of the specialised function.
+``SPECIALISE INLINE`` pragma, just like on an :pragma:`INLINE` pragma; if you do
+so, the same phase is used for the rewrite rule and the INLINE control of the
+specialised function.
 
 .. warning:: You can make GHC diverge by using ``SPECIALISE INLINE`` on an
              ordinarily-recursive function.
@@ -14850,9 +14995,9 @@ control of the specialised function.
 ``SPECIALIZE`` for imported functions
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-Generally, you can only give a ``SPECIALIZE`` pragma for a function
+Generally, you can only give a :pragma:`SPECIALIZE` pragma for a function
 defined in the same module. However if a function ``f`` is given an
-``INLINABLE`` pragma at its definition site, then it can subsequently be
+:pragma:`INLINABLE` pragma at its definition site, then it can subsequently be
 specialised by importing modules (see :ref:`inlinable-pragma`). For example ::
 
     module Map( lookup, blah blah ) where
@@ -14866,7 +15011,7 @@ specialised by importing modules (see :ref:`inlinable-pragma`). For example ::
       data T = T1 | T2 deriving( Eq, Ord )
       {-# SPECIALISE lookup :: [(T,a)] -> T -> Maybe a
 
-Here, ``lookup`` is declared ``INLINABLE``, but it cannot be specialised
+Here, ``lookup`` is declared :pragma:`INLINABLE`, but it cannot be specialised
 for type ``T`` at its definition site, because that type does not exist
 yet. Instead a client module can define ``T`` and then specialise
 ``lookup`` at that type.
@@ -14874,13 +15019,13 @@ yet. Instead a client module can define ``T`` and then specialise
 Moreover, every module that imports ``Client`` (or imports a module that
 imports ``Client``, transitively) will "see", and make use of, the
 specialised version of ``lookup``. You don't need to put a
-``SPECIALIZE`` pragma in every module.
+:pragma:`SPECIALIZE` pragma in every module.
 
-Moreover you often don't even need the ``SPECIALIZE`` pragma in the
+Moreover you often don't even need the :pragma:`SPECIALIZE` pragma in the
 first place. When compiling a module ``M``, GHC's optimiser (when given the
 :ghc-flag:`-O` flag) automatically considers each top-level overloaded function declared
 in ``M``, and specialises it for the different types at which it is called in
-``M``. The optimiser *also* considers each *imported* ``INLINABLE``
+``M``. The optimiser *also* considers each *imported* :pragma:`INLINABLE`
 overloaded function, and specialises it for the different types at which
 it is called in ``M``. So in our example, it would be enough for ``lookup``
 to be called at type ``T``:
@@ -14904,9 +15049,13 @@ be useful.
 ------------------------------
 
 .. index::
-   single: SPECIALIZE pragma
+   single: instance, specializing
    single: overloading, death to
 
+.. pragma:: SPECIALIZE instance ⟨instance head⟩
+
+   :where: instance body
+
 Same idea, except for instance declarations. For example:
 
 ::
@@ -14924,8 +15073,12 @@ declaration.
 ``UNPACK`` pragma
 -----------------
 
-.. index::
-   single: UNPACK
+.. pragma:: UNPACK
+
+    :where: data constructor field
+
+    Instructs the compiler to unpack the contents of a constructor field into
+    the constructor itself.
 
 The ``UNPACK`` indicates to the compiler that it should unpack the
 contents of a constructor field into the constructor itself, removing a
@@ -14966,7 +15119,7 @@ See also the :ghc-flag:`-funbox-strict-fields` flag, which essentially has the
 effect of adding ``{-# UNPACK #-}`` to every strict constructor field.
 
 .. [1]
-   In fact, ``UNPACK`` has no effect without :ghc-flag:`-O`, for technical
+   In fact, :pragma:`UNPACK` has no effect without :ghc-flag:`-O`, for technical
    reasons (see :ghc-ticket:`5252`).
 
 .. _nounpack-pragma:
@@ -14974,8 +15127,11 @@ effect of adding ``{-# UNPACK #-}`` to every strict constructor field.
 ``NOUNPACK`` pragma
 -------------------
 
-.. index::
-   single: NOUNPACK
+.. pragma:: NOUNPACK
+
+    :where: top-level
+
+    Instructs the compiler not to unpack a constructor field.
 
 The ``NOUNPACK`` pragma indicates to the compiler that it should not
 unpack the contents of a constructor field. Example: ::
@@ -14990,9 +15146,11 @@ field of the constructor ``T`` is not unpacked.
 ``SOURCE`` pragma
 -----------------
 
-.. index::
-   single: SOURCE
-   single: pragma; SOURCE
+.. pragma:: SOURCE
+
+    :where: after ``import`` statement
+
+    Import a module by ``hs-boot`` file to break a module loop.
 
 The ``{-# SOURCE #-}`` pragma is used only in ``import`` declarations,
 to break a module loop. It is described in detail in
@@ -15003,6 +15161,13 @@ to break a module loop. It is described in detail in
 ``COMPLETE`` pragmas
 --------------------
 
+.. pragma:: COMPLETE
+
+    :where: at top level
+
+    Specify the set of constructors or pattern synonyms which constitute a total
+    match.
+
 The ``COMPLETE`` pragma is used to inform the pattern match checker that a
 certain set of patterns is complete and that any function which matches
 on all the specified patterns is total.
@@ -15130,6 +15295,13 @@ this order:
    single: INCOHERENT
    single: pragma; INCOHERENT
 
+.. pragma:: OVERLAPPING
+.. pragma:: OVERLAPPABLE
+.. pragma:: OVERLAPS
+.. pragma:: INCOHERENT
+
+    :where: on instance head
+
 The pragmas ``OVERLAPPING``, ``OVERLAPPABLE``, ``OVERLAPS``,
 ``INCOHERENT`` are used to specify the overlap behavior for individual
 instances, as described in Section :ref:`instance-overlap`. The pragmas
@@ -15145,15 +15317,19 @@ Rewrite rules
 =============
 
 .. index::
-   single: RULES pragma
-   single: pragma; RULES
    single: rewrite rules
 
+.. pragma:: RULES "⟨name⟩" forall ⟨binder⟩ ... . ⟨expr⟩ = ⟨expr⟩ ...
+
+    :where: top-level
+
+    Define a rewrite rule to be used to optimize a source program.
+
 The programmer can specify rewrite rules as part of the source program
 (in a pragma). Here is an example: ::
 
       {-# RULES
-      "map/map"    forall f g xs.  map f (map g xs) = map (f.g) xs
+            "map/map"    forall f g xs.  map f (map g xs) = map (f.g) xs
         #-}
 
 Use the debug flag :ghc-flag:`-ddump-simpl-stats` to see what rules fired. If
@@ -15176,7 +15352,7 @@ Syntax
 
 From a syntactic point of view:
 
--  There may be zero or more rules in a ``RULES`` pragma, separated by
+-  There may be zero or more rules in a :pragma:`RULES` pragma, separated by
    semicolons (which may be generated by the layout rule).
 
 -  The layout rule applies in a pragma. Currently no new indentation
@@ -15185,8 +15361,8 @@ From a syntactic point of view:
    the same column as the enclosing definitions. ::
 
          {-# RULES
-         "map/map"    forall f g xs.  map f (map g xs) = map (f.g) xs
-         "map/append" forall f xs ys. map f (xs ++ ys) = map f xs ++ map f ys
+               "map/map"    forall f g xs.  map f (map g xs) = map (f.g) xs
+               "map/append" forall f xs ys. map f (xs ++ ys) = map f xs ++ map f ys
            #-}
 
    Furthermore, the closing ``#-}`` should start in a column to the
@@ -15229,21 +15405,21 @@ From a syntactic point of view:
 
 -  If :extension:`ExplicitForAll` is enabled, type/kind variables can also be
    explicitly bound. For example: ::
-     
+
        {-# RULES "id" forall a. forall (x :: a). id @a x = x #-}
-   
+
    When a type-level explicit ``forall`` is present, each type/kind variable
    mentioned must now also be either in scope or bound by the ``forall``. In
    particular, unlike some other places in Haskell, this means free kind
    variables will not be implicitly bound. For example: ::
-     
+
        "this_is_bad" forall (c :: k). forall (x :: Proxy c) ...
        "this_is_ok"  forall k (c :: k). forall (x :: Proxy c) ...
 
    When bound type/kind variables are needed, both foralls must always be
    included, though if no pattern variables are needed, the second can be left
    empty. For example: ::
-   
+
        {-# RULES "map/id" forall a. forall. map (id @a) = id @[a] #-}
 
 -  The left hand side of a rule must consist of a top-level variable
@@ -15266,12 +15442,12 @@ From a syntactic point of view:
    then C's rules are in force when compiling A.) The situation is very
    similar to that for instance declarations.
 
--  Inside a RULE "``forall``" is treated as a keyword, regardless of any
+-  Inside a :pragma:`RULE` "``forall``" is treated as a keyword, regardless of any
    other flag settings. Furthermore, inside a RULE, the language
    extension :extension:`ScopedTypeVariables` is automatically enabled; see
    :ref:`scoped-type-variables`.
 
--  Like other pragmas, ``RULE`` pragmas are always checked for scope errors,
+-  Like other pragmas, :pragma:`RULE` pragmas are always checked for scope errors,
    and are typechecked. Typechecking means that the LHS and RHS of a
    rule are typechecked, and must have the same type. However, rules are
    only *enabled* if the :ghc-flag:`-fenable-rewrite-rules` flag is on (see
@@ -15360,12 +15536,12 @@ give ::
 
     g y = y
 
-Now ``g`` is inlined into ``h``, but ``f``\'s RULE has no chance to fire.
-If instead GHC had first inlined ``g`` into ``h`` then there would have
-been a better chance that ``f``\'s RULE might fire.
+Now ``g`` is inlined into ``h``, but ``f``\'s :pragma:`RULE` has no chance to
+fire. If instead GHC had first inlined ``g`` into ``h`` then there would have
+been a better chance that ``f``\'s :pragma:`RULE` might fire.
 
-The way to get predictable behaviour is to use a ``NOINLINE`` pragma, or an
-``INLINE[⟨phase⟩]`` pragma, on ``f``, to ensure that it is not inlined until
+The way to get predictable behaviour is to use a :pragma:`NOINLINE` pragma, or an
+INLINE[⟨phase⟩] pragma, on ``f``, to ensure that it is not inlined until
 its RULEs have had a chance to fire. The warning flag
 :ghc-flag:`-Winline-rule-shadowing` (see :ref:`options-sanity`) warns about
 this situation.
@@ -15398,9 +15574,9 @@ an application of ``f`` to one argument (in general, the number of arguments
 to the left of the ``=`` sign) should be considered cheap enough to
 duplicate, if such a duplication would make rule fire. (The name
 "CONLIKE" is short for "constructor-like", because constructors
-certainly have such a property.) The ``CONLIKE`` pragma is a modifier to
-INLINE/NOINLINE because it really only makes sense to match ``f`` on the
-LHS of a rule if you are sure that ``f`` is not going to be inlined
+certainly have such a property.) The :pragma:`CONLIKE` pragma is a modifier to
+:pragma:`INLINE`/:pragma:`NOINLINE` because it really only makes sense to match
+``f`` on the LHS of a rule if you are sure that ``f`` is not going to be inlined
 before the rule has a chance to fire.
 
 .. _rules-class-methods:
@@ -15595,7 +15771,7 @@ Controlling what's going on in rewrite rules
                {-# INLINE build #-}
                build g = g (:) []
 
-   Notice the ``INLINE``! That prevents ``(:)`` from being inlined when
+   Notice the :pragma:`INLINE`! That prevents ``(:)`` from being inlined when
    compiling ``PrelBase``, so that an importing module will “see” the
    ``(:)``, and can match it on the LHS of a rule. ``INLINE`` prevents
    any inlining happening in the RHS of the ``INLINE`` thing. I regret