Adapt to goldfirere/th-desugar#199 and goldfirere/th-desugar#220

As part of a fix for goldfirere/th-desugar#199 and goldfirere/th-desugar#220, goldfirere/th-desugar#227 improves `th-desugar`'s ability to locally reify and desugar precise types for Haskell98-style data constructors and class methods. This has a couple of knock-on effects for `singletons`: * The type of `dsCon` has changes to accept `DTyVarBndrSpec`s instead of `DTyVarBndrUnit`s, so we must adapt the call sites in `singletons-th` accordingly. * Some of the test cases in `singletons-base` need to have their expected output updated to account for the improved kind information and specificity information flowing down from standalone kind signatures.
goldfirere · Jul 13, 2024 · b720f3c · b720f3c
1 parent e3b4a75
commit b720f3c
Show file tree

Hide file tree

Showing 9 changed files with 80 additions and 39 deletions.
diff --git a/.github/workflows/haskell-ci.yml b/.github/workflows/haskell-ci.yml
@@ -215,7 +215,7 @@ jobs:
           source-repository-package
             type:     git
             location: https://github.com/goldfirere/th-desugar
-            tag:      75a0731adb32382d281c2eac62dfff2735723334
+            tag:      c7b460412fe9896597270be94a243972833c0a66
           EOF
           $HCPKG list --simple-output --names-only | perl -ne 'for (split /\s+/) { print "constraints: any.$_ installed\n" unless /^(Cabal|Cabal-syntax|singletons|singletons-base|singletons-th)$/; }' >> cabal.project.local
           cat cabal.project

diff --git a/cabal.project b/cabal.project
@@ -5,4 +5,4 @@ packages: ./singletons
 source-repository-package
   type: git
   location: https://github.com/goldfirere/th-desugar
-  tag: 75a0731adb32382d281c2eac62dfff2735723334
+  tag: c7b460412fe9896597270be94a243972833c0a66
diff --git a/singletons-base/tests/compile-and-dump/Promote/T361.golden b/singletons-base/tests/compile-and-dump/Promote/T361.golden
@@ -1,8 +1,8 @@
 Promote/T361.hs:0:0:: Splicing declarations
     genDefunSymbols [''Proxy]
   ======>
-    type ProxySym0 :: forall k (t :: k). Proxy t
-    type family ProxySym0 @k @(t :: k) :: Proxy t where
+    type ProxySym0 :: forall {k :: Type} (t :: k). Proxy t
+    type family ProxySym0 @(t :: k) :: Proxy t where
       ProxySym0 = 'Proxy
 Promote/T361.hs:(0,0)-(0,0): Splicing declarations
     promote

diff --git a/singletons-base/tests/compile-and-dump/Singletons/T353.golden b/singletons-base/tests/compile-and-dump/Singletons/T353.golden
@@ -33,7 +33,7 @@ Singletons/T353.hs:(0,0)-(0,0): Splicing declarations
 Singletons/T353.hs:0:0:: Splicing declarations
     genDefunSymbols [''Prod]
   ======>
-    type MkProdSym0 :: forall k
+    type MkProdSym0 :: forall {k :: Type}
                               (f :: k -> Type)
                               (g :: k -> Type)
                               (p :: k). (~>) (f p) ((~>) (g p) (Prod f g p))
@@ -44,7 +44,7 @@ Singletons/T353.hs:0:0:: Splicing declarations
     type instance Apply @(f p) @((~>) (g p) (Prod f g p)) MkProdSym0 a0123456789876543210 = MkProdSym1 a0123456789876543210
     instance SuppressUnusedWarnings MkProdSym0 where
       suppressUnusedWarnings = snd ((,) MkProdSym0KindInference ())
-    type MkProdSym1 :: forall k
+    type MkProdSym1 :: forall {k :: Type}
                               (f :: k -> Type)
                               (g :: k -> Type)
                               (p :: k). f p -> (~>) (g p) (Prod f g p)
