Don't promote/single field selectors with NoFieldSelectors

singletons-base/tests/SingletonsBaseTestSuite.hs

@@ -149,6 +149,7 @@ tests =
     , compileAndDumpStdTest "T536"
     , compileAndDumpStdTest "T555"
     , compileAndDumpStdTest "T559"
+    , compileAndDumpStdTest "T563"
     , compileAndDumpStdTest "T567"
     , compileAndDumpStdTest "T571"
     , compileAndDumpStdTest "TypeAbstractions"

singletons-base/tests/compile-and-dump/Singletons/T563.golden

@@ -0,0 +1,71 @@
+Singletons/T563.hs:(0,0)-(0,0): Splicing declarations
+    singletons
+      [d| infixr 6 `unFoo`
+
+          data Foo = MkFoo {unFoo :: Bool} |]
+  ======>
+    infixr 6 `unFoo`
+    data Foo = MkFoo {unFoo :: Bool}
+    type MkFooSym0 :: (~>) Bool Foo
+    data MkFooSym0 :: (~>) Bool Foo
+      where
+        MkFooSym0KindInference :: SameKind (Apply MkFooSym0 arg) (MkFooSym1 arg) =>
+                                  MkFooSym0 a0123456789876543210
+    type instance Apply MkFooSym0 a0123456789876543210 = MkFoo a0123456789876543210
+    instance SuppressUnusedWarnings MkFooSym0 where
+      suppressUnusedWarnings = snd ((,) MkFooSym0KindInference ())
+    type MkFooSym1 :: Bool -> Foo
+    type family MkFooSym1 (a0123456789876543210 :: Bool) :: Foo where
+      MkFooSym1 a0123456789876543210 = MkFoo a0123456789876543210
+    data SFoo :: Foo -> Type
+      where
+        SMkFoo :: forall (n :: Bool). (Sing n) -> SFoo (MkFoo n :: Foo)
+    type instance Sing @Foo = SFoo
+    instance SingKind Foo where
+      type Demote Foo = Foo
+      fromSing (SMkFoo b) = MkFoo (fromSing b)
+      toSing (MkFoo (b :: Demote Bool))
+        = case toSing b :: SomeSing Bool of
+            SomeSing c -> SomeSing (SMkFoo c)
+    instance SingI n => SingI (MkFoo (n :: Bool)) where
+      sing = SMkFoo sing
+    instance SingI1 MkFoo where
+      liftSing = SMkFoo
+    instance SingI (MkFooSym0 :: (~>) Bool Foo) where
+      sing = singFun1 @MkFooSym0 SMkFoo
+Singletons/T563.hs:(0,0)-(0,0): Splicing declarations
+    singletonsOnly
+      [d| unFoo' :: Foo -> Bool
+          unFoo' = unFoo |]
+  ======>
+    type UnFoo'Sym0 :: (~>) Foo Bool
+    data UnFoo'Sym0 :: (~>) Foo Bool
+      where
+        UnFoo'Sym0KindInference :: SameKind (Apply UnFoo'Sym0 arg) (UnFoo'Sym1 arg) =>
+                                   UnFoo'Sym0 a0123456789876543210
+    type instance Apply UnFoo'Sym0 a0123456789876543210 = UnFoo' a0123456789876543210
+    instance SuppressUnusedWarnings UnFoo'Sym0 where
+      suppressUnusedWarnings = snd ((,) UnFoo'Sym0KindInference ())
+    type UnFoo'Sym1 :: Foo -> Bool
+    type family UnFoo'Sym1 (a0123456789876543210 :: Foo) :: Bool where
+      UnFoo'Sym1 a0123456789876543210 = UnFoo' a0123456789876543210
+    type UnFoo' :: Foo -> Bool
+    type family UnFoo' (a :: Foo) :: Bool where
+      UnFoo' a_0123456789876543210 = Apply UnFooSym0 a_0123456789876543210
+    sUnFoo' ::
+      (forall (t :: Foo).
+       Sing t -> Sing (Apply UnFoo'Sym0 t :: Bool) :: Type)
+    sUnFoo' (sA_0123456789876543210 :: Sing a_0123456789876543210)
+      = applySing sUnFoo sA_0123456789876543210
+    instance SingI (UnFoo'Sym0 :: (~>) Foo Bool) where
+      sing = singFun1 @UnFoo'Sym0 sUnFoo'
+
+Singletons/T563.hs:0:0: error: [GHC-76037]
+    Not in scope: type constructor or class ‘UnFooSym0’
+    Suggested fix:
+      Perhaps use one of these:
+        ‘UnFoo'Sym0’ (line 13), ‘MkFooSym0’ (line 7),
+        ‘UnFoo'Sym1’ (line 13)
+   |
+13 | $(singletonsOnly [d|
+   |  ^^^^^^^^^^^^^^^^^^^...

singletons-base/tests/compile-and-dump/Singletons/T563.hs

@@ -0,0 +1,16 @@
+{-# LANGUAGE NoFieldSelectors #-}
+module T563 where
+
+import Data.Singletons.Base.TH
+import Prelude.Singletons
+
+$(singletons [d|
+  infixr 6 `unFoo`
+  data Foo = MkFoo { unFoo :: Bool }
+  |])
+
+-- This should not compile:
+$(singletonsOnly [d|
+  unFoo' :: Foo -> Bool
+  unFoo' = unFoo
+  |])

singletons-th/CHANGES.md

@@ -23,6 +23,8 @@ next [????.??.??]
   generate ill-scoped code when singled.
 * Fix a bug in which singling a local variable that shadows a top-level
   definition would fail to typecheck in some circumstances.
+* Fix a bug in which `singletons-th` would incorrectly promote/single records
+  to top-level field selectors when `NoFieldSelectors` was active.
 
 3.2 [2023.03.12]
 ----------------

singletons-th/src/Data/Singletons/TH/Promote.hs

@@ -236,13 +236,20 @@ promoteDataDecs = concatMapM promoteDataDec
 --    This greatly simplifies the plumbing, since this allows all DLetDecs to
 --    be promoted in a single location.
 --    See Note [singletons-th and record selectors] in D.S.TH.Single.Data.
+--
+-- Note that if @NoFieldSelectors@ is active, then neither steps (2) nor (3)
+-- will promote any records to top-level field selectors.
 promoteDataDec :: DataDecl -> PrM [DLetDec]
 promoteDataDec (DataDecl _ _ _ ctors) = do
   let rec_sel_names = nub $ concatMap extractRecSelNames ctors
                       -- Note the use of nub: the same record selector name can
                       -- be used in multiple constructors!
-  rec_sel_let_decs <- getRecordSelectors ctors
+  fld_sels         <- qIsExtEnabled LangExt.FieldSelectors
+  rec_sel_let_decs <- if fld_sels then getRecordSelectors ctors else pure []
   ctorSyms         <- buildDefunSymsDataD ctors
+  -- NB: If NoFieldSelectors is active, then promoteReifiedInfixDecls will not
+  -- promote any of `rec_sel_names` to field selectors, so there is no need to
+  -- check for it here.
   infix_decs       <- promoteReifiedInfixDecls rec_sel_names
   emitDecs $ ctorSyms ++ infix_decs
   pure rec_sel_let_decs
@@ -610,13 +617,16 @@ promoteLetDecEnv mb_let_uniq (LetDecEnv { lde_defns = value_env
 promoteInfixDecl :: forall q. OptionsMonad q
                  => Maybe Uniq -> Name -> Fixity -> q (Maybe DDec)
 promoteInfixDecl mb_let_uniq name fixity = do
-  opts  <- getOptions
+  opts <- getOptions
+  fld_sels <- qIsExtEnabled LangExt.FieldSelectors
   mb_ns <- reifyNameSpace name
   case mb_ns of
     -- If we can't find the Name for some odd reason, fall back to promote_val
     Nothing          -> promote_val
     Just VarName     -> promote_val
-    Just (FldName _) -> promote_val
+    Just (FldName _)
+      | fld_sels     -> promote_val
+      | otherwise    -> never_mind
     Just DataName    -> never_mind
     Just TcClsName   -> do
       mb_info <- dsReify name
@@ -629,10 +639,16 @@ promoteInfixDecl mb_let_uniq name fixity = do
     finish :: Name -> q (Maybe DDec)
     finish = pure . Just . DLetDec . DInfixD fixity
 
-    -- Don't produce a fixity declaration at all. This happens when promoting a
-    -- fixity declaration for a name whose promoted counterpart is the same as
-    -- the original name.
-    -- See Note [singletons-th and fixity declarations] in D.S.TH.Single.Fixity, wrinkle 1.
+    -- Don't produce a fixity declaration at all. This can happen in the
+    -- following circumstances:
+    --
+    -- - When promoting a fixity declaration for a name whose promoted
+    --   counterpart is the same as the original name.
+    --   See Note [singletons-th and fixity declarations] in
+    --   D.S.TH.Single.Fixity, wrinkle 1.
+    --
+    -- - A fixity declaration contains the name of a record selector when
+    --   NoFieldSelectors is active.
     never_mind :: q (Maybe DDec)
     never_mind = pure Nothing
 

singletons-th/src/Data/Singletons/TH/Single.hs

@@ -341,22 +341,29 @@ singTopLevelDecs locals raw_decls = withLocalDeclarations locals $ do
 buildDataLets :: OptionsMonad q => DataDecl -> q [(Name, DExp)]
 buildDataLets (DataDecl _df _name _tvbs cons) = do
   opts <- getOptions
-  pure $ concatMap (con_num_args opts) cons
+  fld_sels <- qIsExtEnabled LangExt.FieldSelectors
+  pure $ concatMap (con_num_args opts fld_sels) cons
   where
-    con_num_args :: Options -> DCon -> [(Name, DExp)]
-    con_num_args opts (DCon _tvbs _cxt name fields _rty) =
+    con_num_args :: Options -> Bool -> DCon -> [(Name, DExp)]
+    con_num_args opts fld_sels (DCon _tvbs _cxt name fields _rty) =
       (name, wrapSingFun (length (tysOfConFields fields))
                          (DConT $ defunctionalizedName0 opts name)
                          (DConE $ singledDataConName opts name))
-      : rec_selectors opts fields
-
-    rec_selectors :: Options -> DConFields -> [(Name, DExp)]
-    rec_selectors _    (DNormalC {}) = []
-    rec_selectors opts (DRecC fields) =
-      let names = map fstOf3 fields in
-      [ (name, wrapSingFun 1 (DConT $ defunctionalizedName0 opts name)
-                             (DVarE $ singledValueName opts name))
-      | name <- names ]
+      : rec_selectors opts fld_sels fields
+
+    rec_selectors :: Options -> Bool -> DConFields -> [(Name, DExp)]
+    rec_selectors opts fld_sels con
+      | fld_sels
+      = case con of
+          DNormalC {} -> []
+          DRecC fields ->
+            let names = map fstOf3 fields in
+            [ (name, wrapSingFun 1 (DConT $ defunctionalizedName0 opts name)
+                                   (DVarE $ singledValueName opts name))
+            | name <- names ]
+
+      | otherwise
+      = []
 
 -- see comment at top of file
 buildMethLets :: OptionsMonad q => UClassDecl -> q [(Name, DExp)]

singletons-th/src/Data/Singletons/TH/Single/Fixity.hs

@@ -6,32 +6,39 @@ import Language.Haskell.TH.Syntax (NameSpace(..), Quasi(..))
 import Data.Singletons.TH.Options
 import Data.Singletons.TH.Util
 import Language.Haskell.TH.Desugar
+import qualified GHC.LanguageExtensions.Type as LangExt
 
 -- Single a fixity declaration.
 singInfixDecl :: forall q. OptionsMonad q => Name -> Fixity -> q (Maybe DLetDec)
 singInfixDecl name fixity = do
-  opts  <- getOptions
+  opts <- getOptions
+  fld_sels <- qIsExtEnabled LangExt.FieldSelectors
   mb_ns <- reifyNameSpace name
   case mb_ns of
     -- If we can't find the Name for some odd reason,
     -- fall back to singValName
     Nothing          -> finish $ singledValueName   opts name
     Just VarName     -> finish $ singledValueName   opts name
-    Just (FldName _) -> finish $ singledValueName   opts name
+    Just (FldName _)
+      | fld_sels     -> finish $ singledValueName   opts name
+      | otherwise    -> never_mind
     Just DataName    -> finish $ singledDataConName opts name
     Just TcClsName   -> do
       mb_info <- dsReify name
       case mb_info of
         Just (DTyConI DClassD{} _)
           -> finish $ singledClassName opts name
-        _ -> pure Nothing
+        _ -> never_mind
           -- Don't produce anything for other type constructors (type synonyms,
           -- type families, data types, etc.).
           -- See [singletons-th and fixity declarations], wrinkle 1.
   where
     finish :: Name -> q (Maybe DLetDec)
     finish = pure . Just . DInfixD fixity
 
+    never_mind :: q (Maybe DLetDec)
+    never_mind = pure Nothing
+
 -- Try producing singled fixity declarations for Names by reifying them
 -- /without/ consulting quoted declarations. If reification fails, recover and
 -- return the empty list.