User's Guide: forall is a keyword nowadays
[ghc.git] / docs / users_guide / glasgow_exts.rst
index 952b16c..eae0283 100644 (file)
@@ -540,7 +540,7 @@ corresponds closely to the underlying bit-encoding of the number.
 In this notation floating point numbers are written using hexadecimal digits,
 and so the digits are interpreted using base 16, rather then the usual 10.
 This means that digits left of the decimal point correspond to positive
-powers of 16, while the ones to the right correspond to negaitve ones.
+powers of 16, while the ones to the right correspond to negative ones.
 
 You may also write an explicit exponent, which is similar to the exponent
 in decimal notation with the following differences:
@@ -585,7 +585,9 @@ That is, underscores in numeric literals are ignored when
 :extension:`NumericUnderscores` is enabled.
 See also :ghc-ticket:`14473`.
 
-For example: ::
+For example:
+
+.. code-block:: none
 
     -- decimal
     million    = 1_000_000
@@ -617,7 +619,9 @@ For example: ::
 
     test8bit x = (0b01_0000_0000 .&. x) /= 0
 
-About validity: ::
+About validity:
+
+.. code-block:: none
 
     x0 = 1_000_000   -- valid
     x1 = 1__000000   -- valid
@@ -739,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
@@ -1592,14 +1596,13 @@ New monadic failure desugaring mechanism
     when desugaring refutable patterns in ``do`` blocks.
 
 The ``-XMonadFailDesugaring`` extension switches the desugaring of
-``do``-blocks to use ``MonadFail.fail`` instead of ``Monad.fail``. This will
-eventually be the default behaviour in a future GHC release, under the
+``do``-blocks to use ``MonadFail.fail`` instead of ``Monad.fail``.
+
+This extension is enabled by default since GHC 8.6.1, under the
 `MonadFail Proposal (MFP)
 <https://prime.haskell.org/wiki/Libraries/Proposals/MonadFail>`__.
 
-This extension is temporary, and will be deprecated in a future release. It is
-included so that library authors have a hard check for whether their code
-will work with future GHC versions.
+This extension is temporary, and will be deprecated in a future release.
 
 .. _rebindable-syntax:
 
@@ -1639,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.
 
@@ -2230,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::
@@ -2291,6 +2298,9 @@ The following syntax is stolen:
 ``pattern``
     Stolen by: :extension:`PatternSynonyms`
 
+``static``
+    Stolen by: :extension:`StaticPointers`
+
 .. _data-type-extensions:
 
 Extensions to data types and type synonyms
@@ -2308,8 +2318,16 @@ Data types with no constructors
 
     Allow definition of empty ``data`` types.
 
-With the :extension:`EmptyDataDecls` extension, GHC
-lets you declare a data type with no constructors. For example: ::
+With the :extension:`EmptyDataDecls` extension, GHC lets you declare a
+data type with no constructors.
+
+You only need to enable this extension if the language you're using
+is Haskell 98, in which a data type must have at least one constructor.
+Haskell 2010 relaxed this rule to allow data types with no constructors,
+and thus :extension:`EmptyDataDecls` is enabled by default when the
+language is Haskell 2010.
+
+For example: ::
 
       data S      -- S :: Type
       data T a    -- T :: Type -> Type
@@ -2395,8 +2413,7 @@ specifically:
    sets the fixity for both type constructor ``T`` and data constructor
    ``T``, and similarly for ``:*:``. ``Int `a` Bool``.
 
--  Function arrow is ``infixr`` with fixity 0 (this might change; it's
-   not clear what it should be).
+-  The function arrow ``->`` is ``infixr`` with fixity -1.
 
 .. _type-operators:
 
@@ -3212,8 +3229,6 @@ Record field disambiguation
 
     :since: 6.8.1
 
-    :since: 6.8.1
-
     Allow the compiler to automatically choose between identically-named
     record selectors based on type (if the choice is unambiguous).
 
@@ -3546,10 +3561,10 @@ More details:
        module M where
          data R = R { a,b,c :: Int }
        module X where
-         import M( R(a,c) )
-         f b = R { .. }
+         import M( R(R,a,c) )
+         f b = R { .. }
 
-   The ``R{..}`` expands to ``R{M.a=a}``, omitting ``b`` since the
+   The ``R{..}`` expands to ``R{a=a}``, omitting ``b`` since the
    record field is not in scope, and omitting ``c`` since the variable
    ``c`` is not in scope (apart from the binding of the record selector
    ``c``, of course).
