Refine the test for naughty record selectors

The test for naughtiness in record selectors is surprisingly subtle.
See the revised Note [Naughty record selectors] in GHC.Tc.TyCl.Utils.

Fixes #23038.

4 files changed, 77 insertions, 36 deletions

diff --git a/compiler/GHC/Tc/TyCl/Utils.hs b/compiler/GHC/Tc/TyCl/Utils.hs
index 8fb91d9a74..53e58a0e0c 100644
--- a/compiler/GHC/Tc/TyCl/Utils.hs
+++ b/compiler/GHC/Tc/TyCl/Utils.hs
@@ -903,19 +903,30 @@ mkOneRecordSelector all_cons idDetails fl has_sel
     con1 = assert (not (null cons_w_field)) $ head cons_w_field
 
     -- Selector type; Note [Polymorphic selectors]
-    field_ty    = conLikeFieldType con1 lbl
-    data_tv_set = tyCoVarsOfTypes (data_ty : req_theta)
-    data_tvbs   = filter (\tvb -> binderVar tvb `elemVarSet` data_tv_set) $
-                  conLikeUserTyVarBinders con1
+    (univ_tvs, _, _, _, req_theta, _, data_ty) = conLikeFullSig con1
+
+    field_ty     = conLikeFieldType con1 lbl
+    field_ty_tvs = tyCoVarsOfType field_ty
+    data_ty_tvs  = tyCoVarsOfType data_ty
+    sel_tvs      = field_ty_tvs `unionVarSet` data_ty_tvs
+    sel_tvbs     = filter (\tvb -> binderVar tvb `elemVarSet` sel_tvs) $
+                   conLikeUserTyVarBinders con1
 
     -- is_naughty: see Note [Naughty record selectors]
