From e7a8cb145c2450ae12abfb9e30a2b7c1544abf67 Mon Sep 17 00:00:00 2001
From: Richard Eisenberg
Date: Fri, 11 Mar 2016 11:14:04 0500
Subject: [PATCH] Document TypeInType (#11614)
[skip ci]

docs/users_guide/glasgow_exts.rst  870 ++++++++++++++++++++++++++
docs/users_guide/using.rst  4 +
libraries/ghcprim/GHC/Types.hs  6 +
3 files changed, 607 insertions(+), 273 deletions()
diff git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 341a2ee..b42eb80 100644
 a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ 105,6 +105,9 @@ machineaddition 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:`magichash`). For some primitive types we have special syntax for
@@ 113,28 +116,47 @@ literals, also described in the `same section <#magichash>`__.
Primitive values are often represented by a simple bitpattern, such as
``Int#``, ``Float#``, ``Double#``. But this is not necessarily the case:
a primitive value might be represented by a pointer to a heapallocated
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 heapallocated 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 numericallyintensive 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 doubleprecision
+floating point. More details of the ``TYPE`` mechanisms appear in
+the `section on runtime representation polymorphism <#runtimerep>`__.
+
+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.
.. _kindpolymorphism:
+.. _promotion:
Kind polymorphism
=================
+Datatype promotion
+==================
.. ghcflag:: XPolyKinds
+.. ghcflag:: XDataKinds
 :implies: :ghcflag:`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
:ghcflag:`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
+:ghcflag:`XDataKinds`, and described in more detail in the paper `Giving
Haskell a Promotion `__, 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:`typefamilies`) or GADTs
+(:ref:`gadt`), this simple kind system is insufficient, and fails to
+prevent simple errors. Consider the example of typelevel natural
+numbers, and lengthindexed 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 wellkinded type, even though this is not what we
+intend when defining lengthindexed vectors.
+
+With :ghcflag:`XDataKinds`, the example above can then be rewritten to: ::
Currently there is a lot of code duplication in the way ``Typeable`` is
implemented (:ref:`derivingtypeable`): ::
+ 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
+illkinded, and GHC will report an error.
 class Typeable2 (t :: * > * > *) where
 typeOf2 :: t a b > TypeRep
+Overview
+
Kind polymorphism (with :ghcflag:`XPolyKinds`) allows us to merge all these
classes into one: ::
+With :ghcflag:`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 :ghcflag:`XPolyKinds`, GHC will infer a
 polymorphic kind for undecorated 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
 :ghcflag:`fprintexplicitforalls` (see :ref:`optionshelp`): ::
+ Pair :: * > * > *
+ 'Pair :: forall k1 k2. k1 > k2 > Pair k1 k2
 ghci> :set XPolyKinds
 ghci> :set fprintexplicitforalls
 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:`typefamilies`).
 NB: :ghcflag:`XPolyKinds` implies :ghcflag:`XKindSignatures` (see
 :ref:`kinding`).
+ We only promote types whose kinds are of the form
+ ``* > ... > * > *``. In particular, we do not promote
+ higherkinded 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 typevariable
 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 :ghcflag:`XTypeInType` (which implies :ghcflag:`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
 typevariable 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
+.. _promotionsyntax:
 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 errorprone. GHC thus supports