@@ -55,18 +55,18 @@ Singletons/T353.hs:0:0:: Splicing declarations
     type instance Apply @(g p) @(Prod f g p) (MkProdSym1 a0123456789876543210) a0123456789876543210 = 'MkProd a0123456789876543210 a0123456789876543210
     instance SuppressUnusedWarnings (MkProdSym1 a0123456789876543210) where
       suppressUnusedWarnings = snd ((,) MkProdSym1KindInference ())
-    type MkProdSym2 :: forall k
+    type MkProdSym2 :: forall {k :: Type}
                               (f :: k -> Type)
                               (g :: k -> Type)
                               (p :: k). f p -> g p -> Prod f g p
-    type family MkProdSym2 @k @(f :: k -> Type) @(g :: k
-                                                       -> Type) @(p :: k) (a0123456789876543210 :: f p) (a0123456789876543210 :: g p) :: Prod f g p where
+    type family MkProdSym2 @(f :: k -> Type) @(g :: k
+                                                    -> Type) @(p :: k) (a0123456789876543210 :: f p) (a0123456789876543210 :: g p) :: Prod f g p where
       MkProdSym2 a0123456789876543210 a0123456789876543210 = 'MkProd a0123456789876543210 a0123456789876543210
 Singletons/T353.hs:0:0:: Splicing declarations
     genDefunSymbols [''Foo]
   ======>
-    type MkFooSym0 :: forall k
-                             k
+    type MkFooSym0 :: forall {k :: Type}
+                             {k :: Type}
                              (a :: k)
                              (b :: k). (~>) (Proxy a) ((~>) (Proxy b) (Foo a b))
     data MkFooSym0 :: (~>) (Proxy a) ((~>) (Proxy b) (Foo a b))
@@ -76,16 +76,20 @@ Singletons/T353.hs:0:0:: Splicing declarations
     type instance Apply @(Proxy a) @((~>) (Proxy b) (Foo a b)) MkFooSym0 a0123456789876543210 = MkFooSym1 a0123456789876543210
     instance SuppressUnusedWarnings MkFooSym0 where
       suppressUnusedWarnings = snd ((,) MkFooSym0KindInference ())
-    type MkFooSym1 :: forall k k (a :: k) (b :: k). Proxy a
-                                                    -> (~>) (Proxy b) (Foo a b)
+    type MkFooSym1 :: forall {k :: Type}
+                             {k :: Type}
+                             (a :: k)
+                             (b :: k). Proxy a -> (~>) (Proxy b) (Foo a b)
     data MkFooSym1 (a0123456789876543210 :: Proxy a) :: (~>) (Proxy b) (Foo a b)
       where
         MkFooSym1KindInference :: SameKind (Apply (MkFooSym1 a0123456789876543210) arg) (MkFooSym2 a0123456789876543210 arg) =>
                                   MkFooSym1 a0123456789876543210 a0123456789876543210
     type instance Apply @(Proxy b) @(Foo a b) (MkFooSym1 a0123456789876543210) a0123456789876543210 = 'MkFoo a0123456789876543210 a0123456789876543210
     instance SuppressUnusedWarnings (MkFooSym1 a0123456789876543210) where
       suppressUnusedWarnings = snd ((,) MkFooSym1KindInference ())
-    type MkFooSym2 :: forall k k (a :: k) (b :: k). Proxy a
-                                                    -> Proxy b -> Foo a b
-    type family MkFooSym2 @k @k @(a :: k) @(b :: k) (a0123456789876543210 :: Proxy a) (a0123456789876543210 :: Proxy b) :: Foo a b where
+    type MkFooSym2 :: forall {k :: Type}
+                             {k :: Type}
+                             (a :: k)
+                             (b :: k). Proxy a -> Proxy b -> Foo a b
+    type family MkFooSym2 @(a :: k) @(b :: k) (a0123456789876543210 :: Proxy a) (a0123456789876543210 :: Proxy b) :: Foo a b where
       MkFooSym2 a0123456789876543210 a0123456789876543210 = 'MkFoo a0123456789876543210 a0123456789876543210
