User's Guide: forall is a keyword nowadays
[ghc.git] / docs / users_guide / glasgow_exts.rst
index 6c444cc..eae0283 100644 (file)
@@ -148,24 +148,25 @@ stores a pointer. GHC currently does not support this variety of ``Just``
 nodes (nor for any other datatype). Accordingly, the *kind* of an unboxed
 type is different from the kind of a boxed type.
 
-The Haskell Report describes that ``*`` is the kind of ordinary datatypes,
-such as ``Int``. Furthermore, type constructors can have kinds with arrows;
-for example, ``Maybe`` has kind ``* -> *``. Unboxed types have a kind that
-specifies their runtime representation. For example, the type ``Int#`` has
-kind ``TYPE 'IntRep`` and ``Double#`` has kind ``TYPE 'DoubleRep``. These
-kinds say that the runtime representation of an ``Int#`` is a machine integer,
-and the runtime representation of a ``Double#`` is a machine double-precision
-floating point. In contrast, the kind ``*`` is actually just a synonym
-for ``TYPE 'PtrRepLifted``. More details of the ``TYPE`` mechanisms appear in
-the `section on runtime representation polymorphism <#runtime-rep>`__.
-
-Given that ``Int#``'s kind is not ``*``, it then it follows that
-``Maybe Int#`` is disallowed. Similarly, because type variables tend
-to be of kind ``*`` (for example, in ``(.) :: (b -> c) -> (a -> b) -> a -> c``,
-all the type variables have kind ``*``), polymorphism tends not to work
-over primitive types. Stepping back, this makes some sense, because
-a polymorphic function needs to manipulate the pointers to its data,
-and most primitive types are unboxed.
+The Haskell Report describes that ``*`` (spelled ``Type`` and imported from
+``Data.Kind`` in the GHC dialect of Haskell) is the kind of ordinary datatypes,
+such as ``Int``. Furthermore, type constructors can have kinds with arrows; for
+example, ``Maybe`` has kind ``Type -> Type``. Unboxed types have a kind that
+specifies their runtime representation. For example, the type ``Int#`` has kind
+``TYPE 'IntRep`` and ``Double#`` has kind ``TYPE 'DoubleRep``. These kinds say
+that the runtime representation of an ``Int#`` is a machine integer, and the
+runtime representation of a ``Double#`` is a machine double-precision floating
+point. In contrast, the kind ``Type`` is actually just a synonym for ``TYPE
+'LiftedRep``. More details of the ``TYPE`` mechanisms appear in the `section
+on runtime representation polymorphism <#runtime-rep>`__.
+
+Given that ``Int#``'s kind is not ``Type``, it then it follows that ``Maybe
+Int#`` is disallowed. Similarly, because type variables tend to be of kind
+``Type`` (for example, in ``(.) :: (b -> c) -> (a -> b) -> a -> c``, all the
+type variables have kind ``Type``), polymorphism tends not to work over
+primitive types. Stepping back, this makes some sense, because a polymorphic
+function needs to manipulate the pointers to its data, and most primitive types
+are unboxed.
 
 There are some restrictions on the use of primitive types:
 
