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.

2 files changed, 45 insertions, 1 deletions

diff --git a/compiler/GHC/Core/ConLike.hs b/compiler/GHC/Core/ConLike.hs
index 0d538af40a..e6169f7d7c 100644
--- a/compiler/GHC/Core/ConLike.hs
+++ b/compiler/GHC/Core/ConLike.hs
@@ -12,6 +12,7 @@ module GHC.Core.ConLike (
         , conLikeArity
         , conLikeFieldLabels
         , conLikeInstOrigArgTys
+        , conLikeUserTyVarBinders
         , conLikeExTyCoVars
         , conLikeName
         , conLikeStupidTheta
@@ -113,6 +114,18 @@ conLikeInstOrigArgTys (RealDataCon data_con) tys =
 conLikeInstOrigArgTys (PatSynCon pat_syn) tys =
     patSynInstArgTys pat_syn tys
 
+-- | 'TyVarBinder's for the type variables of the 'ConLike'. For pattern
+-- synonyms, this will always consist of the universally quantified variables
+-- followed by the existentially quantified type variables. For data
+-- constructors, the situation is slightly more complicated—see
+-- @Note [DataCon user type variable binders]@ in "GHC.Core.DataCon".
+conLikeUserTyVarBinders :: ConLike -> [TyVarBinder]
+conLikeUserTyVarBinders (RealDataCon data_con) =
+    dataConUserTyVarBinders data_con
+conLikeUserTyVarBinders (PatSynCon pat_syn) =
+    patSynUnivTyVarBinders pat_syn ++ patSynExTyVarBinders pat_syn
+    -- The order here is because of the order in `GHC.Tc.TyCl.PatSyn`.
+
 -- | Existentially quantified type/coercion variables
 conLikeExTyCoVars :: ConLike -> [TyCoVar]
 conLikeExTyCoVars (RealDataCon dcon1) = dataConExTyCoVars dcon1
diff --git a/compiler/GHC/Core/DataCon.hs b/compiler/GHC/Core/DataCon.hs
index c4563202a9..7d767a2416 100644
--- a/compiler/GHC/Core/DataCon.hs
+++ b/compiler/GHC/Core/DataCon.hs
@@ -384,7 +384,9 @@ data DataCon
                 --      MkT :: forall a b. (a ~ [b]) => b -> T a
                 --      MkT :: forall b. b -> T [b]
                 -- Each equality is of the form (a ~ ty), where 'a' is one of
-                -- the universally quantified type variables
+                -- the universally quantified type variables. Moreover, the
+                -- only place in the DataCon where this 'a' will occur is in
+                -- dcUnivTyVars. See [The dcEqSpec domain invariant].
 
                 -- The next two fields give the type context of the data constructor
                 --      (aside from the GADT constraints,
@@ -595,6 +597,35 @@ dcUserTyVarBinders, as the name suggests, is the one that users will see most of
 the time. It's used when computing the type signature of a data constructor (see
 dataConUserType), and as a result, it's what matters from a TypeApplications
 perspective.
+
+Note [The dcEqSpec domain invariant]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this example of a GADT constructor:
+
+  data Y a where
+    MkY :: Bool -> Y Bool
+
+The user-written type of MkY is `Bool -> Y Bool`, but what is the underlying
+Core type for MkY? There are two conceivable possibilities:
+
+1. MkY :: forall a. (a ~# Bool) => Bool -> Y a
+2. MkY :: forall a. (a ~# Bool) => a    -> Y a
+
+In practice, GHC picks (1) as the Core type for MkY. This is because we
+maintain an invariant that the type variables in the domain of dcEqSpec will
+only ever appear in the dcUnivTyVars. As a consequence, the type variables in
+the domain of dcEqSpec will /never/ appear in the dcExTyCoVars, dcOtherTheta,
+dcOrigArgTys, or dcOrigResTy; these can only ever mention variables from
+dcUserTyVarBinders, which excludes things in the domain of dcEqSpec.
+(See Note [DataCon user type variable binders].) This explains why GHC would
+not pick (2) as the Core type, since the argument type `a` mentions a type
+variable in the dcEqSpec.
+
+There are certain parts of the codebase where it is convenient to apply the
+substitution arising from the dcEqSpec to the dcUnivTyVars in order to obtain
+the user-written return type of a GADT constructor. A consequence of the
+dcEqSpec domain invariant is that you /never/ need to apply the substitution
+to any other part of the constructor type, as they don't require it.
 -}
 
 -- | Data Constructor Representation