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.

4 files changed, 100 insertions, 21 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
diff --git a/compiler/GHC/HsToCore/Expr.hs b/compiler/GHC/HsToCore/Expr.hs
index a1727659af..947780bfc3 100644
--- a/compiler/GHC/HsToCore/Expr.hs
+++ b/compiler/GHC/HsToCore/Expr.hs
@@ -641,11 +641,7 @@ dsExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = fields
     mk_alt upd_fld_env con
       = do { let (univ_tvs, ex_tvs, eq_spec,
                   prov_theta, _req_theta, arg_tys, _) = conLikeFullSig con
-                 user_tvs =
-                   case con of
-                     RealDataCon data_con -> dataConUserTyVars data_con
-                     PatSynCon _          -> univ_tvs ++ ex_tvs
-                       -- The order here is because of the order in `GHC.Tc.TyCl.PatSyn`.
+                 user_tvs  = binderVars $ conLikeUserTyVarBinders con
                  in_subst  = zipTvSubst univ_tvs in_inst_tys
                  out_subst = zipTvSubst univ_tvs out_inst_tys
 
diff --git a/compiler/GHC/Tc/TyCl/Utils.hs b/compiler/GHC/Tc/TyCl/Utils.hs
index 80157caa0d..3101a96ac5 100644
--- a/compiler/GHC/Tc/TyCl/Utils.hs
+++ b/compiler/GHC/Tc/TyCl/Utils.hs
@@ -872,19 +872,17 @@ mkOneRecordSelector all_cons idDetails fl
 
     -- Selector type; Note [Polymorphic selectors]
     field_ty   = conLikeFieldType con1 lbl
-    data_tvs   = tyCoVarsOfTypesWellScoped inst_tys
-    data_tv_set= mkVarSet data_tvs
+    data_tvbs  = filter (\tvb -> binderVar tvb `elemVarSet` data_tv_set) $
+                 conLikeUserTyVarBinders con1
+    data_tv_set= tyCoVarsOfTypes inst_tys
     is_naughty = not (tyCoVarsOfType field_ty `subVarSet` data_tv_set)
-    (field_tvs, field_theta, field_tau) = tcSplitSigmaTy field_ty
     sel_ty | is_naughty = unitTy  -- See Note [Naughty record selectors]
-           | otherwise  = mkSpecForAllTys data_tvs          $
+           | otherwise  = mkForAllTys data_tvbs             $
                           mkPhiTy (conLikeStupidTheta con1) $   -- Urgh!
-                          mkVisFunTy data_ty                $
-                          mkSpecForAllTys field_tvs         $
-                          mkPhiTy field_theta               $
                           -- req_theta is empty for normal DataCon
                           mkPhiTy req_theta                 $
-                          field_tau
+                          mkVisFunTy data_ty                $
+                          field_ty
 
     -- Make the binding: sel (C2 { fld = x }) = x
     --                   sel (C7 { fld = x }) = x
@@ -936,6 +934,16 @@ mkOneRecordSelector all_cons idDetails fl
     (univ_tvs, _, eq_spec, _, req_theta, _, data_ty) = conLikeFullSig con1
 
     eq_subst = mkTvSubstPrs (map eqSpecPair eq_spec)
+    -- inst_tys corresponds to one of the following:
+    --
+    -- * The arguments to the user-written return type (for GADT constructors).
+    --   In this scenario, eq_subst provides a mapping from the universally
+    --   quantified type variables to the argument types. Note that eq_subst
+    --   does not need to be applied to any other part of the DataCon
+    --   (see Note [The dcEqSpec domain invariant] in GHC.Core.DataCon).
+    -- * The universally quantified type variables
+    --   (for Haskell98-style constructors and pattern synonyms). In these
+    --   scenarios, eq_subst is an empty substitution.
     inst_tys = substTyVars eq_subst univ_tvs
 
     unit_rhs = mkLHsTupleExpr []
@@ -945,13 +953,44 @@ mkOneRecordSelector all_cons idDetails fl
 Note [Polymorphic selectors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We take care to build the type of a polymorphic selector in the right
-order, so that visible type application works.
-
-  data Ord a => T a = MkT { field :: forall b. (Num a, Show b) => (a, b) }
-
-We want
-
-  field :: forall a. Ord a => T a -> forall b. (Num a, Show b) => (a, b)
+order, so that visible type application works according to the specification in
+the GHC User's Guide (see the "Field selectors and TypeApplications" section).
+We won't bother rehashing the entire specification in this Note, but the tricky
+part is dealing with GADT constructor fields. Here is an appropriately tricky
+example to illustrate the challenges:
+
+  {-# LANGUAGE PolyKinds #-}
+  data T a b where
+    MkT :: forall b a x.
+           { field1 :: forall c. (Num a, Show c) => (Either a c, Proxy b)
+           , field2 :: x
+           }
+        -> T a b
+
+Our goal is to obtain the following type for `field1`:
+
+  field1 :: forall {k} (b :: k) a.
+            T a b -> forall c. (Num a, Show c) => (Either a c, Proxy b)
+
+(`field2` is naughty, per Note [Naughty record selectors], so we cannot turn
+it into a top-level field selector.)
+
+Some potential gotchas, inspired by #18023:
+
+1. Since the user wrote `forall b a x.` in the type of `MkT`, we want the `b`
+   to appear before the `a` when quantified in the type of `field1`.
+2. On the other hand, we *don't* want to quantify `x` in the type of `field1`.
+   This is because `x` does not appear in the GADT return type, so it is not
+   needed in the selector type.
+3. Because of PolyKinds, the kind of `b` is generalized to `k`. Moreover, since
+   this `k` is not written in the source code, it is inferred (i.e., not
+   available for explicit type applications) and thus written as {k} in the type
+   of `field1`.
+
+In order to address these gotchas, we start by looking at the
+conLikeUserTyVarBinders, which gives the order and specificity of each binder.
+This effectively solves (1) and (3). To solve (2), we filter the binders to
+leave only those that are needed for the selector type.
 
 Note [Naughty record selectors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~