Reword: representation instead of levity

fixes #19756, updates haddock submodule

5 files changed, 43 insertions, 27 deletions

diff --git a/docs/users_guide/exts/linear_types.rst b/docs/users_guide/exts/linear_types.rst
index 30c7968854..8029d0ad2f 100644
--- a/docs/users_guide/exts/linear_types.rst
+++ b/docs/users_guide/exts/linear_types.rst
@@ -130,7 +130,7 @@ an error.
 Printing multiplicity-polymorphic types
 ---------------------------------------
 If :extension:`LinearTypes` is disabled, multiplicity variables in types are defaulted
-to ``Many`` when printing, in the same manner as described in :ref:`printing-levity-polymorphic-types`.
+to ``Many`` when printing, in the same manner as described in :ref:`printing-representation-polymorphic-types`.
 In other words, without :extension:`LinearTypes`, multiplicity-polymorphic functions
 ``a %m -> b`` are printed as normal Haskell2010 functions ``a -> b``. This allows
 existing libraries to be generalized to linear types in a backwards-compatible
diff --git a/docs/users_guide/exts/poly_kinds.rst b/docs/users_guide/exts/poly_kinds.rst
index 37068125de..edd1856759 100644
--- a/docs/users_guide/exts/poly_kinds.rst
+++ b/docs/users_guide/exts/poly_kinds.rst
@@ -991,7 +991,7 @@ in GADT-syntax (see :extension:`GADTSyntax`). For example::
 
 There are a number of restrictions around these *return kinds*. The text below
 considers :extension:`UnliftedNewtypes` and data families (enabled by :extension:`TypeFamilies`).
