From b720f3c125df72a5569071361869a619ba638305 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sat, 6 Jul 2024 21:16:19 -0400 Subject: [PATCH] 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, https://github.com/goldfirere/th-desugar/pull/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. --- .github/workflows/haskell-ci.yml | 2 +- cabal.project | 2 +- .../compile-and-dump/Promote/T361.golden | 4 +-- .../compile-and-dump/Singletons/T353.golden | 28 +++++++++++-------- .../compile-and-dump/Singletons/T567.golden | 21 ++++++++------ .../Singletons/TypeAbstractions.golden | 10 ++++--- singletons-th/CHANGES.md | 28 +++++++++++++++++++ .../src/Data/Singletons/TH/Promote.hs | 9 +++--- .../src/Data/Singletons/TH/Single.hs | 15 ++++++---- 9 files changed, 80 insertions(+), 39 deletions(-) diff --git a/.github/workflows/haskell-ci.yml b/.github/workflows/haskell-ci.yml index f24ac92f..2f577343 100644 --- 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 index 04e5bce6..a2de1faa 100644 --- 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 index 7abbba44..be5a55ae 100644 --- 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 index 1b9990fa..9ac70cc5 100644 --- 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,8 +76,10 @@ 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) => @@ -85,7 +87,9 @@ Singletons/T353.hs:0:0:: Splicing declarations 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 index c80b261b..0d324012 100644 --- 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 index 6b94ec22..ce7ae4a5 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/TypeAbstractions.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/TypeAbstractions.golden @@ -157,7 +157,7 @@ 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) => @@ -165,8 +165,8 @@ Singletons/TypeAbstractions.hs:(0,0)-(0,0): Splicing declarations 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 index 6ec9d381..d6d65aa3 100644 --- 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 index 4935aa11..ed41d23f 100644 --- 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 index da80b29c..1b79db91 100644 --- 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 [] $