promoteLetDecName: Fix visibility-related bug

Previously, `promoteLetDecName` would convert every `DTyVarBndrSpec` in an
outermost `forall` to an invisible argument in a promoted type family equation.
This is not quite right, however, as #585 reveals: we do not want to convert
_inferred_ type variable binders to invisible arguments.

To do this properly, we introduce a new `tvbSpecsToBndrVis` function, which
converts a list of `DTyVarBndrSpec`s to a list of `DTyVarBndrVis`es, dropping
any `DTyVarBndrSpec`s with an `InferredSpec` in the process. We then use
`tvbSpecsToBndrVis` in `promoteLetDecName`, which neatly fixes #585.

singletons-base/tests/SingletonsBaseTestSuite.hs

@@ -152,6 +152,7 @@ tests =
     , compileAndDumpStdTest "T563"
     , compileAndDumpStdTest "T567"
     , compileAndDumpStdTest "T571"
+    , compileAndDumpStdTest "T585"
     , compileAndDumpStdTest "TypeAbstractions"
     ],
     testCompileAndDumpGroup "Promote"

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

@@ -0,0 +1,40 @@
+Singletons/T585.hs:(0,0)-(0,0): Splicing declarations
+    singletons
+      [d| konst :: forall a {b}. a -> b -> a
+          konst x _ = x |]
+  ======>
+    konst :: forall a {b}. a -> b -> a
+    konst x _ = x
+    type KonstSym0 :: forall a {b}. (~>) a ((~>) b a)
+    data KonstSym0 :: (~>) a ((~>) b a)
+      where
+        KonstSym0KindInference :: SameKind (Apply KonstSym0 arg) (KonstSym1 arg) =>
+                                  KonstSym0 a0123456789876543210
+    type instance Apply KonstSym0 a0123456789876543210 = KonstSym1 a0123456789876543210
+    instance SuppressUnusedWarnings KonstSym0 where
+      suppressUnusedWarnings = snd ((,) KonstSym0KindInference ())
+    type KonstSym1 :: forall a {b}. a -> (~>) b a
+    data KonstSym1 (a0123456789876543210 :: a) :: (~>) b a
+      where
+        KonstSym1KindInference :: SameKind (Apply (KonstSym1 a0123456789876543210) arg) (KonstSym2 a0123456789876543210 arg) =>
+                                  KonstSym1 a0123456789876543210 a0123456789876543210
+    type instance Apply (KonstSym1 a0123456789876543210) a0123456789876543210 = Konst a0123456789876543210 a0123456789876543210
+    instance SuppressUnusedWarnings (KonstSym1 a0123456789876543210) where
+      suppressUnusedWarnings = snd ((,) KonstSym1KindInference ())
+    type KonstSym2 :: forall a {b}. a -> b -> a
+    type family KonstSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: a where
+      KonstSym2 a0123456789876543210 a0123456789876543210 = Konst a0123456789876543210 a0123456789876543210
+    type Konst :: forall a {b}. a -> b -> a
+    type family Konst (a :: a) (a :: b) :: a where
+      Konst @a (x :: a) (_ :: b) = x
+    sKonst ::
+      forall a {b} (t :: a) (t :: b). Sing t
+                                      -> Sing t -> Sing (Apply (Apply KonstSym0 t) t :: a)
+    sKonst (sX :: Sing x) _ = sX
+    instance SingI (KonstSym0 :: (~>) a ((~>) b a)) where
+      sing = singFun2 @KonstSym0 sKonst
+    instance SingI d => SingI (KonstSym1 (d :: a) :: (~>) b a) where
+      sing = singFun1 @(KonstSym1 (d :: a)) (sKonst (sing @d))
+    instance SingI1 (KonstSym1 :: a -> (~>) b a) where
+      liftSing (s :: Sing (d :: a))
+        = singFun1 @(KonstSym1 (d :: a)) (sKonst s)

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

@@ -0,0 +1,8 @@
+module T585 where
+
+import Data.Singletons.TH
+
+$(singletons [d|
+  konst :: forall a {b}. a -> b -> a
+  konst x _ = x
+  |])

singletons-th/CHANGES.md

@@ -1,6 +1,11 @@
 Changelog for the `singletons-th` project
 =========================================
 
+next [????.??.??]
+-----------------
+* Fix a bug causing definitions with type signatures using inferred type
+  variable binders (e.g., `forall a {b}. a -> b -> a`) to fail to promote.
+
 3.3 [2023.10.13]
 ----------------
 * Require building with GHC 9.8.

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

@@ -1165,9 +1165,23 @@ promoteLetDecName mb_let_uniq name m_ldrki all_locals = do
           Just (LDRKI m_sak tvbs _ _)
             |  isJust m_sak
                -- Per the comments on LetDecRHSKindInfo, `isJust m_sak` is only True
-               -- if there are no local variables. Return the scoped type variables
-               -- `tvbs` as invisible arguments using `DTyArg`...
-            -> map (DTyArg . DVarT . extractTvbName) tvbs
+               -- if there are no local variables. Convert the scoped type variables
+               -- `tvbs` to invisible arguments, making sure to use
+               -- `tvbSpecsToBndrVis` to filter out any inferred type variable
+               -- binders. For instance, we want to promote this example (from #585):
+               --
+               --   konst :: forall a {b}. a -> b -> a
+               --   konst x _ = x
+               --
+               -- To this type family:
+               --
+               --   type Konst :: forall a {b}. a -> b -> a
+               --   type family Konst @a x y where
+               --     Konst @a (x :: a) (_ :: b) = x
+               --
+               -- Note that we apply `a` in `Konst @a` but _not_ `b`, as `b` is
+               -- bound using an inferred type variable binder.
+            -> map dTyVarBndrVisToDTypeArg $ tvbSpecsToBndrVis tvbs
           _ -> -- ...otherwise, return the local variables as explicit arguments
                -- using DTANormal.
                map (DTANormal . DVarT) all_locals

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

@@ -250,6 +250,30 @@ maybeSigT :: DType -> Maybe DKind -> DType
 maybeSigT ty Nothing   = ty
 maybeSigT ty (Just ki) = ty `DSigT` ki
 
+-- | Convert a list of 'DTyVarBndrSpec's to a list of 'DTyVarBndrVis'es. Type
+-- variable binders with a 'SpecifiedSpec' are converted to 'BndrInvis', and
+-- type variable binders with an 'InferredSpec' are dropped entirely.
+--
+-- As an example, if you have this list of 'DTyVarBndrSpec's:
+--
+-- @
+-- forall a {b} c {d e} f. <...>
+-- @
+--
+-- The corresponding list of 'DTyVarBndrVis'es would be:
+--
+-- @
+-- \@a \@b \@f
+-- @
+--
+-- Note that note of @b@, @d@, or @e@ appear in the list.
+tvbSpecsToBndrVis :: [DTyVarBndrSpec] -> [DTyVarBndrVis]
+tvbSpecsToBndrVis = mapMaybe (traverse specificityToBndrVis)
+  where
+    specificityToBndrVis :: Specificity -> Maybe BndrVis
+    specificityToBndrVis SpecifiedSpec = Just BndrInvis
+    specificityToBndrVis InferredSpec  = Nothing
+
 -- Reconstruct a vanilla function type from its individual type variable
 -- binders, constraints, argument types, and result type. (See
 -- Note [Vanilla-type validity checking during promotion] in