diff --git a/singletons-base/tests/compile-and-dump/Singletons/T567.golden b/singletons-base/tests/compile-and-dump/Singletons/T567.golden
@@ -19,29 +19,32 @@ Singletons/T567.hs:(0,0)-(0,0): Splicing declarations
     data D3 x (p :: Proxy x) = MkD3
     type D4 :: forall k. forall (a :: k) -> Proxy a -> Type
     data D4 (x :: j) (p :: Proxy x) = MkD4
-    type MkD1Sym0 :: forall x p. D1 x p
-    type family MkD1Sym0 @x @p :: D1 x p where
+    type MkD1Sym0 :: forall k (x :: k) (p :: Proxy x). D1 x p
+    type family MkD1Sym0 @k @(x :: k) @(p :: Proxy x) :: D1 x p where
       MkD1Sym0 = MkD1
-    type MkD2Sym0 :: forall j (x :: j) p. D2 x p
-    type family MkD2Sym0 @j @(x :: j) @p :: D2 x p where
+    type MkD2Sym0 :: forall j (x :: j) (p :: Proxy x). D2 x p
+    type family MkD2Sym0 @j @(x :: j) @(p :: Proxy x) :: D2 x p where
       MkD2Sym0 = MkD2
-    type MkD3Sym0 :: forall x (p :: Proxy x). D3 x p
-    type family MkD3Sym0 @x @(p :: Proxy x) :: D3 x p where
+    type MkD3Sym0 :: forall k (x :: k) (p :: Proxy x). D3 x p
+    type family MkD3Sym0 @k @(x :: k) @(p :: Proxy x) :: D3 x p where
       MkD3Sym0 = MkD3
     type MkD4Sym0 :: forall j (x :: j) (p :: Proxy x). D4 x p
     type family MkD4Sym0 @j @(x :: j) @(p :: Proxy x) :: D4 x p where
       MkD4Sym0 = MkD4
     type SD1 :: forall k (x :: k) (p :: Proxy x). D1 x p -> Type
     data SD1 :: forall k (x :: k) (p :: Proxy x). D1 x p -> Type
-      where SMkD1 :: forall x p. SD1 (MkD1 :: D1 x p)
+      where
+        SMkD1 :: forall k (x :: k) (p :: Proxy x). SD1 (MkD1 :: D1 x p)
     type instance Sing @(D1 x p) = SD1
     type SD2 :: forall j (x :: j) (p :: Proxy x). D2 x p -> Type
     data SD2 :: forall j (x :: j) (p :: Proxy x). D2 x p -> Type
-      where SMkD2 :: forall j (x :: j) p. SD2 (MkD2 :: D2 x p)
+      where
+        SMkD2 :: forall j (x :: j) (p :: Proxy x). SD2 (MkD2 :: D2 x p)
     type instance Sing @(D2 x p) = SD2
     type SD3 :: forall k (x :: k) (p :: Proxy x). D3 x p -> Type
     data SD3 :: forall k (x :: k) (p :: Proxy x). D3 x p -> Type
-      where SMkD3 :: forall x (p :: Proxy x). SD3 (MkD3 :: D3 x p)
+      where
+        SMkD3 :: forall k (x :: k) (p :: Proxy x). SD3 (MkD3 :: D3 x p)
     type instance Sing @(D3 x p) = SD3
     type SD4 :: forall j (x :: j) (p :: Proxy x). D4 x p -> Type
     data SD4 :: forall j (x :: j) (p :: Proxy x). D4 x p -> Type

