Use conLikeUserTyVarBinders to quantify field selector types

This patch:

1. Writes up a specification for how the types of top-level field
   selectors should be determined in a new section of the GHC User's
   Guide, and
2. Makes GHC actually implement that specification by using
   `conLikeUserTyVarBinders` in `mkOneRecordSelector` to preserve the
   order and specificity of type variables written by the user.

Fixes #18023.

6 files changed, 162 insertions, 2 deletions

diff --git a/docs/users_guide/8.12.1-notes.rst b/docs/users_guide/8.12.1-notes.rst
index 75adb1fb41..4d151d0ab1 100644
--- a/docs/users_guide/8.12.1-notes.rst
+++ b/docs/users_guide/8.12.1-notes.rst
@@ -18,6 +18,34 @@ Full details
 Language
 ~~~~~~~~
 
+* Record field selectors are now given type signatures that preserve the
+  user-written order of quantified type variables. Moreover, field selector
+  type signatures no longer make inferred type variables avaiable for explicit
+  type application. See :ref:`field-selectors-and-type-applications` for more
+  details.
+
+  In certain situations, this will constitute a breaking change as this can
+  affect :extension:`TypeApplications`. For instance, given the following
+  definitions: ::
+
+    {-# LANGUAGE PolyKinds #-}
+
+    newtype P a = MkP { unP :: Proxy a }
+
+    newtype N :: Type -> Type -> Type where
+      MkN :: forall b a. { unN :: Either a b } -> N a b
+
+  Previous versions of GHC would give the following types to ``unP`` and
+  ``unN``: ::
+
+    unP :: forall k (a :: k). P a -> Proxy a
+    unN :: forall a b. N a b -> Either a b
+
+  GHC will now give them the following types instead: ::
+
+    unP :: forall {k} (a :: k). P a -> Proxy a
+    unN :: forall b a. N a b -> Either a b
+
 * In obscure scenarios, GHC now rejects programs it previously accepted, but
   with unhelpful types. For example, if (with ``-XPartialTypeSignatures``) you
   were to write ``x :: forall (f :: forall a (b :: a -> Type). b _). f _``, GHC previously
@@ -40,7 +68,7 @@ Language
 
   There is a chance we will tweak the lookup scheme in the future, to make this
   workaround unnecessary.
-  
+
 Compiler
 ~~~~~~~~
 
diff --git a/docs/users_guide/exts/existential_quantification.rst b/docs/users_guide/exts/existential_quantification.rst
index e4c5a79149..c9cde919dd 100644
--- a/docs/users_guide/exts/existential_quantification.rst
+++ b/docs/users_guide/exts/existential_quantification.rst
@@ -116,7 +116,11 @@ example: ::
         }
 
 Here ``tag`` is a public field, with a well-typed selector function
-``tag :: Counter a -> a``. The ``self`` type is hidden from the outside;
+``tag :: Counter a -> a``. See :ref:`field-selectors-and-type-applications`
+for a full description of how the types of top-level field selectors are
+determined.
+
+The ``self`` type is hidden from the outside;
 any attempt to apply ``_this``, ``_inc`` or ``_display`` as functions
 will raise a compile-time error. In other words, *GHC defines a record
 selector function only for fields whose type does not mention the