@@ -3778,7 +3793,7 @@ GHC extends this mechanism along several axes:
 
 * In Haskell 98, the only derivable classes are ``Eq``,
   ``Ord``, ``Enum``, ``Ix``, ``Bounded``, ``Read``, and ``Show``. `Various
-  langauge extensions <#deriving-extra>`__ extend this list.
+  language extensions <#deriving-extra>`__ extend this list.
 
 * Besides the stock approach to deriving instances by generating all method
   definitions, GHC supports two additional deriving strategies, which can
@@ -4123,7 +4138,7 @@ There are two exceptions to this rule:
 
    That is, :extension:`DeriveFunctor` pattern-matches its way into tuples and maps
    over each type that constitutes the tuple. The generated code is
-   reminiscient of what would be generated from
+   reminiscent of what would be generated from
    ``data Triple a = Triple a Int [a]``, except with extra machinery to handle
    the tuple.
 
@@ -4359,7 +4374,7 @@ There are some other differences regarding what data types can have derived
    polymorphic types that are syntactically equivalent to the last type
    parameter. In particular:
 
-  -  We don't fold over the arguments of ``E1`` or ``E4`` beacause even though
+  -  We don't fold over the arguments of ``E1`` or ``E4`` because even though
      ``(a ~ Int)``, ``Int`` is not syntactically equivalent to ``a``.
 
   -  We don't fold over the argument of ``E3`` because ``a`` is not universally
@@ -4453,7 +4468,7 @@ Deriving ``Data`` instances
 
 .. extension:: DeriveDataTypeable
     :shortdesc: Enable deriving for the Data class.
-       Implied by :extension:`AutoDeriveTypeable`.
+       Implied by (deprecated) :extension:`AutoDeriveTypeable`.
 
     :since: 6.8.1
 
@@ -4508,7 +4523,7 @@ Deriving ``Lift`` instances
 .. extension:: DeriveLift
     :shortdesc: Enable deriving for the Lift class
 
-    :since: 7.2.1
+    :since: 8.0.1
 
     Enable automatic deriving of instances for the ``Lift`` typeclass for
     Template Haskell.
@@ -5435,6 +5450,37 @@ pattern synonym: ::
       pattern StrictJust a <- Just !a where
         StrictJust !a = Just a
 
+Constructing an explicitly bidirectional pattern synonym also:
+
+- can create different data constructors from the underlying data type,
+  not just the one appearing in the pattern match;
+
+- can call any functions or conditional logic, especially validation,
+  of course providing it constructs a result of the right type;
+
+- can use guards on the lhs of the ``=``;
+
+- can have multiple equations.
+
+For example: ::
+
+      data PosNeg = Pos Int | Neg Int
+      pattern Smarter{ nonneg } <- Pos nonneg  where
+        Smarter x = if x >= 0 then (Pos x) else (Neg x)
+
+Or using guards: ::
+
+      pattern Smarter{ nonneg } <- Pos nonneg  where
+        Smarter x | x >= 0    = (Pos x)
+                  | otherwise = (Neg x)
+
+There is an extensive Haskell folk art of `smart constructors
+<https://wiki.haskell.org/Smart_constructor>`_,
+essentially functions that wrap validation around a constructor,
+and avoid exposing its representation.
+The downside is that the underlying constructor can't be used as a matcher.
+Pattern synonyms can be used as genuinely smart constructors, for both validation and matching.
+
 The table below summarises where each kind of pattern synonym can be used.
 
 +---------------+----------------+---------------+---------------------------+
@@ -5508,7 +5554,7 @@ the syntax for bidirectional pattern synonyms is: ::
 and the syntax for explicitly bidirectional pattern synonyms is: ::
 
       pattern pat_lhs <- pat where
-        pat_lhs = expr
+        pat_lhs = expr                      -- lhs restricted, see below
 
 We can define either prefix, infix or record pattern synonyms by modifying
 the form of `pat_lhs`. The syntax for these is as follows:
@@ -5522,6 +5568,9 @@ Infix   ``arg1 `Name` arg2``
 Record  ``Name{arg1,arg2,...,argn}``
 ======= ============================
 
+The `pat_lhs` for explicitly bidirectional construction cannot use Record syntax.
+(Because the rhs *expr* might be constructing different data constructors.)
+It can use guards with multiple equations.
 
 Pattern synonym declarations can only occur in the top level of a
 module. In particular, they are not allowed as local definitions.