diff --git a/singletons-base/tests/compile-and-dump/Singletons/TypeAbstractions.golden b/singletons-base/tests/compile-and-dump/Singletons/TypeAbstractions.golden
@@ -157,16 +157,16 @@ Singletons/TypeAbstractions.hs:(0,0)-(0,0): Splicing declarations
                                                    -> Proxy b -> D3 @j a @k b
     type family MkD3Sym2 @j @(a :: j) @k @(b :: k) (a0123456789876543210 :: Proxy a) (a0123456789876543210 :: Proxy b) :: D3 @j a @k b where
       MkD3Sym2 a0123456789876543210 a0123456789876543210 = MkD3 a0123456789876543210 a0123456789876543210
-    type MkD4Sym0 :: forall a. (~>) a (D4 @a)
+    type MkD4Sym0 :: forall (a :: Type). (~>) a (D4 @a)
     data MkD4Sym0 :: (~>) a (D4 @a)
       where
         MkD4Sym0KindInference :: SameKind (Apply MkD4Sym0 arg) (MkD4Sym1 arg) =>
                                  MkD4Sym0 a0123456789876543210
     type instance Apply @a @(D4 @a) MkD4Sym0 a0123456789876543210 = MkD4 a0123456789876543210
     instance SuppressUnusedWarnings MkD4Sym0 where
       suppressUnusedWarnings = snd ((,) MkD4Sym0KindInference ())
-    type MkD4Sym1 :: forall a. a -> D4 @a
-    type family MkD4Sym1 @a (a0123456789876543210 :: a) :: D4 @a where
+    type MkD4Sym1 :: forall (a :: Type). a -> D4 @a
+    type family MkD4Sym1 @(a :: Type) (a0123456789876543210 :: a) :: D4 @a where
       MkD4Sym1 a0123456789876543210 = MkD4 a0123456789876543210
     type Meth1Sym0 :: forall j
                              k
@@ -260,7 +260,9 @@ Singletons/TypeAbstractions.hs:(0,0)-(0,0): Splicing declarations
     type instance Sing @(D3 @j a @k b) = SD3
     type SD4 :: forall (a :: Type). D4 @a -> Type
     data SD4 :: forall (a :: Type). D4 @a -> Type
-      where SMkD4 :: forall a (n :: a). (Sing n) -> SD4 (MkD4 n :: D4 @a)
+      where
+        SMkD4 :: forall (a :: Type) (n :: a).
+                 (Sing n) -> SD4 (MkD4 n :: D4 @a)
     type instance Sing @(D4 @a) = SD4
     class SC1 @j @k (a :: j) (b :: k) where
       sMeth1 ::

diff --git a/singletons-th/CHANGES.md b/singletons-th/CHANGES.md
@@ -16,6 +16,34 @@ next [????.??.??]
   singled version of `x`.
 * Add support for promoting and singling type variables that scope over the
   bodies of class method defaults and instance methods.
+* `singletons-th` can now generate more precise types for singled data
+  constructors whose parent data types have standalone kind signatures. For
+  instance, consider this data type:
+
+  ```hs
+  $(singletons [d|
+    type D :: forall k. k -> Type
+    data D a = MkD
+    |])
+  ```
+
+  Previously, `singletons-th` would generate the following type for `SMkD` (the
+  singled counterpart to `MkD`):
+
+  ```hs
+  data SD :: forall k. k -> Type where
+    SMkD :: forall a. SD (MkD :: D a)
+  ```
+
+  This was not as precise as it could have been, as the type of `SMkD` did not
+  make the kind variable `k` eligible for visible type application (as is the
+  case in `MkD :: forall k (a :: k). D a`). `singletons-th` now accomplishes
+  this by generating the following code instead:
+
+  ```hs
+  data SD :: forall k. k -> Type where
+    SMkD :: forall k (a :: k). SD (MkD :: D a)
+  ```
 
 3.4 [2024.05.12]
 ----------------