diff --git a/docs/users_guide/exts/field_selectors_and_type_applications.rst b/docs/users_guide/exts/field_selectors_and_type_applications.rst
new file mode 100644
index 0000000000..c01e6ee519
--- /dev/null
+++ b/docs/users_guide/exts/field_selectors_and_type_applications.rst
@@ -0,0 +1,122 @@
+.. _field-selectors-and-type-applications:
+
+Field selectors and ``TypeApplications``
+----------------------------------------
+
+Field selectors can be used in conjunction with :extension:`TypeApplications`,
+as described in :ref:`visible-type-application`. The type of a field selector
+is constructed by using the surrounding definition as context. This section
+provides a specification for how this construction works. We will explain it
+by considering three different forms of field selector, each of which is a
+minor variation of the same general theme.
+
+Field selectors for Haskell98-style data constructors
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Consider the following example: ::
+
+  data T a b = MkT { unT :: forall e. Either e a }
+
+This data type uses a Haskell98-style declaration. The only part of this data
+type that is not Haskell98 code is ``unT``, whose type uses higher-rank
+polymorphism (:ref:`arbitrary-rank-polymorphism`). To construct the type of
+the ``unT`` field selector, we will assemble the following:
+
+1. The type variables quantified by the data type head
+   (``forall a b. <...>``).
+2. The return type of the data constructor
+   (``<...> T a b -> <...>``). By virtue of this being a Haskell98-style
+   declaration, the order of type variables in the return type will always
+   coincide with the order in which they are quantified.
+3. The type of the field
+   (``<...> forall e. Either e a``).
+
+The final type of ``unT`` is therefore
+``forall a b. T a b -> forall e. Either e a``. As a result, one way to use
+``unT`` with :extension:`TypeApplications` is
+``unT @Int @Bool (MkT (Right 1)) @Char``.
+
+Field selectors for GADT constructors
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Field selectors for GADT constructors (:ref:`gadt-style`) are slightly more
+involved. Consider the following example: ::
+
+  data G a b where
+    MkG :: forall x n a. (Eq a, Show n)
+        => { unG1 :: forall e. Either e (a, x), unG2 :: n } -> G a (Maybe x)
+
+The ``MkG`` GADT constructor has two records, ``unG1`` and ``unG2``.
+However, only ``unG1`` can be used as a top-level field selector. ``unG2``
+cannot because it is a "hidden" selector (see :ref:`existential-records`); its
+type mentions a free variable ``n`` that does not appear in the result type
+``G a (Maybe x)``. On the other hand, the only free type variables in the type
+of ``unG1`` are ``a`` and ``x``, so ``unG1`` is fine to use as a top-level
+function.
+
+To construct the type of the ``unG1`` field selector, we will assemble
+the following:
+
+1. The subset of type variables quantified by the GADT constructor that are
+   mentioned in the return type. Note that the order of these variables follows
+   the same principles as in :ref:`ScopedSort`.
+   If the constructor explicitly quantifies its type variables at the beginning
+   of the type, then the field selector type will quantify them in the same
+   order (modulo any variables that are dropped due to not being mentioned in
+   the return type).
+   If the constructor implicitly quantifies its type variables, then the field
+   selector type will quantify them in the left-to-right order that they appear
+   in the field itself.
+
+   In this example, ``MkG`` explicitly quantifies ``forall x n a.``, and of
+   those type variables, ``a`` and ``x`` are mentioned in the return type.
+   Therefore, the type of ``unG1`` starts as ``forall x a. <...>``.
+   If ``MkG`` had not used an explicit ``forall``, then they would have instead
+   been ordered as ``forall a x. <...>``, since ``a`` appears to the left of
+   ``x`` in the field type.
+2. The GADT return type
+   (``<...> G a (Maybe x) -> ...``).
+3. The type of the field
+   (``<...> -> forall e. Either e (a, x)``).
+
+The final type of ``unG1`` is therefore
+``forall x a. G a (Maybe x) -> forall e. Either e (a, x)``. As a result, one
+way to use ``unG1`` with :extension:`TypeApplications` is
+``unG1 @Int @Bool (MkG (Right (True, 42)) ()) @Char``.
+
+Field selectors for pattern synonyms
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Certain record pattern synonyms (:ref:`record-patsyn`) can give rise to
+top-level field selectors. Consider the following example: ::
+
+  pattern P :: forall a. Read a
+            => forall n. (Eq a, Show n)
+            => (forall e. Either e (a, Bool)) -> n -> G a (Maybe Bool)
+  pattern P {unP1, unP2} = MkG unP1 unP2
+
+We can only make field selectors for pattern synonym records that do not
+mention any existential type variables whatsoever in their types, per
+:ref:`record-patsyn`. (This is a stronger requirement than for GADT records,
+whose types can mention existential type variables provided that they are also
+mentioned in the return type.) We can see that ``unP2`` cannot be used as a
+top-level field selector since its type has a free type variable ``n``, which
+is existential. ``unP1`` is fine, on the other hand, as its type only has one
+free variable, the universal type variable ``a``.
+
+To construct the type of the ``unP1`` field selector, we will assemble
+the following:
+
+1. The universal type variables
+   (``forall a. <...>``).
+2. The required constraints
+   (``<...> Read a => <...>``).
+3. The pattern synonym return type
+   (``<...> G a (Maybe Bool) -> <...>``).
+4. The type of the field
+   (``<...> -> forall e. Either e (a, Bool)``).
+
+The final type of ``unP1`` is therefore
+``forall a. Read a => G a (Maybe Bool) -> forall e. Either e (a, Bool)``. As a
+result, one way to use ``unP1`` with :extension:`TypeApplications` is
+``unP1 @Double (MkG (Right (4.5, True)) ()) @Char``.
diff --git a/docs/users_guide/exts/gadt.rst b/docs/users_guide/exts/gadt.rst
index c8f0e750bd..388a055d28 100644
--- a/docs/users_guide/exts/gadt.rst
+++ b/docs/users_guide/exts/gadt.rst
@@ -118,6 +118,9 @@ also sets :extension:`GADTSyntax` and :extension:`MonoLocalBinds`.
          num :: Term Int -> Term Int
          arg :: Term Bool -> Term Int
 
+   See :ref:`field-selectors-and-type-applications` for a full description of
+   how the types of top-level field selectors are determined.
+
 -  When pattern-matching against data constructors drawn from a GADT,
    for example in a ``case`` expression, the following rules apply:
 
diff --git a/docs/users_guide/exts/rank_polymorphism.rst b/docs/users_guide/exts/rank_polymorphism.rst
index 3b33b01d7e..32447228c7 100644
--- a/docs/users_guide/exts/rank_polymorphism.rst
+++ b/docs/users_guide/exts/rank_polymorphism.rst
@@ -1,3 +1,5 @@
+.. _arbitrary-rank-polymorphism:
+
 Arbitrary-rank polymorphism
 ===========================
 
diff --git a/docs/users_guide/exts/records.rst b/docs/users_guide/exts/records.rst
index 66c1b90c76..28f8988220 100644
--- a/docs/users_guide/exts/records.rst
+++ b/docs/users_guide/exts/records.rst
@@ -7,6 +7,7 @@ Records
     :maxdepth: 1
 
     traditional_record_syntax
+    field_selectors_and_type_applications
     disambiguate_record_fields
     duplicate_record_fields
     record_puns