@@ -5688,7 +5737,7 @@ Note also the following points
          pattern P x y v <- MkT True x y (v::a)
 
    Here the universal type variable `a` scopes over the definition of `P`,
-   but the existential `b` does not.  (c.f. disussion on Trac #14998.)
+   but the existential `b` does not.  (c.f. discussion on Trac #14998.)
 
 -  For a bidirectional pattern synonym, a use of the pattern synonym as
    an expression has the type
@@ -5831,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
 
@@ -6416,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
@@ -6747,9 +6794,12 @@ like this:
    target constraint is a substitution instance of :math:`I`. These instance
    declarations are the *candidates*.
 
--  Eliminate any candidate :math:`IX` for which both of the following hold:
+-  If no candidates remain, the search failes
+
+-  Eliminate any candidate :math:`IX` for which there is another candidate
+   :math:`IY` such that both of the following hold:
 
-   -  There is another candidate :math:`IY` that is strictly more specific; that
+   -  :math:`IY` is strictly more specific than :math:`IX`.  That
       is, :math:`IY` is a substitution instance of :math:`IX` but not vice versa.
 
    -  Either :math:`IX` is *overlappable*, or :math:`IY` is *overlapping*. (This
@@ -6757,19 +6807,20 @@ like this:
       client to deliberately override an instance from a library,
       without requiring a change to the library.)
 
--  If exactly one non-incoherent candidate remains, select it. If all
-   remaining candidates are incoherent, select an arbitrary one.
-   Otherwise the search fails (i.e. when more than one surviving
-   candidate is not incoherent).
+-  If all the remaining candidates are incoherent, the search suceeds, returning
+   an arbitrary surviving candidate.
+
+-  If more than one non-incoherent candidate remains, the search fails.
 
--  If the selected candidate (from the previous step) is incoherent, the
-   search succeeds, returning that candidate.
+-  Otherwise there is exactly one non-incoherent candidate; call it the
+   "prime candidate".
 
--  If not, find all instances that *unify* with the target constraint,
+-  Now find all instances, or in-scope given constraints, that *unify* with
+   the target constraint,
    but do not *match* it. Such non-candidate instances might match when
    the target constraint is further instantiated. If all of them are
-   incoherent, the search succeeds, returning the selected candidate; if
-   not, the search fails.
+   incoherent top-level instances, the search succeeds, returning the prime candidate.
+   Otherwise the search fails.
 
 Notice that these rules are not influenced by flag settings in the
 client module, where the instances are *used*. These rules make it
@@ -6811,15 +6862,16 @@ former is a substitution instance of the latter. For example (D) is
 "more specific" than (C) because you can get from (C) to (D) by
 substituting ``a := Int``.
 
-GHC is conservative about committing to an overlapping instance. For
-example: ::
+The final bullet (about unifiying instances)
+makes GHC conservative about committing to an
+overlapping instance. For example: ::
 
       f :: [b] -> [b]
       f x = ...
 
 Suppose that from the RHS of ``f`` we get the constraint ``C b [b]``.
 But GHC does not commit to instance (C), because in a particular call of
-``f``, ``b`` might be instantiate to ``Int``, in which case instance (D)
+``f``, ``b`` might be instantiated to ``Int``, in which case instance (D)
 would be more specific still. So GHC rejects the program.
 
 If, however, you enable the extension :extension:`IncoherentInstances` when compiling
@@ -6860,6 +6912,23 @@ declaration, thus: ::
 
 (You need :extension:`FlexibleInstances` to do this.)
 
+In the unification check in the final bullet, GHC also uses the
+"in-scope given constraints".  Consider for example ::
+
+   instance C a Int
+
+   g :: forall b c. C b Int => blah
+   g = ...needs (C c Int)...
+
+Here GHC will not solve the constraint ``(C c Int)`` from the
+top-level instance, because a particular call of ``g`` might
+instantiate both ``b`` and ``c`` to the same type, which would
+allow the constraint to be solved in a different way.  This latter
+restriction is principally to make the constraint-solver complete.
+(Interested folk can read ``Note [Instance and Given overlap]`` in ``TcInteract``.)
+It is easy to avoid: in a type signature avoid a constraint that
+matches a top-level instance.  The flag :ghc-flag:`-Wsimplifiable-class-constraints` warns about such signatures.
+
 .. warning::
     Overlapping instances must be used with care. They can give
     rise to incoherence (i.e. different instance choices are made in
@@ -7003,7 +7072,7 @@ usual: ::
 
 The class ``IsString`` is not in scope by default. If you want to
 mention it explicitly (for example, to give an instance declaration for
-it), you can import it from module ``GHC.Exts``.
+it), you can import it from module ``Data.String``.
 
 Haskell's defaulting mechanism (`Haskell Report, Section
 4.3.4 <http://www.haskell.org/onlinereport/decls.html#sect4.3.4>`__) is
@@ -7031,7 +7100,7 @@ A small example:
 
     module Main where
 
-    import GHC.Exts( IsString(..) )
+    import Data.String( IsString(..) )
 
     newtype MyString = MyString String deriving (Eq, Show)
     instance IsString MyString where
@@ -7505,6 +7574,17 @@ instance for ``GMap`` is ::
 In this example, the declaration has only one variant. In general, it
 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 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
 variables that are mentioned in the patterns on the left hand side, but not
 used on the right hand side are reported. Variables that occur multiple times
@@ -7518,6 +7598,9 @@ This resembles the wildcards that can be used in
 No error messages reporting the inferred types are generated, nor does
 the extension :extension:`PartialTypeSignatures` have any effect.
 
+A type or kind variable explicitly bound using :extension:`ExplicitForAll` but
+not used on the left hand side will generate an error, not a warning.
+
 Data and newtype instance declarations are only permitted when an
 appropriate family declaration is in scope - just as a class instance
 declaration requires the class declaration to be visible. Moreover, each
@@ -7670,6 +7753,10 @@ with underscores to avoid warnings when the
 :ghc-flag:`-Wunused-type-patterns` flag is enabled. The same rules apply
 as for :ref:`data-instance-declarations`.
 
+Also in the same way as :ref:`data-instance-declarations`, when
+:extension:`ExplicitForAll` is enabled, type and kind variables can be
+explicilty bound in a type instance declaration.
+
 Type family instance declarations are only legitimate when an
 appropriate family declaration is in scope - just like class instances
 require the class declaration to be visible. Moreover, each instance
@@ -7704,8 +7791,14 @@ Note that GHC must be sure that ``a`` cannot unify with ``Int`` or
 their code, GHC will not be able to simplify the type. After all, ``a``
 might later be instantiated with ``Int``.
 
-A closed type family's equations have the same restrictions as the
-equations for open type family instances.
+A closed type family's equations have the same restrictions and extensions as
+the equations for open type family instances. For instance, when
+:extension:`ExplicitForAll` is enabled, type or kind variables used on the
+left hand side of an equation can be explicitly bound, such as in: ::
+
+  type family R a where
+    forall t a. R (t a) = [a]
+    forall a.   R a     = a
 
 A closed type family may be declared with no equations. Such closed type
 families are opaque type-level definitions that will never reduce, are
@@ -7933,7 +8026,7 @@ Hence, the following contrived example is admissible: ::
 Here ``c`` and ``a`` are class parameters, but the type is also indexed
 on a third parameter ``x``.
 
-.. _assoc-data-inst:
+.. _assoc-inst:
 
 Associated instances
 ~~~~~~~~~~~~~~~~~~~~
@@ -7950,7 +8043,7 @@ keyword in the family instance: ::
       type Elem [e] = e
       ...
 
-The data or type family instance for an assocated type must follow
+The data or type family instance for an associated type must follow
 the rule that the type indexes corresponding to class parameters must have
 precisely the same as type given in the instance head. For example: ::
 
@@ -8009,6 +8102,15 @@ Note the following points:
    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
+
 .. _assoc-decl-defs:
 
 Associated type synonym defaults
@@ -8045,6 +8147,10 @@ Note the following points:
    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`.
+
 -  Unlike the associated type family declaration itself, the type variables of
    the default instance are independent of those of the parent class.
 
@@ -8546,12 +8652,24 @@ constructors are prefixed by a tick ``'``): ::
     'L :: k1 -> Sum k1 k2
     'R :: k2 -> Sum k1 k2
 
-.. note::
-    Data family instances cannot be promoted at the moment: GHC’s type theory
-    just isn’t up to the task of promoting data families, which requires full
-    dependent types.
+Virtually all data constructors, even those with rich kinds, can be promoted.
+There are only a couple of exceptions to this rule:
+
+-  Data family instance constructors cannot be promoted at the moment. GHC's
+   type theory just isn’t up to the task of promoting data families, which
+   requires full dependent types.
 
-    See also :ghc-ticket:`15245`.
+-  Data constructors with contexts that contain non-equality constraints cannot
+   be promoted. For example: ::
+
+     data Foo :: Type -> Type where
+       MkFoo1 :: a ~ Int         => Foo a    -- promotable
+       MkFoo2 :: a ~~ Int        => Foo a    -- promotable
+       MkFoo3 :: Show a          => Foo a    -- not promotable
+
+   ``MkFoo1`` and ``MkFoo2`` can be promoted, since their contexts
+   only involve equality-oriented constraints. However, ``MkFoo3``'s context
+   contains a non-equality constraint ``Show a``, and thus cannot be promoted.
 
 .. _promotion-syntax:
 
@@ -8666,12 +8784,12 @@ Kind polymorphism
 .. extension:: TypeInType
     :shortdesc: Deprecated. Enable kind polymorphism and datatype promotion.
 
-    :implies: :extension:`PolyKinds`, :extension:`DataKinds`, :extension:`KindSignatures`,
-              :extension:`NoStarIsType`
+    :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.
@@ -8764,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
@@ -8789,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
@@ -8893,14 +9083,8 @@ example, consider ::
   data Proxy a           -- Proxy :: forall k. k -> Type
   data X (a :: Proxy k)
 
-According to the rules above ``X`` has a CUSK. Yet, what is the kind of ``k``?
-It is impossible to know. This code is thus rejected as masquerading as having
-a CUSK, but not really. If you wish ``k`` to be polykinded, it is straightforward
-to specify this: ::
-
-  data X (a :: Proxy (k1 :: k2))
-
-The above definition is indeed fully fixed, with no masquerade.
+According to the rules above ``X`` has a CUSK. Yet, the kind of ``k`` is undetermined.
+It is thus quantified over, giving ``X`` the kind ``forall k1 (k :: k1). Proxy k -> Type``.
 
 Kind inference in closed type families
 --------------------------------------
@@ -9096,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: ::
 
@@ -9120,13 +9303,12 @@ The kind ``Type``
 -----------------
 
 .. extension:: StarIsType
-    :shortdesc: Desugar ``*`` to ``Data.Kind.Type``.
+    :shortdesc: Treat ``*`` as ``Data.Kind.Type``.
 
     :since: 8.6.1
 
     Treat the unqualified uses of the ``*`` type operator as nullary and desugar
-    to ``Data.Kind.Type``. Disabled by :extension:`TypeOperators` and
-    :extension:`TypeInType`.
+    to ``Data.Kind.Type``.
 
 The kind ``Type`` (imported from ``Data.Kind``) classifies ordinary types. With
 :extension:`StarIsType` (currently enabled by default), ``*`` is desugared to
@@ -9252,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
@@ -9545,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:
 
@@ -9584,7 +9766,7 @@ The following things have kind ``Constraint``:
 
 -  Anything whose form is not yet known, but the user has declared to
    have kind ``Constraint`` (for which they need to import it from
-   ``GHC.Exts``). So for example
+   ``Data.Kind``). So for example
    ``type Foo (f :: Type -> Constraint) = forall b. f b => b -> b``
    is allowed, as well as examples involving type families: ::
 
@@ -9710,7 +9892,7 @@ This idea is very old; see Seciton 7 of `Derivable type classes <https://www.mic
 Syntax changes
 ----------------
 
-`Haskell 2010 <https://www.haskell.org/onlinereport/haskell2010/haskellch10.html#x17-18000010.5>`_ defines a ``context`` (the bit to the left of ``=>`` in a type) like this ::
+`Haskell 2010 <https://www.haskell.org/onlinereport/haskell2010/haskellch10.html#x17-18000010.5>`_ defines a ``context`` (the bit to the left of ``=>`` in a type) like this
 
 .. code-block:: none
 
@@ -9720,26 +9902,26 @@ Syntax changes
     class ::= qtycls tyvar
             |  qtycls (tyvar atype1 ... atypen)
 
-We to extend ``class`` (warning: this is a rather confusingly named non-terminal symbol) with two extra forms, namely precisely what can appear in an instance declaration ::
+We to extend ``class`` (warning: this is a rather confusingly named non-terminal symbol) with two extra forms, namely precisely what can appear in an instance declaration
 
 .. code-block:: none
 
     class ::= ...
-          | context => qtycls inst
-          | context => tyvar inst
+          | [context =>] qtycls inst
+          | [context =>] tyvar inst
 
 The definition of ``inst`` is unchanged from the Haskell Report (roughly, just a type).
-That is the only syntactic change to the language.
+The ``context =>`` part is optional.  That is the only syntactic change to the language.
 
 Notes:
 
-- Where GHC allows extensions instance declarations we allow exactly the same extensions to this new form of ``class``.  Specifically, with :extension:`ExplicitForAll` and :extension:`MultiParameterTypeClasses` the syntax becomes ::
+- Where GHC allows extensions instance declarations we allow exactly the same extensions to this new form of ``class``.  Specifically, with :extension:`ExplicitForAll` and :extension:`MultiParameterTypeClasses` the syntax becomes
 
-.. code-block:: none
+  .. code-block:: none
 
     class ::= ...
-           | [forall tyavrs .] context => qtycls inst1 ... instn
-           | [forall tyavrs .] context => tyvar inst1 ... instn
+           | [forall tyavrs .] [context =>] qtycls inst1 ... instn
+           | [forall tyavrs .] [context =>] tyvar inst1 ... instn
 
   Note that an explicit ``forall`` is often absolutely essential. Consider the rose-tree example ::
 
@@ -9918,10 +10100,11 @@ means this: ::
 The two are treated identically, except that the latter may bring type variables
 into scope (see :ref:`scoped-type-variables`).
 
-Notes:
+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`.
 
-- With :extension:`ExplicitForAll`, ``forall`` becomes a keyword; you can't use ``forall`` as a
-  type variable any more!
+Notes:
 
 - As well in type signatures, you can also use an explicit ``forall``
   in an instance declaration: ::
@@ -10170,8 +10353,7 @@ Lexically scoped type variables
     To trigger those forms of ``ScopedTypeVariables``, the ``forall`` must appear against the top-level signature (or outer expression)
     but *not* against nested signatures referring to the same type variables.
 
-    Explicit ``forall`` is not always required -- see :ref:`pattern signature equivalent pattern-equiv-form` for the example in this section, or :ref:`pattern-type-sigs` .
-
+    Explicit ``forall`` is not always required -- see :ref:`pattern signature equivalent <pattern-equiv-form>` for the example in this section, or :ref:`pattern-type-sigs`.
 
 GHC supports *lexically scoped type variables*, without which some type
 signatures are simply impossible to write. For example: ::
@@ -10392,11 +10574,6 @@ scope, because it is bound by the pattern match.
 The effect is to bring it into scope,
 standing for the existentially-bound type variable.
 
-When a pattern type signature binds a type variable in this way, GHC
-insists that the type variable is bound to a *rigid*, or fully-known,
-type variable. This means that any user-written type signature always
-stands for a completely known type.
-
 It does seem odd that the existentially-bound type variable *must not*
 be already in scope. Contrast that usually name-bindings merely shadow
 (make a 'hole') in a same-named outer variable's scope.
@@ -10519,50 +10696,7 @@ assumptions", and a related `blog post <http://ghc.haskell.org/trac/ghc/blog/Let
 The extension :extension:`MonoLocalBinds` is implied by :extension:`TypeFamilies`
 and :extension:`GADTs`. You can switch it off again with
 :extension:`NoMonoLocalBinds <-XMonoLocalBinds>` but type inference becomes
-less predicatable if you do so. (Read the papers!)
-
-.. _kind-generalisation:
-
-Kind generalisation
--------------------
-
-Just as :extension:`MonoLocalBinds` places limitations on when the *type* of a
-*term* is generalised (see :ref:`mono-local-binds`), it also limits when the
-*kind* of a *type signature* is generalised. Here is an example involving
-:ref:`type signatures on instance declarations <instance-sigs>`: ::
-
-    data Proxy a = Proxy
-    newtype Tagged s b = Tagged b
-
-    class C b where
-      c :: forall (s :: k). Tagged s b
-
-    instance C (Proxy a) where
-      c :: forall s. Tagged s (Proxy a)
-      c = Tagged Proxy
-
-With :extension:`MonoLocalBinds` enabled, this ``C (Proxy a)`` instance will
-fail to typecheck. The reason is that the type signature for ``c`` captures
-``a``, an outer-scoped type variable, which means the type signature is not
-closed. Therefore, the inferred kind for ``s`` will *not* be generalised, and
-as a result, it will fail to unify with the kind variable ``k`` which is
-specified in the declaration of ``c``. This can be worked around by specifying
-an explicit kind variable for ``s``, e.g., ::
-
-    instance C (Proxy a) where
-      c :: forall (s :: k). Tagged s (Proxy a)
-      c = Tagged Proxy
-
-or, alternatively: ::
-
-    instance C (Proxy a) where
-      c :: forall k (s :: k). Tagged s (Proxy a)
-      c = Tagged Proxy
-
-This declarations are equivalent using Haskell's implicit "add implicit
-foralls" rules (see :ref:`implicit-quantification`). The implicit foralls rules
-are purely syntactic and are quite separate from the kind generalisation
-described here.
+less predictable if you do so. (Read the papers!)
 
 .. _visible-type-application:
 
@@ -10570,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
 
@@ -10591,28 +10725,149 @@ 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.
 
-- 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:
+
+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
+  annotations come before any variables never used in kind annotations.
+  This rule is not recursive: if there is an annotation within an annotation,
+  then the variables used therein are on equal footing. Examples::
+
+    f :: Proxy (a :: k) -> Proxy (b :: j) -> ()
+      -- as if f :: forall k j a b. ...
+
+    g :: Proxy (b :: j) -> Proxy (a :: (Proxy :: (k -> Type) -> Type) Proxy) -> ()
+      -- as if g :: forall j k b a. ...
+      -- NB: k is in a kind annotation within a kind annotation
 
 - If any of the variables depend on other variables (that is, if some
   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.
+  stable topological sort on the variables. Example::
+
+    h :: Proxy (a :: (j, k)) -> Proxy (b :: Proxy a) -> ()
+      -- as if h :: forall j k a b. ...
 
-  For example: if we have ``bar :: Proxy (a :: (j, k)) -> b``, then
-  the variables are ordered ``j``, ``k``, ``a``, ``b``.
+  In this example, all of ``a``, ``j``, and ``k`` are considered kind
+  variables and will always be placed before ``b``, a lowly type variable.
+  (Note that ``a`` is used in ``b``\'s kind.) Yet, even though ``a`` appears
+  lexically before ``j`` and ``k``, ``j`` and ``k`` are quantified first,
+  because ``a`` depends on ``j`` and ``k``. Note further that ``j`` and ``k``
+  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
@@ -10631,52 +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.
+The section in this manual on kind polymorphism describes how variables
+in type and class declarations are ordered (:ref:`inferring-variable-order`).
 
 .. _implicit-parameters:
 
@@ -10685,7 +10900,6 @@ Implicit parameters
 
 .. extension:: ImplicitParams
     :shortdesc: Enable Implicit Parameters.
-        Implies :extension:`FlexibleContexts` and :extension:`FlexibleInstances`.
 
     :since: 6.8.1
 
@@ -11118,7 +11332,7 @@ the following pairs are equivalent: ::
                     h x y = y
                  in ...
 
-Notice that GHC always adds implicit quantfiers *at the outermost level*
+Notice that GHC always adds implicit quantifiers *at the outermost level*
 of a user-written type; it
 does *not* find the inner-most possible quantification
 point. For example: ::
@@ -11534,6 +11748,21 @@ configurable by a few flags.
     ``mempty @(Int -> [Int])``. This can be toggled off with
     the reverse of this flag.
 
+.. ghc-flag:: -fshow-docs-of-hole-fits
+    :shortdesc: Toggles whether to show the documentation of the valid
+       hole fits in the output.
+    :type: dynamic
+    :category: verbosity
+    :reverse: -fno-show-docs-of-hole-fits
+
+    :default: off
+
+    It can sometime be the case that the name and type of a valid hole
+    fit is not enough to realize what the fit stands for. This flag
+    adds the documentation of the fit to the message, if the
+    documentation is available (and the module from which the function
+    comes was compiled with the ``-haddock`` flag).
+
 .. ghc-flag:: -fshow-type-app-vars-of-hole-fits
     :shortdesc: Toggles whether to show what type each quantified
        variable takes in a valid hole fit.
@@ -11671,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
@@ -12043,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: ::
@@ -14134,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
@@ -14166,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
@@ -14194,14 +14425,21 @@ other compilers.
 ``WARNING`` and ``DEPRECATED`` pragmas
 --------------------------------------
 
-.. index::
-   single: WARNING
-   single: DEPRECATED
+.. pragma:: WARNING
 
-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.
+    :where: declaration
+
+    The ``WARNING`` pragma allows you to attach an arbitrary warning to a
+    particular function, class, or type.
+
+.. 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: ::
 
@@ -14252,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
@@ -14303,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
@@ -14369,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
@@ -14382,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
@@ -14413,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:
 
@@ -14452,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.
 
@@ -14468,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
+
+    Instructs GHC to consider a value to be especially cheap to inline.
 
-An ``INLINE`` or ``NOINLINE`` pragma may have a ``CONLIKE`` modifier, which affects
-matching in RULEs (only). See :ref:`conlike`.
+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
@@ -14502,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
@@ -14517,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:
@@ -14532,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
@@ -14582,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:
@@ -14595,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:
 
 ::
@@ -14693,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
@@ -14718,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.
@@ -14728,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
@@ -14744,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.
@@ -14752,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``:
@@ -14776,28 +15043,19 @@ to be called at type ``T``:
 However, sometimes there are no such calls, in which case the pragma can
 be useful.
 
-Obsolete ``SPECIALIZE`` syntax
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-In earlier versions of GHC, it was possible to provide your own
-specialised function for a given type:
-
-::
-
-    {-# SPECIALIZE hammeredLookup :: [(Int, value)] -> Int -> value = intLookup #-}
-
-This feature has been removed, as it is now subsumed by the ``RULES``
-pragma (see :ref:`rule-spec`).
-
 .. _specialize-instance-pragma:
 
 ``SPECIALIZE`` instance pragma
 ------------------------------
 
 .. 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:
 
 ::
@@ -14815,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
@@ -14857,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:
@@ -14865,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: ::
@@ -14881,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
@@ -14894,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.
@@ -14940,7 +15214,7 @@ modules. ``COMPLETE`` pragmas should be thought of as asserting a
 universal truth about a set of patterns and as a result, should not be
 used to silence context specific incomplete match warnings.
 
-When specifing a ``COMPLETE`` pragma, the result types of all patterns must
+When specifying a ``COMPLETE`` pragma, the result types of all patterns must
 be consistent with each other. This is a sanity check as it would be impossible
 to match on all the patterns if the types were inconsistent.
 
@@ -15021,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
@@ -15036,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
@@ -15067,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
@@ -15076,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
@@ -15104,7 +15389,7 @@ From a syntactic point of view:
    is never run by GHC, but is nevertheless parsed, typechecked etc, so
    that it is available to the plugin.
 
--  Each variable mentioned in a rule must either be in scope (e.g.
+-  Each (term) variable mentioned in a rule must either be in scope (e.g.
    ``map``), or bound by the ``forall`` (e.g. ``f``, ``g``, ``xs``). The
    variables bound by the ``forall`` are called the *pattern* variables.
    They are separated by spaces, just like in a type ``forall``.
@@ -15118,6 +15403,25 @@ From a syntactic point of view:
 
    Since ``g`` has a polymorphic type, it must have a type signature.
 
+-  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
    applied to arbitrary expressions. For example, this is *not* OK: ::
 
@@ -15138,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
@@ -15232,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.
@@ -15270,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:
@@ -15305,7 +15609,7 @@ The solution is to define the instance-specific function yourself, with
 a pragma to prevent it being inlined too early, and give a RULE for it: ::
 
     instance C Bool where
-      op x y = opBool
+      op = opBool
 
     opBool :: Bool -> Bool -> Bool
     {-# NOINLINE [1] opBool #-}
@@ -15467,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
@@ -15840,8 +16144,8 @@ Here are some examples: ::
 The type ``Simple`` has its parameter at role representational, which is
 generally the most common case. ``Simple Age`` would have the same
 representation as ``Simple Int``. The type ``Complex``, on the other
-hand, has its parameter at role nominal, because ``Simple Age`` and
-``Simple Int`` are *not* the same. Lastly, ``Phant Age`` and
+hand, has its parameter at role nominal, because ``Complex Age`` and
+``Complex Int`` are *not* the same. Lastly, ``Phant Age`` and
 ``Phant Bool`` have the same representation, even though ``Age`` and
 ``Bool`` are unrelated.