Document TypeInType (#11614)
[ghc.git] / docs / users_guide / glasgow_exts.rst
index 341a2ee..b42eb80 100644 (file)
@@ -105,6 +105,9 @@ machine-addition that we all know and love—usually one instruction.
 Primitive (unboxed) types cannot be defined in Haskell, and are
 therefore built into the language and compiler. Primitive types are
 always unlifted; that is, a value of a primitive type cannot be bottom.
+(Note: a "boxed" type means that a value is represented by a pointer to a heap
+object; a "lifted" type means that terms of that type may be bottom. See
+the next paragraph for an example.)
 We use the convention (but it is only a convention) that primitive
 types, values, and operations have a ``#`` suffix (see
 :ref:`magic-hash`). For some primitive types we have special syntax for
@@ -113,28 +116,47 @@ literals, also described in the `same section <#magic-hash>`__.
 Primitive values are often represented by a simple bit-pattern, such as
 ``Int#``, ``Float#``, ``Double#``. But this is not necessarily the case:
 a primitive value might be represented by a pointer to a heap-allocated
-object. Examples include ``Array#``, the type of primitive arrays. A
+object. Examples include ``Array#``, the type of primitive arrays. Thus,
+``Array#`` is an unlifted, boxed type. A
 primitive array is heap-allocated because it is too big a value to fit
 in a register, and would be too expensive to copy around; in a sense, it
 is accidental that it is represented by a pointer. If a pointer
 represents a primitive value, then it really does point to that value:
-no unevaluated thunks, no indirections…nothing can be at the other end
+no unevaluated thunks, no indirections. Nothing can be at the other end
 of the pointer than the primitive value. A numerically-intensive program
 using unboxed types can go a *lot* faster than its “standard”
 counterpart—we saw a threefold speedup on one example.
 
-There are some restrictions on the use of primitive types:
+Unboxed type kinds
+------------------
 