-The discussion also assumes familiarity with :ref:`levity polymorphism <runtime-rep>`.
+The discussion also assumes familiarity with :ref:`representation polymorphism <runtime-rep>`.
 
 1. ``data`` and ``data instance`` declarations must have return kinds that
    end in ``TYPE LiftedRep``. (Recall that ``Type`` is just a synonym for
@@ -1055,5 +1055,6 @@ Examples::
 .. index::
    single: TYPE
    single: levity polymorphism
+   single: representation polymorphism
 
 
diff --git a/docs/users_guide/exts/primitives.rst b/docs/users_guide/exts/primitives.rst
index 80041dd6ad..620b12c24e 100644
--- a/docs/users_guide/exts/primitives.rst
+++ b/docs/users_guide/exts/primitives.rst
@@ -327,8 +327,8 @@ lifted types. In either of the equivalent formulations of ``A`` given above,
 users would additionally have access to a coercion between ``A`` and ``Int#``.
 
 As a consequence of the
-`levity-polymorphic binder restriction <#levity-polymorphic-restrictions>`__,
-levity-polymorphic fields are disallowed in data constructors
+`representation-polymorphic binder restriction <#representation-polymorphism-restrictions>`__,
+representation-polymorphic fields are disallowed in data constructors
 of data types declared using ``data``. However, since ``newtype`` data
 constructor application is implemented as a coercion instead of as function
 application, this restriction does not apply to the field inside a ``newtype``
@@ -422,7 +422,7 @@ You may even declare levity-polymorphic data types: ::
 While ``f`` above could reasonably be levity-polymorphic (as it evaluates its
 argument either way), GHC currently disallows the more general type
 ``PEither @l Int Bool -> Bool``. This is a consequence of the
-`levity-polymorphic binder restriction <#levity-polymorphic-restrictions>`__,
+`representation-polymorphic binder restriction <#representation-polymorphism-restrictions>`__,
 
 Due to `ticket 19487 <https://gitlab.haskell.org/ghc/ghc/-/issues/19487>`, it's
 currently not possible to declare levity-polymorphic data types with nullary
diff --git a/docs/users_guide/exts/levity_polymorphism.rst b/docs/users_guide/exts/representation_polymorphism.rst
index 80a544e54b..3e6d250d27 100644
--- a/docs/users_guide/exts/levity_polymorphism.rst
+++ b/docs/users_guide/exts/representation_polymorphism.rst
@@ -1,12 +1,12 @@
 .. _runtime-rep:
 
-Levity polymorphism
-===================
+Representation polymorphism
+===========================
 
 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 levity
+types (:ref:`primitives`) like ``Int#``. We thus have so-called representation
 polymorphism.
 
 Here are the key definitions, all available from ``GHC.Exts``: ::
@@ -34,10 +34,25 @@ thus say that ``->`` has type
 ``TYPE r1 -> TYPE r2 -> TYPE LiftedRep``. The result is always lifted
 because all functions are lifted in GHC.
 
-.. _levity-polymorphic-restrictions:
+Levity polymorphism
+-------------------
+
+A special case of representation polymorphism is levity polymorphism,
+where we abstract over a variable of kind ``Levity``, such as: ::
+
+  example :: forall (l :: Levity) (a :: TYPE (BoxedRep l)). (Int -> a) -> a
+  example f = f 42
+
+With :extension:`UnliftedDatatypes`, we can even declare levity-polymorphic
+data types: ::
+
+  type PEither :: Type -> Type -> TYPE (BoxedRep l)
+  data PEither l r = PLeft l | PRight r
+
+.. _representation-polymorphism-restrictions:
 
-No levity-polymorphic variables or arguments
---------------------------------------------
+No representation-polymorphic variables or arguments
+----------------------------------------------------
 
 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
@@ -54,10 +69,10 @@ 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, ``a :: TYPE r1`` is
-levity polymorphic. We thus forbid such constructions, via the
+representation-polymorphic. We thus forbid such constructions, via the
 following straightforward rule:
 
-    No variable may have a levity-polymorphic type.
+    No variable may have a representation-polymorphic type.
 
 This eliminates ``bad`` because the variable ``x`` would have a
 representation-polymorphic type.
@@ -68,20 +83,20 @@ However, not all is lost. We can still do this: ::
          (a -> b) -> a -> b
   f $ x = f x
 
-Here, only ``b`` is levity polymorphic. There are no variables
-with a levity-polymorphic type. And the code generator has no
+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.
 
 Because the code generator must store and move arguments as well
 as variables, the logic above applies equally well to function arguments,
-which may not be levity-polymorphic.
+which may not be representation-polymorphic.
 
 
-Levity-polymorphic bottoms
---------------------------
+Representation-polymorphic bottoms
+----------------------------------
 
-We can use levity polymorphism to good effect with ``error``
+We can use representation polymorphism to good effect with ``error``
 and ``undefined``, whose types are given here: ::
 
   undefined :: forall (r :: RuntimeRep) (a :: TYPE r).
@@ -89,14 +104,14 @@ and ``undefined``, whose types are given here: ::
   error :: forall (r :: RuntimeRep) (a :: TYPE r).
            HasCallStack => String -> a
 
-These functions do not bind a levity-polymorphic variable, and
+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.
 
-.. _printing-levity-polymorphic-types:
+.. _printing-representation-polymorphic-types:
 
-Printing levity-polymorphic types
----------------------------------
+Printing representation-polymorphic types
+-----------------------------------------
 
 .. ghc-flag:: -fprint-explicit-runtime-reps
     :shortdesc: Print ``RuntimeRep`` variables in types which are
@@ -108,14 +123,14 @@ Printing levity-polymorphic types
     Print ``RuntimeRep`` parameters as they appear; otherwise, they are
     defaulted to ``LiftedRep``.
 
-Most GHC users will not need to worry about levity polymorphism
-or unboxed types. For these users, seeing the levity polymorphism
+Most GHC users will not need to worry about representation polymorphism
+or unboxed types. For these users, seeing the representation polymorphism
 in the type of ``$`` is unhelpful. And thus, by default, it is suppressed,
 by supposing all type variables of type ``RuntimeRep`` to be ``LiftedRep``
 when printing, and printing ``TYPE LiftedRep`` as ``Type`` (or ``*`` when
 :extension:`StarIsType` is on).
 
-Should you wish to see levity polymorphism in your types, enable
+Should you wish to see representation polymorphism in your types, enable
 the flag :ghc-flag:`-fprint-explicit-runtime-reps`. For example,
 
     .. code-block:: none
diff --git a/docs/users_guide/exts/types.rst b/docs/users_guide/exts/types.rst
index 2cd9d059f5..23f0c118ab 100644
--- a/docs/users_guide/exts/types.rst
+++ b/docs/users_guide/exts/types.rst
@@ -17,7 +17,7 @@ Types
     type_families
     data_kinds
     poly_kinds
-    levity_polymorphism
+    representation_polymorphism
     type_literals
     type_applications
     rank_polymorphism