From 54a0d8dac8f9ba47d2253d932c44920f9e66d463 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 18 Sep 2023 08:01:25 -0400 Subject: [PATCH] Bump th-desugar submodule to version 1.16 This bumps the `th-desugar` submodule to bring in all of the changes in the upcoming `1.16` release. Aside from bumping version bounds, the only other changes that had to be made on the `singletons` side are: * `singletons-th` now has explicit failure cases for typed TH splices. * Due to goldfirere/th-desugar#194, desugared data constructors now look like this: ```hs DataCon :: forall (a :: Type) (b :: Type). DataType a b ``` Instead of this: ```hs DataCon :: forall (a :: Type) (b :: Type). DataType (a :: Type) (b :: Type) ``` This causes the expected output for some test cases to change, but they are benign changes. --- .github/workflows/haskell-ci.yml | 6 +- cabal.project | 2 +- singletons-base/singletons-base.cabal | 2 +- .../compile-and-dump/Promote/T361.golden | 4 +- .../Singletons/BoundedDeriving.golden | 16 ++-- .../compile-and-dump/Singletons/T271.golden | 13 ++-- .../compile-and-dump/Singletons/T296.golden | 7 +- .../compile-and-dump/Singletons/T297.golden | 7 +- .../compile-and-dump/Singletons/T353.golden | 33 +++------ .../compile-and-dump/Singletons/T371.golden | 38 +++++----- .../compile-and-dump/Singletons/T412.golden | 74 ++++++++----------- .../compile-and-dump/Singletons/T450.golden | 13 ++-- .../compile-and-dump/Singletons/T567.golden | 22 +++--- singletons-th/singletons-th.cabal | 2 +- .../src/Data/Singletons/TH/Promote.hs | 2 + .../src/Data/Singletons/TH/Single.hs | 2 + 16 files changed, 105 insertions(+), 138 deletions(-) diff --git a/.github/workflows/haskell-ci.yml b/.github/workflows/haskell-ci.yml index 0362f6b4..15b21774 100644 --- a/.github/workflows/haskell-ci.yml +++ b/.github/workflows/haskell-ci.yml @@ -8,9 +8,9 @@ # # For more information, see https://github.com/haskell-CI/haskell-ci # -# version: 0.16.3 +# version: 0.16.6 # -# REGENDATA ("0.16.3",["github","cabal.project"]) +# REGENDATA ("0.16.6",["github","cabal.project"]) # name: Haskell-CI on: @@ -245,7 +245,7 @@ jobs: source-repository-package type: git location: https://github.com/goldfirere/th-desugar - tag: f7db712e95a125e710cefc7cd819c6480f7e52e3 + tag: 47f6221088ac6185566066b4d45909b0cc704855 EOF $HCPKG list --simple-output --names-only | perl -ne 'for (split /\s+/) { print "constraints: $_ installed\n" unless /^(singletons|singletons-base|singletons-th)$/; }' >> cabal.project.local cat cabal.project diff --git a/cabal.project b/cabal.project index 942af235..00de788c 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: f7db712e95a125e710cefc7cd819c6480f7e52e3 + tag: 47f6221088ac6185566066b4d45909b0cc704855 diff --git a/singletons-base/singletons-base.cabal b/singletons-base/singletons-base.cabal index f0f3ab21..b5b22b03 100644 --- a/singletons-base/singletons-base.cabal +++ b/singletons-base/singletons-base.cabal @@ -78,7 +78,7 @@ library singletons-th >= 3.2 && < 3.3, template-haskell >= 2.20 && < 2.21, text >= 1.2, - th-desugar >= 1.15 && < 1.16 + th-desugar >= 1.16 && < 1.17 default-language: GHC2021 other-extensions: TemplateHaskell exposed-modules: Data.Singletons.Base.CustomStar diff --git a/singletons-base/tests/compile-and-dump/Promote/T361.golden b/singletons-base/tests/compile-and-dump/Promote/T361.golden index e72a8bfb..0a6c6077 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 :: k) - type family ProxySym0 :: Proxy (t :: k) where + type ProxySym0 :: forall k (t :: k). Proxy t + type family ProxySym0 :: 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/BoundedDeriving.golden b/singletons-base/tests/compile-and-dump/Singletons/BoundedDeriving.golden index 86883c14..42866593 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/BoundedDeriving.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/BoundedDeriving.golden @@ -60,13 +60,11 @@ Singletons/BoundedDeriving.hs:(0,0)-(0,0): Splicing declarations type Foo3Sym1 :: forall a. a -> Foo3 a type family Foo3Sym1 (a0123456789876543210 :: a) :: Foo3 a where Foo3Sym1 a0123456789876543210 = Foo3 a0123456789876543210 - type Foo41Sym0 :: forall (a :: Type) - (b :: Type). Foo4 (a :: Type) (b :: Type) - type family Foo41Sym0 :: Foo4 (a :: Type) (b :: Type) where + type Foo41Sym0 :: forall (a :: Type) (b :: Type). Foo4 a b + type family Foo41Sym0 :: Foo4 a b where Foo41Sym0 = Foo41 - type Foo42Sym0 :: forall (a :: Type) - (b :: Type). Foo4 (a :: Type) (b :: Type) - type family Foo42Sym0 :: Foo4 (a :: Type) (b :: Type) where + type Foo42Sym0 :: forall (a :: Type) (b :: Type). Foo4 a b + type family Foo42Sym0 :: Foo4 a b where Foo42Sym0 = Foo42 type PairSym0 :: (~>) Bool ((~>) Bool Pair) data PairSym0 :: (~>) Bool ((~>) Bool Pair) @@ -199,10 +197,8 @@ Singletons/BoundedDeriving.hs:(0,0)-(0,0): Splicing declarations = case toSing b :: SomeSing a of SomeSing c -> SomeSing (SFoo3 c) data SFoo4 :: forall (a :: Type) (b :: Type). Foo4 a b -> Type where - SFoo41 :: forall (a :: Type) (b :: Type). - SFoo4 (Foo41 :: Foo4 (a :: Type) (b :: Type)) - SFoo42 :: forall (a :: Type) (b :: Type). - SFoo4 (Foo42 :: Foo4 (a :: Type) (b :: Type)) + SFoo41 :: forall (a :: Type) (b :: Type). SFoo4 (Foo41 :: Foo4 a b) + SFoo42 :: forall (a :: Type) (b :: Type). SFoo4 (Foo42 :: Foo4 a b) type instance Sing @(Foo4 a b) = SFoo4 instance (SingKind a, SingKind b) => SingKind (Foo4 a b) where type Demote (Foo4 a b) = Foo4 (Demote a) (Demote b) diff --git a/singletons-base/tests/compile-and-dump/Singletons/T271.golden b/singletons-base/tests/compile-and-dump/Singletons/T271.golden index 7e8c076b..7656a3c4 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T271.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T271.golden @@ -14,8 +14,8 @@ Singletons/T271.hs:(0,0)-(0,0): Splicing declarations where Identity :: a -> Identity a deriving (Eq, Ord) type ConstantSym0 :: forall (a :: Type) - (b :: Type). (~>) a (Constant (a :: Type) (b :: Type)) - data ConstantSym0 :: (~>) a (Constant (a :: Type) (b :: Type)) + (b :: Type). (~>) a (Constant a b) + data ConstantSym0 :: (~>) a (Constant a b) where ConstantSym0KindInference :: SameKind (Apply ConstantSym0 arg) (ConstantSym1 arg) => ConstantSym0 a0123456789876543210 @@ -23,8 +23,8 @@ Singletons/T271.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings ConstantSym0 where suppressUnusedWarnings = snd ((,) ConstantSym0KindInference ()) type ConstantSym1 :: forall (a :: Type) (b :: Type). a - -> Constant (a :: Type) (b :: Type) - type family ConstantSym1 (a0123456789876543210 :: a) :: Constant (a :: Type) (b :: Type) where + -> Constant a b + type family ConstantSym1 (a0123456789876543210 :: a) :: Constant a b where ConstantSym1 a0123456789876543210 = Constant a0123456789876543210 type IdentitySym0 :: (~>) a (Identity a) data IdentitySym0 :: (~>) a (Identity a) @@ -157,8 +157,7 @@ Singletons/T271.hs:(0,0)-(0,0): Splicing declarations Constant a b -> Type where SConstant :: forall (a :: Type) (b :: Type) (n :: a). - (Sing n) -> - SConstant (Constant n :: Constant (a :: Type) (b :: Type)) + (Sing n) -> SConstant (Constant n :: Constant a b) type instance Sing @(Constant a b) = SConstant instance (SingKind a, SingKind b) => SingKind (Constant a b) where type Demote (Constant a b) = Constant (Demote a) (Demote b) @@ -285,7 +284,7 @@ Singletons/T271.hs:(0,0)-(0,0): Splicing declarations sing = SConstant sing instance SingI1 Constant where liftSing = SConstant - instance SingI (ConstantSym0 :: (~>) a (Constant (a :: Type) (b :: Type))) where + instance SingI (ConstantSym0 :: (~>) a (Constant a b)) where sing = singFun1 @ConstantSym0 SConstant instance SingI n => SingI (Identity (n :: a)) where sing = SIdentity sing diff --git a/singletons-base/tests/compile-and-dump/Singletons/T296.golden b/singletons-base/tests/compile-and-dump/Singletons/T296.golden index baa3bf10..a99af46d 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T296.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T296.golden @@ -20,8 +20,8 @@ Singletons/T296.hs:(0,0)-(0,0): Splicing declarations z = MyProxy in z in x - type MyProxySym0 :: forall (a :: Type). MyProxy (a :: Type) - type family MyProxySym0 :: MyProxy (a :: Type) where + type MyProxySym0 :: forall (a :: Type). MyProxy a + type family MyProxySym0 :: MyProxy a where MyProxySym0 = MyProxy data Let0123456789876543210ZSym0 a0123456789876543210 where @@ -77,8 +77,7 @@ Singletons/T296.hs:(0,0)-(0,0): Splicing declarations sing = singFun1 @FSym0 sF data SMyProxy :: forall (a :: Type). MyProxy a -> Type where - SMyProxy :: forall (a :: Type). - SMyProxy (MyProxy :: MyProxy (a :: Type)) + SMyProxy :: forall (a :: Type). SMyProxy (MyProxy :: MyProxy a) type instance Sing @(MyProxy a) = SMyProxy instance SingKind a => SingKind (MyProxy a) where type Demote (MyProxy a) = MyProxy (Demote a) diff --git a/singletons-base/tests/compile-and-dump/Singletons/T297.golden b/singletons-base/tests/compile-and-dump/Singletons/T297.golden index 2c561e46..e33a7c9f 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T297.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T297.golden @@ -18,8 +18,8 @@ Singletons/T297.hs:(0,0)-(0,0): Splicing declarations z = MyProxy in z in x - type MyProxySym0 :: forall (a :: Type). MyProxy (a :: Type) - type family MyProxySym0 :: MyProxy (a :: Type) where + type MyProxySym0 :: forall (a :: Type). MyProxy a + type family MyProxySym0 :: MyProxy a where MyProxySym0 = MyProxy type Let0123456789876543210ZSym0 :: MyProxy a type family Let0123456789876543210ZSym0 :: MyProxy a where @@ -56,8 +56,7 @@ Singletons/T297.hs:(0,0)-(0,0): Splicing declarations sing = singFun1 @FSym0 sF data SMyProxy :: forall (a :: Type). MyProxy a -> Type where - SMyProxy :: forall (a :: Type). - SMyProxy (MyProxy :: MyProxy (a :: Type)) + SMyProxy :: forall (a :: Type). SMyProxy (MyProxy :: MyProxy a) type instance Sing @(MyProxy a) = SMyProxy instance SingKind a => SingKind (MyProxy a) where type Demote (MyProxy a) = MyProxy (Demote a) diff --git a/singletons-base/tests/compile-and-dump/Singletons/T353.golden b/singletons-base/tests/compile-and-dump/Singletons/T353.golden index fc6f48d2..7b27978c 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T353.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T353.golden @@ -36,10 +36,8 @@ Singletons/T353.hs:0:0:: Splicing declarations type MkProdSym0 :: forall k (f :: k -> Type) (g :: k -> Type) - (p :: k). (~>) (f p) ((~>) (g p) (Prod (f :: k -> Type) (g :: k - -> Type) (p :: k))) - data MkProdSym0 :: (~>) (f p) ((~>) (g p) (Prod (f :: k - -> Type) (g :: k -> Type) (p :: k))) + (p :: k). (~>) (f p) ((~>) (g p) (Prod f g p)) + data MkProdSym0 :: (~>) (f p) ((~>) (g p) (Prod f g p)) where MkProdSym0KindInference :: SameKind (Apply MkProdSym0 arg) (MkProdSym1 arg) => MkProdSym0 a0123456789876543210 @@ -49,12 +47,8 @@ Singletons/T353.hs:0:0:: Splicing declarations type MkProdSym1 :: forall k (f :: k -> Type) (g :: k -> Type) - (p :: k). f p - -> (~>) (g p) (Prod (f :: k -> Type) (g :: k - -> Type) (p :: k)) - data MkProdSym1 (a0123456789876543210 :: f p) :: (~>) (g p) (Prod (f :: k - -> Type) (g :: k - -> Type) (p :: k)) + (p :: k). f p -> (~>) (g p) (Prod f g p) + data MkProdSym1 (a0123456789876543210 :: f p) :: (~>) (g p) (Prod f g p) where MkProdSym1KindInference :: SameKind (Apply (MkProdSym1 a0123456789876543210) arg) (MkProdSym2 a0123456789876543210 arg) => MkProdSym1 a0123456789876543210 a0123456789876543210 @@ -64,11 +58,8 @@ Singletons/T353.hs:0:0:: Splicing declarations type MkProdSym2 :: forall k (f :: k -> Type) (g :: k -> Type) - (p :: k). f p - -> g p -> Prod (f :: k -> Type) (g :: k -> Type) (p :: k) - type family MkProdSym2 (a0123456789876543210 :: f p) (a0123456789876543210 :: g p) :: Prod (f :: k - -> Type) (g :: k - -> Type) (p :: k) where + (p :: k). f p -> g p -> Prod f g p + type family MkProdSym2 (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] @@ -76,8 +67,8 @@ Singletons/T353.hs:0:0:: Splicing declarations type MkFooSym0 :: forall k k (a :: k) - (b :: k). (~>) (Proxy a) ((~>) (Proxy b) (Foo (a :: k) (b :: k))) - data MkFooSym0 :: (~>) (Proxy a) ((~>) (Proxy b) (Foo (a :: k) (b :: k))) + (b :: k). (~>) (Proxy a) ((~>) (Proxy b) (Foo a b)) + data MkFooSym0 :: (~>) (Proxy a) ((~>) (Proxy b) (Foo a b)) where MkFooSym0KindInference :: SameKind (Apply MkFooSym0 arg) (MkFooSym1 arg) => MkFooSym0 a0123456789876543210 @@ -85,8 +76,8 @@ Singletons/T353.hs:0:0:: Splicing declarations instance SuppressUnusedWarnings MkFooSym0 where suppressUnusedWarnings = snd ((,) MkFooSym0KindInference ()) type MkFooSym1 :: forall k k (a :: k) (b :: k). Proxy a - -> (~>) (Proxy b) (Foo (a :: k) (b :: k)) - data MkFooSym1 (a0123456789876543210 :: Proxy a) :: (~>) (Proxy b) (Foo (a :: k) (b :: k)) + -> (~>) (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 @@ -94,6 +85,6 @@ Singletons/T353.hs:0:0:: Splicing declarations instance SuppressUnusedWarnings (MkFooSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) MkFooSym1KindInference ()) type MkFooSym2 :: forall k k (a :: k) (b :: k). Proxy a - -> Proxy b -> Foo (a :: k) (b :: k) - type family MkFooSym2 (a0123456789876543210 :: Proxy a) (a0123456789876543210 :: Proxy b) :: Foo (a :: k) (b :: k) where + -> Proxy b -> Foo a b + type family MkFooSym2 (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/T371.golden b/singletons-base/tests/compile-and-dump/Singletons/T371.golden index deb6c788..c0799cf9 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T371.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T371.golden @@ -13,33 +13,33 @@ Singletons/T371.hs:(0,0)-(0,0): Splicing declarations data Y (a :: Type) = Y1 | Y2 (X a) deriving Show - type X1Sym0 :: forall (a :: Type). X (a :: Type) - type family X1Sym0 :: X (a :: Type) where + type X1Sym0 :: forall (a :: Type). X a + type family X1Sym0 :: X a where X1Sym0 = X1 - type X2Sym0 :: forall (a :: Type). (~>) (Y a) (X (a :: Type)) - data X2Sym0 :: (~>) (Y a) (X (a :: Type)) + type X2Sym0 :: forall (a :: Type). (~>) (Y a) (X a) + data X2Sym0 :: (~>) (Y a) (X a) where X2Sym0KindInference :: SameKind (Apply X2Sym0 arg) (X2Sym1 arg) => X2Sym0 a0123456789876543210 type instance Apply X2Sym0 a0123456789876543210 = X2 a0123456789876543210 instance SuppressUnusedWarnings X2Sym0 where suppressUnusedWarnings = snd ((,) X2Sym0KindInference ()) - type X2Sym1 :: forall (a :: Type). Y a -> X (a :: Type) - type family X2Sym1 (a0123456789876543210 :: Y a) :: X (a :: Type) where + type X2Sym1 :: forall (a :: Type). Y a -> X a + type family X2Sym1 (a0123456789876543210 :: Y a) :: X a where X2Sym1 a0123456789876543210 = X2 a0123456789876543210 - type Y1Sym0 :: forall (a :: Type). Y (a :: Type) - type family Y1Sym0 :: Y (a :: Type) where + type Y1Sym0 :: forall (a :: Type). Y a + type family Y1Sym0 :: Y a where Y1Sym0 = Y1 - type Y2Sym0 :: forall (a :: Type). (~>) (X a) (Y (a :: Type)) - data Y2Sym0 :: (~>) (X a) (Y (a :: Type)) + type Y2Sym0 :: forall (a :: Type). (~>) (X a) (Y a) + data Y2Sym0 :: (~>) (X a) (Y a) where Y2Sym0KindInference :: SameKind (Apply Y2Sym0 arg) (Y2Sym1 arg) => Y2Sym0 a0123456789876543210 type instance Apply Y2Sym0 a0123456789876543210 = Y2 a0123456789876543210 instance SuppressUnusedWarnings Y2Sym0 where suppressUnusedWarnings = snd ((,) Y2Sym0KindInference ()) - type Y2Sym1 :: forall (a :: Type). X a -> Y (a :: Type) - type family Y2Sym1 (a0123456789876543210 :: X a) :: Y (a :: Type) where + type Y2Sym1 :: forall (a :: Type). X a -> Y a + type family Y2Sym1 (a0123456789876543210 :: X a) :: Y a where Y2Sym1 a0123456789876543210 = Y2 a0123456789876543210 type ShowsPrec_0123456789876543210 :: GHC.Num.Natural.Natural -> X a -> GHC.Types.Symbol -> GHC.Types.Symbol @@ -123,9 +123,8 @@ Singletons/T371.hs:(0,0)-(0,0): Splicing declarations type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a data SX :: forall (a :: Type). X a -> Type where - SX1 :: forall (a :: Type). SX (X1 :: X (a :: Type)) - SX2 :: forall (a :: Type) (n :: Y a). - (Sing n) -> SX (X2 n :: X (a :: Type)) + SX1 :: forall (a :: Type). SX (X1 :: X a) + SX2 :: forall (a :: Type) (n :: Y a). (Sing n) -> SX (X2 n :: X a) type instance Sing @(X a) = SX instance SingKind a => SingKind (X a) where type Demote (X a) = X (Demote a) @@ -136,9 +135,8 @@ Singletons/T371.hs:(0,0)-(0,0): Splicing declarations = case toSing b :: SomeSing (Y a) of SomeSing c -> SomeSing (SX2 c) data SY :: forall (a :: Type). Y a -> Type where - SY1 :: forall (a :: Type). SY (Y1 :: Y (a :: Type)) - SY2 :: forall (a :: Type) (n :: X a). - (Sing n) -> SY (Y2 n :: Y (a :: Type)) + SY1 :: forall (a :: Type). SY (Y1 :: Y a) + SY2 :: forall (a :: Type) (n :: X a). (Sing n) -> SY (Y2 n :: Y a) type instance Sing @(Y a) = SY instance SingKind a => SingKind (Y a) where type Demote (Y a) = Y (Demote a) @@ -235,7 +233,7 @@ Singletons/T371.hs:(0,0)-(0,0): Splicing declarations sing = SX2 sing instance SingI1 X2 where liftSing = SX2 - instance SingI (X2Sym0 :: (~>) (Y a) (X (a :: Type))) where + instance SingI (X2Sym0 :: (~>) (Y a) (X a)) where sing = singFun1 @X2Sym0 SX2 instance SingI Y1 where sing = SY1 @@ -243,5 +241,5 @@ Singletons/T371.hs:(0,0)-(0,0): Splicing declarations sing = SY2 sing instance SingI1 Y2 where liftSing = SY2 - instance SingI (Y2Sym0 :: (~>) (X a) (Y (a :: Type))) where + instance SingI (Y2Sym0 :: (~>) (X a) (Y a)) where sing = singFun1 @Y2Sym0 SY2 diff --git a/singletons-base/tests/compile-and-dump/Singletons/T412.golden b/singletons-base/tests/compile-and-dump/Singletons/T412.golden index ac718d4c..a82f6e43 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T412.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T412.golden @@ -288,8 +288,8 @@ Singletons/T412.hs:0:0:: Splicing declarations T2bSym2 a0123456789876543210 a0123456789876543210 = T2b a0123456789876543210 a0123456789876543210 infixl 5 `T2bSym2` type MkD2Sym0 :: forall (a :: Type) - (b :: Type). (~>) a ((~>) b (D2 (a :: Type) (b :: Type))) - data MkD2Sym0 :: (~>) a ((~>) b (D2 (a :: Type) (b :: Type))) + (b :: Type). (~>) a ((~>) b (D2 a b)) + data MkD2Sym0 :: (~>) a ((~>) b (D2 a b)) where MkD2Sym0KindInference :: SameKind (Apply MkD2Sym0 arg) (MkD2Sym1 arg) => MkD2Sym0 a0123456789876543210 @@ -298,8 +298,8 @@ Singletons/T412.hs:0:0:: Splicing declarations suppressUnusedWarnings = snd ((,) MkD2Sym0KindInference ()) infixr 5 `MkD2Sym0` type MkD2Sym1 :: forall (a :: Type) (b :: Type). a - -> (~>) b (D2 (a :: Type) (b :: Type)) - data MkD2Sym1 (a0123456789876543210 :: a) :: (~>) b (D2 (a :: Type) (b :: Type)) + -> (~>) b (D2 a b) + data MkD2Sym1 (a0123456789876543210 :: a) :: (~>) b (D2 a b) where MkD2Sym1KindInference :: SameKind (Apply (MkD2Sym1 a0123456789876543210) arg) (MkD2Sym2 a0123456789876543210 arg) => MkD2Sym1 a0123456789876543210 a0123456789876543210 @@ -307,70 +307,57 @@ Singletons/T412.hs:0:0:: Splicing declarations instance SuppressUnusedWarnings (MkD2Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) MkD2Sym1KindInference ()) infixr 5 `MkD2Sym1` - type MkD2Sym2 :: forall (a :: Type) (b :: Type). a - -> b -> D2 (a :: Type) (b :: Type) - type family MkD2Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: D2 (a :: Type) (b :: Type) where + type MkD2Sym2 :: forall (a :: Type) (b :: Type). a -> b -> D2 a b + type family MkD2Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: D2 a b where MkD2Sym2 a0123456789876543210 a0123456789876543210 = 'MkD2 a0123456789876543210 a0123456789876543210 infixr 5 `MkD2Sym2` infixr 5 `D2A` infixr 5 `D2B` - type D2BSym0 :: forall (a :: Type) - (b :: Type). (~>) (D2 (a :: Type) (b :: Type)) b - data D2BSym0 :: (~>) (D2 (a :: Type) (b :: Type)) b + type D2BSym0 :: forall (a :: Type) (b :: Type). (~>) (D2 a b) b + data D2BSym0 :: (~>) (D2 a b) b where D2BSym0KindInference :: SameKind (Apply D2BSym0 arg) (D2BSym1 arg) => D2BSym0 a0123456789876543210 type instance Apply D2BSym0 a0123456789876543210 = D2B a0123456789876543210 instance SuppressUnusedWarnings D2BSym0 where suppressUnusedWarnings = snd ((,) D2BSym0KindInference ()) - type D2BSym1 :: forall (a :: Type) - (b :: Type). D2 (a :: Type) (b :: Type) -> b - type family D2BSym1 (a0123456789876543210 :: D2 (a :: Type) (b :: Type)) :: b where + type D2BSym1 :: forall (a :: Type) (b :: Type). D2 a b -> b + type family D2BSym1 (a0123456789876543210 :: D2 a b) :: b where D2BSym1 a0123456789876543210 = D2B a0123456789876543210 - type D2ASym0 :: forall (a :: Type) - (b :: Type). (~>) (D2 (a :: Type) (b :: Type)) a - data D2ASym0 :: (~>) (D2 (a :: Type) (b :: Type)) a + type D2ASym0 :: forall (a :: Type) (b :: Type). (~>) (D2 a b) a + data D2ASym0 :: (~>) (D2 a b) a where D2ASym0KindInference :: SameKind (Apply D2ASym0 arg) (D2ASym1 arg) => D2ASym0 a0123456789876543210 type instance Apply D2ASym0 a0123456789876543210 = D2A a0123456789876543210 instance SuppressUnusedWarnings D2ASym0 where suppressUnusedWarnings = snd ((,) D2ASym0KindInference ()) - type D2ASym1 :: forall (a :: Type) - (b :: Type). D2 (a :: Type) (b :: Type) -> a - type family D2ASym1 (a0123456789876543210 :: D2 (a :: Type) (b :: Type)) :: a where + type D2ASym1 :: forall (a :: Type) (b :: Type). D2 a b -> a + type family D2ASym1 (a0123456789876543210 :: D2 a b) :: a where D2ASym1 a0123456789876543210 = D2A a0123456789876543210 - type D2B :: forall (a :: Type) - (b :: Type). D2 (a :: Type) (b :: Type) -> b - type family D2B (a :: D2 (a :: Type) (b :: Type)) :: b where - D2B @a @b ('MkD2 _ field :: D2 (a :: Type) (b :: Type)) = field - type D2A :: forall (a :: Type) - (b :: Type). D2 (a :: Type) (b :: Type) -> a - type family D2A (a :: D2 (a :: Type) (b :: Type)) :: a where - D2A @a @b ('MkD2 field _ :: D2 (a :: Type) (b :: Type)) = field + type D2B :: forall (a :: Type) (b :: Type). D2 a b -> b + type family D2B (a :: D2 a b) :: b where + D2B @a @b ('MkD2 _ field :: D2 a b) = field + type D2A :: forall (a :: Type) (b :: Type). D2 a b -> a + type family D2A (a :: D2 a b) :: a where + D2A @a @b ('MkD2 field _ :: D2 a b) = field sD2B :: - forall (a :: Type) - (b :: Type) - (t :: D2 (a :: Type) (b :: Type)). Sing t - -> Sing (Apply D2BSym0 t :: b) + forall (a :: Type) (b :: Type) (t :: D2 a b). Sing t + -> Sing (Apply D2BSym0 t :: b) sD2A :: - forall (a :: Type) - (b :: Type) - (t :: D2 (a :: Type) (b :: Type)). Sing t - -> Sing (Apply D2ASym0 t :: a) + forall (a :: Type) (b :: Type) (t :: D2 a b). Sing t + -> Sing (Apply D2ASym0 t :: a) sD2B (SMkD2 _ (sField :: Sing field)) = sField sD2A (SMkD2 (sField :: Sing field) _) = sField - instance SingI (D2BSym0 :: (~>) (D2 (a :: Type) (b :: Type)) b) where + instance SingI (D2BSym0 :: (~>) (D2 a b) b) where sing = singFun1 @D2BSym0 sD2B - instance SingI (D2ASym0 :: (~>) (D2 (a :: Type) (b :: Type)) a) where + instance SingI (D2ASym0 :: (~>) (D2 a b) a) where sing = singFun1 @D2ASym0 sD2A type SD2 :: forall (a :: Type) (b :: Type). D2 a b -> Type data SD2 :: forall (a :: Type) (b :: Type). D2 a b -> Type where SMkD2 :: forall (a :: Type) (b :: Type) (n :: a) (n :: b). - (Sing n) -> - (Sing n) -> - SD2 ('MkD2 n n :: D2 (a :: Type) (b :: Type)) + (Sing n) -> (Sing n) -> SD2 ('MkD2 n n :: D2 a b) type instance Sing @(D2 a b) = SD2 instance (SingKind a, SingKind b) => SingKind (D2 a b) where type Demote (D2 a b) = D2 (Demote a) (Demote b) @@ -388,12 +375,11 @@ Singletons/T412.hs:0:0:: Splicing declarations liftSing = SMkD2 sing instance SingI2 'MkD2 where liftSing2 = SMkD2 - instance SingI (MkD2Sym0 :: (~>) a ((~>) b (D2 (a :: Type) (b :: Type)))) where + instance SingI (MkD2Sym0 :: (~>) a ((~>) b (D2 a b))) where sing = singFun2 @MkD2Sym0 SMkD2 instance SingI d => - SingI (MkD2Sym1 (d :: a) :: (~>) b (D2 (a :: Type) (b :: Type))) where + SingI (MkD2Sym1 (d :: a) :: (~>) b (D2 a b)) where sing = singFun1 @(MkD2Sym1 (d :: a)) (SMkD2 (sing @d)) - instance SingI1 (MkD2Sym1 :: a - -> (~>) b (D2 (a :: Type) (b :: Type))) where + instance SingI1 (MkD2Sym1 :: a -> (~>) b (D2 a b)) where liftSing (s :: Sing (d :: a)) = singFun1 @(MkD2Sym1 (d :: a)) (SMkD2 s) diff --git a/singletons-base/tests/compile-and-dump/Singletons/T450.golden b/singletons-base/tests/compile-and-dump/Singletons/T450.golden index 60182b9f..2d6296c4 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T450.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T450.golden @@ -118,8 +118,8 @@ Singletons/T450.hs:(0,0)-(0,0): Splicing declarations liftSing (s :: Sing (d :: PMessage)) = singFun1 @(AppendMessageSym1 (d :: PMessage)) (sAppendMessage s) type PMkFunctionSym0 :: forall (a :: Type) - (b :: Type). (~>) ((~>) a b) (PFunction (a :: Type) (b :: Type)) - data PMkFunctionSym0 :: (~>) ((~>) a b) (PFunction (a :: Type) (b :: Type)) + (b :: Type). (~>) ((~>) a b) (PFunction a b) + data PMkFunctionSym0 :: (~>) ((~>) a b) (PFunction a b) where PMkFunctionSym0KindInference :: SameKind (Apply PMkFunctionSym0 arg) (PMkFunctionSym1 arg) => PMkFunctionSym0 a0123456789876543210 @@ -127,8 +127,8 @@ Singletons/T450.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings PMkFunctionSym0 where suppressUnusedWarnings = snd ((,) PMkFunctionSym0KindInference ()) type PMkFunctionSym1 :: forall (a :: Type) (b :: Type). (~>) a b - -> PFunction (a :: Type) (b :: Type) - type family PMkFunctionSym1 (a0123456789876543210 :: (~>) a b) :: PFunction (a :: Type) (b :: Type) where + -> PFunction a b + type family PMkFunctionSym1 (a0123456789876543210 :: (~>) a b) :: PFunction a b where PMkFunctionSym1 a0123456789876543210 = 'PMkFunction a0123456789876543210 type SFunction :: forall (a :: Type) (b :: Type). PFunction a b -> Type @@ -136,8 +136,7 @@ Singletons/T450.hs:(0,0)-(0,0): Splicing declarations PFunction a b -> Type where SMkFunction :: forall (a :: Type) (b :: Type) (n :: (~>) a b). - (Sing n) -> - SFunction ('PMkFunction n :: PFunction (a :: Type) (b :: Type)) + (Sing n) -> SFunction ('PMkFunction n :: PFunction a b) type instance Sing @(PFunction a b) = SFunction instance (SingKind a, SingKind b) => SingKind (PFunction a b) where type Demote (PFunction a b) = Function (Demote a) (Demote b) @@ -149,7 +148,7 @@ Singletons/T450.hs:(0,0)-(0,0): Splicing declarations sing = SMkFunction sing instance SingI1 'PMkFunction where liftSing = SMkFunction - instance SingI (PMkFunctionSym0 :: (~>) ((~>) a b) (PFunction (a :: Type) (b :: Type))) where + instance SingI (PMkFunctionSym0 :: (~>) ((~>) a b) (PFunction a b)) where sing = singFun1 @PMkFunctionSym0 SMkFunction composeFunction :: Function b c -> Function a b -> Function a c composeFunction diff --git a/singletons-base/tests/compile-and-dump/Singletons/T567.golden b/singletons-base/tests/compile-and-dump/Singletons/T567.golden index 02f91f57..6e2fca69 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T567.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T567.golden @@ -22,16 +22,14 @@ Singletons/T567.hs:(0,0)-(0,0): Splicing declarations type MkD1Sym0 :: forall x p. D1 x p type family MkD1Sym0 :: D1 x p where MkD1Sym0 = MkD1 - type MkD2Sym0 :: forall j (x :: j) p. D2 (x :: j) p - type family MkD2Sym0 :: D2 (x :: j) p where + type MkD2Sym0 :: forall j (x :: j) p. D2 x p + type family MkD2Sym0 :: D2 x p where MkD2Sym0 = MkD2 - type MkD3Sym0 :: forall x (p :: Proxy x). D3 x (p :: Proxy x) - type family MkD3Sym0 :: D3 x (p :: Proxy x) where + type MkD3Sym0 :: forall x (p :: Proxy x). D3 x p + type family MkD3Sym0 :: D3 x p where MkD3Sym0 = MkD3 - type MkD4Sym0 :: forall j - (x :: j) - (p :: Proxy x). D4 (x :: j) (p :: Proxy x) - type family MkD4Sym0 :: D4 (x :: j) (p :: Proxy x) where + type MkD4Sym0 :: forall j (x :: j) (p :: Proxy x). D4 x p + type family MkD4Sym0 :: 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 @@ -39,18 +37,16 @@ Singletons/T567.hs:(0,0)-(0,0): Splicing declarations 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 :: j) p) + where SMkD2 :: forall j (x :: j) p. 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 :: Proxy x)) + where SMkD3 :: forall x (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 where - SMkD4 :: forall j (x :: j) (p :: Proxy x). - SD4 (MkD4 :: D4 (x :: j) (p :: Proxy x)) + SMkD4 :: forall j (x :: j) (p :: Proxy x). SD4 (MkD4 :: D4 x p) type instance Sing @(D4 x p) = SD4 instance SingI MkD1 where sing = SMkD1 diff --git a/singletons-th/singletons-th.cabal b/singletons-th/singletons-th.cabal index fbfc87d3..93dab2ba 100644 --- a/singletons-th/singletons-th.cabal +++ b/singletons-th/singletons-th.cabal @@ -59,7 +59,7 @@ library singletons == 3.0.*, syb >= 0.4, template-haskell >= 2.20 && < 2.21, - th-desugar >= 1.15 && < 1.16, + th-desugar >= 1.16 && < 1.17, th-orphans >= 0.13.11 && < 0.14, transformers >= 0.5.2 default-language: GHC2021 diff --git a/singletons-th/src/Data/Singletons/TH/Promote.hs b/singletons-th/src/Data/Singletons/TH/Promote.hs index 69d454f2..5627ada6 100644 --- a/singletons-th/src/Data/Singletons/TH/Promote.hs +++ b/singletons-th/src/Data/Singletons/TH/Promote.hs @@ -1087,6 +1087,8 @@ promoteExp (DSigE exp ty) = do ty' <- promoteType ty return (DSigT exp' ty', ADSigE exp' ann_exp ty') promoteExp e@(DStaticE _) = fail ("Static expressions cannot be promoted: " ++ show e) +promoteExp e@(DTypedBracketE _) = fail ("Typed bracket expressions cannot be promoted: " ++ show e) +promoteExp e@(DTypedSpliceE _) = fail ("Typed splice expressions cannot be promoted: " ++ show e) promoteLitExp :: OptionsMonad q => Lit -> q DType promoteLitExp (IntegerL n) = do diff --git a/singletons-th/src/Data/Singletons/TH/Single.hs b/singletons-th/src/Data/Singletons/TH/Single.hs index e69fae8f..b7cf9994 100644 --- a/singletons-th/src/Data/Singletons/TH/Single.hs +++ b/singletons-th/src/Data/Singletons/TH/Single.hs @@ -994,6 +994,8 @@ isException (DCaseE e _) = isException e isException (DLetE _ e) = isException e isException (DSigE e _) = isException e isException (DStaticE e) = isException e +isException (DTypedBracketE e) = isException e +isException (DTypedSpliceE e) = isException e singMatch :: ADMatch -> SgM DMatch singMatch (ADMatch var_proms pat exp) = do