diff --git a/docs/users_guide/extending_ghc.rst b/docs/users_guide/extending_ghc.rst
index 9db7f5ffaae1d61185d954a5f71c779e7068763f..d89b51b87ccf20e7c951430b4033b1e309c63ca0 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 49e248a64552bae2d3bb4752683851f6cd67e2cb..2843819bfecc04922ed1f07dc9548c83c8f32b1c 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 516caecf7bdbe84e6310fa950c99ec26037587e8..e08a52e4d19848a4ca4a00c8d26011350a44e9eb 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 608ea3406213f3b4a874c578a098af3f8d65c8f0..b900234c4305b996e4fa98598c49af940f626bf0 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 4d461e06fdf6cb3860729adc0e5ee4aacb84187c..95304e7b70fce4ead8371b53e5a0b21e71d34022 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 01e5394817c6da11428021c404b297f24ecd6620..1cd7db47018088e3465ec8d72c740964290068fa 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.