@@ -284,21 +285,21 @@ for an unboxed sum type with N alternatives is ::
 
     (# t_1 | t_2 | ... | t_N #)
 
-where `t_1` ... `t_N` are types (which can be unlifted, including unboxed tuple
-and sums).
+where ``t_1`` ... ``t_N`` are types (which can be unlifted, including unboxed
+tuples and sums).
 
 Unboxed tuples can be used for multi-arity alternatives. For example: ::
 
     (# (# Int, String #) | Bool #)
 
-Term level syntax is similar. Leading and preceding bars (`|`) indicate which
-alternative it is. Here is two terms of the type shown above: ::
+The term level syntax is similar. Leading and preceding bars (`|`) indicate which
+alternative it is. Here are two terms of the type shown above: ::
 
     (# (# 1, "foo" #) | #) -- first alternative
 
     (# | True #) -- second alternative
 
-Pattern syntax reflects the term syntax: ::
+The pattern syntax reflects the term syntax: ::
 
     case x of
       (# (# i, str #) | #) -> ...
@@ -307,45 +308,56 @@ Pattern syntax reflects the term syntax: ::
 Unboxed sums are "unboxed" in the sense that, instead of allocating sums in the
 heap and representing values as pointers, unboxed sums are represented as their
 components, just like unboxed tuples. These "components" depend on alternatives
-of a sum type. Code generator tries to generate as compact layout as possible.
-In the best case, size of an unboxed sum is size of its biggest alternative +
-one word (for tag). The algorithm for generating memory layout for a sum type
-works like this:
+of a sum type. Like unboxed tuples, unboxed sums are lazy in their lifted
+components.
+
+The code generator tries to generate as compact layout as possible for each
+unboxed sum. In the best case, size of an unboxed sum is size of its biggest
+alternative plus one word (for a tag). The algorithm for generating the memory
+layout for a sum type works like this:
 
 - All types are classified as one of these classes: 32bit word, 64bit word,
   32bit float, 64bit float, pointer.
 
 - For each alternative of the sum type, a layout that consists of these fields
-  is generated. For example, if an alternative has `Int`, `Float#` and `String`
-  fields, the layout will have an 32bit word, 32bit float and pointer fields.
+  is generated. For example, if an alternative has ``Int``, ``Float#`` and
+  ``String`` fields, the layout will have an 32bit word, 32bit float and
+  pointer fields.
 
 - Layout fields are then overlapped so that the final layout will be as compact
-  as possible. E.g. say two alternatives have these fields: ::
+  as possible. For example, suppose we have the unboxed sum: ::
 
-    Word32, String, Float#
-    Float#, Float#, Maybe Int
+    (# (# Word32#, String, Float# #)
+    |  (# Float#, Float#, Maybe Int #) #)
 
-  Final layout will be something like ::
+  The final layout will be something like ::
 
     Int32, Float32, Float32, Word32, Pointer
 
-  First `Int32` is for the tag. It has two `Float32` fields because floating
-  point types can't overlap with other types, because of limitations of the code
-  generator that we're hoping to overcome in the future, and second alternative
-  needs two `Float32` fields. `Word32` field is for the `Word32` in the first
-  alternative. `Pointer` field is shared between `String` and `Maybe Int` values
-  of the alternatives.
-
-  In the case of enumeration types (like `Bool`), the unboxed sum layout only
-  has an `Int32` field (i.e. the whole thing is represented by an integer).
+  The first ``Int32`` is for the tag. There are two ``Float32`` fields because
+  floating point types can't overlap with other types, because of limitations of
+  the code generator that we're hoping to overcome in the future. The second
+  alternative needs two ``Float32`` fields: The ``Word32`` field is for the
+  ``Word32#`` in the first alternative. The ``Pointer`` field is shared between
+  ``String`` and ``Maybe Int`` values of the alternatives.
 
-In the example above, a value of this type is thus represented as 5 values. As
-an another example, this is the layout for unboxed version of `Maybe a` type: ::
+  As another example, this is the layout for the unboxed version of ``Maybe a``
+  type, ``(# (# #) | a #)``: ::
 
     Int32, Pointer
 
-The `Pointer` field is not used when tag says that it's `Nothing`. Otherwise
-`Pointer` points to the value in `Just`.
+  The ``Pointer`` field is not used when tag says that it's ``Nothing``.
+  Otherwise ``Pointer`` points to the value in ``Just``. As mentioned
+  above, this type is lazy in its lifted field. Therefore, the type ::
+
+    data Maybe' a = Maybe' (# (# #) | a #)
+
+  is *precisely* isomorphic to the type ``Maybe a``, although its memory
+  representation is different.
+
+  In the degenerate case where all the alternatives have zero width, such
+  as the ``Bool``-like ``(# (# #) | (# #) #)``, the unboxed sum layout only
+  has an ``Int32`` tag field (i.e., the whole thing is represented by an integer).
 
 .. _syntax-extns:
 
@@ -514,11 +526,8 @@ instance, the binary integer literal ``0b11001001`` will be desugared into
 Hexadecimal floating point literals
 -----------------------------------
 
-.. ghc-flag:: -XHexFloatLiterals
+.. extension:: HexFloatLiterals
     :shortdesc: Enable support for :ref:`hexadecimal floating point literals <hex-float-literals>`.
-    :type: dynamic
-    :reverse: -XNoHexFloatLIterals
-    :category:
 
     :since: 8.4.1
 
@@ -531,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:
@@ -553,6 +562,94 @@ by one bit left (negative) or right (positive).  Here are some examples:
 
 
 
+.. _numeric-underscores:
+
+Numeric underscores
+-------------------
+
+.. extension:: NumericUnderscores
+    :shortdesc: Enable support for :ref:`numeric underscores <numeric-underscores>`.
+
+    :since: 8.6.1
+
+    Allow the use of underscores in numeric literals.
+
+GHC allows for numeric literals to be given in decimal, octal, hexadecimal,
+binary, or float notation.
+
+The language extension :extension:`NumericUnderscores` adds support for expressing
+underscores in numeric literals.
+For instance, the numeric literal ``1_000_000`` will be parsed into
+``1000000`` when :extension:`NumericUnderscores` is enabled.
+That is, underscores in numeric literals are ignored when
+:extension:`NumericUnderscores` is enabled.
+See also :ghc-ticket:`14473`.
+
+For example:
+
+.. code-block:: none
+
+    -- decimal
+    million    = 1_000_000
+    billion    = 1_000_000_000
+    lightspeed = 299_792_458
+    version    = 8_04_1
+    date       = 2017_12_31
+
+    -- hexadecimal
+    red_mask = 0xff_00_00
+    size1G   = 0x3fff_ffff
+
+    -- binary
+    bit8th   = 0b01_0000_0000
+    packbits = 0b1_11_01_0000_0_111
+    bigbits  = 0b1100_1011__1110_1111__0101_0011
+
+    -- float
+    pi       = 3.141_592_653_589_793
+    faraday  = 96_485.332_89
+    avogadro = 6.022_140_857e+23
+
+    -- function
+    isUnderMillion = (< 1_000_000)
+
+    clip64M x
+        | x > 0x3ff_ffff = 0x3ff_ffff
+        | otherwise = x
+
+    test8bit x = (0b01_0000_0000 .&. x) /= 0
+
+About validity:
+
+.. code-block:: none
+
+    x0 = 1_000_000   -- valid
+    x1 = 1__000000   -- valid
+    x2 = 1000000_    -- invalid
+    x3 = _1000000    -- invalid
+
+    e0 = 0.0001      -- valid
+    e1 = 0.000_1     -- valid
+    e2 = 0_.0001     -- invalid
+    e3 = _0.0001     -- invalid
+    e4 = 0._0001     -- invalid
+    e5 = 0.0001_     -- invalid
+
+    f0 = 1e+23       -- valid
+    f1 = 1_e+23      -- valid
+    f2 = 1__e+23     -- valid
+    f3 = 1e_+23      -- invalid
+
+    g0 = 1e+23       -- valid
+    g1 = 1e+_23      -- invalid
+    g2 = 1e+23_      -- invalid
+
+    h0 = 0xffff      -- valid
+    h1 = 0xff_ff     -- valid
+    h2 = 0x_ffff     -- valid
+    h3 = 0x__ffff    -- valid
+    h4 = _0xffff     -- invalid
+
 .. _pattern-guards:
 
 Pattern guards
@@ -646,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
@@ -1136,7 +1233,6 @@ Parallel List Comprehensions
 
 .. extension:: ParallelListComp
     :shortdesc: Enable parallel list comprehensions.
-        Implied by :extension:`ParallelArrays`.
 
     :since: 6.8.1
 
@@ -1500,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:
 
@@ -1547,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.
 
@@ -2011,6 +2109,104 @@ data constructor in an import or export list with the keyword
 ``pattern``, to allow the import or export of a data constructor without
 its parent type constructor (see :ref:`patsyn-impexp`).
 
+.. _block-arguments:
+
+More liberal syntax for function arguments
+------------------------------------------
+
+.. extension:: BlockArguments
+    :shortdesc: Allow ``do`` blocks and other constructs as function arguments.
+
+    :since: 8.6.1
+
+    Allow ``do`` expressions, lambda expressions, etc. to be directly used as
+    a function argument.
+
+In Haskell 2010, certain kinds of expressions can be used without parentheses
+as an argument to an operator, but not as an argument to a function.
+They include ``do``, lambda, ``if``, ``case``, and ``let``
+expressions. Some GHC extensions also define language constructs of this type:
+``mdo`` (:ref:`recursive-do-notation`), ``\case`` (:ref:`lambda-case`), and
+``proc`` (:ref:`arrow-notation`).
+
+The :extension:`BlockArguments` extension allows these constructs to be directly
+used as a function argument. For example::
+
+    when (x > 0) do
+      print x
+      exitFailure
+
+will be parsed as::
+
+    when (x > 0) (do
+      print x
+      exitFailure)
+
+and
+
+::
+
+    withForeignPtr fptr \ptr -> c_memcpy buf ptr size
+
+will be parsed as::
+
+    withForeignPtr fptr (\ptr -> c_memcpy buf ptr size)
+
+Changes to the grammar
+~~~~~~~~~~~~~~~~~~~~~~
+
+The Haskell report `defines
+<https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-220003>`_
+the ``lexp`` nonterminal thus (``*`` indicates a rule of interest)::
+
+    lexp  →  \ apat1 … apatn -> exp            (lambda abstraction, n ≥ 1)  *
+          |  let decls in exp                  (let expression)             *
+          |  if exp [;] then exp [;] else exp  (conditional)                *
+          |  case exp of { alts }              (case expression)            *
+          |  do { stmts }                      (do expression)              *
+          |  fexp
+
+    fexp  →  [fexp] aexp                       (function application)
+
+    aexp  →  qvar                              (variable)
+          |  gcon                              (general constructor)
+          |  literal
+          |  ( exp )                           (parenthesized expression)
+          |  qcon { fbind1 … fbindn }          (labeled construction)
+          |  aexp { fbind1 … fbindn }          (labelled update)
+          |  …
+
+The :extension:`BlockArguments` extension moves these production rules under
+``aexp``::
+
+    lexp  →  fexp
+
+    fexp  →  [fexp] aexp                       (function application)
+
+    aexp  →  qvar                              (variable)
+          |  gcon                              (general constructor)
+          |  literal
+          |  ( exp )                           (parenthesized expression)
+          |  qcon { fbind1 … fbindn }          (labeled construction)
+          |  aexp { fbind1 … fbindn }          (labelled update)
+          |  \ apat1 … apatn -> exp            (lambda abstraction, n ≥ 1)  *
+          |  let decls in exp                  (let expression)             *
+          |  if exp [;] then exp [;] else exp  (conditional)                *
+          |  case exp of { alts }              (case expression)            *
+          |  do { stmts }                      (do expression)              *
+          |  …
+
+Now the ``lexp`` nonterminal is redundant and can be dropped from the grammar.
+
+Note that this change relies on an existing meta-rule to resolve ambiguities:
+
+    The grammar is ambiguous regarding the extent of lambda abstractions, let
+    expressions, and conditionals. The ambiguity is resolved by the meta-rule
+    that each of these constructs extends as far to the right as possible.
+
+For example, ``f \a -> a b`` will be parsed as ``f (\a -> a b)``, not as ``f
+(\a -> a) b``.
+
 .. _syntax-stolen:
 
 Summary of stolen syntax
@@ -2040,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::
@@ -2101,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
@@ -2118,15 +2318,23 @@ 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.
 
-      data S      -- S :: *
-      data T a    -- T :: * -> *
+For example: ::
+
+      data S      -- S :: Type
+      data T a    -- T :: Type -> Type
 
-Syntactically, the declaration lacks the "= constrs" part. The type can
-be parameterised over types of any kind, but if the kind is not ``*``
-then an explicit kind annotation must be used (see :ref:`kinding`).
+Syntactically, the declaration lacks the "= constrs" part. The type can be
+parameterised over types of any kind, but if the kind is not ``Type`` then an
+explicit kind annotation must be used (see :ref:`kinding`).
 
 Such data types have only one value, namely bottom. Nevertheless, they
 can be useful when defining "phantom types".
@@ -2205,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:
 
@@ -2755,16 +2962,16 @@ type declarations.
    in the "``data Set a where``" header have no scope. Indeed, one can
    write a kind signature instead: ::
 
-         data Set :: * -> * where ...
+         data Set :: Type -> Type where ...
 
    or even a mixture of the two: ::
 
-         data Bar a :: (* -> *) -> * where ...
+         data Bar a :: (Type -> Type) -> Type where ...
 
    The type variables (if given) may be explicitly kinded, so we could
    also write the header for ``Foo`` like this: ::
 
-         data Bar a (b :: * -> *) where ...
+         data Bar a (b :: Type -> Type) where ...
 
 -  You can use strictness annotations, in the obvious places in the
    constructor type: ::
@@ -3022,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).
 
@@ -3356,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).
@@ -3583,12 +3788,12 @@ declaration, to generate a standard instance declaration for specified class.
 GHC extends this mechanism along several axes:
 
 * The derivation mechanism can be used separtely from the data type
-  declaration, using the the `standalone deriving mechanism
+  declaration, using the `standalone deriving mechanism
   <#stand-alone-deriving>`__.
 
 * 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
@@ -3712,11 +3917,21 @@ number of important ways:
    module as the data type declaration. (But be aware of the dangers of
    orphan instances (:ref:`orphan-modules`).
 
--  You must supply an explicit context (in the example the context is
-   ``(Eq a)``), exactly as you would in an ordinary instance
+-  In most cases, you must supply an explicit context (in the example the
+   context is ``(Eq a)``), exactly as you would in an ordinary instance
    declaration. (In contrast, in a ``deriving`` clause attached to a
    data type declaration, the context is inferred.)
 
+   The exception to this rule is that the context of a standalone deriving
+   declaration can infer its context when a single, extra-wildcards constraint
+   is used as the context, such as in: ::
+
+         deriving instance _ => Eq (Foo a)
+
+   This is essentially the same as if you had written ``deriving Foo`` after
+   the declaration for ``data Foo a``. Using this feature requires the use of
+   :extension:`PartialTypeSignatures` (:ref:`partial-type-signatures`).
+
 -  Unlike a ``deriving`` declaration attached to a ``data`` declaration,
    the instance can be more specific than the data type (assuming you
    also use :extension:`FlexibleInstances`, :ref:`instance-rules`). Consider
@@ -3847,7 +4062,7 @@ Deriving ``Functor`` instances
 
 
 With :extension:`DeriveFunctor`, one can derive ``Functor`` instances for data types
-of kind ``* -> *``. For example, this declaration::
+of kind ``Type -> Type``. For example, this declaration::
 
     data Example a = Ex a Char (Example a) (Example Char)
       deriving Functor
@@ -3903,7 +4118,7 @@ causes the generated code to be ill-typed.
 
 As a general rule, if a data type has a derived ``Functor`` instance and its
 last type parameter occurs on the right-hand side of the data declaration, then
-either it must (1) occur bare (e.g., ``newtype Id a = a``), or (2) occur as the
+either it must (1) occur bare (e.g., ``newtype Id a = Id a``), or (2) occur as the
 last argument of a type constructor (as in ``Right`` above).
 
 There are two exceptions to this rule:
@@ -3923,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.
 
@@ -4040,7 +4255,7 @@ Deriving ``Foldable`` instances
     Allow automatic deriving of instances for the ``Foldable`` typeclass.
 
 With :extension:`DeriveFoldable`, one can derive ``Foldable`` instances for data types
-of kind ``* -> *``. For example, this declaration::
+of kind ``Type -> Type``. For example, this declaration::
 
     data Example a = Ex a Char (Example a) (Example Char)
       deriving Foldable
@@ -4159,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
@@ -4182,7 +4397,7 @@ Deriving ``Traversable`` instances
     Allow automatic deriving of instances for the ``Traversable`` typeclass.
 
 With :extension:`DeriveTraversable`, one can derive ``Traversable`` instances for data
-types of kind ``* -> *``. For example, this declaration::
+types of kind ``Type -> Type``. For example, this declaration::
 
     data Example a = Ex a Char (Example a) (Example Char)
       deriving (Functor, Foldable, Traversable)
@@ -4253,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
 
@@ -4308,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.
@@ -4390,7 +4605,7 @@ Generalised derived instances for newtypes
                GeneralizedNewtypeDeriving
     :shortdesc: Enable newtype deriving.
 
-    :since: 6.8.1
+    :since: 6.8.1. British spelling since 8.6.1.
 
     Enable GHC's cunning generalised deriving mechanism for ``newtype``\s
 
@@ -4414,6 +4629,9 @@ It is particularly galling that, since the constructor doesn't appear at
 run-time, this instance declaration defines a dictionary which is
 *wholly equivalent* to the ``Int`` dictionary, only slower!
 
+:extension:`DerivingVia` (see :ref:`deriving-via`) is a generalization of
+this idea.
+
 .. _generalized-newtype-deriving:
 
 Generalising the deriving clause
@@ -4466,7 +4684,7 @@ In this case the derived instance declaration is of the form ::
       instance Monad (State [tok] (Failure m)) => Monad (Parser tok m)
 
 Notice that, since ``Monad`` is a constructor class, the instance is a
-*partial application* of the new type, not the entire left hand side. We
+*partial application* of the newtype, not the entire left hand side. We
 can imagine that the type declaration is "eta-converted" to generate the
 context of the instance declaration.
 
@@ -4494,6 +4712,43 @@ declarations are treated uniformly (and implemented just by reusing the
 dictionary for the representation type), *except* ``Show`` and ``Read``,
 which really behave differently for the newtype and its representation.
 
+.. note::
+
+    It is sometimes necessary to enable additional language extensions when
+    deriving instances via :extension:`GeneralizedNewtypeDeriving`. For instance,
+    consider a simple class and instance using :extension:`UnboxedTuples`
+    syntax: ::
+
+        {-# LANGUAGE UnboxedTuples #-}
+
+        module Lib where
+
+        class AClass a where
+          aMethod :: a -> (# Int, a #)
+
+        instance AClass Int where
+          aMethod x = (# x, x #)
+
+    The following will fail with an "Illegal unboxed tuple" error, since the
+    derived instance produced by the compiler makes use of unboxed tuple syntax,
+    ::
+
+        {-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+        import Lib
+
+        newtype Int' = Int' Int
+                     deriving (AClass)
+
+    However, enabling the :extension:`UnboxedTuples` extension allows the module
+    to compile. Similar errors may occur with a variety of extensions,
+    including:
+
+      * :extension:`UnboxedTuples`
+      * :extension:`PolyKinds`
+      * :extension:`MultiParamTypeClasses`
+      * :extension:`FlexibleContexts`
+
 .. _precise-gnd-specification:
 
 A more precise specification
@@ -4704,6 +4959,11 @@ isn't sophisticated enough to determine this, so you'll need to enable
 you do go down this route, make sure you can convince yourself that all of
 the type family instances you're deriving will eventually terminate if used!
 
+Note that :extension:`DerivingVia` (see :ref:`deriving-via`) uses essentially
+the same specification to derive instances of associated type families as well
+(except that it uses the ``via`` type instead of the underlying ``rep-type``
+of a newtype).
+
 .. _derive-any-class:
 
 Deriving any other class
@@ -4907,10 +5167,12 @@ Currently, the deriving strategies are:
 - ``stock``: Have GHC implement a "standard" instance for a data type,
   if possible (e.g., ``Eq``, ``Ord``, ``Generic``, ``Data``, ``Functor``, etc.)
 
-- ``anyclass``: Use :extension:`DeriveAnyClass`
+- ``anyclass``: Use :extension:`DeriveAnyClass` (see :ref:`derive-any-class`)
 
 - ``newtype``: Use :extension:`GeneralizedNewtypeDeriving`
+               (see :ref:`newtype-deriving`)
 
+- ``via``: Use :extension:`DerivingVia` (see :ref:`deriving-via`)
 
 .. _default-deriving-strategy:
 
@@ -4944,6 +5206,118 @@ In that case, GHC chooses the strategy as follows:
    user is warned about the ambiguity. The warning can be avoided by explicitly
    stating the desired deriving strategy.
 
+.. _deriving-via:
+
+Deriving via
+------------
+
+.. extension:: DerivingVia
+    :shortdesc: Enable deriving instances ``via`` types of the same runtime
+        representation.
+        Implies :extension:`DerivingStrategies`.
+
+    :implies: :extension:`DerivingStrategies`
+
+    :since: 8.6.1
+
+This allows ``deriving`` a class instance for a type by specifying
+another type of equal runtime representation (such that there exists a
+``Coercible`` instance between the two: see :ref:`coercible`) that is
+already an instance of the that class.
+
+:extension:`DerivingVia` is indicated by the use of the ``via``
+deriving strategy. ``via`` requires specifying another type (the ``via`` type)
+to ``coerce`` through. For example, this code: ::
+
+    {-# LANGUAGE DerivingVia #-}
+
+    import Numeric
+
+    newtype Hex a = Hex a
+
+    instance (Integral a, Show a) => Show (Hex a) where
+      show (Hex a) = "0x" ++ showHex a ""
+
+    newtype Unicode = U Int
+      deriving Show
+        via (Hex Int)
+
+    -- >>> euroSign
+    -- 0x20ac
+    euroSign :: Unicode
+    euroSign = U 0x20ac
+
+Generates the following instance ::
+
+    instance Show Unicode where
+      show :: Unicode -> String
+      show = Data.Coerce.coerce
+        @(Hex Int -> String)
+        @(Unicode -> String)
+        show
+
+This extension generalizes :extension:`GeneralizedNewtypeDeriving`. To
+derive ``Num Unicode`` with GND (``deriving newtype Num``) it must
+reuse the ``Num Int`` instance. With ``DerivingVia``, we can explicitly
+specify the representation type ``Int``: ::
+
+    newtype Unicode = U Int
+      deriving Num
+        via Int
+
+      deriving Show
+        via (Hex Int)
+
+    euroSign :: Unicode
+    euroSign = 0x20ac
+
+Code duplication is common in instance declarations. A familiar
+pattern is lifting operations over an ``Applicative`` functor.
+Instead of having catch-all instances for ``f a`` which overlap
+with all other such instances, like so: ::
+
+    instance (Applicative f, Semigroup a) => Semigroup (f a) ..
+    instance (Applicative f, Monoid    a) => Monoid    (f a) ..
+
+We can instead create a newtype ``App``
+(where ``App f a`` and ``f a`` are represented the same in memory)
+and use :extension:`DerivingVia` to explicitly enable uses of this
+pattern: ::
+
+    {-# LANGUAGE DerivingVia, DeriveFunctor, GeneralizedNewtypeDeriving #-}
+
+    import Control.Applicative
+
+    newtype App f a = App (f a) deriving newtype (Functor, Applicative)
+
+    instance (Applicative f, Semigroup a) => Semigroup (App f a) where
+      (<>) = liftA2 (<>)
+
+    instance (Applicative f, Monoid a) => Monoid (App f a) where
+      mempty = pure mempty
+
+    data Pair a = MkPair a a
+      deriving stock
+        Functor
+
+      deriving (Semigroup, Monoid)
+        via (App Pair a)
+
+    instance Applicative Pair where
+      pure a = MkPair a a
+
+      MkPair f g <*> MkPair a b = MkPair (f a) (g b)
+
+Note that the ``via`` type does not have to be a ``newtype``.
+The only restriction is that it is coercible with the
+original data type. This means there can be arbitrary nesting of newtypes,
+as in the following example: ::
+
+    newtype Kleisli m a b = (a -> m b)
+      deriving (Semigroup, Monoid)
+        via (a -> App m b)
+
+Here we make use of the ``Monoid ((->) a)`` instance.
 
 .. _pattern-synonyms:
 
@@ -4959,7 +5333,7 @@ Pattern synonyms
 
 Pattern synonyms are enabled by the language extension :extension:`PatternSynonyms`, which is
 required for defining them, but *not* for using them. More information and
-examples of view patterns can be found on the `Wiki page <PatternSynonyms>`.
+examples of pattern synonyms can be found on the :ghc-wiki:`Wiki page <PatternSynonyms>`.
 
 Pattern synonyms enable giving names to parametrized pattern schemes.
 They can also be thought of as abstract constructors that don't have a
@@ -5076,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.
 
 +---------------+----------------+---------------+---------------------------+
@@ -5149,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:
@@ -5163,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.
@@ -5329,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
@@ -5390,6 +5798,24 @@ Matching of pattern synonyms
 
 A pattern synonym occurrence in a pattern is evaluated by first matching
 against the pattern synonym itself, and then on the argument patterns.
+
+More precisely, the semantics of pattern matching is given in
+`Section 3.17 of the Haskell 2010 report <https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-580003.17>`__.   To the informal semantics in Section 3.17.2 we add this extra rule:
+
+* If the pattern is a constructor pattern ``(P p1 ... pn)``, where ``P`` is
+  a pattern synonym defined by ``P x1 ... xn = p`` or ``P x1 ... xn <- p``, then:
+
+  (a) Match the value ``v`` against ``p``. If this match fails or diverges,
+      so does the whole (pattern synonym) match.   Otherwise the match
+      against ``p`` must bind the variables ``x1 ... xn``; let them be bound to values ``v1 ... vn``.
+
+  (b) Match ``v1`` against ``p1``, ``v2`` against ``p2`` and so on.
+      If any of these matches fail or diverge, so does the whole match.
+
+  (c) If all the matches against the ``pi`` succeed, the match succeeds,
+      binding the variables bound by the ``pi`` . (The ``xi`` are not
+      bound; they remain local to the pattern synonym declaration.)
+
 For example, in the following program, ``f`` and ``f'`` are equivalent: ::
 
     pattern Pair x y <- [x, y]
@@ -5454,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
 
@@ -5939,9 +6364,9 @@ original definition of ``Collects`` with a simple dependency: ::
 
 The dependency ``ce -> e`` here specifies that the type ``e`` of elements is
 uniquely determined by the type of the collection ``ce``. Note that both
-parameters of Collects are of kind ``*``; there are no constructor classes
-here. Note too that all of the instances of ``Collects`` that we gave
-earlier can be used together with this new definition.
+parameters of Collects are of kind ``Type``; there are no constructor classes
+here. Note too that all of the instances of ``Collects`` that we gave earlier
+can be used together with this new definition.
 
 What about the ambiguity problems that we encountered with the original
 definition? The empty function still has type ``Collects e ce => ce``, but
@@ -6039,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
@@ -6326,7 +6750,7 @@ Overlapping instances
 
 In general, as discussed in :ref:`instance-resolution`, *GHC requires
 that it be unambiguous which instance declaration should be used to
-resolve a type-class constraint*. GHC also provides a way to to loosen
+resolve a type-class constraint*. GHC also provides a way to loosen
 the instance resolution, by allowing more than one instance to match,
 *provided there is a most specific one*. Moreover, it can be loosened
 further, by allowing more than one instance to match irrespective of
@@ -6370,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
 
-   -  There is another candidate :math:`IY` that is strictly more specific; that
+-  Eliminate any candidate :math:`IX` for which there is another candidate
+   :math:`IY` such that both of the following hold:
+
+   -  :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
@@ -6380,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
@@ -6434,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
@@ -6483,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
@@ -6626,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
@@ -6654,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
@@ -6685,7 +7131,7 @@ Overloaded labels
 
 GHC supports *overloaded labels*, a form of identifier whose interpretation may
 depend both on its type and on its literal text.  When the
-:extension:`OverloadedLabels` extension is enabled, an overloaded label can written
+:extension:`OverloadedLabels` extension is enabled, an overloaded label can be written
 with a prefix hash, for example ``#foo``.  The type of this expression is
 ``IsLabel "foo" a => a``.
 
@@ -6982,7 +7428,7 @@ example (Trac #10318) ::
             Fractional (Frac a),
             IntegralDomain (Frac a))
          => IntegralDomain a where
-      type Frac a :: *
+      type Frac a :: Type
 
 Here the superclass cycle does terminate but it's not entirely straightforward
 to see that it does.
@@ -7088,11 +7534,11 @@ Data family declarations
 
 Indexed data families are introduced by a signature, such as ::
 
-    data family GMap k :: * -> *
+    data family GMap k :: Type -> Type
 
 The special ``family`` distinguishes family from standard data
 declarations. The result kind annotation is optional and, as usual,
-defaults to ``*`` if omitted. An example is ::
+defaults to ``Type`` if omitted. An example is ::
 
     data family Array e
 
@@ -7100,12 +7546,12 @@ Named arguments can also be given explicit kind signatures if needed.
 Just as with :ref:`GADT declarations <gadt>` named arguments are
 entirely optional, so that we can declare ``Array`` alternatively with ::
 
-    data family Array :: * -> *
+    data family Array :: Type -> Type
 
 Unlike with ordinary data definitions, the result kind of a data family
-does not need to be ``*``: it can alternatively be a kind variable
+does not need to be ``Type``: it can alternatively be a kind variable
 (with :extension:`PolyKinds`). Data instances' kinds must end in
-``*``, however.
+``Type``, however.
 
 .. _data-instance-declarations:
 
@@ -7128,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
@@ -7141,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
@@ -7232,35 +7692,36 @@ Type family declarations
 
 Open indexed type families are introduced by a signature, such as ::
 
-    type family Elem c :: *
+    type family Elem c :: Type
 
 The special ``family`` distinguishes family from standard type
 declarations. The result kind annotation is optional and, as usual,
-defaults to ``*`` if omitted. An example is ::
+defaults to ``Type`` if omitted. An example is ::
 
     type family Elem c
 
 Parameters can also be given explicit kind signatures if needed. We call
 the number of parameters in a type family declaration, the family's
 arity, and all applications of a type family must be fully saturated
-with respect to to that arity. This requirement is unlike ordinary type synonyms
+with respect to that arity. This requirement is unlike ordinary type synonyms
 and it implies that the kind of a type family is not sufficient to
 determine a family's arity, and hence in general, also insufficient to
 determine whether a type family application is well formed. As an
 example, consider the following declaration: ::
 
-    type family F a b :: * -> *   -- F's arity is 2,
-                                  -- although its overall kind is * -> * -> * -> *
+    type family F a b :: Type -> Type
+      -- F's arity is 2,
+      -- although its overall kind is Type -> Type -> Type -> Type
 
 Given this declaration the following are examples of well-formed and
 malformed types: ::
 
-    F Char [Int]       -- OK!  Kind: * -> *
-    F Char [Int] Bool  -- OK!  Kind: *
+    F Char [Int]       -- OK!  Kind: Type -> Type
+    F Char [Int] Bool  -- OK!  Kind: Type
     F IO Bool          -- WRONG: kind mismatch in the first argument
     F Bool             -- WRONG: unsaturated application
 
-The result kind annotation is optional and defaults to ``*`` (like
+The result kind annotation is optional and defaults to ``Type`` (like
 argument kinds) if omitted. Polykinded type families can be declared
 using a parameter in the kind annotation: ::
 
@@ -7292,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
@@ -7326,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
@@ -7344,7 +7815,7 @@ Type family examples
 
 Here are some examples of admissible and illegal type instances: ::
 
-    type family F a :: *
+    type family F a :: Type
     type instance F [Int]   = Int   -- OK!
     type instance F String  = Char  -- OK!
     type instance F (F a)   = a     -- WRONG: type parameter mentions a type family
@@ -7359,7 +7830,7 @@ Here are some examples of admissible and illegal type instances: ::
     type instance H Char = Char    -- WRONG: cannot have instances of closed family
     type family K a where          -- OK!
 
-    type family G a b :: * -> *
+    type family G a b :: Type -> Type
     type instance G Int            = (,)     -- WRONG: must be two type parameters
     type instance G Int Char Float = Double  -- WRONG: must be two type parameters
 
@@ -7410,8 +7881,8 @@ like types. For example, the following is accepted: ::
     type instance J Int = Bool
     type instance J Int = Maybe
 
-These instances are compatible because they differ in their implicit
-kind parameter; the first uses ``*`` while the second uses ``* -> *``.
+These instances are compatible because they differ in their implicit kind
+parameter; the first uses ``Type`` while the second uses ``Type -> Type``.
 
 The definition for "compatible" uses a notion of "apart", whose
 definition in turn relies on type family reduction. This condition of
@@ -7503,11 +7974,11 @@ When the name of a type argument of a data or type instance
 declaration doesn't matter, it can be replaced with an underscore
 (``_``). This is the same as writing a type variable with a unique name. ::
 
-    data family F a b :: *
+    data family F a b :: Type
     data instance F Int _ = Int
     -- Equivalent to  data instance F Int b = Int
 
-    type family T a :: *
+    type family T a :: Type
     type instance T (a,_) = a
     -- Equivalent to  type instance T (a,b) = a
 
@@ -7534,11 +8005,11 @@ A data or type synonym family can be declared as part of a type class,
 thus: ::
 
     class GMapKey k where
-      data GMap k :: * -> *
+      data GMap k :: Type -> Type
       ...
 
     class Collects ce where
-      type Elem ce :: *
+      type Elem ce :: Type
       ...
 
 When doing so, we (optionally) may drop the "``family``" keyword.
@@ -7550,12 +8021,12 @@ may be omitted and they may be in an order other than in the class head.
 Hence, the following contrived example is admissible: ::
 
       class C a b c where
-        type T c a x :: *
+        type T c a x :: Type
 
 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
 ~~~~~~~~~~~~~~~~~~~~
@@ -7572,12 +8043,12 @@ 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: ::
 
     class Collects ce where
-      type Elem ce :: *
+      type Elem ce :: Type
 
     instance Eq (Elem [e]) => Collects [e] where
       -- Choose one of the following alternatives:
@@ -7598,17 +8069,17 @@ Note the following points:
    to mention kind variables that are implicitly bound. For example, these are
    legitimate: ::
 
-    data family Nat :: k -> k -> *
+    data family Nat :: k -> k -> Type
     -- k is implicitly bound by an invisible kind pattern
-    newtype instance Nat :: (k -> *) -> (k -> *) -> * where
+    newtype instance Nat :: (k -> Type) -> (k -> Type) -> Type where
       Nat :: (forall xx. f xx -> g xx) -> Nat f g
 
     class Funct f where
-      type Codomain f :: *
+      type Codomain f :: Type
     instance Funct ('KProxy :: KProxy o) where
       -- o is implicitly bound by the kind signature
       -- of the LHS type pattern ('KProxy)
-      type Codomain 'KProxy = NatTr (Proxy :: o -> *)
+      type Codomain 'KProxy = NatTr (Proxy :: o -> Type)
 
 -  The instance for an associated type can be omitted in class
    instances. In that case, unless there is a default instance (see
@@ -7629,7 +8100,16 @@ Note the following points:
    parameter is ``[v]``, and one for which it is ``Int``. Since you
    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 ``*``).
+   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:
 
@@ -7667,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.
 
@@ -7674,8 +8158,8 @@ Here are some examples:
 
 ::
 
-      class C (a :: *) where
-        type F1 a :: *
+      class C (a :: Type) where
+        type F1 a :: Type
         type instance F1 a = [a]     -- OK
         type instance F1 a = a->a    -- BAD; only one default instance is allowed
 
@@ -7810,7 +8294,7 @@ Recall our running ``GMapKey`` class example:
 ::
 
     class GMapKey k where
-      data GMap k :: * -> *
+      data GMap k :: Type -> Type
       insert :: GMap k v -> k -> v -> GMap k v
       lookup :: GMap k v -> k -> Maybe v
       empty  :: GMap k v
@@ -8106,7 +8590,7 @@ Motivation
 Standard Haskell has a rich type language. Types classify terms and
 serve to avoid many common programming mistakes. The kind language,
 however, is relatively simple, distinguishing only regular types (kind
-``*``) and type constructors (e.g. kind ``* -> * -> *``).
+``Type``) and type constructors (e.g. kind ``Type -> Type -> Type``).
 In particular when using advanced type
 system features, such as type families (:ref:`type-families`) or GADTs
 (:ref:`gadt`), this simple kind system is insufficient, and fails to
@@ -8116,11 +8600,11 @@ numbers, and length-indexed vectors: ::
     data Ze
     data Su n
 
-    data Vec :: * -> * -> * where
+    data Vec :: Type -> Type -> Type where
       Nil  :: Vec a Ze
       Cons :: a -> Vec a n -> Vec a (Su n)
 
-The kind of ``Vec`` is ``* -> * -> *``. This means that, e.g.,
+The kind of ``Vec`` is ``Type -> Type -> Type``. This means that, e.g.,
 ``Vec Int Char`` is a well-kinded type, even though this is not what we
 intend when defining length-indexed vectors.
 
@@ -8128,7 +8612,7 @@ With :extension:`DataKinds`, the example above can then be rewritten to: ::
 
     data Nat = Ze | Su Nat
 
-    data Vec :: * -> Nat -> * where
+    data Vec :: Type -> Nat -> Type where
       Nil  :: Vec a 'Ze
       Cons :: a -> Vec a n -> Vec a ('Su n)
 
@@ -8153,48 +8637,39 @@ following types ::
 give rise to the following kinds and type constructors (where promoted
 constructors are prefixed by a tick ``'``): ::
 
-    Nat :: *
+    Nat :: Type
     'Zero :: Nat
     'Succ :: Nat -> Nat
 
-    List :: * -> *
+    List :: Type -> Type
     'Nil  :: forall k. List k
     'Cons :: forall k. k -> List k -> List k
 
-    Pair  :: * -> * -> *
+    Pair  :: Type -> Type -> Type
     'Pair :: forall k1 k2. k1 -> k2 -> Pair k1 k2
 
-    Sum :: * -> * -> *
+    Sum :: Type -> Type -> Type
     'L :: k1 -> Sum k1 k2
     'R :: k2 -> Sum k1 k2
 
-The following restrictions apply to promotion:
-
--  We promote ``data`` types and ``newtypes``; type synonyms and
-   type/data families are not promoted (:ref:`type-families`).
-
--  We only promote types whose kinds are of the form
-   ``* -> ... -> * -> *``. In particular, we do not promote
-   higher-kinded datatypes such as ``data Fix f = In (f (Fix f))``, or
-   datatypes whose kinds involve promoted types such as
-   ``Vec :: * -> Nat -> *``.
-
--  We do not promote data constructors that are kind polymorphic,
-   involve constraints, mention type or data families, or involve types
-   that are not promotable.
+Virtually all data constructors, even those with rich kinds, can be promoted.
+There are only a couple of exceptions to this rule:
 
-The flag :extension:`TypeInType` (which implies :extension:`DataKinds`)
-relaxes some of these restrictions, allowing:
+-  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.
 
--  Promotion of type synonyms and type families, but not data families.
-   GHC's type theory just isn't up to the task of promoting data families,
-   which requires full dependent types.
+-  Data constructors with contexts that contain non-equality constraints cannot
+   be promoted. For example: ::
 
--  All datatypes, even those with rich kinds, get 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
 
-     data Proxy a = Proxy
-     data App f a = MkApp (f a)   -- App :: forall k. (k -> *) -> k -> *
-     x = Proxy :: Proxy ('MkApp ('Just 'True))
+   ``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:
 
@@ -8236,11 +8711,11 @@ With :extension:`DataKinds`, Haskell's list and tuple types are natively
 promoted to kinds, and enjoy the same convenient syntax at the type
 level, albeit prefixed with a quote: ::
 
-    data HList :: [*] -> * where
+    data HList :: [Type] -> Type where
       HNil  :: HList '[]
       HCons :: a -> HList t -> HList (a ': t)
 
-    data Tuple :: (*,*) -> * where
+    data Tuple :: (Type,Type) -> Type where
       Tuple :: a -> b -> Tuple '(a,b)
 
     foo0 :: HList '[]
@@ -8260,7 +8735,7 @@ Haskell.
 
 .. note::
     The declaration for ``HCons`` also requires :extension:`TypeOperators`
-    because of infix type operator ``(:')``
+    because of infix type operator ``(':)``
 
 
 .. _promotion-existentials:
@@ -8271,7 +8746,7 @@ Promoting existential data constructors
 Note that we do promote existential data constructors that are otherwise
 suitable. For example, consider the following: ::
 
-    data Ex :: * where
+    data Ex :: Type where
       MkEx :: forall a. a -> Ex
 
 Both the type ``Ex`` and the data constructor ``MkEx`` get promoted,
@@ -8290,7 +8765,7 @@ The return kind ``k`` is an implicit parameter to ``UnEx``. The
 elaborated definitions are as follows (where implicit parameters are
 denoted by braces): ::
 
-    type family UnEx {k :: *} (ex :: Ex) :: k
+    type family UnEx {k :: Type} (ex :: Ex) :: k
     type instance UnEx {k} (MkEx @k x) = x
 
 Thus, the instance triggers only when the implicit parameter to ``UnEx``
@@ -8303,22 +8778,18 @@ See also :ghc-ticket:`7347`.
 .. _type-in-type:
 .. _kind-polymorphism:
 
-Kind polymorphism and Type-in-Type
+Kind polymorphism
 ==================================
 
 .. extension:: TypeInType
-    :shortdesc: Allow kinds to be used as types,
-        including explicit kind variable quantification, higher-rank
-        kinds, kind synonyms, and kind families.
-        Implies :extension:`DataKinds`, :extension:`KindSignatures`,
-        and :extension:`PolyKinds`.
+    :shortdesc: Deprecated. Enable kind polymorphism and datatype promotion.
 
     :implies: :extension:`PolyKinds`, :extension:`DataKinds`, :extension:`KindSignatures`
     :since: 8.0.1
 
-    Allow kinds to be as intricate as types, allowing explicit quantification
-    over kind variables, higher-rank kinds, and the use of type synonyms and
-    families in kinds, among other features.
+    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.
@@ -8335,31 +8806,6 @@ although it is a conservative extension beyond standard Haskell. The extensions
 above simply enable syntax and tweak the inference algorithm to allow users to
 take advantage of the extra expressiveness of GHC's kind system.
 
-The difference between :extension:`TypeInType` and :extension:`PolyKinds`
----------------------------------------------------------------------------
-
-It is natural to consider :extension:`TypeInType` as an extension of
-:extension:`PolyKinds`. The latter simply enables fewer features of GHC's
-rich kind system than does the former. The need for two separate extensions
-stems from their history: :extension:`PolyKinds` was introduced for GHC 7.4,
-when it was experimental and temperamental. The wrinkles were smoothed out for
-GHC 7.6. :extension:`TypeInType` was introduced for GHC 8.0, and is currently
-experimental and temperamental, with the wrinkles to be smoothed out in due
-course. The intent of having the two extensions is that users can rely on
-:extension:`PolyKinds` to work properly while being duly sceptical of
-:extension:`TypeInType`. In particular, we recommend enabling
-:ghc-flag:`-dcore-lint` whenever using :extension:`TypeInType`; that extension
-turns on a set of internal checks within GHC that will discover bugs in the
-implementation of :extension:`TypeInType`. Please report bugs at `our bug
-tracker <https://ghc.haskell.org/trac/ghc/wiki/ReportABug>`__.
-
-Although we have tried to allow the new behavior only when
-:extension:`TypeInType` is enabled, some particularly thorny cases may have
-slipped through. It is thus possible that some construct is available in GHC
-8.0 with :extension:`PolyKinds` that was not possible in GHC 7.x. If you spot
-such a case, you are welcome to submit that as a bug as well. We flag
-newly-available capabilities below.
-
 Overview of kind polymorphism
 -----------------------------
 
@@ -8367,22 +8813,22 @@ Consider inferring the kind for ::
 
   data App f a = MkApp (f a)
 
-In Haskell 98, the inferred kind for ``App`` is ``(* -> *) -> * -> *``.
-But this is overly specific, because another suitable Haskell 98 kind for
-``App`` is ``((* -> *) -> *) -> (* -> *) -> *``, where the kind assigned
-to ``a`` is ``* -> *``. Indeed, without kind signatures
-(:extension:`KindSignatures`), it is necessary to use a dummy constructor
-to get a Haskell compiler to infer the second kind. With kind polymorphism
-(:extension:`PolyKinds`), GHC infers the kind ``forall k. (k -> *) -> k -> *``
-for ``App``, which is its most general kind.
+In Haskell 98, the inferred kind for ``App`` is ``(Type -> Type) -> Type ->
+Type``. But this is overly specific, because another suitable Haskell 98 kind
+for ``App`` is ``((Type -> Type) -> Type) -> (Type -> Type) -> Type``, where the
+kind assigned to ``a`` is ``Type -> Type``. Indeed, without kind signatures
+(:extension:`KindSignatures`), it is necessary to use a dummy constructor to get
+a Haskell compiler to infer the second kind. With kind polymorphism
+(:extension:`PolyKinds`), GHC infers the kind ``forall k. (k -> Type) -> k ->
+Type`` for ``App``, which is its most general kind.
 
 Thus, the chief benefit of kind polymorphism is that we can now infer these
 most general kinds and use ``App`` at a variety of kinds: ::
 
-  App Maybe Int   -- `k` is instantiated to *
+  App Maybe Int   -- `k` is instantiated to Type
 
-  data T a = MkT (a Int)    -- `a` is inferred to have kind (* -> *)
-  App T Maybe     -- `k` is instantiated to (* -> *)
+  data T a = MkT (a Int)    -- `a` is inferred to have kind (Type -> Type)
+  App T Maybe     -- `k` is instantiated to (Type -> Type)
 
 Overview of Type-in-Type
 ------------------------
@@ -8397,16 +8843,15 @@ between types and kinds is a hallmark of dependently typed languages.
 Full dependently typed languages also remove the difference between expressions
 and types, but doing that in GHC is a story for another day.
 
-One simplification allowed by combining types and kinds is that the type
-of ``*`` is just ``*``. It is true that the ``* :: *`` axiom can lead to
-non-termination, but this is not a problem in GHC, as we already have other
-means of non-terminating programs in both types and expressions. This
-decision (among many, many others) *does* mean that despite the expressiveness
-of GHC's type system, a "proof" you write in Haskell is not an irrefutable
-mathematical proof. GHC promises only partial correctness, that if your
-programs compile and run to completion, their results indeed have the types
-assigned. It makes no claim about programs that do not finish in a finite
-amount of time.
+One simplification allowed by combining types and kinds is that the type of
+``Type`` is just ``Type``. It is true that the ``Type :: Type`` axiom can lead
+to non-termination, but this is not a problem in GHC, as we already have other
+means of non-terminating programs in both types and expressions. This decision
+(among many, many others) *does* mean that despite the expressiveness of GHC's
+type system, a "proof" you write in Haskell is not an irrefutable mathematical
+proof. GHC promises only partial correctness, that if your programs compile and
+run to completion, their results indeed have the types assigned. It makes no
+claim about programs that do not finish in a finite amount of time.
 
 To learn more about this decision and the design of GHC under the hood
 please see the `paper <http://www.seas.upenn.edu/~sweirich/papers/fckinds.pdf>`__
@@ -8417,7 +8862,8 @@ Principles of kind inference
 
 Generally speaking, when :extension:`PolyKinds` is on, GHC tries to infer the
 most general kind for a declaration.
-In this case the definition has a right-hand side to inform kind
+In many cases (for example, in a datatype declaration)
+the definition has a right-hand side to inform kind
 inference. But that is not always the case. Consider ::
 
     type family F a
@@ -8425,42 +8871,114 @@ inference. But that is not always the case. Consider ::
 Type family declarations have no right-hand side, but GHC must still
 infer a kind for ``F``. Since there are no constraints, it could infer
 ``F :: forall k1 k2. k1 -> k2``, but that seems *too* polymorphic. So
-GHC defaults those entirely-unconstrained kind variables to ``*`` and we
-get ``F :: * -> *``. You can still declare ``F`` to be kind-polymorphic
+GHC defaults those entirely-unconstrained kind variables to ``Type`` and we
+get ``F :: Type -> Type``. You can still declare ``F`` to be kind-polymorphic
 using kind signatures: ::
 
-    type family F1 a                -- F1 :: * -> *
-    type family F2 (a :: k)         -- F2 :: forall k. k -> *
-    type family F3 a :: k           -- F3 :: forall k. * -> k
+    type family F1 a                -- F1 :: Type -> Type
+    type family F2 (a :: k)         -- F2 :: forall k. k -> Type
+    type family F3 a :: k           -- F3 :: forall k. Type -> k
     type family F4 (a :: k1) :: k2  -- F4 :: forall k1 k2. k1 -> k2
 
 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 ``*``, 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
       data D1 a        -- No right hand side for these two family
       type F1 a        -- declarations, but the class forces (a :: k)
-                       -- so   D1, F1 :: forall k. k -> *
+                       -- so   D1, F1 :: forall k. k -> Type
 
-    data D2 a   -- No right-hand side so D2 :: * -> *
-    type F2 a   -- No right-hand side so F2 :: * -> *
+    data D2 a   -- No right-hand side so D2 :: Type -> Type
+    type F2 a   -- No right-hand side so F2 :: Type -> Type
 
 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
@@ -8474,21 +8992,21 @@ Just as in type inference, kind inference for recursive types can only
 use *monomorphic* recursion. Consider this (contrived) example: ::
 
     data T m a = MkT (m a) (T Maybe (m a))
-    -- GHC infers kind  T :: (* -> *) -> * -> *
+    -- GHC infers kind  T :: (Type -> Type) -> Type -> Type
 
 The recursive use of ``T`` forced the second argument to have kind
-``*``. However, just as in type inference, you can achieve polymorphic
+``Type``. However, just as in type inference, you can achieve polymorphic
 recursion by giving a *complete user-supplied kind signature* (or CUSK)
 for ``T``. A CUSK is present when all argument kinds and the result kind
 are known, without any need for inference. For example: ::
 
-    data T (m :: k -> *) :: k -> * where
+    data T (m :: k -> Type) :: k -> Type where
       MkT :: m a -> T Maybe (m a) -> T m a
 
 The complete user-supplied kind signature specifies the polymorphic kind
 for ``T``, and this signature is used for all the calls to ``T``
 including the recursive ones. In particular, the recursive use of ``T``
-is at kind ``*``.
+is at kind ``Type``.
 
 What exactly is considered to be a "complete user-supplied kind
 signature" for a type constructor? These are the forms:
@@ -8499,35 +9017,30 @@ signature" for a type constructor? These are the forms:
    annotation does not affect whether or not the declaration has a
    complete signature. ::
 
-       data T1 :: (k -> *) -> k -> *       where ...
-       -- Yes;  T1 :: forall k. (k->*) -> k -> *
+       data T1 :: (k -> Type) -> k -> Type       where ...
+       -- Yes;  T1 :: forall k. (k->Type) -> k -> Type
 
-       data T2 (a :: k -> *) :: k -> *     where ...
-       -- Yes;  T2 :: forall k. (k->*) -> k -> *
+       data T2 (a :: k -> Type) :: k -> Type     where ...
+       -- Yes;  T2 :: forall k. (k->Type) -> k -> Type
 
-       data T3 (a :: k -> *) (b :: k) :: * where ...
-       -- Yes;  T3 :: forall k. (k->*) -> k -> *
+       data T3 (a :: k -> Type) (b :: k) :: Type where ...
+       -- Yes;  T3 :: forall k. (k->Type) -> k -> Type
 
-       data T4 (a :: k -> *) (b :: k)      where ...
-       -- Yes;  T4 :: forall k. (k->*) -> k -> *
+       data T4 (a :: k -> Type) (b :: k)      where ...
+       -- Yes;  T4 :: forall k. (k->Type) -> k -> Type
 
-       data T5 a (b :: k) :: *             where ...
+       data T5 a (b :: k) :: Type             where ...
        -- No;  kind is inferred
 
        data T6 a b                         where ...
        -- No;  kind is inferred
 
--  For a datatype with a top-level ``::`` when :extension:`TypeInType`
-   is in effect: all kind variables introduced after the ``::`` must
-   be explicitly quantified. ::
+-  For a datatype with a top-level ``::``: all kind variables introduced after
+   the ``::`` must be explicitly quantified. ::
 
-     -- -XTypeInType is on
-     data T1 :: k -> *            -- No CUSK: `k` is not explicitly quantified
-     data T2 :: forall k. k -> *  -- CUSK: `k` is bound explicitly
-     data T3 :: forall (k :: *). k -> *   -- still a CUSK
-
-   Note that the first example would indeed have a CUSK without
-   :extension:`TypeInType`.
+     data T1 :: k -> Type            -- No CUSK: `k` is not explicitly quantified
+     data T2 :: forall k. k -> Type  -- CUSK: `k` is bound explicitly
+     data T3 :: forall (k :: Type). k -> Type   -- still a CUSK
 
 -  For a class, every type variable must be annotated with a kind.
 
@@ -8543,13 +9056,12 @@ signature" for a type constructor? These are the forms:
    signature -- no inference can be done before detecting the signature.
 
 -  An un-associated open type or data family declaration *always* has a CUSK;
-   un-annotated type variables default to
-   kind ``*``: ::
+   un-annotated type variables default to kind ``Type``: ::
 
-       data family D1 a               -- D1 :: * -> *
-       data family D2 (a :: k)        -- D2 :: forall k. k -> *
-       data family D3 (a :: k) :: *   -- D3 :: forall k. k -> *
-       type family S1 a :: k -> *     -- S1 :: forall k. * -> k -> *
+       data family D1 a                  -- D1 :: Type -> Type
+       data family D2 (a :: k)           -- D2 :: forall k. k -> Type
+       data family D3 (a :: k) :: Type   -- D3 :: forall k. k -> Type
+       type family S1 a :: k -> Type     -- S1 :: forall k. Type -> k -> Type
 
 -  An associated type or data family declaration has a CUSK precisely if
    its enclosing class has a CUSK. ::
@@ -8564,21 +9076,15 @@ signature" for a type constructor? These are the forms:
    variables are annotated and a return kind (with a top-level ``::``)
    is supplied.
 
-With :extension:`TypeInType` enabled, it is possible to write a datatype
-that syntactically has a CUSK (according to the rules above)
-but actually requires some inference. As a very contrived example, consider ::
+It is possible to write a datatype that syntactically has a CUSK (according to
+the rules above) but actually requires some inference. As a very contrived
+example, consider ::
 
-  data Proxy a           -- Proxy :: forall k. k -> *
+  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
 --------------------------------------
@@ -8631,9 +9137,9 @@ for it: ::
 In the class declaration, nothing constrains the kind of the type ``a``,
 so it becomes a poly-kinded type variable ``(a :: k)``. Yet, in the
 instance declaration, the right-hand side of the associated type
-instance ``b -> b`` says that ``b`` must be of kind ``*``. GHC could
+instance ``b -> b`` says that ``b`` must be of kind ``Type``. GHC could
 theoretically propagate this information back into the instance head,
-and make that instance declaration apply only to type of kind ``*``, as
+and make that instance declaration apply only to type of kind ``Type``, as
 opposed to types of any kind. However, GHC does *not* do this.
 
 In short: GHC does *not* propagate kind information from the members of
@@ -8654,23 +9160,23 @@ type when figuring out how to generalise the type's kind.
 For example,
 consider these definitions (with :extension:`ScopedTypeVariables`): ::
 
-  data Proxy a    -- Proxy :: forall k. k -> *
+  data Proxy a    -- Proxy :: forall k. k -> Type
   p :: forall a. Proxy a
-  p = Proxy :: Proxy (a :: *)
+  p = Proxy :: Proxy (a :: Type)
 
 GHC reports an error, saying that the kind of ``a`` should be a kind variable
-``k``, not ``*``. This is because, by looking at the type signature
+``k``, not ``Type``. This is because, by looking at the type signature
 ``forall a. Proxy a``, GHC assumes ``a``'s kind should be generalised, not
-restricted to be ``*``. The function definition is then rejected for being
+restricted to be ``Type``. The function definition is then rejected for being
 more specific than its type signature.
 
 Explicit kind quantification
 ----------------------------
 
-Enabled by :extension:`TypeInType`, GHC now supports explicit kind quantification,
+Enabled by :extension:`PolyKinds`, GHC supports explicit kind quantification,
 as in these examples: ::
 
-  data Proxy :: forall k. k -> *
+  data Proxy :: forall k. k -> Type
   f :: (forall k (a :: k). Proxy a -> ()) -> Int
 
 Note that the second example has a ``forall`` that binds both a kind ``k`` and
@@ -8701,8 +9207,8 @@ Consider the type ::
 
 This datatype ``G`` is GADT-like in both its kind and its type. Suppose you
 have ``g :: G a``, where ``a :: k``. Then pattern matching to discover that
-``g`` is in fact ``GMaybe`` tells you both that ``k ~ (* -> *)`` and
-``a ~ Maybe``. The definition for ``G`` requires that :extension:`TypeInType`
+``g`` is in fact ``GMaybe`` tells you both that ``k ~ (Type -> Type)`` and
+``a ~ Maybe``. The definition for ``G`` requires that :extension:`PolyKinds`
 be in effect, but pattern-matching on ``G`` requires no extension beyond
 :extension:`GADTs`. That this works is actually a straightforward extension
 of regular GADTs and a consequence of the fact that kinds and types are the
@@ -8753,12 +9259,29 @@ In this redefinition, we give an explicit kind for ``(:~~:)``, deferring the cho
 of ``k2`` until after the first argument (``a``) has been given. With this declaration
 for ``(:~~:)``, the instance for ``HTestEquality`` is accepted.
 
+Another difference between higher-rank kinds and types can be found in their
+treatment of inferred and user-specified type variables. Consider the following
+program: ::
+
+  newtype Foo (f :: forall k. k -> Type) = MkFoo (f Int)
+  data Proxy a = Proxy
+
+  foo :: Foo Proxy
+  foo = MkFoo Proxy
+
+The kind of ``Foo``'s parameter is ``forall k. k -> Type``, but the kind of
+``Proxy`` is ``forall {k}. k -> Type``, where ``{k}`` denotes that the kind
+variable ``k`` is to be inferred, not specified by the user. (See
+:ref:`visible-type-application` for more discussion on the inferred-specified
+distinction). GHC does not consider ``forall k. k -> Type`` and
+``forall {k}. k -> Type`` to be equal at the kind level, and thus rejects
+``Foo Proxy`` as ill-kinded.
+
 Constraints in kinds
 --------------------
 
-As kinds and types are the same, kinds can now (with :extension:`TypeInType`)
-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: ::
 
@@ -8767,7 +9290,7 @@ Here is an example of a constrained kind: ::
     IsTypeLit Symbol = 'True
     IsTypeLit a      = 'False
 
-  data T :: forall a. (IsTypeLit a ~ 'True) => a -> * where
+  data T :: forall a. (IsTypeLit a ~ 'True) => a -> Type where
     MkNat    :: T 42
     MkSymbol :: T "Don't panic!"
 
@@ -8776,50 +9299,22 @@ we get an error that the equality constraint is not satisfied; ``Int`` is
 not a type literal. Note that explicitly quantifying with ``forall a`` is
 not necessary here.
 
-The kind ``*``
---------------
-
-The kind ``*`` classifies ordinary types. Without :extension:`TypeInType`,
-this identifier is always in scope when writing a kind. However, with
-:extension:`TypeInType`, a user may wish to use ``*`` in a type or a
-type operator ``*`` in a kind. To make this all more manageable, ``*``
-becomes an (almost) ordinary name with :extension:`TypeInType` enabled.
-So as not to cause naming collisions, it is not imported by default;
-you must ``import Data.Kind`` to get ``*`` (but only with :extension:`TypeInType`
-enabled).
-
-The only way ``*`` is unordinary is in its parsing. In order to be backward
-compatible, ``*`` is parsed as if it were an alphanumeric identifier; note
-that we do not write ``Int :: (*)`` but just plain ``Int :: *``. Due to the
-bizarreness with which ``*`` is parsed--and the fact that it is the only such
-operator in GHC--there are some corner cases that are
-not handled. We are aware of three:
-
-- In a Haskell-98-style data constructor, you must put parentheses around
-  ``*``, like this: ::
-
-    data Universe = Ty (*) | Num Int | ...
-
-- In an import/export list, you must put parentheses around ``*``, like this: ::
-
-    import Data.Kind ( type (*) )
-
-  Note that the keyword ``type`` there is just to disambiguate the import
-  from a term-level ``(*)``. (:ref:`explicit-namespaces`)
+The kind ``Type``
+-----------------
 
-- In an instance declaration head (the part after the word ``instance``), you
-  must parenthesize ``*``. This applies to all manners of instances, including
-  the left-hand sides of individual equations of a closed type family.
+.. extension:: StarIsType
+    :shortdesc: Treat ``*`` as ``Data.Kind.Type``.
 
-The ``Data.Kind`` module also exports ``Type`` as a synonym for ``*``.
-Now that type synonyms work in kinds, it is conceivable that we will deprecate
-``*`` when there is a good migration story for everyone to use ``Type``.
-If you like neither of these names, feel free to write your own synonym: ::
+    :since: 8.6.1
 
-  type Set = *   -- silly Agda programmers...
+    Treat the unqualified uses of the ``*`` type operator as nullary and desugar
+    to ``Data.Kind.Type``.
 
-All the affordances for ``*`` also apply to ``★``, the Unicode variant
-of ``*``.
+The kind ``Type`` (imported from ``Data.Kind``) classifies ordinary types. With
+:extension:`StarIsType` (currently enabled by default), ``*`` is desugared to
+``Type``, but using this legacy syntax is not recommended due to conflicts with
+:extension:`TypeOperators`. This also applies to ``★``, the Unicode variant of
+``*``.
 
 Inferring dependency in datatype declarations
 ---------------------------------------------
@@ -8852,19 +9347,44 @@ system does not have principal types) or merely practical (inferring this
 dependency is hard, given GHC's implementation). So, GHC takes the easy
 way out and requires a little help from the user.
 
+Inferring dependency in user-written ``forall``\s
+-------------------------------------------------
+
+A programmer may use ``forall`` in a type to introduce new quantified type
+variables. These variables may depend on each other, even in the same
+``forall``. However, GHC requires that the dependency be inferrable from
+the body of the ``forall``. Here are some examples::
+
+  data Proxy k (a :: k) = MkProxy   -- just to use below
+
+  f :: forall k a. Proxy k a        -- This is just fine. We see that (a :: k).
+  f = undefined
+
+  g :: Proxy k a -> ()              -- This is to use below.
+  g = undefined
+
+  data Sing a
+  h :: forall k a. Sing k -> Sing a -> ()  -- No obvious relationship between k and a
+  h _ _ = g (MkProxy :: Proxy k a)  -- This fails. We didn't know that a should have kind k.
+
+Note that in the last example, it's impossible to learn that ``a`` depends on ``k`` in the
+body of the ``forall`` (that is, the ``Sing k -> Sing a -> ()``). And so GHC rejects
+the program.
+
 Kind defaulting without :extension:`PolyKinds`
 -----------------------------------------------
 
-Without :extension:`PolyKinds` or :extension:`TypeInType` enabled, GHC
-refuses to generalise over kind variables. It thus defaults kind variables
-to ``*`` when possible; when this is not possible, an error is issued.
+Without :extension:`PolyKinds`, GHC refuses to generalise over kind variables.
+It thus defaults kind variables to ``Type`` when possible; when this is not
+possible, an error is issued.
 
 Here is an example of this in action: ::
 
-  {-# LANGUAGE TypeInType #-}
-  data Proxy a = P   -- inferred kind: Proxy :: k -> *
+  {-# LANGUAGE PolyKinds #-}
+  import Data.Kind (Type)
+  data Proxy a = P   -- inferred kind: Proxy :: k -> Type
   data Compose f g x = MkCompose (f (g x))
-    -- inferred kind: Compose :: (b -> *) -> (a -> b) -> a -> *
+    -- inferred kind: Compose :: (b -> Type) -> (a -> b) -> a -> Type
 
   -- separate module having imported the first
   {-# LANGUAGE NoPolyKinds, DataKinds #-}
@@ -8873,13 +9393,13 @@ Here is an example of this in action: ::
 In the last line, we use the promoted constructor ``'MkCompose``, which has
 kind ::
 
-  forall (a :: *) (b :: *) (f :: b -> *) (g :: a -> b) (x :: a).
+  forall (a :: Type) (b :: Type) (f :: b -> Type) (g :: a -> b) (x :: a).
     f (g x) -> Compose f g x
 
 Now we must infer a type for ``z``. To do so without generalising over kind
-variables, we must default the kind variables of ``'MkCompose``. We can
-easily default ``a`` and ``b`` to ``*``, but ``f`` and ``g`` would be ill-kinded
-if defaulted. The definition for ``z`` is thus an error.
+variables, we must default the kind variables of ``'MkCompose``. We can easily
+default ``a`` and ``b`` to ``Type``, but ``f`` and ``g`` would be ill-kinded if
+defaulted. The definition for ``z`` is thus an error.
 
 Pretty-printing in the presence of kind polymorphism
 ----------------------------------------------------
@@ -8909,16 +9429,16 @@ polymorphism.
 
 Here are the key definitions, all available from ``GHC.Exts``: ::
 
-  TYPE :: RuntimeRep -> *   -- highly magical, built into GHC
+  TYPE :: RuntimeRep -> Type   -- highly magical, built into GHC
 
   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 LiftedRep    -- * is just an ordinary type synonym
+  type Type = TYPE LiftedRep    -- Type is just an ordinary type synonym
 
 The idea is that we have a new fundamental type constant ``TYPE``, which
 is parameterised by a ``RuntimeRep``. We thus get ``Int# :: TYPE 'IntRep``
@@ -8956,7 +9476,7 @@ representation-polymorphic type.
 
 However, not all is lost. We can still do this: ::
 
-  ($) :: forall r (a :: *) (b :: TYPE r).
+  ($) :: forall r (a :: Type) (b :: TYPE r).
          (a -> b) -> a -> b
   f $ x = f x
 
@@ -8988,7 +9508,7 @@ stub out functions that return unboxed types.
 Printing levity-polymorphic types
 ---------------------------------
 
-.. ghc-flag:: -fprint-explicit-runtime-rep
+.. ghc-flag:: -fprint-explicit-runtime-reps
     :shortdesc: Print ``RuntimeRep`` variables in types which are
         runtime-representation polymorphic.
     :type: dynamic
@@ -9002,7 +9522,8 @@ Most GHC users will not need to worry about levity polymorphism
 or unboxed types. For these users, seeing the levity polymorphism
 in the type of ``$`` is unhelpful. And thus, by default, it is suppressed,
 by supposing all type variables of type ``RuntimeRep`` to be ``'LiftedRep``
-when printing, and printing ``TYPE 'LiftedRep`` as ``*``.
+when printing, and printing ``TYPE 'LiftedRep`` as ``Type`` (or ``*`` when
+:extension:`StarIsType` is on).
 
 Should you wish to see levity polymorphism in your types, enable
 the flag :ghc-flag:`-fprint-explicit-runtime-reps`.
@@ -9128,8 +9649,8 @@ the type level:
     GHC.TypeLits> natVal (lg (Proxy :: Proxy 2) (Proxy :: Proxy 8))
     3
 
-Constraints in types
-====================
+Equality constraints, Coercible, and the kind Constraint
+========================================================
 
 .. _equality-constraints:
 
@@ -9206,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:
 
@@ -9245,8 +9766,8 @@ 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
-   ``type Foo (f :: \* -> Constraint) = forall b. f b => b -> b``
+   ``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: ::
 
        type family Typ a b :: Constraint
@@ -9288,74 +9809,333 @@ contexts and superclasses, but to do so you must use
 :extension:`UndecidableInstances` to signal that you don't mind if the type
 checker fails to terminate.
 
-.. _extensions-to-type-signatures:
+.. _quantified-constraints:
 
-Extensions to type signatures
-=============================
+Quantified constraints
+======================
 
-.. _explicit-foralls:
+.. extension:: QuantifiedConstraints
+    :shortdesc: Allow ``forall`` quantifiers in constraints.
 
-Explicit universal quantification (forall)
-------------------------------------------
+    :since: 8.6.1
 
-.. extension:: ExplicitForAll
-    :shortdesc: Enable explicit universal quantification.
-        Implied by :extension:`ScopedTypeVariables`, :extension:`LiberalTypeSynonyms`,
-        :extension:`RankNTypes` and :extension:`ExistentialQuantification`.
+    Allow constraints to quantify over types.
 
-    :since: 6.12.1
+The extension :extension:`QuantifiedConstraints` introduces **quantified constraints**,
+which give a new level of expressiveness in constraints. For example, consider ::
 
-    Allow use of the ``forall`` keyword in places where universal quantification
-    is implicit.
+ data Rose f a = Branch a (f (Rose f a))
 
-Haskell type signatures are implicitly quantified. When the language
-option :extension:`ExplicitForAll` is used, the keyword ``forall`` allows us to
-say exactly what this means. For example: ::
+ instance (Eq a, ???) => Eq (Rose f a)
+   where
+     (Branch x1 c1) == (Branch x2 c2)
+        = x1==x1 && c1==c2
 
-    g :: b -> b
+From the ``x1==x2`` we need ``Eq a``, which is fine.  From ``c1==c2`` we need ``Eq (f (Rose f a))`` which
+is *not* fine in Haskell today; we have no way to solve such a constraint.
 
-means this: ::
+:extension:`QuantifiedConstraints` lets us write this ::
 
-    g :: forall b. (b -> b)
+ instance (Eq a, forall b. (Eq b) => Eq (f b))
+        => Eq (Rose f a)
+   where
+     (Branch x1 c1) == (Branch x2 c2)
+        = x1==x1 && c1==c2
 
-The two are treated identically, except that the latter may bring type variables
-into scope (see :ref:`scoped-type-variables`).
+Here, the quantified constraint ``forall b. (Eq b) => Eq (f b)`` behaves
+a bit like a local instance declaration, and makes the instance typeable.
 
-Notes:
+The paper `Quantified class constraints <http://i.cs.hku.hk/~bruno//papers/hs2017.pdf>`_ (by Bottu, Karachalias, Schrijvers, Oliveira, Wadler, Haskell Symposium 2017) describes this feature in technical detail, with examples, and so is a primary reference source for this proposal.
 
-- With :extension:`ExplicitForAll`, ``forall`` becomes a keyword; you can't use ``forall`` as a
-  type variable any more!
+Motivation
+----------------
+Introducing quantified constraints offers two main benefits:
 
-- As well in type signatures, you can also use an explicit ``forall``
-  in an instance declaration: ::
+- Firstly, they enable terminating resolution where this was not possible before.  Consider for instance the following instance declaration for the general rose datatype ::
 
-      instance forall a. Eq a => Eq [a] where ...
+   data Rose f x = Rose x (f (Rose f x))
 
-- If the :ghc-flag:`-Wunused-foralls` flag is enabled, a warning will be emitted
-  when you write a type variable in an explicit ``forall`` statement that is
-  otherwise unused. For instance: ::
+   instance (Eq a, forall b. Eq b => Eq (f b)) => Eq (Rose f a) where
+     (Rose x1 rs1) == (Rose x2 rs2) = x1 == x2 && rs1 == rs2
 
-    g :: forall a b. (b -> b)
+  This extension allows us to write constraints of the form ``forall b. Eq b =>
+  Eq (f b)``, which is needed to solve the ``Eq (f (Rose f x))`` constraint
+  arising from the second usage of the ``(==)`` method.
 
-  would warn about the unused type variable `a`.
+- Secondly, quantified constraints allow for more concise and precise specifications. As an example, consider the MTL type class for monad transformers::
 
-.. _flexible-contexts:
+   class Trans t where
+     lift :: Monad m => m a -> (t m) a
 
-The context of a type signature
--------------------------------
+  The developer knows that a monad transformer takes a monad ``m`` into a new monad ``t m``.
+  But this property is not formally specified in the above declaration.
+  This omission becomes an issue when defining monad transformer composition::
 
-The :extension:`FlexibleContexts` extension lifts the Haskell 98 restriction that
-the type-class constraints in a type signature must have the form *(class
-type-variable)* or *(class (type-variable type1 type2 ... typen))*. With
-:extension:`FlexibleContexts` these type signatures are perfectly okay
-::
+    newtype (t1 * t2) m a = C { runC :: t1 (t2 m) a }
 
-      g :: Eq [a] => ...
-      g :: Ord (T a ()) => ...
+    instance (Trans t1, Trans t2) => Trans (t1 * t2) where
+      lift = C . lift . lift
 
-The flag :extension:`FlexibleContexts` also lifts the corresponding restriction
-on class declarations (:ref:`superclass-rules`) and instance
-declarations (:ref:`instance-rules`).
+  The goal here is to ``lift`` from monad ``m`` to ``t2 m`` and
+  then ``lift`` this again into ``t1 (t2 m)``.
+  However, this second ``lift`` can only be accepted when ``(t2 m)`` is a monad
+  and there is no way of establishing that this fact universally holds.
+
+  Quantified constraints enable this property to be made explicit in the ``Trans``
+  class declaration::
+
+    class (forall m. Monad m => Monad (t m)) => Trans t where
+      lift :: Monad m => m a -> (t m) a
+
+This idea is very old; see Seciton 7 of `Derivable type classes <https://www.microsoft.com/en-us/research/publication/derivable-type-classes/>`_.
+
+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
+
+.. code-block:: none
+
+    context ::= class
+            |   ( class1, ..., classn )
+
+    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
+
+.. code-block:: none
+
+    class ::= ...
+          | [context =>] qtycls inst
+          | [context =>] tyvar inst
+
+The definition of ``inst`` is unchanged from the Haskell Report (roughly, just a type).
+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
+
+  .. code-block:: none
+
+    class ::= ...
+           | [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 ::
+
+    instance (Eq a, forall b. Eq b => Eq (f b)) => Eq (Rose f a) where ...
+
+  Without the ``forall b``, the type variable ``b`` would be quantified over the whole instance declaration, which is not what is intended.
+
+- One of these new quantified constraints can appear anywhere that any other constraint can, not just in instance declarations.  Notably, it can appear in a type signature for a value binding, data constructor, or expression.  For example ::
+
+   f :: (Eq a, forall b. Eq b => Eq (f b)) => Rose f a -> Rose f a -> Bool
+   f t1 t2 = not (t1 == t2)
+
+- The form with a type variable at the head allows this::
+
+   instance (forall xx. c (Free c xx)) => Monad (Free c) where
+       Free f >>= g = f g
+
+  See `Iceland Jack's summary <https://ghc.haskell.org/trac/ghc/ticket/14733#comment:6>`_.  The key point is that the bit to the right of the ``=>`` may be headed by a type *variable* (``c`` in this case), rather than a class.  It should not be one of the forall'd variables, though.
+
+  (NB: this goes beyond what is described in `the paper <http://i.cs.hku.hk/~bruno//papers/hs2017.pdf>`_, but does not seem to introduce any new technical difficulties.)
+
+
+Typing changes
+----------------
+
+See `the paper <http://i.cs.hku.hk/~bruno//papers/hs2017.pdf>`_.
+
+Superclasses
+----------------
+
+Suppose we have::
+
+     f :: forall m. (forall a. Ord a => Ord (m a)) => m Int -> Bool
+     f x = x == x
+
+From the ``x==x`` we need an ``Eq (m Int)`` constraint, but the context only gives us a way to figure out ``Ord (m a)`` constraints.  But from the given constraint ``forall a. Ord a => Ord (m a)`` we derive a second given constraint ``forall a. Ord a => Eq (m a)``, and from that we can readily solve ``Eq (m Int)``.  This process is very similar to the way that superclasses already work: given an ``Ord a`` constraint we derive a second given ``Eq a`` constraint.
+
+NB: This treatment of superclasses goes beyond `the paper <http://i.cs.hku.hk/~bruno//papers/hs2017.pdf>`_, but is specifically desired by users.
+
+Overlap
+-------------
+
+Quantified constraints can potentially lead to overlapping local axioms.
+Consider for instance the following example::
+
+ class A a where {}
+ class B a where {}
+ class C a where {}
+ class (A a => C a) => D a where {}
+ class (B a => C a) => E a where {}
+
+ class C a => F a where {}
+ instance (B a, D a, E a) => F a where {}
+
+When type checking the instance declaration for ``F a``,
+we need to check that the superclass ``C`` of ``F`` holds.
+We thus try to entail the constraint ``C a`` under the theory containing:
+
+- The instance axioms : ``(B a, D a, E a) => F a``
+- The local axioms from the instance context : ``B a``, ``D a`` and ``E a``
+- The closure of the superclass relation over these local axioms : ``A a => C a`` and ``B a => C a``
+
+However, the ``A a => C a`` and ``B a => C a`` axioms both match the wanted constraint ``C a``.
+There are several possible approaches for handling these overlapping local axioms:
+
+- **Pick first**.  We can simply select the **first matching axiom** we encounter.
+  In the above example, this would be ``A a => C a``.
+  We'd then need to entail ``A a``, for which we have no matching axioms available, causing the above program to be rejected.
+
+  But suppose we made a slight adjustment to the order of the instance context, putting ``E a`` before ``D a``::
+
+   instance (B a, E a, D a) => F a where {}
+
+  The first matching axiom we encounter while entailing ``C a``, is ``B a => C a``.
+  We have a local axiom ``B a`` available, so now the program is suddenly accepted.
+  This behaviour, where the ordering of an instance context determines
+  whether or not the program is accepted, seems rather confusing for the developer.
+
+- **Reject if in doubt**.  An alternative approach would be to check for overlapping axioms,
+  when solving a constraint.
+  When multiple matching axioms are discovered, we **reject the program**.
+  This approach is a bit conservative, in that it may reject working programs.
+  But it seem much more transparent towards the developer, who
+  can be presented with a clear message, explaining why the program is rejected.
+
+- **Backtracking**.  Lastly, a simple form of **backtracking** could be introduced.
+  We simply select the first matching axiom we encounter and when the entailment fails,
+  we backtrack and look for other axioms that might match the wanted constraint.
+
+  This seems the most intuitive and transparent approach towards the developer,
+  who no longer needs to concern himself with the fact that his code might contain
+  overlapping axioms or with the ordering of his instance contexts.  But backtracking
+  would apply equally to ordinary instance selection (in the presence of overlapping
+  instances), so it is a much more pervasive change, with substantial consequences
+  for the type inference engine.
+
+GHC adopts **Reject if in doubt** for now.  We can see how painful it
+is in practice, and try something more ambitious if necessary.
+
+Instance lookup
+-------------------
+
+In the light of the overlap decision, instance lookup works like this when
+trying to solve a class constraint ``C t``
+
+1. First see if there is a given un-quantified constraint ``C t``.  If so, use it to solve the constraint.
+
+2. If not, look at all the available given quantified constraints; if exactly one one matches ``C t``, choose it; if more than one matches, report an error.
+
+3. If no quantified constraints match, look up in the global instances, as described in :ref:`instance-resolution` and :ref:`instance-overlap`.
+
+Termination
+---------------
+
+GHC uses the :ref:`Paterson Conditions <instance-termination>` to ensure
+that instance resolution terminates. How are those rules modified for quantified
+constraints? In two ways.
+
+- Each quantified constraint, taken by itself, must satisfy the termination rules for an instance declaration.
+
+- After "for each class constraint ``(C t1 ... tn)``", add "or each quantified constraint ``(forall as. context => C t1 .. tn)``"
+
+Note that the second item only at the *head* of the quantified constraint, not its context.  Reason: the head is the new goal that has to be solved if we use the instance declaration.
+
+Of course, ``UndecidableInstances`` lifts the Paterson Conditions, as now.
+
+Coherence
+-----------
+
+Although quantified constraints are a little like local instance declarations, they differ
+in one big way: the local instances are written by the compiler, not the user, and hence
+cannot introduce incoherence.  Consider ::
+
+  f :: (forall a. Eq a => Eq (f a)) => f b -> f Bool
+  f x = ...rhs...
+
+In ``...rhs...`` there is, in effect a local instance for ``Eq (f a)`` for any ``a``.  But
+at a call site for ``f`` the compiler itself produces evidence to pass to ``f``. For example,
+if we called ``f Nothing``, then ``f`` is ``Maybe`` and the compiler must prove (at the
+call site) that ``forall a. Eq a => Eq (Maybe a)`` holds.  It can do this easily, by
+appealing to the existing instance declaration for ``Eq (Maybe a)``.
+
+In short, quantifed constraints do not introduce incoherence.
+
+
+.. _extensions-to-type-signatures:
+
+Extensions to type signatures
+=============================
+
+.. _explicit-foralls:
+
+Explicit universal quantification (forall)
+------------------------------------------
+
+.. extension:: ExplicitForAll
+    :shortdesc: Enable explicit universal quantification.
+        Implied by :extension:`ScopedTypeVariables`, :extension:`LiberalTypeSynonyms`,
+        :extension:`RankNTypes` and :extension:`ExistentialQuantification`.
+
+    :since: 6.12.1
+
+    Allow use of the ``forall`` keyword in places where universal quantification
+    is implicit.
+
+Haskell type signatures are implicitly quantified. When the language
+option :extension:`ExplicitForAll` is used, the keyword ``forall`` allows us to
+say exactly what this means. For example: ::
+
+    g :: b -> b
+
+means this: ::
+
+    g :: forall b. (b -> b)
+
+The two are treated identically, except that the latter may bring type variables
+into scope (see :ref:`scoped-type-variables`).
+
+This extension also enables explicit quantification of type and kind variables
+in :ref:`data-instance-declarations`, :ref:`type-instance-declarations`,
+:ref:`closed-type-families`, :ref:`assoc-inst`, and :ref:`rewrite-rules`.
+
+Notes:
+
+- As well in type signatures, you can also use an explicit ``forall``
+  in an instance declaration: ::
+
+      instance forall a. Eq a => Eq [a] where ...
+
+- If the :ghc-flag:`-Wunused-foralls` flag is enabled, a warning will be emitted
+  when you write a type variable in an explicit ``forall`` statement that is
+  otherwise unused. For instance: ::
+
+    g :: forall a b. (b -> b)
+
+  would warn about the unused type variable `a`.
+
+.. _flexible-contexts:
+
+The context of a type signature
+-------------------------------
+
+The :extension:`FlexibleContexts` extension lifts the Haskell 98 restriction that
+the type-class constraints in a type signature must have the form *(class
+type-variable)* or *(class (type-variable type1 type2 ... typen))*. With
+:extension:`FlexibleContexts` these type signatures are perfectly okay
+::
+
+      g :: Eq [a] => ...
+      g :: Ord (T a ()) => ...
+
+The flag :extension:`FlexibleContexts` also lifts the corresponding restriction
+on class declarations (:ref:`superclass-rules`) and instance
+declarations (:ref:`instance-rules`).
 
 .. _ambiguity:
 
@@ -9518,29 +10298,27 @@ This extension enables kind signatures in the following places:
 
 -  ``data`` declarations: ::
 
-         data Set (cxt :: * -> *) a = Set [a]
+         data Set (cxt :: Type -> Type) a = Set [a]
 
 -  ``type`` declarations: ::
 
-         type T (f :: * -> *) = f Int
+         type T (f :: Type -> Type) = f Int
 
 -  ``class`` declarations: ::
 
-         class (Eq a) => C (f :: * -> *) a where ...
+         class (Eq a) => C (f :: Type -> Type) a where ...
 
 -  ``forall``\'s in type signatures: ::
 
-         f :: forall (cxt :: * -> *). Set cxt Int
+         f :: forall (cxt :: Type -> Type). Set cxt Int
 
-The parentheses are required. Some of the spaces are required too, to
-separate the lexemes. If you write ``(f::*->*)`` you will get a parse
-error, because ``::*->*`` is a single lexeme in Haskell.
+The parentheses are required.
 
 As part of the same extension, you can put kind annotations in types as
 well. Thus: ::
 
-       f :: (Int :: *) -> Int
-       g :: forall a. a -> (a :: *)
+       f :: (Int :: Type) -> Int
+       g :: forall a. a -> (a :: Type)
 
 The syntax is
 
@@ -9566,6 +10344,17 @@ Lexically scoped type variables
     Enable lexical scoping of type variables explicitly introduced with
     ``forall``.
 
+.. tip::
+
+    ``ScopedTypeVariables`` breaks GHC's usual rule that explicit ``forall`` is optional and doesn't affect semantics.
+    For the :ref:`decl-type-sigs` (or :ref:`exp-type-sigs`) examples in this section,
+    the explicit ``forall`` is required.
+    (If omitted, usually the program will not compile; in a few cases it will compile but the functions get a different signature.)
+    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`.
+
 GHC supports *lexically scoped type variables*, without which some type
 signatures are simply impossible to write. For example: ::
 
@@ -9584,6 +10373,21 @@ signature for ``ys``. In Haskell 98 it is not possible to declare a type
 for ``ys``; a major benefit of scoped type variables is that it becomes
 possible to do so.
 
+.. _pattern-equiv-form:
+
+An equivalent form for that example, avoiding explicit ``forall`` uses :ref:`pattern-type-sigs`: ::
+
+    f :: [a] -> [a]
+    f (xs :: [aa]) = xs ++ ys
+      where
+        ys :: [aa]
+        ys = reverse xs
+
+Unlike the ``forall`` form, type variable ``a`` from ``f``'s signature is not scoped over ``f``'s equation(s).
+Type variable ``aa`` bound by the pattern signature is scoped over the right-hand side of ``f``'s equation.
+(Therefore there is no need to use a distinct type variable; using ``a`` would be equivalent.)
+
+
 Overview
 --------
 
@@ -9650,6 +10454,26 @@ This only happens if:
    the definition of "``g``", so "``x::a``" means "``x::forall a. a``"
    by Haskell's usual implicit quantification rules.
 
+-  The type variable is quantified by the single, syntactically visible,
+   outermost ``forall`` of the type signature. For example, GHC will reject
+   all of the following examples: ::
+
+         f1 :: forall a. forall b. a -> [b] -> [b]
+         f1 _ (x:xs) = xs ++ [ x :: b ]
+
+         f2 :: forall a. a -> forall b. [b] -> [b]
+         f2 _ (x:xs) = xs ++ [ x :: b ]
+
+         type Foo = forall b. [b] -> [b]
+
+         f3 :: Foo
+         f3 (x:xs) = xs ++ [ x :: b ]
+
+   In ``f1`` and ``f2``, the type variable ``b`` is not quantified by the
+   outermost ``forall``, so it is not in scope over the bodies of the
+   functions. Neither is ``b`` in scope over the body of ``f3``, as the
+   ``forall`` is tucked underneath the ``Foo`` type synonym.
+
 -  The signature gives a type for a function binding or a bare variable
    binding, not a pattern binding. For example: ::
 
@@ -9662,10 +10486,12 @@ This only happens if:
          f3 :: forall a. [a] -> [a]
          Just f3 = Just (\(x:xs) -> xs ++ [ x :: a ])   -- Not OK!
 
-   The binding for ``f3`` is a pattern binding, and so its type
-   signature does not bring ``a`` into scope. However ``f1`` is a
-   function binding, and ``f2`` binds a bare variable; in both cases the
-   type signature brings ``a`` into scope.
+   ``f1`` is a function binding, and ``f2`` binds a bare variable;
+   in both cases the type signature brings ``a`` into scope.
+   However the binding for ``f3`` is a pattern binding,
+   and so ``f3`` is a fresh variable brought into scope by the pattern,
+   not connected with top level ``f3``.
+   Then type variable ``a`` is not in scope of the right-hand side of ``Just f3 = ...``.
 
 .. _exp-type-sigs:
 
@@ -9711,17 +10537,28 @@ example: ::
     f xs = (n, zs)
       where
         (ys::[a], n) = (reverse xs, length xs) -- OK
-        zs::[a] = xs ++ ys                     -- OK
+        (zs::[a])    = xs ++ ys                     -- OK
 
-        Just (v::b) = ...  -- Not OK; b is not in scope
+        Just (v::b)  = ...  -- Not OK; b is not in scope
 
 Here, the pattern signatures for ``ys`` and ``zs`` are fine, but the one
 for ``v`` is not because ``b`` is not in scope.
 
 However, in all patterns *other* than pattern bindings, a pattern type
 signature may mention a type variable that is not in scope; in this
-case, *the signature brings that type variable into scope*. This is
-particularly important for existential data constructors. For example: ::
+case, *the signature brings that type variable into scope*. For example: ::
+
+    -- same f and g as above, now assuming that 'a' is not already in scope
+    f = \(x::Int, y::a) -> x           -- 'a' is in scope on RHS of ->
+
+    g (x::a) = x :: a
+
+    hh (Just (v :: b)) = v :: b
+
+The pattern type signature makes the type variable available on the right-hand side of the equation.
+
+Bringing type variables into scope is particularly important
+for existential data constructors. For example: ::
 
     data T = forall a. MkT [a]
 
@@ -9729,28 +10566,25 @@ particularly important for existential data constructors. For example: ::
     k (MkT [t::a]) =
         MkT t3
       where
-        t3::[a] = [t,t,t]
-
-Here, the pattern type signature ``(t::a)`` mentions a lexical type
-variable that is not already in scope. Indeed, it *cannot* already be in
-scope, because it is bound by the pattern match. GHC's rule is that in
-this situation (and only then), a pattern type signature can mention a
-type variable that is not already in scope; 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.
-
-If all this seems a little odd, we think so too. But we must have *some*
-way to bring such type variables into scope, else we could not name
-existentially-bound type variables in subsequent type signatures.
-
-This is (now) the *only* situation in which a pattern type signature is
-allowed to mention a lexical variable that is not already in scope. For
-example, both ``f`` and ``g`` would be illegal if ``a`` was not already
-in scope.
+        (t3::[a]) = [t,t,t]
+
+Here, the pattern type signature ``[t::a]`` mentions a lexical type
+variable that is not already in scope. Indeed, it *must not* already be in
+scope, because it is bound by the pattern match.
+The effect is to bring it into scope,
+standing for the existentially-bound type variable.
+
+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.
+But we must have *some* way to bring such type variables into scope,
+else we could not name existentially-bound type variables
+in subsequent type signatures.
+
+Compare the two (identical) definitions for examples ``f``, ``g``;
+they are both legal whether or not ``a`` is already in scope.
+They differ in that *if* ``a`` is already in scope, the signature constrains
+the pattern, rather than the pattern binding the variable.
 
 .. _cls-inst-scoped-tyvars:
 
@@ -9862,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:
 
@@ -9913,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
 
@@ -9934,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.
+
+.. _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 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``.
+- 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
@@ -9974,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:
 
@@ -10028,7 +10900,6 @@ Implicit parameters
 
 .. extension:: ImplicitParams
     :shortdesc: Enable Implicit Parameters.
-        Implies :extension:`FlexibleContexts` and :extension:`FlexibleInstances`.
 
     :since: 6.8.1
 
@@ -10461,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: ::
@@ -10562,7 +11433,8 @@ written with a leading underscore (e.g., "``_``", "``_foo``",
 will generate an error message that describes which type is expected at
 the hole's location, information about the origin of any free type
 variables, and a list of local bindings that might help fill the hole
-with actual code. Typed holes are always enabled in GHC.
+and bindings in scope that fit the type of the hole that might help fill
+the hole with actual code. Typed holes are always enabled in GHC.
 
 The goal of typed holes is to help with writing Haskell code rather than
 to change the type system. Typed holes can be used to obtain extra
@@ -10584,11 +11456,12 @@ will fail with the following error: ::
         Found hole `_' with type: a
         Where: `a' is a rigid type variable bound by
                    the type signature for f :: a -> a at hole.hs:1:6
-        Relevant bindings include
-          f :: a -> a (bound at hole.hs:2:1)
-          x :: a (bound at hole.hs:2:3)
         In the expression: _
         In an equation for `f': f x = _
+        Relevant bindings include
+          x :: a (bound at hole.hs:2:3)
+          f :: a -> a (bound at hole.hs:2:1)
+        Valid hole fits include x :: a (bound at hole.hs:2:3)
 
 Here are some more details:
 
@@ -10625,13 +11498,36 @@ Here are some more details:
 
    .. code-block:: none
 
-       Foo.hs:5:15: error:
-           Found hole: _x :: Bool
-           Relevant bindings include
-             p :: Bool (bound at Foo.hs:3:6)
-             cons :: Bool -> [Bool] (bound at Foo.hs:3:1)
-
-       Foo.hs:5:20: error:
+       Foo.hs:3:21: error:
+          Found hole: _x :: Bool
+          Or perhaps ‘_x’ is mis-spelled, or not in scope
+          In the first argument of ‘(:)’, namely ‘_x’
+          In the second argument of ‘(:)’, namely ‘_x : y’
+          In the second argument of ‘(:)’, namely ‘True : _x : y’
+          Relevant bindings include
+            z :: Bool (bound at Foo.hs:3:6)
+          cons :: Bool -> [Bool] (bound at Foo.hs:3:1)
+          Valid hole fits include
+            z :: Bool (bound at mpt.hs:2:6)
+            otherwise :: Bool
+              (imported from ‘Prelude’ at mpt.hs:1:8-10
+              (and originally defined in ‘GHC.Base’))
+            False :: Bool
+              (imported from ‘Prelude’ at mpt.hs:1:8-10
+              (and originally defined in ‘GHC.Types’))
+            True :: Bool
+              (imported from ‘Prelude’ at mpt.hs:1:8-10
+              (and originally defined in ‘GHC.Types’))
+            maxBound :: forall a. Bounded a => a
+              with maxBound @Bool
+              (imported from ‘Prelude’ at mpt.hs:1:8-10
+              (and originally defined in ‘GHC.Enum’))
+            minBound :: forall a. Bounded a => a
+              with minBound @Bool
+              (imported from ‘Prelude’ at mpt.hs:1:8-10
+              (and originally defined in ‘GHC.Enum’))
+
+       Foo.hs:3:26: error:
            Variable not in scope: y :: [Bool]
 
    More information is given for explicit holes (i.e. ones that start
@@ -10649,24 +11545,33 @@ Here are some more details:
 
    .. code-block:: none
 
-       unbound.hs:1:8:
-           Found hole '_x' with type: a
-           Where: `a' is a rigid type variable bound by
-                      the inferred type of cons :: [a] at unbound.hs:1:1
-           Relevant bindings include cons :: [a] (bound at unbound.hs:1:1)
-           In the first argument of `(:)', namely `_x'
-           In the expression: _x : _x
-           In an equation for `cons': cons = _x : _x
-
-       unbound.hs:1:13:
-           Found hole '_x' with type: [a]
-           Arising from: an undeclared identifier `_x' at unbound.hs:1:13-14
-           Where: `a' is a rigid type variable bound by
-                      the inferred type of cons :: [a] at unbound.hs:1:1
-           Relevant bindings include cons :: [a] (bound at unbound.hs:1:1)
-           In the second argument of `(:)', namely `_x'
-           In the expression: _x : _x
-           In an equation for `cons': cons = _x : _x
+      unbound.hs:1:8:
+          Found hole '_x' with type: a
+          Where: `a' is a rigid type variable bound by
+                     the inferred type of cons :: [a] at unbound.hs:1:1
+          In the first argument of `(:)', namely `_x'
+          In the expression: _x : _x
+          In an equation for `cons': cons = _x : _x
+          Relevant bindings include cons :: [a] (bound at unbound.hs:1:1)
+
+      unbound.hs:1:13:
+          Found hole: _x :: [a]
+          Where: ‘a’ is a rigid type variable bound by
+                  the inferred type of cons :: [a]
+                  at unbound.hs:3:1-12
+          Or perhaps ‘_x’ is mis-spelled, or not in scope
+          In the second argument of ‘(:)’, namely ‘_x’
+          In the expression: _x : _x
+          In an equation for ‘cons’: cons = _x : _x
+          Relevant bindings include cons :: [a] (bound at unbound.hs:3:1)
+          Valid hole fits include
+            cons :: forall a. [a]
+              with cons @a
+              (defined at mpt.hs:3:1)
+            mempty :: forall a. Monoid a => a
+              with mempty @[a]
+              (imported from ‘Prelude’ at mpt.hs:1:8-10
+              (and originally defined in ‘GHC.Base’))
 
    Notice the two different types reported for the two different
    occurrences of ``_x``.
@@ -10690,11 +11595,67 @@ Here are some more details:
    implementation terms, they are reported by the renamer rather than
    the type checker.)
 
-There's a flag for controlling the amount of context information shown for
-typed holes:
+- The list of valid hole fits is found by checking which bindings in scope
+  would fit into the hole. As an example, compiling the following module with
+  GHC: ::
+
+      import Data.List (inits)
+
+      g :: [String]
+      g = _ "hello, world"
+
+  yields the errors:
+
+
+  .. code-block:: none
+
+
+    • Found hole: _ :: [Char] -> [String]
+    • In the expression: _
+      In the expression: _ "hello, world"
+      In an equation for ‘g’: g = _ "hello, world"
+    • Relevant bindings include g :: [String] (bound at mpt.hs:6:1)
+      Valid hole fits include
+        lines :: String -> [String]
+          (imported from ‘Prelude’ at mpt.hs:3:8-9
+           (and originally defined in ‘base-4.11.0.0:Data.OldList’))
+        words :: String -> [String]
+          (imported from ‘Prelude’ at mpt.hs:3:8-9
+           (and originally defined in ‘base-4.11.0.0:Data.OldList’))
+        inits :: forall a. [a] -> [[a]]
+          with inits @Char
+          (imported from ‘Data.List’ at mpt.hs:4:19-23
+           (and originally defined in ‘base-4.11.0.0:Data.OldList’))
+        repeat :: forall a. a -> [a]
+          with repeat @String
+          (imported from ‘Prelude’ at mpt.hs:3:8-9
+           (and originally defined in ‘GHC.List’))
+        fail :: forall (m :: * -> *). Monad m => forall a. String -> m a
+          with fail @[] @String
+          (imported from ‘Prelude’ at mpt.hs:3:8-9
+           (and originally defined in ‘GHC.Base’))
+        return :: forall (m :: * -> *). Monad m => forall a. a -> m a
+          with return @[] @String
+          (imported from ‘Prelude’ at mpt.hs:3:8-9
+           (and originally defined in ‘GHC.Base’))
+        pure :: forall (f :: * -> *). Applicative f => forall a. a -> f a
+          with pure @[] @String
+          (imported from ‘Prelude’ at mpt.hs:3:8-9
+           (and originally defined in ‘GHC.Base’))
+        read :: forall a. Read a => String -> a
+          with read @[String]
+          (imported from ‘Prelude’ at mpt.hs:3:8-9
+           (and originally defined in ‘Text.Read’))
+        mempty :: forall a. Monoid a => a
+          with mempty @([Char] -> [String])
+          (imported from ‘Prelude’ at mpt.hs:3:8-9
+           (and originally defined in ‘GHC.Base’))
+
+There are a few flags for controlling the amount of context information shown
+for typed holes:
 
 .. ghc-flag:: -fshow-hole-constraints
-    :shortdesc: Show constraints when reporting typed holes
+    :shortdesc: Show constraints when reporting typed holes.
     :type: dynamic
     :category: verbosity
 
@@ -10708,18 +11669,325 @@ typed holes:
 
     .. code-block:: none
 
-        show_constraints.hs:4:7: error:
-            • Found hole: _ :: Bool
-            • In the expression: _
-              In an equation for ‘f’: f x = _
-            • Relevant bindings include
-                x :: a (bound at show_constraints.hs:4:3)
-                f :: a -> Bool (bound at show_constraints.hs:4:1)
-              Constraints include
-                Eq a (from the type signature for:
-                             f :: Eq a => a -> Bool
-                      at show_constraints.hs:3:1-22)
+      show_constraints.hs:4:7: error:
+          • Found hole: _ :: Bool
+          • In the expression: _
+            In an equation for ‘f’: f x = _
+          • Relevant bindings include
+              x :: a (bound at show_constraints.hs:4:3)
+              f :: a -> Bool (bound at show_constraints.hs:4:1)
+            Constraints include Eq a (from show_constraints.hs:3:1-22)
+            Valid hole fits include
+              otherwise :: Bool
+              False :: Bool
+              True :: Bool
+              maxBound :: forall a. Bounded a => a
+                with maxBound @Bool
+              minBound :: forall a. Bounded a => a
+                with minBound @Bool
+
+.. _typed-hole-valid-hole-fits:
+
+Valid Hole Fits
+-------------------
+GHC sometimes suggests valid hole fits for typed holes, which is
+configurable by a few flags.
+
+.. ghc-flag:: -fno-show-valid-hole-fits
+    :shortdesc: Disables showing a list of valid hole fits for typed holes
+        in type error messages.
+    :type: dynamic
+    :category: verbosity
+
+    :default: off
+
+    This flag can be toggled to turn off the display of valid hole fits
+    entirely.
+
+.. ghc-flag:: -fmax-valid-hole-fits=⟨n⟩
+    :shortdesc: *default: 6.* Set the maximum number of valid hole fits for
+        typed holes to display in type error messages.
+    :type: dynamic
+    :reverse: -fno-max-valid-hole-fits
+    :category: verbosity
+
+    :default: 6
+
+    The list of valid hole fits is limited by displaying up to 6
+    hole fits per hole. The number of hole fits shown can be set by this
+    flag. Turning the limit off with :ghc-flag:`-fno-max-valid-hole-fits`
+    displays all found hole fits.
+
+
+.. ghc-flag:: -fshow-type-of-hole-fits
+    :shortdesc: Toggles whether to show the type of the valid hole fits
+       in the output.
+    :type: dynamic
+    :category: verbosity
+    :reverse: -fno-type-of-hole-fits
+
+    :default: on
+
+    By default, the hole fits show the type of the hole fit.
+    This can be turned off by the reverse of this flag.
+
+
+
+.. ghc-flag:: -fshow-type-app-of-hole-fits
+    :shortdesc: Toggles whether to show the type application of the valid
+       hole fits in the output.
+    :type: dynamic
+    :category: verbosity
+    :reverse: -fno-show-type-app-of-hole-fits
+
+    :default: on
+
+    By default, the hole fits show the type application needed to make
+    this hole fit fit the type of the hole, e.g. for the hole
+    ``(_ :: Int -> [Int])``, ``mempty`` is a hole fit with
+    ``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.
+    :type: dynamic
+    :category: verbosity
+    :reverse: -fno-show-type-app-vars-of-hole-fits
+
+    :default: on
+
+    By default, the hole fits show the type application needed to make
+    this hole fit fit the type of the hole, e.g. for the hole
+    ``(_ :: Int -> [Int])``, ``mempty :: Monoid a => a`` is a hole fit
+    with ``mempty @(Int -> [Int])``. This flag toggles whether to show
+    ``a ~ (Int -> [Int])`` instead of ``mempty @(Int -> [Int])`` in the where
+    clause of the valid hole fit message.
+
+.. ghc-flag:: -fshow-provenance-of-hole-fits
+    :shortdesc: Toggles whether to show the provenance of the valid hole fits
+       in the output.
+    :type: dynamic
+    :category: verbosity
+    :reverse: -fno-show-provenance-of-hole-fits
+
+    :default: on
+
+    By default, each hole fit shows the provenance information of its
+    hole fit, i.e. where it was bound or defined, and what module
+    it was originally defined in if it was imported. This can be toggled
+    off using the reverse of this flag.
+
+
+.. ghc-flag:: -funclutter-valid-hole-fits
+    :shortdesc: Unclutter the list of valid hole fits by not showing
+        provenance nor type applications of suggestions.
+    :type: dynamic
+    :category: verbosity
+
+    :default: off
+
+    This flag can be toggled to decrease the verbosity of the valid hole fit
+    suggestions by not showing the provenance nor type application of the
+    suggestions.
+
+
+
+.. _typed-holes-refinement-hole-fits:
+
+Refinement Hole Fits
+~~~~~~~~~~~~~~~~~~~~~~~~
+
+When the flag :ghc-flag:`-frefinement-level-hole-fits=⟨n⟩` is set to an
+``n`` larger than ``0``, GHC will offer up a list of valid refinement
+hole fits, which are valid hole fits that need up to ``n`` levels of
+additional refinement to be complete, where each level represents an additional
+hole in the hole fit that requires filling in.  As an example, consider the
+hole in ::
+
+  f :: [Integer] -> Integer
+  f = _
+
+When the refinement level is not set, it will only offer valid hole fits
+suggestions: ::
+
+  Valid hole fits include
+    f :: [Integer] -> Integer
+    head :: forall a. [a] -> a
+      with head @Integer
+    last :: forall a. [a] -> a
+      with last @Integer
+    maximum :: forall (t :: * -> *).
+                Foldable t =>
+                forall a. Ord a => t a -> a
+      with maximum @[] @Integer
+    minimum :: forall (t :: * -> *).
+                Foldable t =>
+                forall a. Ord a => t a -> a
+      with minimum @[] @Integer
+    product :: forall (t :: * -> *).
+                Foldable t =>
+                forall a. Num a => t a -> a
+      with product @[] @Integer
+    sum :: forall (t :: * -> *).
+            Foldable t =>
+            forall a. Num a => t a -> a
+      with sum @[] @Integer
+
+However, with :ghc-flag:`-frefinement-level-hole-fits=⟨n⟩` set to e.g. `1`,
+it will additionally offer up a list of refinement hole fits, in this case: ::
+
+  Valid refinement hole fits include
+    foldl1 (_ :: Integer -> Integer -> Integer)
+      with foldl1 @[] @Integer
+      where foldl1 :: forall (t :: * -> *).
+                      Foldable t =>
+                      forall a. (a -> a -> a) -> t a -> a
+    foldr1 (_ :: Integer -> Integer -> Integer)
+      with foldr1 @[] @Integer
+      where foldr1 :: forall (t :: * -> *).
+                      Foldable t =>
+                      forall a. (a -> a -> a) -> t a -> a
+    const (_ :: Integer)
+      with const @Integer @[Integer]
+      where const :: forall a b. a -> b -> a
+    ($) (_ :: [Integer] -> Integer)
+      with ($) @'GHC.Types.LiftedRep @[Integer] @Integer
+      where ($) :: forall a b. (a -> b) -> a -> b
+    fail (_ :: String)
+      with fail @((->) [Integer]) @Integer
+      where fail :: forall (m :: * -> *).
+                    Monad m =>
+                    forall a. String -> m a
+    return (_ :: Integer)
+      with return @((->) [Integer]) @Integer
+      where return :: forall (m :: * -> *). Monad m => forall a. a -> m a
+    (Some refinement hole fits suppressed;
+      use -fmax-refinement-hole-fits=N or -fno-max-refinement-hole-fits)
+
+Which shows that the hole could be replaced with e.g. ``foldl1 _``. While not
+fixing the hole, this can help users understand what options they have.
+
+.. ghc-flag:: -frefinement-level-hole-fits=⟨n⟩
+    :shortdesc: *default: off.* Sets the level of refinement of the
+         refinement hole fits, where level ``n`` means that hole fits
+         of up to ``n`` holes will be considered.
+    :type: dynamic
+    :reverse: -fno-refinement-level-hole-fits
+    :category: verbosity
+
+    :default: off
+
+    The list of valid refinement hole fits is generated by considering
+    hole fits with a varying amount of additional holes. The amount of
+    holes in a refinement can be set by this flag. If the flag is set to 0
+    or not set at all, no valid refinement hole fits will be suggested.
+
+.. ghc-flag:: -fabstract-refinement-hole-fits
+    :shortdesc: *default: off.* Toggles whether refinements where one or more
+         of the holes are abstract are reported.
+    :type: dynamic
+    :reverse: -fno-abstract-refinement-hole-fits
+    :category: verbosity
+
+    :default: off
+
+    Valid list of valid refinement hole fits can often grow large when
+    the refinement level is ``>= 2``, with holes like ``head _ _`` or
+    ``fst _ _``, which are valid refinements, but which are unlikely to be
+    relevant since one or more of the holes are still completely open, in that
+    neither the type nor kind of those holes are constrained by the proposed
+    identifier at all. By default, such holes are not reported. By turning this
+    flag on, such holes are included in the list of valid refinement hole fits.
+
+.. ghc-flag:: -fmax-refinement-hole-fits=⟨n⟩
+    :shortdesc: *default: 6.* Set the maximum number of refinement hole fits
+         for typed holes to display in type error messages.
+    :type: dynamic
+    :reverse: -fno-max-refinement-hole-fits
+    :category: verbosity
+
+    :default: 6
+
+    The list of valid refinement hole fits is limited by displaying up to 6
+    hole fits per hole. The number of hole fits shown can be set by this
+    flag. Turning the limit off with :ghc-flag:`-fno-max-refinement-hole-fits`
+    displays all found hole fits.
+
+.. ghc-flag:: -fshow-hole-matches-of-hole-fits
+    :shortdesc: Toggles whether to show the type of the additional holes
+       in refinement hole fits.
+    :type: dynamic
+    :category: verbosity
+    :reverse: -fno-show-hole-matches-of-hole-fits
+
+    :default: on
+
+    The types of the additional holes in refinement hole fits are displayed
+    in the output, e.g. ``foldl1 (_ :: a -> a -> a)`` is a refinement
+    for the hole ``_ :: [a] -> a``. If this flag is toggled off, the output
+    will display only ``foldl1 _``, which can be used as a direct replacement
+    for the hole, without requiring ``-XScopedTypeVariables``.
+
+
+
+
+Sorting Valid Hole Fits
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+There are currently two ways to sort valid hole fits.
+Sorting can be toggled with :ghc-flag:`-fsort-valid-hole-fits`
+
+.. ghc-flag:: -fno-sort-valid-hole-fits
+    :shortdesc: Disables the sorting of the list of valid hole fits for typed holes
+        in type error messages.
+    :type: dynamic
+    :category: verbosity
+
+    :default: off
+
+    By default the valid hole fits are sorted to show the most relevant
+    hole fits at the top of the list of valid hole fits. This can be
+    toggled off with this flag.
+
+.. ghc-flag:: -fsort-by-size-hole-fits
+    :shortdesc: Sort valid hole fits by size.
+    :type: dynamic
+    :reverse: -fno-sort-by-size-hole-fits
+
+    :default: on
+
+    Sorts by how big the types the quantified type variables in the type of the
+    function would have to be in order to match the type of the hole.
+
+
+.. ghc-flag:: -fsort-by-subsumption-hole-fits
+    :shortdesc: Sort valid hole fits by subsumption.
+    :type: dynamic
+    :reverse: -fno-sort-by-subsumption-hole-fits
+
+    :default: off
 
+    An alternative sort. Sorts by checking which hole fits subsume other
+    hole fits, such that if hole fit a could be used as hole fits for
+    hole fit b, then b appears before a in the output. It is more precise than
+    the default sort, but also a lot slower, since a subsumption check has to be
+    run for each pair of valid hole fits.
 
 .. _partial-type-signatures:
 
@@ -11004,10 +12272,19 @@ 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: ::
+
+   deriving instance _ => Eq (Foo a)
+
+This denotes a derived ``Eq (Foo a)`` instance where the context is inferred,
+in much the same way that ordinary ``deriving`` clauses do. Any other use of
+wildcards in a standalone ``deriving`` declaration is prohibited.
 
 In all other contexts, type wildcards are disallowed, and a named wildcard is treated
 as an ordinary type variable.  For example: ::
@@ -11211,6 +12488,29 @@ demonstrates:
     Prelude> fst x
     True
 
+Limitations of deferred type errors
+-----------------------------------
+The errors that can be deferred are:
+
+- Out of scope term variables
+- Equality constraints; e.g. `ord True` gives rise to an insoluble equality constraint `Char ~ Bool`, which can be deferred.
+- Type-class and implicit-parameter constraints
+
+All other type errors are reported immediately, and cannot be deferred; for
+example, an ill-kinded type signature, an instance declaration that is
+non-terminating or ill-formed, a type-family instance that does not
+obey the declared injectivity constraints, etc etc.
+
+In a few cases, even equality constraints cannot be deferred.  Specifically:
+
+- Kind-equalities cannot be deferred, e.g. ::
+
+    f :: Int Bool -> Char
+
+  This type signature contains a kind error which cannot be deferred.
+
+- Type equalities under a forall cannot be deferred (c.f. Trac #14605).
+
 .. _template-haskell:
 
 Template Haskell
@@ -11227,7 +12527,7 @@ page on the GHC Wiki has a wealth of information. You may also consult the
 :th-ref:`Haddock reference documentation <Language.Haskell.TH.>`.
 Many changes to the original
 design are described in `Notes on Template Haskell version
-2 <http://research.microsoft.com/~simonpj/papers/meta-haskell/notes2.ps>`__.
+2 <https://www.haskell.org/ghc/docs/papers/th2.ps>`__.
 Not all of these changes are in GHC, however.
 
 The first example from that paper is set out below (:ref:`th-example`)
@@ -11610,9 +12910,9 @@ non-trivial program, you may be interested in combining this with the
 :ghc-flag:`-ddump-to-file` flag (see :ref:`dumping-output`. For each file using
 Template Haskell, this will show the output in a ``.dump-splices`` file.
 
-The flag :ghc-flag:`-dth-dec-file=⟨file⟩` shows the expansions of all top-level
+The flag :ghc-flag:`-dth-dec-file` dumps the expansions of all top-level
 TH declaration splices, both typed and untyped, in the file :file:`M.th.hs`
-where M is the name of the module being compiled. Note that other types of
+for each module `M` being compiled. Note that other types of
 splices (expressions, types, and patterns) are not shown. Application
 developers can check this into their repository so that they can grep for
 identifiers that were defined in Template Haskell. This is similar to using
@@ -11631,7 +12931,7 @@ Below is a sample output of :ghc-flag:`-ddump-splices` ::
       foo :: Int -> Int
       foo x = (x + 1)
 
-Below is the output of the same sample using :ghc-flag:`-dth-dec-file=⟨file⟩` ::
+Below is the output of the same sample using :ghc-flag:`-dth-dec-file` ::
 
     -- TH_pragma.hs:(6,4)-(8,26): Splicing declarations
     foo :: Int -> Int
@@ -12361,7 +13661,7 @@ Bang patterns and Strict Haskell
 In high-performance Haskell code (e.g. numeric code) eliminating
 thunks from an inner loop can be a huge win.
 GHC supports three extensions to allow the programmer to specify
-use of strict (call-by-value) evalution rather than lazy (call-by-need)
+use of strict (call-by-value) evaluation rather than lazy (call-by-need)
 evaluation.
 
 - Bang patterns (:extension:`BangPatterns`) makes pattern matching and
@@ -12541,7 +13841,7 @@ optionally had by adding ``!`` in front of a variable.
 
    Turning patterns into irrefutable ones requires ``~(~p)`` or ``(~ ~p)`` when ``Strict`` is enabled.
 
-   
+
 
 -  **Let/where bindings**
 
@@ -12858,7 +14158,7 @@ GHC offers a helping hand here, doing all of this for you. For every use
 of ``assert`` in the user's source: ::
 
     kelvinToC :: Double -> Double
-    kelvinToC k = assert (k >= 0.0) (k+273.15)
+    kelvinToC k = assert (k >= 0.0) (k-273.15)
 
 GHC will rewrite this to also include the source location where the
 assertion was made, ::
@@ -13063,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
@@ -13095,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
@@ -13123,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.
+
+.. pragma:: DEPRECATED
+
+    :where: declaration
 
-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.
+    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: ::
 
@@ -13181,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
@@ -13214,9 +14525,8 @@ Conjunction binds stronger than disjunction.
 
 If no ``MINIMAL`` pragma is given in the class declaration, it is just as if
 a pragma ``{-# MINIMAL op1, op2, ..., opn #-}`` was given, where the
-``opi`` are the methods (a) that lack a default method in the class
-declaration, and (b) whose name that does not start with an underscore
-(c.f. :ghc-flag:`-Wmissing-methods`, :ref:`options-sanity`).
+``opi`` are the methods that lack a default method in the class
+declaration (c.f. :ghc-flag:`-Wmissing-methods`, :ref:`options-sanity`).
 
 This warning can be turned off with the flag
 :ghc-flag:`-Wno-missing-methods <-Wmissing-methods>`.
@@ -13233,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
@@ -13299,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
@@ -13312,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
@@ -13343,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:
 
@@ -13382,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.
 
@@ -13398,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
@@ -13432,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
@@ -13447,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:
@@ -13462,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
@@ -13512,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:
@@ -13525,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:
 
 ::
@@ -13623,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
@@ -13648,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.
@@ -13658,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
@@ -13674,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.
@@ -13682,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``:
@@ -13706,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:
 
 ::
@@ -13745,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
@@ -13787,19 +15119,19 @@ 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
-   -O
-   , for technical reasons (see
-   tick 5252
-   )
+   In fact, :pragma:`UNPACK` has no effect without :ghc-flag:`-O`, for technical
+   reasons (see :ghc-ticket:`5252`).
 
 .. _nounpack-pragma:
 
 ``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: ::
@@ -13814,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
@@ -13827,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.
@@ -13873,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.
 
@@ -13954,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
@@ -13969,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
@@ -14000,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
@@ -14009,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
@@ -14037,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``.
@@ -14051,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: ::
 
@@ -14071,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
@@ -14165,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.
@@ -14203,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:
@@ -14238,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 #-}
@@ -14400,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
@@ -14462,7 +15833,7 @@ Haskell datatypes: ::
     -- | Unit: used for constructors without arguments
     data U1 p = U1
 
-    -- | Constants, additional parameters and recursion of kind *
+    -- | Constants, additional parameters and recursion of kind Type
     newtype K1 i c p = K1 { unK1 :: c }
 
     -- | Meta-information (constructor names, etc.)
@@ -14481,22 +15852,22 @@ datatypes and their internal representation as a sum-of-products: ::
 
     class Generic a where
       -- Encode the representation of a user datatype
-      type Rep a :: * -> *
+      type Rep a :: Type -> Type
       -- Convert from the datatype to its representation
       from  :: a -> (Rep a) x
       -- Convert from the representation to the datatype
       to    :: (Rep a) x -> a
 
-    class Generic1 (f :: k -> *) where
-      type Rep1 f :: k -> *
+    class Generic1 (f :: k -> Type) where
+      type Rep1 f :: k -> Type
 
       from1  :: f a -> Rep1 f a
       to1    :: Rep1 f a -> f a
 
 ``Generic1`` is used for functions that can only be defined over type
 containers, such as ``map``. Note that ``Generic1`` ranges over types of kind
-``* -> *`` by default, but if the :extension:`PolyKinds` extension is enabled,
-then it can range of types of kind ``k -> *``, for any kind ``k``.
+``Type -> Type`` by default, but if the :extension:`PolyKinds` extension is
+enabled, then it can range of types of kind ``k -> Type``, for any kind ``k``.
 
 .. extension:: DeriveGeneric
     :shortdesc: Enable deriving for the Generic class.
@@ -14687,7 +16058,7 @@ Roles
    single: roles
 
 Using :extension:`GeneralizedNewtypeDeriving`
-(:ref:`generalized-newtype-deriving`), a programmer can take existing
+(:ref:`newtype-deriving`), a programmer can take existing
 instances of classes and "lift" these into instances of that class for a
 newtype. However, this is not always safe. For example, consider the
 following:
@@ -14773,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.
 
@@ -14915,28 +16286,67 @@ HasCallStack
 ``GHC.Stack.HasCallStack`` is a lightweight method of obtaining a
 partial call-stack at any point in the program.
 
-A function can request its call-site with the ``HasCallStack`` constraint.
-For example, we can define ::
+A function can request its call-site with the ``HasCallStack`` constraint
+and access it as a Haskell value by using ``callStack``.
+
+One can then use functions from ``GHC.Stack`` to inspect or pretty
+print (as is done in ``f`` below) the call stack.
+
+   f :: HasCallStack => IO ()
+   f = putStrLn (prettyCallStack callStack)
+
+   g :: HasCallStack => IO ()
+   g = f
 
-   errorWithCallStack :: HasCallStack => String -> a
+Evaluating ``f`` directly shows a call stack with a single entry,
+while evaluating ``g``, which also requests its call-site, shows
+two entries, one for each computation "annotated" with
+``HasCallStack``.
 
-as a variant of ``error`` that will get its call-site (as of GHC 8.0,
-``error`` already gets its call-site, but let's assume for the sake of
-demonstration that it does not). We can access the call-stack inside
-``errorWithCallStack`` with ``GHC.Stack.callStack``. ::
+.. code-block:: none
+
+   ghci> f
+   CallStack (from HasCallStack):
+     f, called at <interactive>:19:1 in interactive:Ghci1
+   ghci> g
+   CallStack (from HasCallStack):
+     f, called at <interactive>:17:5 in main:Main
+     g, called at <interactive>:20:1 in interactive:Ghci2
+
+The ``error`` function from the Prelude supports printing the call stack that
+led to the error in addition to the usual error message:
+
+.. code-block:: none
+
+   ghci> error "bad"
+   *** Exception: bad
+   CallStack (from HasCallStack):
+     error, called at <interactive>:25:1 in interactive:Ghci5
 
-   errorWithCallStack :: HasCallStack => String -> a
-   errorWithCallStack msg = error (msg ++ "\n" ++ prettyCallStack callStack)
+The call stack here consists of a single entry, pinpointing the source
+of the call to ``error``. However, by annotating several computations
+with ``HasCallStack``, figuring out the exact circumstances and sequences
+of calls that lead to a call to ``error`` becomes a lot easier, as demonstrated
+with the simple example below. ::
 
-Thus, if we call ``errorWithCallStack`` we will get a formatted call-stack
-alongside our error message.
+   f :: HasCallStack => IO ()
+   f = error "bad bad bad"
+
+   g :: HasCallStack => IO ()
+   g = f
+
+   h :: HasCallStack => IO ()
+   h = g
 
 .. code-block:: none
 
-   ghci> errorWithCallStack "die"
-   *** Exception: die
+   ghci> h
+   *** Exception: bad bad bad
    CallStack (from HasCallStack):
-     errorWithCallStack, called at <interactive>:2:1 in interactive:Ghci1
+     error, called at call-stack.hs:4:5 in main:Main
+     f, called at call-stack.hs:7:5 in main:Main
+     g, called at call-stack.hs:10:5 in main:Main
+     h, called at <interactive>:28:1 in interactive:Ghci1
 
 The ``CallStack`` will only extend as far as the types allow it, for
 example ::
@@ -15013,4 +16423,3 @@ compilation with ``-prof``. On the other hand, as the ``CallStack`` is
 built up explicitly via the ``HasCallStack`` constraints, it will
 generally not contain as much information as the simulated call-stacks
 maintained by the RTS.
-