-    is_naughty = not (tyCoVarsOfType field_ty `subVarSet` data_tv_set)
-              || has_sel == NoFieldSelectors  -- No field selectors => all are naughty
-                                              -- thus suppressing making a binding
-                                              -- A slight hack!
+    is_naughty = not ok_scoping || no_selectors
+    ok_scoping = case con1 of
+                   RealDataCon {} -> field_ty_tvs `subVarSet` data_ty_tvs
+                   PatSynCon {}   -> field_ty_tvs `subVarSet` mkVarSet univ_tvs
+       -- In the PatSynCon case, the selector type is (data_ty -> field_ty), but
+       -- fvs(data_ty) are all universals (see Note [Pattern synonym result type] in
+       -- GHC.Core.PatSyn, so no need to check them.
+
+    no_selectors   = has_sel == NoFieldSelectors  -- No field selectors => all are naughty
+                                                  -- thus suppressing making a binding
+                                                  -- A slight hack!
 
     sel_ty | is_naughty = unitTy  -- See Note [Naughty record selectors]
-           | otherwise  = mkForAllTys (tyVarSpecToBinders data_tvbs) $
+           | otherwise  = mkForAllTys (tyVarSpecToBinders sel_tvbs) $
                           -- Urgh! See Note [The stupid context] in GHC.Core.DataCon
                           mkPhiTy (conLikeStupidTheta con1) $
                           -- req_theta is empty for normal DataCon
@@ -926,7 +937,7 @@ mkOneRecordSelector all_cons idDetails fl has_sel
                             -- fields in all the constructor have multiplicity Many.
                           field_ty
 
-    -- Make the binding: sel (C2 { fld = x }) = x
+    -- make the binding: sel (C2 { fld = x }) = x
     --                   sel (C7 { fld = x }) = x
     --    where cons_w_field = [C2,C7]
     sel_bind = mkTopFunBind Generated sel_lname alts
@@ -976,8 +987,6 @@ mkOneRecordSelector all_cons idDetails fl has_sel
       where
         inst_tys = dataConResRepTyArgs dc
 
-    (_, _, _, _, req_theta, _, data_ty) = conLikeFullSig con1
-
     unit_rhs = mkLHsTupleExpr [] noExtField
     msg_lit = HsStringPrim NoSourceText (bytesFS (field_label lbl))
 
@@ -1036,36 +1045,42 @@ so that if the user tries to use 'x' as a selector we can bleat
 helpfully, rather than saying unhelpfully that 'x' is not in scope.
 Hence the sel_naughty flag, to identify record selectors that don't really exist.
 
-In general, a field is "naughty" if its type mentions a type variable that
-isn't in
-  * the (original, user-written) result type of the constructor, or
-  * the "required theta" for the constructor
-
-Note that this *allows* GADT record selectors (Note [GADT record
-selectors]) whose types may look like sel :: T [a] -> a
-
-The "required theta" part is illustrated by test patsyn/should_run/records_run
-where we have
-
-  pattern ReadP :: Read a => a -> String
-  pattern ReadP {readp} <- (read -> readp)
-
-The selector is defined like this:
-
-  $selreadp :: ReadP a => String -> a
-  $selReadP s = readp s
-
-Perfectly fine!  The (ReadP a) constraint lets us contructor a value
-of type 'a' from a bare String.  NB: "required theta" is empty for
-data cons (see conLikeFullSig), so this reasoning only bites for
-patttern synonyms.
-
 For naughty selectors we make a dummy binding
    sel = ()
 so that the later type-check will add them to the environment, and they'll be
 exported.  The function is never called, because the typechecker spots the
 sel_naughty field.
 
+To determine naughtiness we distingish two cases:
+
+* For RealDataCons, a field is "naughty" if its type mentions a
+  type variable that isn't in the (original, user-written) result type
+  of the constructor. Note that this *allows* GADT record selectors
+  (Note [GADT record selectors]) whose types may look like sel :: T [a] -> a
+
+* For a PatSynCon, a field is "naughty" if its type mentions a type variable
+  that isn't in the universal type variables.
+
+  This is a bit subtle. Consider test patsyn/should_run/records_run:
+    pattern ReadP :: forall a. ReadP a => a -> String
+    pattern ReadP {fld} <- (read -> readp)
+  The selector is defined like this:
+    $selReadPfld :: forall a. ReadP a => String -> a
+    $selReadPfld @a (d::ReadP a) s = readp @a d s
+  Perfectly fine!  The (ReadP a) constraint lets us contruct a value of type
+  'a' from a bare String.
+
+  Another curious case (#23038):
+     pattern N :: forall a. () => forall. () => a -> Any
+     pattern N { fld } <- ( unsafeCoerce -> fld1 ) where N = unsafeCoerce
+  The selector looks like this
+     $selNfld :: forall a. Any -> a
+     $selNfld @a x = unsafeCoerce @Any @a x
+  Pretty strange (but used in the `cleff` package).
+
+  TL;DR for pattern synonyms, the selector is OK if the field type mentions only
+  the universal type variables of the pattern synonym.
+
 Note [NoFieldSelectors and naughty record selectors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Under NoFieldSelectors (see Note [NoFieldSelectors] in GHC.Rename.Env), record
diff --git a/testsuite/tests/patsyn/should_compile/T23038.hs b/testsuite/tests/patsyn/should_compile/T23038.hs
new file mode 100644
index 0000000000..b00878642f
--- /dev/null
+++ b/testsuite/tests/patsyn/should_compile/T23038.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE PatternSynonyms, ViewPatterns, ScopedTypeVariables #-}
+
+module T23038 where
+
+import GHC.Types( Any )
+import Unsafe.Coerce( unsafeCoerce )
+
+pattern N1 :: forall a. () => forall. () => a -> Any
+pattern N1 { fld1 } <- ( unsafeCoerce -> fld1 )
+  where N1 = unsafeCoerce
+
+pattern N2 :: forall. () => forall a. () => a -> Any
+pattern N2 { fld2 } <- ( unsafeCoerce -> fld2 )
+  where N2 = unsafeCoerce
+
+test1, test2 :: forall a. Any -> a
+
+test1 = fld1  -- Should be OK
+test2 = fld2  -- Should be rejected
diff --git a/testsuite/tests/patsyn/should_compile/T23038.stderr b/testsuite/tests/patsyn/should_compile/T23038.stderr
new file mode 100644
index 0000000000..b96cec2afa
--- /dev/null
+++ b/testsuite/tests/patsyn/should_compile/T23038.stderr
@@ -0,0 +1,6 @@
+
+T23038.hs:19:9: error: [GHC-55876]
+    • Cannot use record selector ‘fld2’ as a function due to escaped type variables
+    • In the expression: fld2
+      In an equation for ‘test2’: test2 = fld2
+    Suggested fix: Use pattern-matching syntax instead
diff --git a/testsuite/tests/patsyn/should_compile/all.T b/testsuite/tests/patsyn/should_compile/all.T
index 93a0bdb123..3a5b3aef5a 100644
--- a/testsuite/tests/patsyn/should_compile/all.T
+++ b/testsuite/tests/patsyn/should_compile/all.T
@@ -83,3 +83,4 @@ test('T17775-singleton', normal, compile, [''])
 test('T14630', normal, compile, ['-Wname-shadowing'])
 test('T21531', [ grep_errmsg(r'INLINE') ], compile, ['-ddump-ds'])
 test('T22521', normal, compile, [''])
+test('T23038', normal, compile_fail, [''])