diff --git a/singletons-th/src/Data/Singletons/TH/Promote.hs b/singletons-th/src/Data/Singletons/TH/Promote.hs
@@ -162,10 +162,11 @@ promoteInstance :: OptionsMonad q => DerivDesc q -> String -> Name -> q [Dec]
 promoteInstance mk_inst class_name name = do
   (df, tvbs, cons) <- getDataD ("I cannot make an instance of " ++ class_name
                                 ++ " for it.") name
-  tvbs' <- mapM dsTvbVis tvbs
-  let data_ty   = foldTypeTvbs (DConT name) tvbs'
-  cons' <- concatMapM (dsCon tvbs' data_ty) cons
-  let data_decl = DataDecl df name tvbs' cons'
+  dtvbs <- mapM dsTvbVis tvbs
+  let data_ty   = foldTypeTvbs (DConT name) dtvbs
+      dtvbSpecs = changeDTVFlags SpecifiedSpec dtvbs
+  cons' <- concatMapM (dsCon dtvbSpecs data_ty) cons
+  let data_decl = DataDecl df name dtvbs cons'
   raw_inst <- mk_inst Nothing data_ty data_decl
   decs <- promoteM_ [] $ void $
           promoteInstanceDec OMap.empty Map.empty raw_inst

diff --git a/singletons-th/src/Data/Singletons/TH/Single.hs b/singletons-th/src/Data/Singletons/TH/Single.hs
@@ -148,8 +148,9 @@ singDecideInstance :: OptionsMonad q => Name -> q [Dec]
 singDecideInstance name = do
   (_df, tvbs, cons) <- getDataD ("I cannot make an instance of SDecide for it.") name
   dtvbs <- mapM dsTvbVis tvbs
-  let data_ty = foldTypeTvbs (DConT name) dtvbs
-  dcons <- concatMapM (dsCon dtvbs data_ty) cons
+  let data_ty   = foldTypeTvbs (DConT name) dtvbs
+      dtvbSpecs = changeDTVFlags SpecifiedSpec dtvbs
+  dcons <- concatMapM (dsCon dtvbSpecs data_ty) cons
   (scons, _) <- singM [] $ mapM (singCtor name) dcons
   sDecideInstance <- mkDecideInstance Nothing data_ty dcons scons
   eqInstance <- mkEqInstanceForSingleton data_ty name
@@ -200,8 +201,9 @@ showSingInstance :: OptionsMonad q => Name -> q [Dec]
 showSingInstance name = do
   (df, tvbs, cons) <- getDataD ("I cannot make an instance of Show for it.") name
   dtvbs <- mapM dsTvbVis tvbs
-  let data_ty = foldTypeTvbs (DConT name) dtvbs
-  dcons <- concatMapM (dsCon dtvbs data_ty) cons
+  let data_ty   = foldTypeTvbs (DConT name) dtvbs
+      dtvbSpecs = changeDTVFlags SpecifiedSpec dtvbs
+  dcons <- concatMapM (dsCon dtvbSpecs data_ty) cons
   let tyvars    = map (DVarT . extractTvbName) dtvbs
       kind      = foldType (DConT name) tyvars
       data_decl = DataDecl df name dtvbs dcons
@@ -272,8 +274,9 @@ singInstance mk_inst inst_name name = do
   (df, tvbs, cons) <- getDataD ("I cannot make an instance of " ++ inst_name
                                 ++ " for it.") name
   dtvbs <- mapM dsTvbVis tvbs
-  let data_ty = foldTypeTvbs (DConT name) dtvbs
-  dcons <- concatMapM (dsCon dtvbs data_ty) cons
+  let data_ty   = foldTypeTvbs (DConT name) dtvbs
+      dtvbSpecs = changeDTVFlags SpecifiedSpec dtvbs
+  dcons <- concatMapM (dsCon dtvbSpecs data_ty) cons
   let data_decl = DataDecl df name dtvbs dcons
   raw_inst <- mk_inst Nothing data_ty data_decl
   (a_inst, decs) <- promoteM [] $