From a64678343d7f977bc87fe6d97c6a89a8c20e1fb8 Mon Sep 17 00:00:00 2001
From: Krzysztof Gogolewski <krzysztof.gogolewski@tweag.io>
Date: Mon, 13 Nov 2023 22:58:12 +0100
Subject: [PATCH] Document defaulting of RuntimeReps
Fixes #24099
---
docs/users_guide/extending_ghc.rst | 1 +
docs/users_guide/exts/data_kinds.rst | 10 +++----
docs/users_guide/exts/linear_types.rst | 5 +++-
docs/users_guide/exts/primitives.rst | 2 +-
.../exts/representation_polymorphism.rst | 29 +++++++++++++++++++
docs/users_guide/using-warnings.rst | 2 +-
6 files changed, 41 insertions(+), 8 deletions(-)
diff --git a/docs/users_guide/extending_ghc.rst b/docs/users_guide/extending_ghc.rst
index 9db7f5ffaae1..d89b51b87ccf 100644
--- a/docs/users_guide/extending_ghc.rst
+++ b/docs/users_guide/extending_ghc.rst
@@ -1383,6 +1383,7 @@ The plugin has type ``WantedConstraints -> [DefaultingProposal]``.
* It is given the currently unsolved constraints.
* It returns a list of independent "defaulting proposals".
* Each proposal of type ``DefaultingProposal`` specifies:
+
* ``deProposals``: specifies a list,
in priority order, of sets of type variable assignments
* ``deProposalCts :: [Ct]`` gives a set of constraints (always a
diff --git a/docs/users_guide/exts/data_kinds.rst b/docs/users_guide/exts/data_kinds.rst
index 49e248a64552..2843819bfecc 100644
--- a/docs/users_guide/exts/data_kinds.rst
+++ b/docs/users_guide/exts/data_kinds.rst
@@ -100,13 +100,13 @@ The following kinds and promoted data constructors can be used even when
:extension:`DataKinds` is not enabled:
- ``Type``
-- ``TYPE`` (see :ref:`_runtime-rep`)
+- ``TYPE`` (see :ref:`runtime-rep`)
- ``Constraint`` (see :ref:`constraint-kind`)
- ``CONSTRAINT``
- ``Multiplicity`` and its promoted data constructors (see :extension:`LinearTypes`)
-- ``LiftedRep`` (see :ref:`_runtime-rep`)
-- ``RuntimeRep`` and its promoted data constructors (see :ref:`_runtime-rep`)
-- ``Levity`` and its promoted data constructors (see :ref:`_runtime-rep`)
+- ``LiftedRep`` (see :ref:`runtime-rep`)
+- ``RuntimeRep`` and its promoted data constructors (see :ref:`runtime-rep`)
+- ``Levity`` and its promoted data constructors (see :ref:`runtime-rep`)
- ``VecCount`` and its promoted data constructors
- ``VecElem`` and its promoted data constructors
@@ -231,7 +231,7 @@ See also :ghc-ticket:`7347`.
:extension:`DataKinds` and type synonyms
----------------------------------------
-The :extensions:`DataKinds` extension interacts with type synonyms in the
+The :extension:`DataKinds` extension interacts with type synonyms in the
following ways:
1. In a *type* context: :extension:`DataKinds` is not required to use a type
diff --git a/docs/users_guide/exts/linear_types.rst b/docs/users_guide/exts/linear_types.rst
index 516caecf7bdb..e08a52e4d198 100644
--- a/docs/users_guide/exts/linear_types.rst
+++ b/docs/users_guide/exts/linear_types.rst
@@ -1,3 +1,5 @@
+.. _linear-types:
+
Linear types
============
@@ -58,7 +60,8 @@ partially. See, however :ref:`linear-types-limitations`.
Linear and multiplicity-polymorphic arrows are *always declared*,
never inferred. That is, if you don't give an appropriate type
signature to a function, it will be inferred as being a regular
-function of type ``a -> b``.
+function of type ``a -> b``. The same principle holds for
+representation polymorphism (see :ref:`representation-polymorphism-defaulting`).
Data types
----------
diff --git a/docs/users_guide/exts/primitives.rst b/docs/users_guide/exts/primitives.rst
index 608ea3406213..b900234c4305 100644
--- a/docs/users_guide/exts/primitives.rst
+++ b/docs/users_guide/exts/primitives.rst
@@ -438,7 +438,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
-`representation-polymorphic binder restriction <#representation-polymorphism-restrictions>`__,
+`representation-polymorphic binder restriction <#representation-polymorphism-restrictions>`__.
Pattern matching against an unlifted data type work just like that for lifted
types; but see :ref:`recursive-and-polymorphic-let-bindings` for the semantics of
diff --git a/docs/users_guide/exts/representation_polymorphism.rst b/docs/users_guide/exts/representation_polymorphism.rst
index 4d461e06fdf6..95304e7b70fc 100644
--- a/docs/users_guide/exts/representation_polymorphism.rst
+++ b/docs/users_guide/exts/representation_polymorphism.rst
@@ -108,6 +108,35 @@ 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.
+.. _representation-polymorphism-defaulting:
+
+Inference and defaulting
+------------------------
+
+GHC does not infer representation-polymorphic types.
+If the representation of a variable is not specified, it will be assumed
+to be ``LiftedRep``.
+For example, if you write ``f a b = a b``, the inferred type of ``f``
+will be ::
+
+ f :: forall {a :: Type} {b :: Type}. (a -> b) -> a -> b
+
+even though ::
+
+ f :: forall {rep} {a :: Type} {b :: TYPE rep}. (a -> b) -> a -> b
+
+would also be legal, as described above.
+
+Likewise, in a user-written signature ``f :: forall a b. (a -> b) -> a -> b``
+GHC will assume that both ``a`` and ``b`` have kind ``Type``. To use
+a different representation, you have to specify the kinds of ``a`` and ``b``.
+
+During type inference, GHC does not quantify over variables of kind
+``RuntimeRep`` nor ``Levity``.
+Instead, they are defaulted to ``LiftedRep`` and ``Lifted`` respectively.
+Likewise, ``Multiplicity`` variables (:ref:`linear-types`) are defaulted
+to ``Many``.
+
.. _printing-representation-polymorphic-types:
Printing representation-polymorphic types
diff --git a/docs/users_guide/using-warnings.rst b/docs/users_guide/using-warnings.rst
index 01e5394817c6..1cd7db470180 100644
--- a/docs/users_guide/using-warnings.rst
+++ b/docs/users_guide/using-warnings.rst
@@ -2574,7 +2574,7 @@ of ``-W(no-)*``.
Introduced in GHC 9.10.1, this warns when an illegal use of a type or kind
(without having enabled the :extension:`DataKinds` extension) is caught in
the typechecker (hence the ``-tc`` suffix). These warnings complement the
- existing :extensions:`DataKinds` checks (that have existed since
+ existing :extension:`DataKinds` checks (that have existed since
:extension:`DataKinds` was first introduced), which result in errors
instead of warnings.
--
GitLab