--  The main restriction is that you can't pass a primitive value to a
-   polymorphic function or store one in a polymorphic data type. This
-   rules out things like ``[Int#]`` (i.e. lists of primitive integers).
-   The reason for this restriction is that polymorphic arguments and
-   constructor fields are assumed to be pointers: if an unboxed integer
-   is stored in one of these, the garbage collector would attempt to
-   follow it, leading to unpredictable space leaks. Or a ``seq``
-   operation on the polymorphic component may attempt to dereference the
-   pointer, with disastrous results. Even worse, the unboxed value might
-   be larger than a pointer (``Double#`` for instance).
+Because unboxed types are represented without the use of pointers, we
+cannot store them in standard datatypes. For example, the ``Just`` node
+of ``Just 42#`` would have to be different from the ``Just`` node of
+``Just 42``; the former stores an integer directly, while the latter
+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. 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 is easy to see 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.
+
+There are some restrictions on the use of primitive types:
 
 -  You cannot define a newtype whose representation type (the argument
    type of the data constructor) is an unboxed type. Thus, this is
@@ -6853,131 +6875,329 @@ Note that for the purpose of injectivity check in bullets (4) and (5)
 GHC uses a special variant of unification algorithm that treats type
 family applications as possibly unifying with anything.
 
-.. _kind-polymorphism:
+.. _promotion:
 
-Kind polymorphism
-=================
+Datatype promotion
+==================
 
-.. ghc-flag:: -XPolyKinds
+.. ghc-flag:: -XDataKinds
 
-    :implies: :ghc-flag:`-XKindSignatures`
     :since: 7.4.1
 
-    Allow kind polymorphic types.
+    Allow promotion of data types to kind level.
 
-This section describes *kind polymorphism*, and extension enabled by
-:ghc-flag:`-XPolyKinds`. It is described in more detail in the paper `Giving
+This section describes *data type promotion*, an extension to the kind
+system that complements kind polymorphism. It is enabled by
+:ghc-flag:`-XDataKinds`, and described in more detail in the paper `Giving
 Haskell a Promotion <http://dreixel.net/research/pdf/ghp.pdf>`__, which
 appeared at TLDI 2012.
 
-Overview of kind polymorphism
------------------------------
+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 ``* -> * -> *``).
+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
+prevent simple errors. Consider the example of type-level natural
+numbers, and length-indexed vectors: ::
+
+    data Ze
+    data Su n
+
+    data Vec :: * -> * -> * where
+      Nil  :: Vec a Ze
+      Cons :: a -> Vec a n -> Vec a (Su n)
+
+The kind of ``Vec`` is ``* -> * -> *``. 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.
+
+With :ghc-flag:`-XDataKinds`, the example above can then be rewritten to: ::
 
-Currently there is a lot of code duplication in the way ``Typeable`` is
-implemented (:ref:`deriving-typeable`): ::
+    data Nat = Ze | Su Nat
 
-    class Typeable (t :: *) where
-      typeOf :: t -> TypeRep
+    data Vec :: * -> Nat -> * where
+      Nil  :: Vec a 'Ze
+      Cons :: a -> Vec a n -> Vec a ('Su n)
 
-    class Typeable1 (t :: * -> *) where
-      typeOf1 :: t a -> TypeRep
+With the improved kind of ``Vec``, things like ``Vec Int Char`` are now
+ill-kinded, and GHC will report an error.
 
-    class Typeable2 (t :: * -> * -> *) where
-      typeOf2 :: t a b -> TypeRep
+Overview
+--------
 
-Kind polymorphism (with :ghc-flag:`-XPolyKinds`) allows us to merge all these
-classes into one: ::
+With :ghc-flag:`-XDataKinds`, GHC automatically promotes every datatype
+to be a kind and its (value) constructors to be type constructors. The
+following types ::
 
-    data Proxy t = Proxy
+    data Nat = Ze | Su Nat
 
-    class Typeable t where
-      typeOf :: Proxy t -> TypeRep
+    data List a = Nil | Cons a (List a)
 
-    instance Typeable Int  where typeOf _ = TypeRep
-    instance Typeable []   where typeOf _ = TypeRep
+    data Pair a b = Pair a b
 
-Note that the datatype ``Proxy`` has kind ``forall k. k -> *`` (inferred
-by GHC), and the new ``Typeable`` class has kind
-``forall k. k -> Constraint``.
+    data Sum a b = L a | R b
 
-Note the following specific points:
+give rise to the following kinds and type constructors: ::
 
--  Generally speaking, with :ghc-flag:`-XPolyKinds`, GHC will infer a
-   polymorphic kind for un-decorated declarations, whenever possible.
-   For example, in GHCi ::
+    Nat :: *
+    'Ze :: Nat
+    'Su :: Nat -> Nat
 
-       ghci> :set -XPolyKinds
-       ghci> data T m a = MkT (m a)
-       ghci> :k T
-       T :: (k -> *) -> k -> *
+    List :: * -> *
+    'Nil  :: forall k. List k
+    'Cons :: forall k. k -> List k -> List k
 
--  GHC does not usually print explicit ``forall``\ s, including kind
-   ``forall``\ s. You can make GHC show them explicitly with
-   :ghc-flag:`-fprint-explicit-foralls` (see :ref:`options-help`): ::
+    Pair  :: * -> * -> *
+    'Pair :: forall k1 k2. k1 -> k2 -> Pair k1 k2
 
-       ghci> :set -XPolyKinds
-       ghci> :set -fprint-explicit-foralls
-       ghci> data T m a = MkT (m a)
-       ghci> :k T
-       T :: forall (k :: BOX). (k -> *) -> k -> *
+    Sum :: * -> * -> *
+    'L :: k1 -> Sum k1 k2
+    'R :: k2 -> Sum k1 k2
 
--  Just as in the world of terms, you can restrict polymorphism using a
-   kind signature (sometimes called a kind annotation) ::
+The following restrictions apply to promotion:
 
-       data T m (a :: *) = MkT (m a)
-       -- GHC now infers kind   T :: (* -> *) -> * -> *
+-  We promote ``data`` types and ``newtypes``, but not type synonyms, or
+   type/data families (:ref:`type-families`).
 
-   NB: :ghc-flag:`-XPolyKinds` implies :ghc-flag:`-XKindSignatures` (see
-   :ref:`kinding`).
+-  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 -> *``.
 
--  The source language does not support an explicit ``forall`` for kind
-   variables. Instead, when binding a type variable, you can simply
-   mention a kind variable in a kind annotation for that type-variable
-   binding, thus: ::
+-  We do not promote data constructors that are kind polymorphic,
+   involve constraints, mention type or data families, or involve types
+   that are not promotable.
+
+The flag :ghc-flag:`-XTypeInType` (which implies :ghc-flag:`-XDataKinds`)
+relaxes some of these restrictions, allowing:
+
+-  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 T (m :: k -> *) a = MkT (m a)
-       -- GHC now infers kind   T :: forall k. (k -> *) -> k -> *
+-  All datatypes, even those with rich kinds, get promoted. For example: ::
 
--  The (implicit) kind "forall" is placed just outside the outermost
-   type-variable binding whose kind annotation mentions the kind
-   variable. For example ::
+     data Proxy a = Proxy
+     data App f a = MkApp (f a)   -- App :: forall k. (k -> *) -> k -> *
+     x = Proxy :: Proxy ('MkApp ('Just 'True))
 
-       f1 :: (forall a m. m a -> Int) -> Int
-                -- f1 :: forall (k::BOX).
-                --       (forall (a::k) (m::k->*). m a -> Int)
-                --       -> Int
+.. _promotion-syntax:
 
-       f2 :: (forall (a::k) m. m a -> Int) -> Int
-                -- f2 :: (forall (k::BOX) (a::k) (m::k->*). m a -> Int)
-                --       -> Int
+Distinguishing between types and constructors
+---------------------------------------------
 
-   Here in ``f1`` there is no kind annotation mentioning the polymorphic
-   kind variable, so ``k`` is generalised at the top level of the
-   signature for ``f1``. But in the case of of ``f2`` we give a kind
-   annotation in the ``forall (a:k)`` binding, and GHC therefore puts
-   the kind ``forall`` right there too. This design decision makes
-   default case (``f1``) as polymorphic as possible; remember that a
-   *more* polymorphic argument type (as in ``f2`` makes the overall
-   function *less* polymorphic, because there are fewer acceptable
-   arguments.
+In the examples above, all promoted constructors are prefixed with a single
+quote mark ``'``. This mark tells GHC to look in the data constructor namespace
+for a name, not the type (constructor) namespace. Consider ::
+
+    data P = MkP    -- 1
+
+    data Prom = P   -- 2
+
+We can thus distinguish the type ``P`` (which has a constructor ``MkP``)
+from the promoted data constructor ``'P`` (of kind ``Prom``).
+
+As a convenience, GHC allows you to omit the quote mark when the name is
+unambiguous. However, our experience has shown that the quote mark helps
+to make code more readable and less error-prone. GHC thus supports
+:ghc-flag:`-Wunticked-promoted-constructors` that will warn you if you
+use a promoted data constructor without a preceding quote mark.
+
+Just as in the case of Template Haskell (:ref:`th-syntax`), GHC gets
+confused if you put a quote mark before a data constructor whose second
+character is a quote mark. In this case, just put a space between the
+promotion quote and the data constructor: ::
+
+  data T = A'
+  type S = 'A'   -- ERROR: looks like a character
+  type R = ' A'  -- OK: promoted `A'`
+
+.. _promoted-lists-and-tuples:
+
+Promoted list and tuple types
+-----------------------------
+
+With :ghc-flag:`-XDataKinds`, 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
+      HNil  :: HList '[]
+      HCons :: a -> HList t -> HList (a ': t)
+
+    data Tuple :: (*,*) -> * where
+      Tuple :: a -> b -> Tuple '(a,b)
+
+    foo0 :: HList '[]
+    foo0 = HNil
+
+    foo1 :: HList '[Int]
+    foo1 = HCons (3::Int) HNil
+
+    foo2 :: HList [Int, Bool]
+    foo2 = ...
+
+For type-level lists of *two or more elements*, such as the signature of
+``foo2`` above, the quote may be omitted because the meaning is unambiguous. But
+for lists of one or zero elements (as in ``foo0`` and ``foo1``), the quote is
+required, because the types ``[]`` and ``[Int]`` have existing meanings in
+Haskell.
 
 .. note::
+    The declaration for ``HCons`` also requires :ghc-flag:`-XTypeOperators`
+    because of infix type operator ``(:')``
+
+
+.. _promotion-existentials:
+
+Promoting existential data constructors
+---------------------------------------
+
+Note that we do promote existential data constructors that are otherwise
+suitable. For example, consider the following: ::
+
+    data Ex :: * where
+      MkEx :: forall a. a -> Ex
+
+Both the type ``Ex`` and the data constructor ``MkEx`` get promoted,
+with the polymorphic kind ``'MkEx :: forall k. k -> Ex``. Somewhat
+surprisingly, you can write a type family to extract the member of a
+type-level existential: ::
+
+    type family UnEx (ex :: Ex) :: k
+    type instance UnEx (MkEx x) = x
+
+At first blush, ``UnEx`` seems poorly-kinded. The return kind ``k`` is
+not mentioned in the arguments, and thus it would seem that an instance
+would have to return a member of ``k`` *for any* ``k``. However, this is
+not the case. The type family ``UnEx`` is a kind-indexed type family.
+The return kind ``k`` is an implicit parameter to ``UnEx``. The
+elaborated definitions are as follows: ::
+
+    type family UnEx {k :: *} (ex :: Ex) :: k
+    type instance UnEx {k} (MkEx @k x) = x
+
+Thus, the instance triggers only when the implicit parameter to ``UnEx``
+matches the implicit parameter to ``MkEx``. Because ``k`` is actually a
+parameter to ``UnEx``, the kind is not escaping the existential, and the
+above code is valid.
+
+See also :ghc-ticket:`7347`.
+
+.. _type-in-type:
+.. _kind-polymorphism:
+
+Kind polymorphism and Type-in-Type
+==================================
+
+.. ghc-flag: -XTypeInType
+
+    :implies: :ghc-flag:`-XPolyKinds`, :ghc-flag:`-XDataKinds`, :ghc-flag:`-XKindSignatures`
+    :since: 8.0.1
+
+    Allow kinds to be as intricate as types.
+
+.. ghc-flag:: -XPolyKinds
+
+    :implies: :ghc-flag:`-XKindSignatures`
+    :since: 7.4.1
+
+    Allow kind polymorphic types.
+
+This section describes GHC's kind system, as it appears in version 8.0 and beyond.
+The kind system as described here is always in effect, with or without extensions,
+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 :ghc-flag:`-XTypeInType` and :ghc-flag:`-XPolyKinds`
+---------------------------------------------------------------------------
+
+It is natural to consider :ghc-flag:`-XTypeInType` as an extension of
+:ghc-flag:`-XPolyKinds`. 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: :ghc-flag:`-XPolyKinds` was introduced for GHC 7.4,
+when it was experimental and temperamental. The wrinkles were smoothed out for
+GHC 7.6. :ghc-flag:`-XTypeInType` 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
+:ghc-flag:`-XPolyKinds` to work properly while being duly sceptical of
+:ghc-flag:`-XTypeInType`. In particular, we recommend enabling
+:ghc-flag:`-dcore-lint` whenever using :ghc-flag:`-XTypeInType`; that flag
+turns on a set of internal checks within GHC that will discover bugs in the
+implementation of :ghc-flag:`-XTypeInType`. 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
+:ghc-flag:`-XTypeInType` is enabled, some particularly thorny cases may have
+slipped through. It is thus possible that some construct is available in GHC
+8.0 with :ghc-flag:`-XPolyKinds` 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
+-----------------------------
+
+Consider inferring the kind for ::
+
+  data App f a = MkApp (f a)
 
-   These rules are a bit indirect and clumsy. Perhaps GHC should
-   allow explicit kind quantification. But the implicit quantification
-   (e.g. in the declaration for data type T above) is certainly very
-   convenient, and it is not clear what the syntax for explicit
-   quantification should be.
+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
+(:ghc-flag:`-XKindSignatures`), it is necessary to use a dummy constructor
+to get a Haskell compiler to infer the second kind. With kind polymorphism
+(:ghc-flag:`-XPolyKinds`), GHC infers the kind ``forall k. (k -> *) -> k -> *``
+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 *
+
+  data T a = MkT (a Int)    -- `a` is inferred to have kind (* -> *)
+  App T Maybe     -- `k` is instantiated to (* -> *)
+
+Overview of Type-in-Type
+------------------------
+
+GHC 8 extends the idea of kind polymorphism by declaring that types and kinds
+are indeed one and the same. Nothing within GHC distinguishes between types
+and kinds. Another way of thinking about this is that the type ``Bool`` and
+the "promoted kind" ``Bool`` are actually identical. (Note that term
+``True`` and the type ``'True`` are still distinct, because the former can
+be used in expressions and the latter in types.) This lack of distinction
+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.
+
+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>`__
+introducing this kind system to GHC/Haskell.
 
 Principles of kind inference
 ----------------------------
 
 Generally speaking, when :ghc-flag:`-XPolyKinds` is on, GHC tries to infer the
-most general kind for a declaration. For example: ::
-
-    data T f a = MkT (f a)   -- GHC infers:
-                             -- T :: forall k. (k->*) -> k -> *
-
+most general kind for a declaration.
 In this case the definition has a right-hand side to inform kind
 inference. But that is not always the case. Consider ::
 
@@ -6990,10 +7210,10 @@ GHC defaults those entirely-unconstrained kind variables to ``*`` and we
 get ``F :: * -> *``. 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 F4 (a :: k1) :: k  -- F4 :: forall k1 k2. k1 -> k2
+    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 F4 (a :: k1) :: k2  -- F4 :: forall k1 k2. k1 -> k2
 
 The general principle is this:
 
@@ -7005,7 +7225,7 @@ The general principle is this:
 
 -  *When there is no right hand side, GHC defaults argument and result
    kinds to ``*``, except when directed otherwise by a kind signature*.
-   Examples: data and type family declarations.
+   Examples: data and open type family declarations.
 
 This rule has occasionally-surprising consequences (see
 :ghc-ticket:`10132`. ::
@@ -7035,8 +7255,8 @@ use *monomorphic* recursion. Consider this (contrived) example: ::
 
 The recursive use of ``T`` forced the second argument to have kind
 ``*``. However, just as in type inference, you can achieve polymorphic
-recursion by giving a *complete kind signature* for ``T``. A complete
-kind signature is present when all argument kinds and the result kind
+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
@@ -7057,22 +7277,22 @@ signature" for a type constructor? These are the forms:
    complete signature. ::
 
        data T1 :: (k -> *) -> k -> *       where ...
-       -- Yes  T1 :: forall k. (k->*) -> k -> *
+       -- Yes;  T1 :: forall k. (k->*) -> k -> *
 
        data T2 (a :: k -> *) :: k -> *     where ...
-       -- Yes  T2 :: forall k. (k->*) -> k -> *
+       -- Yes;  T2 :: forall k. (k->*) -> k -> *
 
        data T3 (a :: k -> *) (b :: k) :: * where ...
-       -- Yes  T3 :: forall k. (k->*) -> k -> *
+       -- Yes;  T3 :: forall k. (k->*) -> k -> *
 
        data T4 (a :: k -> *) (b :: k)      where ...
-       -- Yes  T4 :: forall k. (k->*) -> k -> *
+       -- Yes;  T4 :: forall k. (k->*) -> k -> *
 
        data T5 a (b :: k) :: *             where ...
-       -- No  kind is inferred
+       -- No;  kind is inferred
 
        data T6 a b                         where ...
-       -- No  kind is inferred
+       -- No;  kind is inferred
 
 -  For a class, every type variable must be annotated with a kind.
 
@@ -7087,8 +7307,8 @@ signature" for a type constructor? These are the forms:
    rather apparent, but it is still not considered to have a complete
    signature -- no inference can be done before detecting the signature.
 
--  An open type or data family declaration *always* has a complete
-   user-specified kind signature; un-annotated type variables default to
+-  An open type or data family declaration *always* has a CUSK;
+   un-annotated type variables default to
    kind ``*``: ::
 
        data family D1 a               -- D1 :: * -> *
@@ -7108,11 +7328,27 @@ signature" for a type constructor? These are the forms:
    variables are annotated and a return kind (with a top-level ``::``)
    is supplied.
 
+With :ghc-flag:`-XTypeInType` 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 ::
+
+  data Proxy a           -- Proxy :: forall k. k -> *
+  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.
+
 Kind inference in closed type families
 --------------------------------------
 
 Although all open type families are considered to have a complete
-user-specified kind signature, we can relax this condition for closed
+user-supplied kind signature, we can relax this condition for closed
 type families, where we have equations on which to perform kind
 inference. GHC will infer kinds for the arguments and result types of a
 closed type family.
@@ -7120,7 +7356,9 @@ closed type family.
 GHC supports *kind-indexed* type families, where the family matches both
 on the kind and type. GHC will *not* infer this behaviour without a
 complete user-supplied kind signature, as doing so would sometimes infer
-non-principal types.
+non-principal types. Indeed, we can see kind-indexing as a form
+of polymorphic recursion, where a type is used at a kind other than
+its most general in its own definition.
 
 For example: ::
 
@@ -7171,219 +7409,284 @@ infrastructure, and it's not clear the payoff is worth it. If you want
 to restrict ``b``\ 's kind in the instance above, just use a kind
 signature in the instance head.
 
-.. _promotion:
+Kind inference in type signatures
+---------------------------------
 
-Datatype promotion
-==================
+When kind-checking a type, GHC considers only what is written in that
+type when figuring out how to generalise the type's kind.
 
-.. ghc-flag:: -XDataKinds
+For example,
+consider these definitions (with :ghc-flag:`-XScopedTypeVariables`): ::
 
-    :since: 7.4.1
+  data Proxy a    -- Proxy :: forall k. k -> *
+  p :: forall a. Proxy a
+  p = Proxy :: Proxy (a :: *)
 
-    Allow promotion of data types to kind level.
+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
+``forall a. Proxy a``, GHC assumes ``a``'s kind should be generalised, not
+restricted to be ``*``. The function definition is then rejected for being
+more specific than its type signature.
 
-This section describes *data type promotion*, an extension to the kind
-system that complements kind polymorphism. It is enabled by
-:ghc-flag:`-XDataKinds`, and described in more detail in the paper `Giving
-Haskell a Promotion <http://dreixel.net/research/pdf/ghp.pdf>`__, which
-appeared at TLDI 2012.
+Explicit kind quantification
+----------------------------
 
-Motivation
-----------
+Enabled by :ghc-flag:`-XTypeInType`, GHC now supports explicit kind quantification,
+as in these examples: ::
+  
+  data Proxy :: forall k. k -> *
+  f :: (forall k (a :: k). Proxy a -> ()) -> Int
+
+Note that the second example has a ``forall`` that binds both a kind ``k`` and
+a type variable ``a`` of kind ``k``. In general, there is no limit to how
+deeply nested this sort of dependency can work. However, the dependency must
+be well-scoped: ``forall (a :: k) k. ...`` is an error.
+
+For backward compatibility, kind variables *do not* need to be bound explicitly,
+even if the type starts with ``forall``.
+
+Accordingly, the rule for kind quantification in higher-rank contexts has
+changed slightly. In GHC 7, if a kind variable was mentioned for the first
+time in the kind of a variable bound in a non-top-level ``forall``, the kind
+variable was bound there, too.
+That is, in ``f :: (forall (a :: k). ...) -> ...``, the ``k`` was bound
+by the same ``forall`` as the ``a``. In GHC 8, however, all kind variables
+mentioned in a type are bound at the outermost level. If you want one bound
+in a higher-rank ``forall``, include it explicitly.
+
+Kind-indexed GADTs
+------------------
 
-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 lifted types (kind
-``*``), type constructors (e.g. kind ``* -> * -> *``), and unlifted
-types (:ref:`glasgow-unboxed`). 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
-prevent simple errors. Consider the example of type-level natural
-numbers, and length-indexed vectors: ::
+Consider the type ::
 
-    data Ze
-    data Su n
+  data G (a :: k) where
+    GInt    :: G Int
+    GMaybe  :: G Maybe
 
-    data Vec :: * -> * -> * where
-      Nil  :: Vec a Ze
-      Cons :: a -> Vec a n -> Vec a (Su n)
+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 :ghc-flag:`-XTypeInType`
+be in effect, but pattern-matching on ``G`` requires no extension beyond
+:ghc-flag:`-XGADTs`. That this works is actually a straightforward extension
+of regular GADTs and a consequence of the fact that kinds and types are the
+same.
 
-The kind of ``Vec`` is ``* -> * -> *``. This means that eg.
-``Vec Int Char`` is a well-kinded type, even though this is not what we
-intend when defining length-indexed vectors.
+Note that the datatype ``G`` is used at different kinds in its body, and
+therefore that kind-indexed GADTs use a form of polymorphic recursion.
+It is thus only possible to use this feature if you have provided a
+complete user-supplied kind signature
+for the datatype (:ref:`complete-kind-signatures`).
 
-With :ghc-flag:`-XDataKinds`, the example above can then be rewritten to: ::
+Constraints in kinds
+--------------------
 
-    data Nat = Ze | Su Nat
+As kinds and types are the same, kinds can now (with :ghc-flag:`-XTypeInType`)
+contain type constraints. Only equality constraints are currently supported,
+however. We expect this to extend to other constraints in the future.
 
-    data Vec :: * -> Nat -> * where
-      Nil  :: Vec a Ze
-      Cons :: a -> Vec a n -> Vec a (Su n)
+Here is an example of a constrained kind: ::
 
-With the improved kind of ``Vec``, things like ``Vec Int Char`` are now
-ill-kinded, and GHC will report an error.
+  type family IsTypeLit a where
+    IsTypeLit Nat    = 'True
+    IsTypeLit Symbol = 'True
+    IsTypeLit a      = 'False
 
-Overview
---------
+  data T :: forall a. (IsTypeLit a ~ 'True) => a -> * where
+    MkNat    :: T 42
+    MkSymbol :: T "Don't panic!"
 
-With :ghc-flag:`-XDataKinds`, GHC automatically promotes every suitable datatype
-to be a kind, and its (value) constructors to be type constructors. The
-following types ::
+The declarations above are accepted. However, if we add ``MkOther :: T Int``,
+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.
 
-    data Nat = Ze | Su Nat
+The kind ``*``
+--------------
 
-    data List a = Nil | Cons a (List a)
+The kind ``*`` classifies ordinary types. Without :ghc-flag:`-XTypeInType`,
+this identifier is always in scope when writing a kind. However, with
+:ghc-flag:`-XTypeInType`, 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 :ghc-flag:`-XTypeInType` enabled.
+So as not to cause naming collisions, it is not imported by default;
+you must ``import Data.Kind`` to get ``*`` (but only with :ghc-flag:`-XTypeInType`
+enabled).
 
-    data Pair a b = Pair a b
+The only way ``*`` is unordinary is in its parsing. In order to be backward
+compatible, ``*`` is parsed as if it were an alphanumeric idenfifier; 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 two:
 
-    data Sum a b = L a | R b
+- In a Haskell-98-style data constructor, you must put parentheses around
+  ``*``, like this: ::
 
-give rise to the following kinds and type constructors: ::
+    data Universe = Ty (*) | Num Int | ...
 
-    Nat :: BOX
-    Ze :: Nat
-    Su :: Nat -> Nat
+- In an import/export list, you must put parentheses around ``*``, like this: ::
 
-    List k :: BOX
-    Nil  :: List k
-    Cons :: k -> List k -> List k
+    import Data.Kind ( type (*) )
 
-    Pair k1 k2 :: BOX
-    Pair :: k1 -> k2 -> Pair k1 k2
+  Note that the keyword ``type`` there is just to disambiguate the import
+  from a term-level ``(*)``. (:ref:`explicit-namespaces`)
 
-    Sum k1 k2 :: BOX
-    L :: k1 -> Sum k1 k2
-    R :: k2 -> Sum k1 k2
+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: ::
 
-where ``BOX`` is the (unique) sort that classifies kinds. Note that
-``List``, for instance, does not get sort ``BOX -> BOX``, because we do
-not further classify kinds; all kinds have sort ``BOX``.
+  type Set = *   -- silly Agda programmers...
 
-The following restrictions apply to promotion:
+All the affordances for ``*`` also apply to ``★``, the Unicode variant
+of ``*``.
 
--  We promote ``data`` types and ``newtypes``, but not type synonyms, or
-   type/data families (:ref:`type-families`).
+Kind defaulting without :ghc-flag:`-XPolyKinds`
+-----------------------------------------------
 
--  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 -> *``.
+Without :ghc-flag:`-XPolyKinds` or :ghc-flag:`-XTypeInType` 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.
 
--  We do not promote data constructors that are kind polymorphic,
-   involve constraints, mention type or data families, or involve types
-   that are not promotable.
+Here is an example of this in action: ::
 
-.. _promotion-syntax:
+  {-# LANGUAGE TypeInType #-}
+  data Proxy a = P   -- inferred kind: Proxy :: k -> *
+  data Compose f g x = MkCompose (f (g x))
+    -- inferred kind: Compose :: (b -> *) -> (a -> b) -> a -> *
 
-Distinguishing between types and constructors
----------------------------------------------
+  -- separate module having imported the first
+  {-# LANGUAGE NoPolyKinds, DataKinds #-}
+  z = Proxy :: Proxy 'MkCompose
 
-Since constructors and types share the same namespace, with promotion
-you can get ambiguous type names: ::
+In the last line, we use the promoted constructor ``'MkCompose``, which has
+kind ::
+  
+  forall (a :: *) (b :: *) (f :: b -> *) (g :: a -> b) (x :: a).
+    f (g x) -> Compose f g x
 
-    data P          -- 1
+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.
 
-    data Prom = P   -- 2
+Pretty-printing in the presence of kind polymorphism
+----------------------------------------------------
 
-    type T = P      -- 1 or promoted 2?
+With kind polymorphism, there is quite a bit going on behind the scenes that
+may be invisible to a Haskell programmer. GHC supports several flags that
+control how types are printed in error messages and at the GHCi prompt.
+See :ref:`pretty-printing-types` for the details. If you are using
+kind polymorphism and are confused as to why GHC is rejecting (or accepting)
+your program, we encourage you to turn on these flags, especially
+:ghc-flag:`-fprint-explicit-kinds`.
 
-In these cases, if you want to refer to the promoted constructor, you
-should prefix its name with a quote: ::
+.. _runtime-rep:
 
-    type T1 = P     -- 1
+Runtime representation polymorphism
+===================================
 
-    type T2 = 'P    -- promoted 2
+In order to allow full flexibility in how kinds are used, it is necessary
+to use the kind system to differentiate between boxed, lifted types
+(normal, everyday types like ``Int`` and ``[Bool]``) and unboxed, primitive
+types (:ref:`primitives`) like ``Int#``. We thus have so-called representation
+polymorphism.
 
-Note that promoted datatypes give rise to named kinds. Since these can
-never be ambiguous, we do not allow quotes in kind names.
+.. note::
+   For quite some time, this idea was known as *levity* polymorphism, when
+   it differentiated between only lifted and unlifted types. Now that it
+   differentiates between any runtime representations, the name has been
+   changed. But anything you've read or heard about levity polymorphism
+   likely applies to the story told here -- this is just a small generalisation.
+
+Here are the key definitions, all available from ``GHC.Exts``: ::
+
+  TYPE :: RuntimeRep -> *   -- highly magical, built into GHC
+
+  data RuntimeRep = PtrRepLifted     -- for things like `Int`
+                  | PtrRepUnlifted   -- for things like `Array#`
+                 | IntRep           -- for things like `Int#`
+                 | ...
+  
+  type * = TYPE PtrRepLifted    -- * 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``
+and ``Bool :: TYPE 'PtrRepLifted``. Anything with a type of the form
+``TYPE x`` can appear to either side of a function arrow ``->``. We can
+thus say that ``->`` has type
+``TYPE r1 -> TYPE r2 -> TYPE 'PtrRepLifted``. The result is always lifted
+because all functions are lifted in GHC.
+
+No representation-polymorphic variables
+---------------------------------------
 
-Just as in the case of Template Haskell (:ref:`th-syntax`), there is no
-way to quote a data constructor or type constructor whose second
-character is a single quote.
+If GHC didn't have to compile programs that run in the real world, that
+would be the end of the story. But representation polymorphism can cause
+quite a bit of trouble for GHC's code generator. Consider ::
 
-.. _promoted-lists-and-tuples:
+  bad :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
+                (a :: TYPE r1) (b :: TYPE r2).
+         (a -> b) -> a -> b
+  bad f x = f x
 
-Promoted list and tuple types
------------------------------
+This seems like a generalisation of the standard ``$`` operator. If we
+think about compiling this to runnable code, though, problems appear.
+In particular, when we call ``bad``, we must somehow pass ``x`` into
+``bad``. How wide (that is, how many bits) is ``x``? Is it a pointer?
+What kind of register (floating-point or integral) should ``x`` go in?
+It's all impossible to say, because ``x``'s type, ``TYPE r2`` is
+representation polymorphic. We thus forbid such constructions, via the
+following straightforward rule:
 
-With :ghc-flag:`-XDataKinds`, 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: ::
+    No variable may have a representation-polymorphic type.
 
-    data HList :: [*] -> * where
-      HNil  :: HList '[]
-      HCons :: a -> HList t -> HList (a ': t)
+This eliminates ``bad`` because the variable ``x`` would have a
+representation-polymorphic type.
 
-    data Tuple :: (*,*) -> * where
-      Tuple :: a -> b -> Tuple '(a,b)
+However, not all is lost. We can still do this: ::
 
-    foo0 :: HList '[]
-    foo0 = HNil
-
-    foo1 :: HList '[Int]
-    foo1 = HCons (3::Int) HNil
+  ($) :: forall r (a :: *) (b :: TYPE r).
+         (a -> b) -> a -> b
+  f $ x = f x
 
-    foo2 :: HList [Int, Bool]
-    foo2 = ...
+Here, only ``b`` is representation polymorphic. There are no variables
+with a representation polymorphic type. And the code generator has no
+trouble with this. Indeed, this is the true type of GHC's ``$`` operator,
+slightly more general than the Haskell 98 version.
 
-For type-level lists of *two or more elements*, such as the signature of
-``foo2`` above, the quote may be omitted because the meaning is unambiguous. But
-for lists of one or zero elements (as in ``foo0`` and ``foo1``), the quote is
-required, because the types ``[]`` and ``[Int]`` have existing meanings in
-Haskell.
-
-.. note::
-    The declaration for ``HCons`` also requires :ghc-flag:`-XTypeOperators`
-    because of infix type operator ``(:')``
-
-
-.. _promotion-existentials:
-
-Promoting existential data constructors
----------------------------------------
-
-Note that we do promote existential data constructors that are otherwise
-suitable. For example, consider the following: ::
-
-    data Ex :: * where
-      MkEx :: forall a. a -> Ex
-
-Both the type ``Ex`` and the data constructor ``MkEx`` get promoted,
-with the polymorphic kind ``'MkEx :: forall k. k -> Ex``. Somewhat
-surprisingly, you can write a type family to extract the member of a
-type-level existential: ::
+Representation-polymorphic bottoms
+----------------------------------
 
-    type family UnEx (ex :: Ex) :: k
-    type instance UnEx (MkEx x) = x
+We can use representation polymorphism to good effect with ``error``
+and ``undefined``, whose types are given here: ::
 
-At first blush, ``UnEx`` seems poorly-kinded. The return kind ``k`` is
-not mentioned in the arguments, and thus it would seem that an instance
-would have to return a member of ``k`` *for any* ``k``. However, this is
-not the case. The type family ``UnEx`` is a kind-indexed type family.
-The return kind ``k`` is an implicit parameter to ``UnEx``. The
-elaborated definitions are as follows: ::
+  undefined :: forall (r :: RuntimeRep) (a :: TYPE r).
+               HasCallStack => a
+  error :: forall (r :: RuntimeRep) (a :: TYPE r).
+           HasCallStack => String -> a
 
-    type family UnEx (k :: BOX) (ex :: Ex) :: k
-    type instance UnEx k (MkEx k x) = x
+These functions do not bind a representation-polymorphic variable, and
+so are accepted. Their polymorphism allows users to use these to conveniently
+stub out functions that return unboxed types.
 
-Thus, the instance triggers only when the implicit parameter to ``UnEx``
-matches the implicit parameter to ``MkEx``. Because ``k`` is actually a
-parameter to ``UnEx``, the kind is not escaping the existential, and the
-above code is valid.
+Printing representation-polymorphic types
+-----------------------------------------
 
-See also :ghc-ticket:`7347`.
+.. ghc-flag:: -Wprint-explicit-runtime-rep
 
-Promoting type operators
-------------------------
+  Print ``RuntimeRep`` parameters as they appear; otherwise, they are
+  defaulted to ``'PtrRepLifted``.
 
-Type operators are *not* promoted to the kind level. Why not? Because
-``*`` is a kind, parsed the way identifiers are. Thus, if a programmer
-tried to write ``Either * Bool``, would it be ``Either`` applied to
-``*`` and ``Bool``? Or would it be ``*`` applied to ``Either`` and
-``Bool``. To avoid this quagmire, we simply forbid promoting type
-operators to the kind level.
+Most GHC users will not need to worry about representation polymorphism
+or unboxed types. For these users, see the representation polymorphism
+in the type of ``$`` is unhelpful. And thus, by default, it is suppressed,
+by supposing all type variables of type ``RuntimeType`` to be ``'PtrRepLifted``
+when printing, and printing ``TYPE 'PtrRepLifted`` as ``*``.
 
+Should you wish to see representation polymorphism in your types, enable
+the flag :ghc-flag:`-Wprint-explicit-runtime-rep`.
 
 .. _type-level-literals:
 
@@ -7546,6 +7849,31 @@ dependency. In class instances, we define the type instances of FD
 families in accordance with the class head. Method signatures are not
 affected by that process.
 
+Heterogeneous equality
+----------------------
+
+GHC also supports *heterogeneous* equality, which relates two types of potentially
+different kinds. Heterogeneous equality is spelled ``~~``. Here are the
+kinds of ``~`` and ``~~`` to better understand their difference: ::
+
+  (~)  :: forall k. k -> k -> Constraint
+  (~~) :: forall k1 k2. k1 -> k2 -> Constraint
+
+Users will most likely want ``~``, but ``~~`` is available if GHC cannot know,
+a priori, that the two types of interest have the same kind. Evidence that
+``(a :: k1) ~~ (b :: k2)`` tells GHC both that ``k1`` and ``k2`` are the same
+and that ``a`` and ``b`` are the same.
+
+Because ``~`` is the more common equality relation, GHC prints out ``~~`` like
+``~`` unless :ghc-flag:`-fprint-equality-relations` is set.
+
+Unlifted heterogeneous equality
+-------------------------------
+
+Internal to GHC is yet a third equality relation ``(~#)``. It is heterogeneous
+(like ``~~``) and is used only internally. It may appear in error messages
+and other output only when :ghc-flag:`-fprint-equality-relations` is enabled.
+
 .. _coercible:
 
 The ``Coercible`` constraint