+:ghcflag:`Wuntickedpromotedconstructors` 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:`thsyntax`), 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'`
+
+.. _promotedlistsandtuples:
+
+Promoted list and tuple types
+
+
+With :ghcflag:`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 typelevel 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 :ghcflag:`XTypeOperators`
+ because of infix type operator ``(:')``
+
+
+.. _promotionexistentials:
+
+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
+typelevel existential: ::
+
+ type family UnEx (ex :: Ex) :: k
+ type instance UnEx (MkEx x) = x
+
+At first blush, ``UnEx`` seems poorlykinded. 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 kindindexed 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 :ghcticket:`7347`.
+
+.. _typeintype:
+.. _kindpolymorphism:
+
+Kind polymorphism and TypeinType
+==================================
+
+.. ghcflag: XTypeInType
+
+ :implies: :ghcflag:`XPolyKinds`, :ghcflag:`XDataKinds`, :ghcflag:`XKindSignatures`
+ :since: 8.0.1
+
+ Allow kinds to be as intricate as types.
+
+.. ghcflag:: XPolyKinds
+
+ :implies: :ghcflag:`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 :ghcflag:`XTypeInType` and :ghcflag:`XPolyKinds`
+
+
+It is natural to consider :ghcflag:`XTypeInType` as an extension of
+:ghcflag:`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: :ghcflag:`XPolyKinds` was introduced for GHC 7.4,
+when it was experimental and temperamental. The wrinkles were smoothed out for
+GHC 7.6. :ghcflag:`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
+:ghcflag:`XPolyKinds` to work properly while being duly sceptical of
+:ghcflag:`XTypeInType`. In particular, we recommend enabling
+:ghcflag:`dcorelint` whenever using :ghcflag:`XTypeInType`; that flag
+turns on a set of internal checks within GHC that will discover bugs in the
+implementation of :ghcflag:`XTypeInType`. Please report bugs at `our bug
+tracker `__.
+
+Although we have tried to allow the new behavior only when
+:ghcflag:`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 :ghcflag:`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
+newlyavailable 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
+(:ghcflag:`XKindSignatures`), it is necessary to use a dummy constructor
+to get a Haskell compiler to infer the second kind. With kind polymorphism
+(:ghcflag:`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 TypeinType
+
+
+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
+nontermination, but this is not a problem in GHC, as we already have other
+means of nonterminating 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 `__
+introducing this kind system to GHC/Haskell.
Principles of kind inference

Generally speaking, when :ghcflag:`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 righthand side to inform kind
inference. But that is not always the case. Consider ::
@@ 6990,10 +7210,10 @@ GHC defaults those entirelyunconstrained kind variables to ``*`` and we
get ``F :: * > *``. You can still declare ``F`` to be kindpolymorphic
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 occasionallysurprising consequences (see
:ghcticket:`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 usersupplied 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
 userspecified kind signature; unannotated type variables default to
+ An open type or data family declaration *always* has a CUSK;
+ unannotated 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 toplevel ``::``)
is supplied.
+With :ghcflag:`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
userspecified kind signature, we can relax this condition for closed
+usersupplied 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 *kindindexed* type families, where the family matches both
on the kind and type. GHC will *not* infer this behaviour without a
complete usersupplied kind signature, as doing so would sometimes infer
nonprincipal types.
+nonprincipal types. Indeed, we can see kindindexing 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 kindchecking a type, GHC considers only what is written in that
+type when figuring out how to generalise the type's kind.
.. ghcflag:: XDataKinds
+For example,
+consider these definitions (with :ghcflag:`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
:ghcflag:`XDataKinds`, and described in more detail in the paper `Giving
Haskell a Promotion `__, which
appeared at TLDI 2012.
+Explicit kind quantification
+
Motivation

+Enabled by :ghcflag:`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 wellscoped: ``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 higherrank 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 nontoplevel ``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 higherrank ``forall``, include it explicitly.
+
+Kindindexed 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:`glasgowunboxed`). In particular when using advanced type
system features, such as type families (:ref:`typefamilies`) or GADTs
(:ref:`gadt`), this simple kind system is insufficient, and fails to
prevent simple errors. Consider the example of typelevel natural
numbers, and lengthindexed 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 GADTlike 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 :ghcflag:`XTypeInType`
+be in effect, but patternmatching on ``G`` requires no extension beyond
+:ghcflag:`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 wellkinded type, even though this is not what we
intend when defining lengthindexed vectors.
+Note that the datatype ``G`` is used at different kinds in its body, and
+therefore that kindindexed GADTs use a form of polymorphic recursion.
+It is thus only possible to use this feature if you have provided a
+complete usersupplied kind signature
+for the datatype (:ref:`completekindsignatures`).
With :ghcflag:`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 :ghcflag:`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
illkinded, 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 :ghcflag:`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 :ghcflag:`XTypeInType`,
+this identifier is always in scope when writing a kind. However, with
+:ghcflag:`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 :ghcflag:`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 :ghcflag:`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 parsedand the fact that it is the only such
+operator in GHCthere are some corner cases that are
+not handled. We are aware of two:
 data Sum a b = L a  R b
