implement proposal 106 (Define Kinds Without Promotion) (fixes #6024)

includes corresponding changes to haddock submodule

4 files changed, 68 insertions, 0 deletions

diff --git a/docs/users_guide/9.6.1-notes.rst b/docs/users_guide/9.6.1-notes.rst
index 355fc63838..f66ba9e06a 100644
--- a/docs/users_guide/9.6.1-notes.rst
+++ b/docs/users_guide/9.6.1-notes.rst
@@ -62,6 +62,12 @@ Language
 
 - Error messages are now assigned unique error codes, of the form ``[GHC-12345]``.
 
+- GHC Proposal `#106
+  <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0106-type-data.rst>`_
+  has been implemented, introducing a new language extension
+  :extension:`TypeData`. This extension permits ``type data`` declarations
+  as a more fine-grained alternative to :extension:`DataKinds`.
+
 Compiler
 ~~~~~~~~
 
diff --git a/docs/users_guide/exts/data_kinds.rst b/docs/users_guide/exts/data_kinds.rst
index 50816cbb53..bf99065907 100644
--- a/docs/users_guide/exts/data_kinds.rst
+++ b/docs/users_guide/exts/data_kinds.rst
@@ -15,6 +15,7 @@ system that complements kind polymorphism. It is enabled by
 :extension:`DataKinds`, and described in more detail in the paper `Giving
 Haskell a Promotion <https://dreixel.net/research/pdf/ghp.pdf>`__, which
 appeared at TLDI 2012.
+See also :extension:`TypeData` for a more fine-grained alternative.
 
 Motivation
 ----------
diff --git a/docs/users_guide/exts/type_data.rst b/docs/users_guide/exts/type_data.rst
new file mode 100644
index 0000000000..0779b23273
--- /dev/null
+++ b/docs/users_guide/exts/type_data.rst
@@ -0,0 +1,60 @@
+Type-level data declarations
+============================
+
+.. extension:: TypeData
+    :shortdesc: Enable type data declarations.
+
+    :since: 9.6.1
+
+    Allow ``type data`` declarations, which define constructors at the type level.
+
+This extension facilitates type-level (compile-time) programming by
+allowing a type-level counterpart of ``data`` declarations, such as this
+definition of type-level natural numbers: ::
+
+    type data Nat = Zero | Succ Nat
+
+This is similar to the corresponding ``data`` declaration, except that
+the constructors ``Zero`` and ``Succ`` it introduces belong to the type
+constructor namespace, so they can be used in types, such as the type
+of length-indexed vectors: ::
+
+    data Vec :: Type -> Nat -> Type where
+      Nil  :: Vec a Zero
+      Cons :: a -> Vec a n -> Vec a (Succ n)
+
+:extension:`TypeData` is a more fine-grained alternative to the
+:extension:`DataKinds` extension, which defines *all* the constructors
+in *all* ``data`` declarations as both data constructors and type
+constructors.
+
+A ``type data`` declaration has the same syntax as a ``data`` declaration,
+either an ordinary algebraic data type or a GADT, prefixed with the keyword
+``type``, except that it may not contain
+a datatype context (even with :extension:`DatatypeContexts`),
+labelled fields,
+strictness flags, or
+a ``deriving`` clause.
+
+The only constraints permitted in the types of constructors are
+equality constraints, e.g.: ::
+
+    type data P :: Type -> Type -> Type where
+      MkP :: (a ~ Natural, b ~~ Char) => P a b
+
+Because ``type data`` declarations introduce type constructors, they do
+not permit constructors with the same names as types, so the following
+declaration is invalid: ::
+
+    type data T = T     // Invalid
+
+The compiler will reject this declaration, because the type constructor
+``T`` is defined twice (as the datatype being defined and as a type
+constructor).
+
+The main type constructor of a ``type data`` declaration can be defined
+recursively, as in the ``Nat`` example above, but its constructors may not
+be used in types within the same mutually recursive group of declarations,
+so the following is forbidden: ::
+
+    type data T f = K (f (K Int))  // Invalid
diff --git a/docs/users_guide/exts/types.rst b/docs/users_guide/exts/types.rst
index 23f0c118ab..ea85223184 100644
--- a/docs/users_guide/exts/types.rst
+++ b/docs/users_guide/exts/types.rst
@@ -16,6 +16,7 @@ Types
     gadt
     type_families
     data_kinds
+    type_data
     poly_kinds
     representation_polymorphism
     type_literals