+ In a Haskell98style 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 termlevel ``(*)``. (:ref:`explicitnamespaces`)
 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:`typefamilies`).
+Kind defaulting without :ghcflag:`XPolyKinds`
+
 We only promote types whose kinds are of the form
 ``* > ... > * > *``. In particular, we do not promote
 higherkinded datatypes such as ``data Fix f = In (f (Fix f))``, or
 datatypes whose kinds involve promoted types such as
 ``Vec :: * > Nat > *``.
+Without :ghcflag:`XPolyKinds` or :ghcflag:`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: ::
.. _promotionsyntax:
+ {# 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 illkinded
+if defaulted. The definition for ``z`` is thus an error.
 data Prom = P  2
+Prettyprinting 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:`prettyprintingtypes` 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
+:ghcflag:`fprintexplicitkinds`.
In these cases, if you want to refer to the promoted constructor, you
should prefix its name with a quote: ::
+.. _runtimerep:
 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 socalled 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 representationpolymorphic variables
+
Just as in the case of Template Haskell (:ref:`thsyntax`), 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 ::
.. _promotedlistsandtuples:
+ 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 (floatingpoint 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 :ghcflag:`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 representationpolymorphic type.
 data HList :: [*] > * where
 HNil :: HList '[]
 HCons :: a > HList t > HList (a ': t)
+This eliminates ``bad`` because the variable ``x`` would have a
+representationpolymorphic 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 typelevel 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 :ghcflag:`XTypeOperators`
 because of infix type operator ``(:')``


.. _promotionexistentials:

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
typelevel existential: ::
+Representationpolymorphic 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 poorlykinded. 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 kindindexed 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 representationpolymorphic 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 representationpolymorphic types
+
See also :ghcticket:`7347`.
+.. ghcflag:: Wprintexplicitruntimerep
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 :ghcflag:`Wprintexplicitruntimerep`.
.. _typelevelliterals:
@@ 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 :ghcflag:`fprintequalityrelations` 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 :ghcflag:`fprintequalityrelations` is enabled.
+
.. _coercible:
The ``Coercible`` constraint
diff git a/docs/users_guide/using.rst b/docs/users_guide/using.rst
index 96bd0a1..ba0e223 100644
 a/docs/users_guide/using.rst
+++ b/docs/users_guide/using.rst
@@ 630,6 +630,8 @@ messages and in GHCi:
ghci> :t (>>)
(>>) :: â (m :: * â *) a b. Monad m â m a â m b â m b
+.. _prettyprintingtypes:
+
.. ghcflag:: fprintexplicitforalls
Using :ghcflag:`fprintexplicitforalls` makes
@@ 699,7 +701,7 @@ messages and in GHCi:
the internal equality relation used in GHC's solver. Generally,
users should not need to worry about the subtleties here; ``~`` is
probably what you want. Without :ghcflag:`fprintequalityrelations`, GHC
 prints all of these as ``~``.
+ prints all of these as ``~``. See also :ref:`equalityconstraints`.
.. ghcflag:: fprintexpandedsynonyms
diff git a/libraries/ghcprim/GHC/Types.hs b/libraries/ghcprim/GHC/Types.hs
index 6f9e09f..736ea3d 100644
 a/libraries/ghcprim/GHC/Types.hs
+++ b/libraries/ghcprim/GHC/Types.hs
@@ 193,7 +193,11 @@ inside GHC, to change the kind and type.
  Lifted, heterogeneous equality. By lifted, we mean that it
 can be bogus (deferred type error). By heterogeneous, the two
 types @a@ and @b@ might have different kinds.
+ types @a@ and @b@ might have different kinds. Because @~~@ can
+ appear unexpectedly in error messages to users who do not care
+ about the difference between heterogeneous equality @~~@ and
+ homogeneous equality @~@, this is printed as @~@ unless
+ @fprintequalityrelations@ is set.
class a ~~ b
 See also Note [The equality types story] in TysPrim

1.9.1