From 467a9af318a48e68b954c8393f75b865cc1d387d Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sun, 21 Aug 2022 18:55:30 -0400 Subject: [PATCH] singletons-{th,base}: Require building with GHC 9.4 This patch: * Allows `singletons` to build with GHC 9.4 * Requires `singletons-th` and `singletons-base` to build with GHC 9.4 * Updates the golden tests accordingly --- .github/workflows/haskell-ci.yml | 57 +++---- README.md | 2 +- cabal.haskell-ci | 2 + cabal.project | 2 +- singletons-base/CHANGES.md | 4 + singletons-base/README.md | 2 +- singletons-base/singletons-base.cabal | 20 +-- .../Singletons/AsPattern.golden | 2 +- .../Singletons/BoxUnBox.golden | 2 +- .../Singletons/Classes.golden | 10 +- .../Singletons/Classes2.golden | 4 +- .../Singletons/DataValues.golden | 4 +- .../compile-and-dump/Singletons/Empty.golden | 2 +- .../Singletons/EmptyShowDeriving.golden | 4 +- .../Singletons/EnumDeriving.golden | 12 +- .../Singletons/EqInstances.golden | 4 +- .../Singletons/FunctorLikeDeriving.golden | 10 +- .../Singletons/HigherOrder.golden | 2 +- .../Singletons/Lambdas.golden | 2 +- .../compile-and-dump/Singletons/Maybe.golden | 12 +- .../compile-and-dump/Singletons/Nat.golden | 14 +- .../Singletons/Natural.golden | 2 +- .../Singletons/Operators.golden | 2 +- .../Singletons/OrdDeriving.golden | 84 +++++------ .../Singletons/PatternMatching.golden | 4 +- .../Singletons/Records.golden | 2 +- .../Singletons/ShowDeriving.golden | 13 +- .../Singletons/StandaloneDeriving.golden | 32 ++-- .../compile-and-dump/Singletons/T136.golden | 10 +- .../compile-and-dump/Singletons/T136b.golden | 2 +- .../compile-and-dump/Singletons/T159.golden | 10 +- .../compile-and-dump/Singletons/T163.golden | 2 +- .../compile-and-dump/Singletons/T178.golden | 12 +- .../compile-and-dump/Singletons/T187.golden | 10 +- .../compile-and-dump/Singletons/T190.golden | 18 +-- .../compile-and-dump/Singletons/T197b.golden | 4 +- .../compile-and-dump/Singletons/T200.golden | 2 +- .../compile-and-dump/Singletons/T209.golden | 2 +- .../compile-and-dump/Singletons/T271.golden | 4 +- .../compile-and-dump/Singletons/T326.golden | 12 +- .../compile-and-dump/Singletons/T33.golden | 4 +- .../compile-and-dump/Singletons/T332.golden | 3 +- .../compile-and-dump/Singletons/T412.golden | 140 ++++++++---------- .../compile-and-dump/Singletons/T450.golden | 36 ++--- .../Singletons/TopLevelPatterns.golden | 4 +- singletons-th/CHANGES.md | 6 + singletons-th/README.md | 2 +- singletons-th/singletons-th.cabal | 14 +- singletons/CHANGES.md | 8 + singletons/singletons.cabal | 11 +- 50 files changed, 309 insertions(+), 319 deletions(-) diff --git a/.github/workflows/haskell-ci.yml b/.github/workflows/haskell-ci.yml index b796abbc..fd683ac9 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.13.20211116 +# version: 0.15.20220822 # -# REGENDATA ("0.13.20211116",["github","cabal.project"]) +# REGENDATA ("0.15.20220822",["github","cabal.project"]) # name: Haskell-CI on: @@ -19,7 +19,7 @@ on: jobs: linux: name: Haskell-CI - Linux - ${{ matrix.compiler }} - runs-on: ubuntu-18.04 + runs-on: ubuntu-20.04 timeout-minutes: 60 container: @@ -33,15 +33,20 @@ jobs: compilerVersion: "8.4" setup-method: hvr-ppa allow-failure: false - - compiler: ghc-9.2.1 + - compiler: ghc-9.4.1 compilerKind: ghc - compilerVersion: 9.2.1 + compilerVersion: 9.4.1 setup-method: ghcup allow-failure: false - - compiler: ghc-9.0.1 + - compiler: ghc-9.2.4 compilerKind: ghc - compilerVersion: 9.0.1 - setup-method: hvr-ppa + compilerVersion: 9.2.4 + setup-method: ghcup + allow-failure: false + - compiler: ghc-9.0.2 + compilerKind: ghc + compilerVersion: 9.0.2 + setup-method: ghcup allow-failure: false - compiler: ghc-8.10.7 compilerKind: ghc @@ -94,10 +99,10 @@ jobs: apt-get install -y --no-install-recommends gnupg ca-certificates dirmngr curl git software-properties-common libtinfo5 if [ "${{ matrix.setup-method }}" = ghcup ]; then mkdir -p "$HOME/.ghcup/bin" - curl -sL https://downloads.haskell.org/ghcup/0.1.17.3/x86_64-linux-ghcup-0.1.17.3 > "$HOME/.ghcup/bin/ghcup" + curl -sL https://downloads.haskell.org/ghcup/0.1.18.0/x86_64-linux-ghcup-0.1.18.0 > "$HOME/.ghcup/bin/ghcup" chmod a+x "$HOME/.ghcup/bin/ghcup" - "$HOME/.ghcup/bin/ghcup" install ghc "$HCVER" - "$HOME/.ghcup/bin/ghcup" install cabal 3.6.2.0 + "$HOME/.ghcup/bin/ghcup" install ghc "$HCVER" || (cat "$HOME"/.ghcup/logs/*.* && false) + "$HOME/.ghcup/bin/ghcup" install cabal 3.6.2.0 || (cat "$HOME"/.ghcup/logs/*.* && false) else apt-add-repository -y 'ppa:hvr/ghc' if [ $((GHCJSARITH)) -ne 0 ] ; then apt-add-repository -y 'ppa:hvr/ghcjs' ; fi @@ -106,9 +111,9 @@ jobs: apt-get update if [ $((GHCJSARITH)) -ne 0 ] ; then apt-get install -y "$HCNAME" ghc-8.4.4 nodejs ; else apt-get install -y "$HCNAME" ; fi mkdir -p "$HOME/.ghcup/bin" - curl -sL https://downloads.haskell.org/ghcup/0.1.17.3/x86_64-linux-ghcup-0.1.17.3 > "$HOME/.ghcup/bin/ghcup" + curl -sL https://downloads.haskell.org/ghcup/0.1.18.0/x86_64-linux-ghcup-0.1.18.0 > "$HOME/.ghcup/bin/ghcup" chmod a+x "$HOME/.ghcup/bin/ghcup" - "$HOME/.ghcup/bin/ghcup" install cabal 3.6.2.0 + "$HOME/.ghcup/bin/ghcup" install cabal 3.6.2.0 || (cat "$HOME"/.ghcup/logs/*.* && false) fi env: HCKIND: ${{ matrix.compilerKind }} @@ -200,8 +205,8 @@ jobs: run: | touch cabal.project echo "packages: $GITHUB_WORKSPACE/source/./singletons" >> cabal.project - if [ $((! GHCJSARITH && HCNUMVER >= 90200)) -ne 0 ] ; then echo "packages: $GITHUB_WORKSPACE/source/./singletons-th" >> cabal.project ; fi - if [ $((! GHCJSARITH && HCNUMVER >= 90200)) -ne 0 ] ; then echo "packages: $GITHUB_WORKSPACE/source/./singletons-base" >> cabal.project ; fi + if [ $((! GHCJSARITH && HCNUMVER >= 90400)) -ne 0 ] ; then echo "packages: $GITHUB_WORKSPACE/source/./singletons-th" >> cabal.project ; fi + if [ $((! GHCJSARITH && HCNUMVER >= 90400)) -ne 0 ] ; then echo "packages: $GITHUB_WORKSPACE/source/./singletons-base" >> cabal.project ; fi cat cabal.project - name: sdist run: | @@ -223,19 +228,19 @@ jobs: touch cabal.project touch cabal.project.local echo "packages: ${PKGDIR_singletons}" >> cabal.project - if [ $((! GHCJSARITH && HCNUMVER >= 90200)) -ne 0 ] ; then echo "packages: ${PKGDIR_singletons_th}" >> cabal.project ; fi - if [ $((! GHCJSARITH && HCNUMVER >= 90200)) -ne 0 ] ; then echo "packages: ${PKGDIR_singletons_base}" >> cabal.project ; fi + if [ $((! GHCJSARITH && HCNUMVER >= 90400)) -ne 0 ] ; then echo "packages: ${PKGDIR_singletons_th}" >> cabal.project ; fi + if [ $((! GHCJSARITH && HCNUMVER >= 90400)) -ne 0 ] ; then echo "packages: ${PKGDIR_singletons_base}" >> cabal.project ; fi if [ $((GHCJSARITH || ! GHCJSARITH && HCNUMVER >= 80200)) -ne 0 ] ; then echo "package singletons" >> cabal.project ; fi if [ $((GHCJSARITH || ! GHCJSARITH && HCNUMVER >= 80200)) -ne 0 ] ; then echo " ghc-options: -Werror=missing-methods" >> cabal.project ; fi - if [ $((! GHCJSARITH && HCNUMVER >= 90200)) -ne 0 ] ; then echo "package singletons-th" >> cabal.project ; fi - if [ $((! GHCJSARITH && HCNUMVER >= 90200)) -ne 0 ] ; then echo " ghc-options: -Werror=missing-methods" >> cabal.project ; fi - if [ $((! GHCJSARITH && HCNUMVER >= 90200)) -ne 0 ] ; then echo "package singletons-base" >> cabal.project ; fi - if [ $((! GHCJSARITH && HCNUMVER >= 90200)) -ne 0 ] ; then echo " ghc-options: -Werror=missing-methods" >> cabal.project ; fi + if [ $((! GHCJSARITH && HCNUMVER >= 90400)) -ne 0 ] ; then echo "package singletons-th" >> cabal.project ; fi + if [ $((! GHCJSARITH && HCNUMVER >= 90400)) -ne 0 ] ; then echo " ghc-options: -Werror=missing-methods" >> cabal.project ; fi + if [ $((! GHCJSARITH && HCNUMVER >= 90400)) -ne 0 ] ; then echo "package singletons-base" >> cabal.project ; fi + if [ $((! GHCJSARITH && HCNUMVER >= 90400)) -ne 0 ] ; then echo " ghc-options: -Werror=missing-methods" >> cabal.project ; fi cat >> cabal.project <> cabal.project.local cat cabal.project @@ -264,10 +269,10 @@ jobs: run: | cd ${PKGDIR_singletons} || false ${CABAL} -vnormal check - if [ $((! GHCJSARITH && HCNUMVER >= 90200)) -ne 0 ] ; then cd ${PKGDIR_singletons_th} || false ; fi - if [ $((! GHCJSARITH && HCNUMVER >= 90200)) -ne 0 ] ; then ${CABAL} -vnormal check ; fi - if [ $((! GHCJSARITH && HCNUMVER >= 90200)) -ne 0 ] ; then cd ${PKGDIR_singletons_base} || false ; fi - if [ $((! GHCJSARITH && HCNUMVER >= 90200)) -ne 0 ] ; then ${CABAL} -vnormal check ; fi + if [ $((! GHCJSARITH && HCNUMVER >= 90400)) -ne 0 ] ; then cd ${PKGDIR_singletons_th} || false ; fi + if [ $((! GHCJSARITH && HCNUMVER >= 90400)) -ne 0 ] ; then ${CABAL} -vnormal check ; fi + if [ $((! GHCJSARITH && HCNUMVER >= 90400)) -ne 0 ] ; then cd ${PKGDIR_singletons_base} || false ; fi + if [ $((! GHCJSARITH && HCNUMVER >= 90400)) -ne 0 ] ; then ${CABAL} -vnormal check ; fi - name: haddock run: | if [ $((! GHCJSARITH)) -ne 0 ] ; then $CABAL v2-haddock $ARG_COMPILER --with-haddock $HADDOCK $ARG_TESTS $ARG_BENCH all ; fi diff --git a/README.md b/README.md index f22f81f5..76ca7d38 100644 --- a/README.md +++ b/README.md @@ -65,7 +65,7 @@ windows for requirements on the compiler version needed to build each library: GHC language extensions, even more so than `singletons` itself. As such, it is difficult to maintain support for multiple GHC versions in any given release of either library, so they only support the latest major GHC version - (currently GHC 9.2). + (currently GHC 9.4). Any code that uses the singleton-generation functionality from `singletons-th` or `singletons-base` needs to enable a long list of GHC extensions. This list diff --git a/cabal.haskell-ci b/cabal.haskell-ci index de706a50..0f5a9817 100644 --- a/cabal.haskell-ci +++ b/cabal.haskell-ci @@ -2,3 +2,5 @@ distribution: bionic no-tests-no-benchmarks: False unconstrained: False jobs-selection: any +-- Needed to avoid https://github.com/haskell/cabal/issues/5423 +haddock-components: libs diff --git a/cabal.project b/cabal.project index 918a7e83..e171fd22 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: b2b9db81d26dc767e7eb4481b7f20cfae6fa0eda + tag: b64e24b67c91991f5d9b97b055d05693fd99cb9b diff --git a/singletons-base/CHANGES.md b/singletons-base/CHANGES.md index 33398fb5..33934c5b 100644 --- a/singletons-base/CHANGES.md +++ b/singletons-base/CHANGES.md @@ -1,6 +1,10 @@ Changelog for the `singletons-base` project =========================================== +3.1.1 [????.??.??] +------------------ +* Require building with GHC 9.4. + 3.1 [2021.10.30] ---------------- * Require building with GHC 9.2. diff --git a/singletons-base/README.md b/singletons-base/README.md index 3239cedc..7ce1beff 100644 --- a/singletons-base/README.md +++ b/singletons-base/README.md @@ -18,7 +18,7 @@ that code with `singletons-base`. `singletons-base` uses code that relies on bleeding-edge GHC language extensions. As such, `singletons-base` only supports the latest major version -of GHC (currently GHC 9.2). For more information, +of GHC (currently GHC 9.4). For more information, consult the `singletons` [`README`](https://github.com/goldfirere/singletons/blob/master/README.md). diff --git a/singletons-base/singletons-base.cabal b/singletons-base/singletons-base.cabal index 064bdd47..32efa51f 100644 --- a/singletons-base/singletons-base.cabal +++ b/singletons-base/singletons-base.cabal @@ -1,5 +1,5 @@ name: singletons-base -version: 3.1 +version: 3.1.1 cabal-version: 1.24 synopsis: A promoted and singled version of the base library homepage: http://www.github.com/goldfirere/singletons @@ -8,7 +8,7 @@ author: Richard Eisenberg , Jan Stolarek bug-reports: https://github.com/goldfirere/singletons/issues stability: experimental -tested-with: GHC == 9.2.1 +tested-with: GHC == 9.4.1 extra-source-files: README.md, CHANGES.md, tests/README.md, tests/compile-and-dump/GradingClient/*.hs, tests/compile-and-dump/InsertionSort/*.hs, @@ -38,7 +38,7 @@ description: . @singletons-base@ uses code that relies on bleeding-edge GHC language extensions. As such, @singletons-base@ only supports the latest major version - of GHC (currently GHC 9.2). For more information, + of GHC (currently GHC 9.4). For more information, consult the @singletons@ @@. . @@ -65,20 +65,20 @@ source-repository head custom-setup setup-depends: - base >= 4.16 && < 4.17, - Cabal >= 3.0 && < 3.7, + base >= 4.17 && < 4.18, + Cabal >= 3.0 && < 3.9, directory >= 1, filepath >= 1.3 library hs-source-dirs: src - build-depends: base >= 4.16 && < 4.17, + build-depends: base >= 4.17 && < 4.18, pretty, - singletons == 3.0.1, + singletons == 3.0.*, singletons-th == 3.1.*, - template-haskell >= 2.18 && < 2.19, + template-haskell >= 2.19 && < 2.20, text >= 1.2, - th-desugar >= 1.13 && < 1.14 + th-desugar >= 1.14 && < 1.15 default-language: GHC2021 other-extensions: TemplateHaskell exposed-modules: Data.Singletons.Base.CustomStar @@ -153,7 +153,7 @@ test-suite singletons-base-test-suite main-is: SingletonsBaseTestSuite.hs other-modules: SingletonsBaseTestSuiteUtils - build-depends: base >= 4.16 && < 4.17, + build-depends: base >= 4.17 && < 4.18, bytestring >= 0.10.9, deepseq >= 1.4.4, filepath >= 1.3, diff --git a/singletons-base/tests/compile-and-dump/Singletons/AsPattern.golden b/singletons-base/tests/compile-and-dump/Singletons/AsPattern.golden index 89d99b1b..4d8cb09b 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/AsPattern.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/AsPattern.golden @@ -360,7 +360,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations sing = (singFun1 @BarSym0) sBar instance SingI (MaybePlusSym0 :: (~>) (Maybe Nat) (Maybe Nat)) where sing = (singFun1 @MaybePlusSym0) sMaybePlus - data SBaz :: Baz -> GHC.Types.Type + data SBaz :: Baz -> Type where SBaz :: forall (n :: Nat) (n :: Nat) (n :: Nat). (Sing n) -> (Sing n) -> (Sing n) -> SBaz (Baz n n n :: Baz) diff --git a/singletons-base/tests/compile-and-dump/Singletons/BoxUnBox.golden b/singletons-base/tests/compile-and-dump/Singletons/BoxUnBox.golden index a1f28769..423f5787 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/BoxUnBox.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/BoxUnBox.golden @@ -38,7 +38,7 @@ Singletons/BoxUnBox.hs:(0,0)-(0,0): Splicing declarations sUnBox (SFBox (sA :: Sing a)) = sA instance SingI (UnBoxSym0 :: (~>) (Box a) a) where sing = (singFun1 @UnBoxSym0) sUnBox - data SBox :: forall a. Box a -> GHC.Types.Type + data SBox :: forall a. Box a -> Type where SFBox :: forall a (n :: a). (Sing n) -> SBox (FBox n :: Box a) type instance Sing @(Box a) = SBox diff --git a/singletons-base/tests/compile-and-dump/Singletons/Classes.golden b/singletons-base/tests/compile-and-dump/Singletons/Classes.golden index 42ecb5b0..f8037786 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/Classes.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/Classes.golden @@ -324,7 +324,7 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations instance SingI1 (ConstSym1 :: a -> (~>) b a) where liftSing (s :: Sing (d :: a)) = (singFun1 @(ConstSym1 (d :: a))) (sConst s) - data SFoo :: Foo -> GHC.Types.Type + data SFoo :: Foo -> Type where SA :: SFoo (A :: Foo) SB :: SFoo (B :: Foo) @@ -335,7 +335,7 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations fromSing SB = B toSing A = SomeSing SA toSing B = SomeSing SB - data SFoo2 :: Foo2 -> GHC.Types.Type + data SFoo2 :: Foo2 -> Type where SF :: SFoo2 (F :: Foo2) SG :: SFoo2 (G :: Foo2) @@ -402,7 +402,7 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations forall (t1 :: Foo2) (t2 :: Foo2). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun Foo2 ((~>) Foo2 Bool) - -> GHC.Types.Type) t1) t2) + -> Type) t1) t2) (%==) SF SF = STrue (%==) SG SG = STrue (%==) SF SG = SFalse @@ -571,7 +571,7 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations Mycompare_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Mycompare_0123456789876543210 a0123456789876543210 a0123456789876543210 instance PMyOrd Nat' where type Mycompare a a = Apply (Apply Mycompare_0123456789876543210Sym0 a) a - data SNat' :: Nat' -> GHC.Types.Type + data SNat' :: Nat' -> Type where SZero' :: SNat' (Zero' :: Nat') SSucc' :: forall (n :: Nat'). (Sing n) -> SNat' (Succ' n :: Nat') @@ -589,7 +589,7 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations forall (t :: Nat') (t :: Nat'). Sing t -> Sing t -> Sing (Apply (Apply (MycompareSym0 :: TyFun Nat' ((~>) Nat' Ordering) - -> GHC.Types.Type) t) t) + -> Type) t) t) sMycompare SZero' SZero' = SEQ sMycompare SZero' (SSucc' _) = SLT sMycompare (SSucc' _) SZero' = SGT diff --git a/singletons-base/tests/compile-and-dump/Singletons/Classes2.golden b/singletons-base/tests/compile-and-dump/Singletons/Classes2.golden index a9704962..4bf9d4dd 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/Classes2.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/Classes2.golden @@ -59,7 +59,7 @@ Singletons/Classes2.hs:(0,0)-(0,0): Splicing declarations Mycompare_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Mycompare_0123456789876543210 a0123456789876543210 a0123456789876543210 instance PMyOrd NatFoo where type Mycompare a a = Apply (Apply Mycompare_0123456789876543210Sym0 a) a - data SNatFoo :: NatFoo -> GHC.Types.Type + data SNatFoo :: NatFoo -> Type where SZeroFoo :: SNatFoo (ZeroFoo :: NatFoo) SSuccFoo :: forall (n :: NatFoo). @@ -78,7 +78,7 @@ Singletons/Classes2.hs:(0,0)-(0,0): Splicing declarations forall (t1 :: NatFoo) (t2 :: NatFoo). Sing t1 -> Sing t2 -> Sing (Apply (Apply (MycompareSym0 :: TyFun NatFoo ((~>) NatFoo Ordering) - -> GHC.Types.Type) t1) t2) + -> Type) t1) t2) sMycompare SZeroFoo SZeroFoo = SEQ sMycompare SZeroFoo (SSuccFoo _) = SLT sMycompare (SSuccFoo _) SZeroFoo = SGT diff --git a/singletons-base/tests/compile-and-dump/Singletons/DataValues.golden b/singletons-base/tests/compile-and-dump/Singletons/DataValues.golden index 1003a056..d024ec72 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/DataValues.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/DataValues.golden @@ -122,7 +122,7 @@ Singletons/DataValues.hs:(0,0)-(0,0): Splicing declarations ((applySing ((singFun2 @PairSym0) SPair)) ((applySing ((singFun1 @SuccSym0) SSucc)) SZero))) ((applySing ((applySing ((singFun2 @(:@#@$)) SCons)) SZero)) SNil) - data SPair :: forall a b. Pair a b -> GHC.Types.Type + data SPair :: forall a b. Pair a b -> Type where SPair :: forall a b (n :: a) (n :: b). (Sing n) -> (Sing n) -> SPair (Pair n n :: Pair a b) @@ -141,7 +141,7 @@ Singletons/DataValues.hs:(0,0)-(0,0): Splicing declarations -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) (Pair a b) ((~>) Symbol Symbol)) - -> GHC.Types.Type) t1) t2) t3) + -> Type) t1) t2) t3) sShowsPrec (sP_0123456789876543210 :: Sing p_0123456789876543210) (SPair (sArg_0123456789876543210 :: Sing arg_0123456789876543210) diff --git a/singletons-base/tests/compile-and-dump/Singletons/Empty.golden b/singletons-base/tests/compile-and-dump/Singletons/Empty.golden index 956be686..39216696 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/Empty.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/Empty.golden @@ -2,7 +2,7 @@ Singletons/Empty.hs:(0,0)-(0,0): Splicing declarations singletons [d| data Empty |] ======> data Empty - data SEmpty :: Empty -> GHC.Types.Type + data SEmpty :: Empty -> Type type instance Sing @Empty = SEmpty instance SingKind Empty where type Demote Empty = Empty diff --git a/singletons-base/tests/compile-and-dump/Singletons/EmptyShowDeriving.golden b/singletons-base/tests/compile-and-dump/Singletons/EmptyShowDeriving.golden index a17cdb70..3a1d2c23 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/EmptyShowDeriving.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/EmptyShowDeriving.golden @@ -46,7 +46,7 @@ Singletons/EmptyShowDeriving.hs:(0,0)-(0,0): Splicing declarations ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance PShow Foo where type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a - data SFoo :: Foo -> GHC.Types.Type + data SFoo :: Foo -> Type type instance Sing @Foo = SFoo instance SingKind Foo where type Demote Foo = Foo @@ -60,7 +60,7 @@ Singletons/EmptyShowDeriving.hs:(0,0)-(0,0): Splicing declarations -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) Foo ((~>) GHC.Types.Symbol GHC.Types.Symbol)) - -> GHC.Types.Type) t1) t2) t3) + -> Type) t1) t2) t3) sShowsPrec _ (sV_0123456789876543210 :: Sing v_0123456789876543210) diff --git a/singletons-base/tests/compile-and-dump/Singletons/EnumDeriving.golden b/singletons-base/tests/compile-and-dump/Singletons/EnumDeriving.golden index 381b3779..295051da 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/EnumDeriving.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/EnumDeriving.golden @@ -70,7 +70,7 @@ Singletons/EnumDeriving.hs:(0,0)-(0,0): Splicing declarations instance PEnum Foo where type ToEnum a = Apply ToEnum_0123456789876543210Sym0 a type FromEnum a = Apply FromEnum_0123456789876543210Sym0 a - data SFoo :: Foo -> GHC.Types.Type + data SFoo :: Foo -> Type where SBar :: SFoo (Bar :: Foo) SBaz :: SFoo (Baz :: Foo) @@ -84,7 +84,7 @@ Singletons/EnumDeriving.hs:(0,0)-(0,0): Splicing declarations toSing Bar = SomeSing SBar toSing Baz = SomeSing SBaz toSing Bum = SomeSing SBum - data SQuux :: Quux -> GHC.Types.Type + data SQuux :: Quux -> Type where SQ1 :: SQuux (Q1 :: Quux) SQ2 :: SQuux (Q2 :: Quux) @@ -99,11 +99,11 @@ Singletons/EnumDeriving.hs:(0,0)-(0,0): Splicing declarations sToEnum :: forall (t :: GHC.Num.Natural.Natural). Sing t -> Sing (Apply (Data.Singletons.Base.Enum.ToEnumSym0 :: TyFun GHC.Num.Natural.Natural Foo - -> GHC.Types.Type) t) + -> Type) t) sFromEnum :: forall (t :: Foo). Sing t -> Sing (Apply (Data.Singletons.Base.Enum.FromEnumSym0 :: TyFun Foo GHC.Num.Natural.Natural - -> GHC.Types.Type) t) + -> Type) t) sToEnum (sN :: Sing n) = (id @(Sing (Case_0123456789876543210 n (Apply (Apply (==@#@$) n) (FromInteger 0))))) @@ -192,11 +192,11 @@ Singletons/EnumDeriving.hs:0:0:: Splicing declarations sToEnum :: forall (t :: GHC.Num.Natural.Natural). Sing t -> Sing (Apply (Data.Singletons.Base.Enum.ToEnumSym0 :: TyFun GHC.Num.Natural.Natural Quux - -> GHC.Types.Type) t) + -> Type) t) sFromEnum :: forall (t :: Quux). Sing t -> Sing (Apply (Data.Singletons.Base.Enum.FromEnumSym0 :: TyFun Quux GHC.Num.Natural.Natural - -> GHC.Types.Type) t) + -> Type) t) sToEnum (sN :: Sing n) = (id @(Sing (Case_0123456789876543210 n (Apply (Apply (==@#@$) n) (FromInteger 0))))) diff --git a/singletons-base/tests/compile-and-dump/Singletons/EqInstances.golden b/singletons-base/tests/compile-and-dump/Singletons/EqInstances.golden index ca0d77af..5ee2efec 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/EqInstances.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/EqInstances.golden @@ -35,7 +35,7 @@ Singletons/EqInstances.hs:0:0:: Splicing declarations forall (t1 :: Foo) (t2 :: Foo). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun Foo ((~>) Foo Bool) - -> GHC.Types.Type) t1) t2) + -> Type) t1) t2) (%==) SFLeaf SFLeaf = STrue (%==) SFLeaf ((:%+:) _ _) = SFalse (%==) ((:%+:) _ _) SFLeaf = SFalse @@ -83,5 +83,5 @@ Singletons/EqInstances.hs:0:0:: Splicing declarations forall (t1 :: Empty) (t2 :: Empty). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun Empty ((~>) Empty Bool) - -> GHC.Types.Type) t1) t2) + -> Type) t1) t2) (%==) _ _ = STrue diff --git a/singletons-base/tests/compile-and-dump/Singletons/FunctorLikeDeriving.golden b/singletons-base/tests/compile-and-dump/Singletons/FunctorLikeDeriving.golden index 162957c4..9c4ff50c 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/FunctorLikeDeriving.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/FunctorLikeDeriving.golden @@ -954,11 +954,11 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations (n :: a) (n :: Maybe a) (n :: Maybe (Maybe a)). - (Sing n) - -> (Sing n) - -> (Sing n) - -> (Sing n) - -> ST (MkT1 n n n n :: T x a) + (Sing n) -> + (Sing n) -> + (Sing n) -> + (Sing n) -> + ST (MkT1 n n n n :: T x a) SMkT2 :: forall x a (n :: Maybe x). (Sing n) -> ST (MkT2 n :: T x a) type instance Sing @(T x a) = ST diff --git a/singletons-base/tests/compile-and-dump/Singletons/HigherOrder.golden b/singletons-base/tests/compile-and-dump/Singletons/HigherOrder.golden index c3dc61a4..508a4d35 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/HigherOrder.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/HigherOrder.golden @@ -476,7 +476,7 @@ Singletons/HigherOrder.hs:(0,0)-(0,0): Splicing declarations instance SingI1 (MapSym1 :: (~>) a b -> (~>) [a] [b]) where liftSing (s :: Sing (d :: (~>) a b)) = (singFun1 @(MapSym1 (d :: (~>) a b))) (sMap s) - data SEither :: forall a b. Either a b -> GHC.Types.Type + data SEither :: forall a b. Either a b -> Type where SLeft :: forall a b (n :: a). (Sing n) -> SEither (Left n :: Either a b) diff --git a/singletons-base/tests/compile-and-dump/Singletons/Lambdas.golden b/singletons-base/tests/compile-and-dump/Singletons/Lambdas.golden index d752bfe7..ac64d780 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/Lambdas.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/Lambdas.golden @@ -752,7 +752,7 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations instance SingI1 (Foo0Sym1 :: a -> (~>) b a) where liftSing (s :: Sing (d :: a)) = (singFun1 @(Foo0Sym1 (d :: a))) (sFoo0 s) - data SFoo :: forall a b. Foo a b -> GHC.Types.Type + data SFoo :: forall a b. Foo a b -> Type where SFoo :: forall a b (n :: a) (n :: b). (Sing n) -> (Sing n) -> SFoo (Foo n n :: Foo a b) diff --git a/singletons-base/tests/compile-and-dump/Singletons/Maybe.golden b/singletons-base/tests/compile-and-dump/Singletons/Maybe.golden index ba802951..0cb6a1fc 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/Maybe.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/Maybe.golden @@ -91,7 +91,7 @@ Singletons/Maybe.hs:(0,0)-(0,0): Splicing declarations ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance PShow (Maybe a) where type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a - data SMaybe :: forall a. Maybe a -> GHC.Types.Type + data SMaybe :: forall a. Maybe a -> Type where SNothing :: forall a. SMaybe (Nothing :: Maybe a) SJust :: forall a (n :: a). (Sing n) -> SMaybe (Just n :: Maybe a) @@ -108,7 +108,7 @@ Singletons/Maybe.hs:(0,0)-(0,0): Splicing declarations forall (t1 :: Maybe a) (t2 :: Maybe a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (Maybe a) ((~>) (Maybe a) Bool) - -> GHC.Types.Type) t1) t2) + -> Type) t1) t2) (%==) SNothing SNothing = STrue (%==) SNothing (SJust _) = SFalse (%==) (SJust _) SNothing = SFalse @@ -126,7 +126,7 @@ Singletons/Maybe.hs:(0,0)-(0,0): Splicing declarations -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) (Maybe a) ((~>) GHC.Types.Symbol GHC.Types.Symbol)) - -> GHC.Types.Type) t1) t2) t3) + -> Type) t1) t2) t3) sShowsPrec _ SNothing @@ -164,13 +164,11 @@ Singletons/Maybe.hs:(0,0)-(0,0): Splicing declarations Disproved contra -> Disproved (\ refl -> case refl of Refl -> contra Refl) instance SDecide a => - Data.Type.Equality.TestEquality (SMaybe :: Maybe a - -> GHC.Types.Type) where + Data.Type.Equality.TestEquality (SMaybe :: Maybe a -> Type) where Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality instance SDecide a => - Data.Type.Coercion.TestCoercion (SMaybe :: Maybe a - -> GHC.Types.Type) where + Data.Type.Coercion.TestCoercion (SMaybe :: Maybe a -> Type) where Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion deriving instance Data.Singletons.ShowSing.ShowSing a => diff --git a/singletons-base/tests/compile-and-dump/Singletons/Nat.golden b/singletons-base/tests/compile-and-dump/Singletons/Nat.golden index 9e748f20..f28a0b9c 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/Nat.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/Nat.golden @@ -195,7 +195,7 @@ Singletons/Nat.hs:(0,0)-(0,0): Splicing declarations instance SingI1 (PlusSym1 :: Nat -> (~>) Nat Nat) where liftSing (s :: Sing (d :: Nat)) = (singFun1 @(PlusSym1 (d :: Nat))) (sPlus s) - data SNat :: Nat -> GHC.Types.Type + data SNat :: Nat -> Type where SZero :: SNat (Zero :: Nat) SSucc :: forall (n :: Nat). (Sing n) -> SNat (Succ n :: Nat) @@ -212,7 +212,7 @@ Singletons/Nat.hs:(0,0)-(0,0): Splicing declarations forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun Nat ((~>) Nat Bool) - -> GHC.Types.Type) t1) t2) + -> Type) t1) t2) (%==) SZero SZero = STrue (%==) SZero (SSucc _) = SFalse (%==) (SSucc _) SZero = SFalse @@ -230,7 +230,7 @@ Singletons/Nat.hs:(0,0)-(0,0): Splicing declarations -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) Nat ((~>) GHC.Types.Symbol GHC.Types.Symbol)) - -> GHC.Types.Type) t1) t2) t3) + -> Type) t1) t2) t3) sShowsPrec _ SZero @@ -263,7 +263,7 @@ Singletons/Nat.hs:(0,0)-(0,0): Splicing declarations forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (CompareSym0 :: TyFun Nat ((~>) Nat Ordering) - -> GHC.Types.Type) t1) t2) + -> Type) t1) t2) sCompare SZero SZero = (applySing ((applySing @@ -298,13 +298,11 @@ Singletons/Nat.hs:(0,0)-(0,0): Splicing declarations Disproved contra -> Disproved (\ refl -> case refl of Refl -> contra Refl) instance SDecide Nat => - Data.Type.Equality.TestEquality (SNat :: Nat - -> GHC.Types.Type) where + Data.Type.Equality.TestEquality (SNat :: Nat -> Type) where Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality instance SDecide Nat => - Data.Type.Coercion.TestCoercion (SNat :: Nat - -> GHC.Types.Type) where + Data.Type.Coercion.TestCoercion (SNat :: Nat -> Type) where Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion deriving instance Data.Singletons.ShowSing.ShowSing Nat => diff --git a/singletons-base/tests/compile-and-dump/Singletons/Natural.golden b/singletons-base/tests/compile-and-dump/Singletons/Natural.golden index c1c49abe..310cac29 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/Natural.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/Natural.golden @@ -60,7 +60,7 @@ Singletons/Natural.hs:(0,0)-(0,0): Splicing declarations instance SingI1 (AddAgeSym1 :: Age -> (~>) Age Age) where liftSing (s :: Sing (d :: Age)) = (singFun1 @(AddAgeSym1 (d :: Age))) (sAddAge s) - data SAge :: Age -> GHC.Types.Type + data SAge :: Age -> Type where SMkAge :: forall (n :: Natural). (Sing n) -> SAge (MkAge n :: Age) type instance Sing @Age = SAge diff --git a/singletons-base/tests/compile-and-dump/Singletons/Operators.golden b/singletons-base/tests/compile-and-dump/Singletons/Operators.golden index d43db11d..1e314503 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/Operators.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/Operators.golden @@ -103,7 +103,7 @@ Singletons/Operators.hs:(0,0)-(0,0): Splicing declarations = (singFun1 @((+@#@$$) (d :: Nat))) ((%+) s) instance SingI (ChildSym0 :: (~>) Foo Foo) where sing = (singFun1 @ChildSym0) sChild - data SFoo :: Foo -> GHC.Types.Type + data SFoo :: Foo -> Type where SFLeaf :: SFoo (FLeaf :: Foo) (:%+:) :: forall (n :: Foo) (n :: Foo). diff --git a/singletons-base/tests/compile-and-dump/Singletons/OrdDeriving.golden b/singletons-base/tests/compile-and-dump/Singletons/OrdDeriving.golden index 37e38003..4e5bc3b5 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/OrdDeriving.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/OrdDeriving.golden @@ -463,7 +463,7 @@ Singletons/OrdDeriving.hs:(0,0)-(0,0): Splicing declarations Compare_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210 instance POrd (Foo a b c d) where type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a - data SNat :: Nat -> GHC.Types.Type + data SNat :: Nat -> Type where SZero :: SNat (Zero :: Nat) SSucc :: forall (n :: Nat). (Sing n) -> SNat (Succ n :: Nat) @@ -475,44 +475,44 @@ Singletons/OrdDeriving.hs:(0,0)-(0,0): Splicing declarations toSing Zero = SomeSing SZero toSing (Succ (b :: Demote Nat)) = case toSing b :: SomeSing Nat of SomeSing c -> SomeSing (SSucc c) - data SFoo :: forall a b c d. Foo a b c d -> GHC.Types.Type + data SFoo :: forall a b c d. Foo a b c d -> Type where SA :: forall a b c d (n :: a) (n :: b) (n :: c) (n :: d). - (Sing n) - -> (Sing n) - -> (Sing n) - -> (Sing n) - -> SFoo (A n n n n :: Foo a b c d) + (Sing n) -> + (Sing n) -> + (Sing n) -> + (Sing n) -> + SFoo (A n n n n :: Foo a b c d) SB :: forall a b c d (n :: a) (n :: b) (n :: c) (n :: d). - (Sing n) - -> (Sing n) - -> (Sing n) - -> (Sing n) - -> SFoo (B n n n n :: Foo a b c d) + (Sing n) -> + (Sing n) -> + (Sing n) -> + (Sing n) -> + SFoo (B n n n n :: Foo a b c d) SC :: forall a b c d (n :: a) (n :: b) (n :: c) (n :: d). - (Sing n) - -> (Sing n) - -> (Sing n) - -> (Sing n) - -> SFoo (C n n n n :: Foo a b c d) + (Sing n) -> + (Sing n) -> + (Sing n) -> + (Sing n) -> + SFoo (C n n n n :: Foo a b c d) SD :: forall a b c d (n :: a) (n :: b) (n :: c) (n :: d). - (Sing n) - -> (Sing n) - -> (Sing n) - -> (Sing n) - -> SFoo (D n n n n :: Foo a b c d) + (Sing n) -> + (Sing n) -> + (Sing n) -> + (Sing n) -> + SFoo (D n n n n :: Foo a b c d) SE :: forall a b c d (n :: a) (n :: b) (n :: c) (n :: d). - (Sing n) - -> (Sing n) - -> (Sing n) - -> (Sing n) - -> SFoo (E n n n n :: Foo a b c d) + (Sing n) -> + (Sing n) -> + (Sing n) -> + (Sing n) -> + SFoo (E n n n n :: Foo a b c d) SF :: forall a b c d (n :: a) (n :: b) (n :: c) (n :: d). - (Sing n) - -> (Sing n) - -> (Sing n) - -> (Sing n) - -> SFoo (F n n n n :: Foo a b c d) + (Sing n) -> + (Sing n) -> + (Sing n) -> + (Sing n) -> + SFoo (F n n n n :: Foo a b c d) type instance Sing @(Foo a b c d) = SFoo instance (SingKind a, SingKind b, SingKind c, SingKind d) => SingKind (Foo a b c d) where @@ -588,7 +588,7 @@ Singletons/OrdDeriving.hs:(0,0)-(0,0): Splicing declarations forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun Nat ((~>) Nat Bool) - -> GHC.Types.Type) t1) t2) + -> Type) t1) t2) (%==) SZero SZero = STrue (%==) SZero (SSucc _) = SFalse (%==) (SSucc _) SZero = SFalse @@ -603,7 +603,7 @@ Singletons/OrdDeriving.hs:(0,0)-(0,0): Splicing declarations forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (CompareSym0 :: TyFun Nat ((~>) Nat Ordering) - -> GHC.Types.Type) t1) t2) + -> Type) t1) t2) sCompare SZero SZero = (applySing ((applySing @@ -633,7 +633,7 @@ Singletons/OrdDeriving.hs:(0,0)-(0,0): Splicing declarations forall (t1 :: Foo a b c d) (t2 :: Foo a b c d). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (Foo a b c d) ((~>) (Foo a b c d) Bool) - -> GHC.Types.Type) t1) t2) + -> Type) t1) t2) (%==) (SA (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) @@ -832,7 +832,7 @@ Singletons/OrdDeriving.hs:(0,0)-(0,0): Splicing declarations forall (t1 :: Foo a b c d) (t2 :: Foo a b c d). Sing t1 -> Sing t2 -> Sing (Apply (Apply (CompareSym0 :: TyFun (Foo a b c d) ((~>) (Foo a b c d) Ordering) - -> GHC.Types.Type) t1) t2) + -> Type) t1) t2) sCompare (SA (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) @@ -1107,13 +1107,11 @@ Singletons/OrdDeriving.hs:(0,0)-(0,0): Splicing declarations Disproved contra -> Disproved (\ refl -> case refl of Refl -> contra Refl) instance SDecide Nat => - Data.Type.Equality.TestEquality (SNat :: Nat - -> GHC.Types.Type) where + Data.Type.Equality.TestEquality (SNat :: Nat -> Type) where Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality instance SDecide Nat => - Data.Type.Coercion.TestCoercion (SNat :: Nat - -> GHC.Types.Type) where + Data.Type.Coercion.TestCoercion (SNat :: Nat -> Type) where Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion instance (SDecide a, SDecide b, SDecide c, SDecide d) => @@ -1233,13 +1231,11 @@ Singletons/OrdDeriving.hs:(0,0)-(0,0): Splicing declarations (,,,) _ _ _ (Disproved contra) -> Disproved (\ refl -> case refl of Refl -> contra Refl) instance (SDecide a, SDecide b, SDecide c, SDecide d) => - Data.Type.Equality.TestEquality (SFoo :: Foo a b c d - -> GHC.Types.Type) where + Data.Type.Equality.TestEquality (SFoo :: Foo a b c d -> Type) where Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality instance (SDecide a, SDecide b, SDecide c, SDecide d) => - Data.Type.Coercion.TestCoercion (SFoo :: Foo a b c d - -> GHC.Types.Type) where + Data.Type.Coercion.TestCoercion (SFoo :: Foo a b c d -> Type) where Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion instance SingI Zero where diff --git a/singletons-base/tests/compile-and-dump/Singletons/PatternMatching.golden b/singletons-base/tests/compile-and-dump/Singletons/PatternMatching.golden index 97f0680b..e1e0f48d 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/PatternMatching.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/PatternMatching.golden @@ -122,7 +122,7 @@ Singletons/PatternMatching.hs:(0,0)-(0,0): Splicing declarations ((applySing ((singFun2 @PairSym0) SPair)) ((applySing ((singFun1 @SuccSym0) SSucc)) SZero))) ((applySing ((applySing ((singFun2 @(:@#@$)) SCons)) SZero)) SNil) - data SPair :: forall a b. Pair a b -> GHC.Types.Type + data SPair :: forall a b. Pair a b -> Type where SPair :: forall a b (n :: a) (n :: b). (Sing n) -> (Sing n) -> SPair (Pair n n :: Pair a b) @@ -141,7 +141,7 @@ Singletons/PatternMatching.hs:(0,0)-(0,0): Splicing declarations -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) (Pair a b) ((~>) Symbol Symbol)) - -> GHC.Types.Type) t1) t2) t3) + -> Type) t1) t2) t3) sShowsPrec (sP_0123456789876543210 :: Sing p_0123456789876543210) (SPair (sArg_0123456789876543210 :: Sing arg_0123456789876543210) diff --git a/singletons-base/tests/compile-and-dump/Singletons/Records.golden b/singletons-base/tests/compile-and-dump/Singletons/Records.golden index 211e1207..d54a45bd 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/Records.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/Records.golden @@ -61,7 +61,7 @@ Singletons/Records.hs:(0,0)-(0,0): Splicing declarations sing = (singFun1 @Field2Sym0) sField2 instance SingI (Field1Sym0 :: (~>) (Record a) a) where sing = (singFun1 @Field1Sym0) sField1 - data SRecord :: forall a. Record a -> GHC.Types.Type + data SRecord :: forall a. Record a -> Type where SMkRecord :: forall a (n :: a) (n :: Bool). (Sing n) -> (Sing n) -> SRecord (MkRecord n n :: Record a) diff --git a/singletons-base/tests/compile-and-dump/Singletons/ShowDeriving.golden b/singletons-base/tests/compile-and-dump/Singletons/ShowDeriving.golden index 2d30a4f2..e22ab38e 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/ShowDeriving.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/ShowDeriving.golden @@ -292,14 +292,13 @@ Singletons/ShowDeriving.hs:(0,0)-(0,0): Splicing declarations sing = (singFun1 @(***@#@$)) (%***) instance SingI (GetFoo3aSym0 :: (~>) Foo3 Bool) where sing = (singFun1 @GetFoo3aSym0) sGetFoo3a - data SFoo1 :: Foo1 -> GHC.Types.Type - where SMkFoo1 :: SFoo1 (MkFoo1 :: Foo1) + data SFoo1 :: Foo1 -> Type where SMkFoo1 :: SFoo1 (MkFoo1 :: Foo1) type instance Sing @Foo1 = SFoo1 instance SingKind Foo1 where type Demote Foo1 = Foo1 fromSing SMkFoo1 = MkFoo1 toSing MkFoo1 = SomeSing SMkFoo1 - data SFoo2 :: forall a. Foo2 a -> GHC.Types.Type + data SFoo2 :: forall a. Foo2 a -> Type where SMkFoo2a :: forall a (n :: a) (n :: a). (Sing n) -> (Sing n) -> SFoo2 (MkFoo2a n n :: Foo2 a) @@ -328,7 +327,7 @@ Singletons/ShowDeriving.hs:(0,0)-(0,0): Splicing declarations toSing ((:&:) (b :: Demote a) (b :: Demote a)) = case ((,) (toSing b :: SomeSing a)) (toSing b :: SomeSing a) of (,) (SomeSing c) (SomeSing c) -> SomeSing (((:%&:) c) c) - data SFoo3 :: Foo3 -> GHC.Types.Type + data SFoo3 :: Foo3 -> Type where SMkFoo3 :: forall (n :: Bool) (n :: Bool). (Sing n) -> (Sing n) -> SFoo3 (MkFoo3 n n :: Foo3) @@ -349,7 +348,7 @@ Singletons/ShowDeriving.hs:(0,0)-(0,0): Splicing declarations -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) Foo1 ((~>) Symbol Symbol)) - -> GHC.Types.Type) t1) t2) t3) + -> Type) t1) t2) t3) sShowsPrec _ SMkFoo1 @@ -366,7 +365,7 @@ Singletons/ShowDeriving.hs:(0,0)-(0,0): Splicing declarations -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) (Foo2 a) ((~>) Symbol Symbol)) - -> GHC.Types.Type) t1) t2) t3) + -> Type) t1) t2) t3) sShowsPrec (sP_0123456789876543210 :: Sing p_0123456789876543210) (SMkFoo2a (sArg_0123456789876543210 :: Sing arg_0123456789876543210) @@ -485,7 +484,7 @@ Singletons/ShowDeriving.hs:(0,0)-(0,0): Splicing declarations -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) Foo3 ((~>) Symbol Symbol)) - -> GHC.Types.Type) t1) t2) t3) + -> Type) t1) t2) t3) sShowsPrec (sP_0123456789876543210 :: Sing p_0123456789876543210) (SMkFoo3 (sArg_0123456789876543210 :: Sing arg_0123456789876543210) diff --git a/singletons-base/tests/compile-and-dump/Singletons/StandaloneDeriving.golden b/singletons-base/tests/compile-and-dump/Singletons/StandaloneDeriving.golden index 3907edbf..ca4346e0 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/StandaloneDeriving.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/StandaloneDeriving.golden @@ -302,7 +302,7 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations type ToEnum a = Apply ToEnum_0123456789876543210Sym0 a type FromEnum a = Apply FromEnum_0123456789876543210Sym0 a infixl 6 :%*: - data ST :: forall a b. T a b -> GHC.Types.Type + data ST :: forall a b. T a b -> Type where (:%*:) :: forall a b (n :: a) (n :: b). (Sing n) -> (Sing n) -> ST ((:*:) n n :: T a b) @@ -313,7 +313,7 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations toSing ((:*:) (b :: Demote a) (b :: Demote b)) = case ((,) (toSing b :: SomeSing a)) (toSing b :: SomeSing b) of (,) (SomeSing c) (SomeSing c) -> SomeSing (((:%*:) c) c) - data SS :: S -> GHC.Types.Type + data SS :: S -> Type where SS1 :: SS (S1 :: S) SS2 :: SS (S2 :: S) @@ -329,7 +329,7 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations forall (t1 :: T a ()) (t2 :: T a ()). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (T a ()) ((~>) (T a ()) Bool) - -> GHC.Types.Type) t1) t2) + -> Type) t1) t2) (%==) ((:%*:) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210)) @@ -348,7 +348,7 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations forall (t1 :: T a ()) (t2 :: T a ()). Sing t1 -> Sing t2 -> Sing (Apply (Apply (CompareSym0 :: TyFun (T a ()) ((~>) (T a ()) Ordering) - -> GHC.Types.Type) t1) t2) + -> Type) t1) t2) sCompare ((:%*:) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210)) @@ -380,7 +380,7 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) (T a ()) ((~>) Symbol Symbol)) - -> GHC.Types.Type) t1) t2) t3) + -> Type) t1) t2) t3) sShowsPrec (sP_0123456789876543210 :: Sing p_0123456789876543210) ((:%*:) (sArgL_0123456789876543210 :: Sing argL_0123456789876543210) @@ -412,7 +412,7 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations forall (t1 :: S) (t2 :: S). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun S ((~>) S Bool) - -> GHC.Types.Type) t1) t2) + -> Type) t1) t2) (%==) SS1 SS1 = STrue (%==) SS1 SS2 = SFalse (%==) SS2 SS1 = SFalse @@ -422,7 +422,7 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations forall (t1 :: S) (t2 :: S). Sing t1 -> Sing t2 -> Sing (Apply (Apply (CompareSym0 :: TyFun S ((~>) S Ordering) - -> GHC.Types.Type) t1) t2) + -> Type) t1) t2) sCompare SS1 SS1 = (applySing ((applySing @@ -447,7 +447,7 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) S ((~>) Symbol Symbol)) - -> GHC.Types.Type) t1) t2) t3) + -> Type) t1) t2) t3) sShowsPrec _ SS1 @@ -473,11 +473,11 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations sToEnum :: forall (t :: GHC.Num.Natural.Natural). Sing t -> Sing (Apply (ToEnumSym0 :: TyFun GHC.Num.Natural.Natural S - -> GHC.Types.Type) t) + -> Type) t) sFromEnum :: forall (t :: S). Sing t -> Sing (Apply (FromEnumSym0 :: TyFun S GHC.Num.Natural.Natural - -> GHC.Types.Type) t) + -> Type) t) sToEnum (sN :: Sing n) = (id @(Sing (Case_0123456789876543210 n (Apply (Apply (==@#@$) n) (FromInteger 0))))) @@ -506,13 +506,11 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations (,) _ (Disproved contra) -> Disproved (\ refl -> case refl of Refl -> contra Refl) instance SDecide a => - Data.Type.Equality.TestEquality (ST :: T a () - -> GHC.Types.Type) where + Data.Type.Equality.TestEquality (ST :: T a () -> Type) where Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality instance SDecide a => - Data.Type.Coercion.TestCoercion (ST :: T a () - -> GHC.Types.Type) where + Data.Type.Coercion.TestCoercion (ST :: T a () -> Type) where Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion instance SDecide S where @@ -520,12 +518,10 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations (%~) SS1 SS2 = Disproved (\ x -> case x of {}) (%~) SS2 SS1 = Disproved (\ x -> case x of {}) (%~) SS2 SS2 = Proved Refl - instance Data.Type.Equality.TestEquality (SS :: S - -> GHC.Types.Type) where + instance Data.Type.Equality.TestEquality (SS :: S -> Type) where Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality - instance Data.Type.Coercion.TestCoercion (SS :: S - -> GHC.Types.Type) where + instance Data.Type.Coercion.TestCoercion (SS :: S -> Type) where Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion deriving instance Data.Singletons.ShowSing.ShowSing a => diff --git a/singletons-base/tests/compile-and-dump/Singletons/T136.golden b/singletons-base/tests/compile-and-dump/Singletons/T136.golden index ef73c010..52314495 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T136.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T136.golden @@ -115,20 +115,18 @@ Singletons/T136.hs:(0,0)-(0,0): Splicing declarations instance SEnum [Bool] where sSucc :: forall (t :: [Bool]). Sing t - -> Sing (Apply (SuccSym0 :: TyFun [Bool] [Bool] - -> GHC.Types.Type) t) + -> Sing (Apply (SuccSym0 :: TyFun [Bool] [Bool] -> Type) t) sPred :: forall (t :: [Bool]). Sing t - -> Sing (Apply (PredSym0 :: TyFun [Bool] [Bool] - -> GHC.Types.Type) t) + -> Sing (Apply (PredSym0 :: TyFun [Bool] [Bool] -> Type) t) sToEnum :: forall (t :: GHC.Num.Natural.Natural). Sing t -> Sing (Apply (ToEnumSym0 :: TyFun GHC.Num.Natural.Natural [Bool] - -> GHC.Types.Type) t) + -> Type) t) sFromEnum :: forall (t :: [Bool]). Sing t -> Sing (Apply (FromEnumSym0 :: TyFun [Bool] GHC.Num.Natural.Natural - -> GHC.Types.Type) t) + -> Type) t) sSucc SNil = (applySing ((applySing ((singFun2 @(:@#@$)) SCons)) STrue)) SNil sSucc (SCons SFalse (sAs :: Sing as)) diff --git a/singletons-base/tests/compile-and-dump/Singletons/T136b.golden b/singletons-base/tests/compile-and-dump/Singletons/T136b.golden index 763fc640..9bc9a639 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T136b.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T136b.golden @@ -49,6 +49,6 @@ Singletons/T136b.hs:(0,0)-(0,0): Splicing declarations instance SC Bool where sMeth :: forall (t :: Bool). Sing t - -> Sing (Apply (MethSym0 :: TyFun Bool Bool -> GHC.Types.Type) t) + -> Sing (Apply (MethSym0 :: TyFun Bool Bool -> Type) t) sMeth (sA_0123456789876543210 :: Sing a_0123456789876543210) = (applySing ((singFun1 @NotSym0) sNot)) sA_0123456789876543210 diff --git a/singletons-base/tests/compile-and-dump/Singletons/T159.golden b/singletons-base/tests/compile-and-dump/Singletons/T159.golden index 933e7f12..7a5f2e58 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T159.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T159.golden @@ -19,8 +19,8 @@ Singletons/T159.hs:0:0:: Splicing declarations type FSym0 :: T0 type family FSym0 :: T0 where FSym0 = 'F - type ST0 :: T0 -> GHC.Types.Type - data ST0 :: T0 -> GHC.Types.Type + type ST0 :: T0 -> Type + data ST0 :: T0 -> Type where SA :: ST0 ('A :: T0) SB :: ST0 ('B :: T0) @@ -102,8 +102,8 @@ Singletons/T159.hs:0:0:: Splicing declarations type family (:&&@#@$$$) (a0123456789876543210 :: T0) (a0123456789876543210 :: T1) :: T1 where (:&&@#@$$$) a0123456789876543210 a0123456789876543210 = '(:&&) a0123456789876543210 a0123456789876543210 infixr 5 :&&@#@$$$ - type ST1 :: T1 -> GHC.Types.Type - data ST1 :: T1 -> GHC.Types.Type + type ST1 :: T1 -> Type + data ST1 :: T1 -> Type where SN1 :: ST1 ('N1 :: T1) SC1 :: forall (n :: T0) (n :: T1). @@ -215,7 +215,7 @@ Singletons/T159.hs:(0,0)-(0,0): Splicing declarations infixr 5 :||@#@$$$ infixr 5 :%|| infixr 5 `SC2` - data ST2 :: T2 -> GHC.Types.Type + data ST2 :: T2 -> Type where SN2 :: ST2 (N2 :: T2) SC2 :: forall (n :: T0) (n :: T2). diff --git a/singletons-base/tests/compile-and-dump/Singletons/T163.golden b/singletons-base/tests/compile-and-dump/Singletons/T163.golden index 513b0e8f..293e7f24 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T163.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T163.golden @@ -24,7 +24,7 @@ Singletons/T163.hs:0:0:: Splicing declarations type RSym1 :: forall a b. b -> (+) a b type family RSym1 (a0123456789876543210 :: b) :: (+) a b where RSym1 a0123456789876543210 = R a0123456789876543210 - data (%+) :: forall a b. (+) a b -> GHC.Types.Type + data (%+) :: forall a b. (+) a b -> Type where SL :: forall a b (n :: a). (Sing n) -> (%+) (L n :: (+) a b) SR :: forall a b (n :: b). (Sing n) -> (%+) (R n :: (+) a b) diff --git a/singletons-base/tests/compile-and-dump/Singletons/T178.golden b/singletons-base/tests/compile-and-dump/Singletons/T178.golden index c677fabf..15c42a5c 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T178.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T178.golden @@ -142,7 +142,7 @@ Singletons/T178.hs:(0,0)-(0,0): Splicing declarations type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a sEmpty :: Sing (EmptySym0 :: [(Symbol, Occ)]) sEmpty = SNil - data SOcc :: Occ -> GHC.Types.Type + data SOcc :: Occ -> Type where SStr :: SOcc (Str :: Occ) SOpt :: SOcc (Opt :: Occ) @@ -161,7 +161,7 @@ Singletons/T178.hs:(0,0)-(0,0): Splicing declarations forall (t1 :: Occ) (t2 :: Occ). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun Occ ((~>) Occ Bool) - -> GHC.Types.Type) t1) t2) + -> Type) t1) t2) (%==) SStr SStr = STrue (%==) SStr SOpt = SFalse (%==) SStr SMany = SFalse @@ -176,7 +176,7 @@ Singletons/T178.hs:(0,0)-(0,0): Splicing declarations forall (t1 :: Occ) (t2 :: Occ). Sing t1 -> Sing t2 -> Sing (Apply (Apply (CompareSym0 :: TyFun Occ ((~>) Occ Ordering) - -> GHC.Types.Type) t1) t2) + -> Type) t1) t2) sCompare SStr SStr = (applySing ((applySing @@ -210,7 +210,7 @@ Singletons/T178.hs:(0,0)-(0,0): Splicing declarations -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun Natural ((~>) Occ ((~>) Symbol Symbol)) - -> GHC.Types.Type) t1) t2) t3) + -> Type) t1) t2) t3) sShowsPrec _ SStr @@ -246,11 +246,11 @@ Singletons/T178.hs:(0,0)-(0,0): Splicing declarations (%~) SMany SOpt = Disproved (\ x -> case x of {}) (%~) SMany SMany = Proved Refl instance Data.Type.Equality.TestEquality (SOcc :: Occ - -> GHC.Types.Type) where + -> Type) where Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality instance Data.Type.Coercion.TestCoercion (SOcc :: Occ - -> GHC.Types.Type) where + -> Type) where Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion deriving instance Show (SOcc (z :: Occ)) diff --git a/singletons-base/tests/compile-and-dump/Singletons/T187.golden b/singletons-base/tests/compile-and-dump/Singletons/T187.golden index c0892b1f..b18474c4 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T187.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T187.golden @@ -61,7 +61,7 @@ Singletons/T187.hs:(0,0)-(0,0): Splicing declarations Compare_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210 instance POrd Empty where type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a - data SEmpty :: Empty -> GHC.Types.Type + data SEmpty :: Empty -> Type type instance Sing @Empty = SEmpty instance SingKind Empty where type Demote Empty = Empty @@ -72,22 +72,22 @@ Singletons/T187.hs:(0,0)-(0,0): Splicing declarations forall (t1 :: Empty) (t2 :: Empty). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun Empty ((~>) Empty Bool) - -> GHC.Types.Type) t1) t2) + -> Type) t1) t2) (%==) _ _ = STrue instance SOrd Empty where sCompare :: forall (t1 :: Empty) (t2 :: Empty). Sing t1 -> Sing t2 -> Sing (Apply (Apply (CompareSym0 :: TyFun Empty ((~>) Empty Ordering) - -> GHC.Types.Type) t1) t2) + -> Type) t1) t2) sCompare _ _ = SEQ instance SDecide Empty where (%~) x _ = Proved (case x of {}) instance Data.Type.Equality.TestEquality (SEmpty :: Empty - -> GHC.Types.Type) where + -> Type) where Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality instance Data.Type.Coercion.TestCoercion (SEmpty :: Empty - -> GHC.Types.Type) where + -> Type) where Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion diff --git a/singletons-base/tests/compile-and-dump/Singletons/T190.golden b/singletons-base/tests/compile-and-dump/Singletons/T190.golden index 22113e19..0db1c6ac 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T190.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T190.golden @@ -153,7 +153,7 @@ Singletons/T190.hs:0:0:: Splicing declarations ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance PShow T where type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a - data ST :: T -> GHC.Types.Type where ST :: ST (T :: T) + data ST :: T -> Type where ST :: ST (T :: T) type instance Sing @T = ST instance SingKind T where type Demote T = T @@ -164,14 +164,14 @@ Singletons/T190.hs:0:0:: Splicing declarations forall (t1 :: T) (t2 :: T). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun T ((~>) T Bool) - -> GHC.Types.Type) t1) t2) + -> Type) t1) t2) (%==) ST ST = STrue instance SOrd T where sCompare :: forall (t1 :: T) (t2 :: T). Sing t1 -> Sing t2 -> Sing (Apply (Apply (CompareSym0 :: TyFun T ((~>) T Ordering) - -> GHC.Types.Type) t1) t2) + -> Type) t1) t2) sCompare ST ST = (applySing ((applySing @@ -183,11 +183,11 @@ Singletons/T190.hs:0:0:: Splicing declarations sToEnum :: forall (t :: GHC.Num.Natural.Natural). Sing t -> Sing (Apply (Data.Singletons.Base.Enum.ToEnumSym0 :: TyFun GHC.Num.Natural.Natural T - -> GHC.Types.Type) t) + -> Type) t) sFromEnum :: forall (t :: T). Sing t -> Sing (Apply (Data.Singletons.Base.Enum.FromEnumSym0 :: TyFun T GHC.Num.Natural.Natural - -> GHC.Types.Type) t) + -> Type) t) sToEnum (sN :: Sing n) = (id @(Sing (Case_0123456789876543210 n (Apply (Apply (==@#@$) n) (FromInteger 0))))) @@ -211,7 +211,7 @@ Singletons/T190.hs:0:0:: Splicing declarations -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) T ((~>) GHC.Types.Symbol GHC.Types.Symbol)) - -> GHC.Types.Type) t1) t2) t3) + -> Type) t1) t2) t3) sShowsPrec _ ST @@ -222,12 +222,10 @@ Singletons/T190.hs:0:0:: Splicing declarations sA_0123456789876543210 instance SDecide T where (%~) ST ST = Proved Refl - instance Data.Type.Equality.TestEquality (ST :: T - -> GHC.Types.Type) where + instance Data.Type.Equality.TestEquality (ST :: T -> Type) where Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality - instance Data.Type.Coercion.TestCoercion (ST :: T - -> GHC.Types.Type) where + instance Data.Type.Coercion.TestCoercion (ST :: T -> Type) where Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion deriving instance Show (ST (z :: T)) diff --git a/singletons-base/tests/compile-and-dump/Singletons/T197b.golden b/singletons-base/tests/compile-and-dump/Singletons/T197b.golden index 61efd8cf..a278247b 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T197b.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T197b.golden @@ -51,7 +51,7 @@ Singletons/T197b.hs:(0,0)-(0,0): Splicing declarations MkPairSym2 a0123456789876543210 a0123456789876543210 = MkPair a0123456789876543210 a0123456789876543210 infixr 9 `MkPairSym2` infixr 9 `SMkPair` - data (%:*:) :: forall a b. (:*:) a b -> GHC.Types.Type + data (%:*:) :: forall a b. (:*:) a b -> Type where (:%*:) :: forall a b (n :: a) (n :: b). (Sing n) -> (Sing n) -> (%:*:) ((:*:) n n :: (:*:) a b) @@ -62,7 +62,7 @@ Singletons/T197b.hs:(0,0)-(0,0): Splicing declarations toSing ((:*:) (b :: Demote a) (b :: Demote b)) = case ((,) (toSing b :: SomeSing a)) (toSing b :: SomeSing b) of (,) (SomeSing c) (SomeSing c) -> SomeSing (((:%*:) c) c) - data SPair :: forall a b. Pair a b -> GHC.Types.Type + data SPair :: forall a b. Pair a b -> Type where SMkPair :: forall a b (n :: a) (n :: b). (Sing n) -> (Sing n) -> SPair (MkPair n n :: Pair a b) diff --git a/singletons-base/tests/compile-and-dump/Singletons/T200.golden b/singletons-base/tests/compile-and-dump/Singletons/T200.golden index 0019a776..5c804917 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T200.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T200.golden @@ -143,7 +143,7 @@ Singletons/T200.hs:(0,0)-(0,0): Splicing declarations -> (~>) ErrorMessage ErrorMessage) where liftSing (s :: Sing (d :: ErrorMessage)) = (singFun1 @(($$:@#@$$) (d :: ErrorMessage))) ((%$$:) s) - data SErrorMessage :: ErrorMessage -> GHC.Types.Type + data SErrorMessage :: ErrorMessage -> Type where (:%$$:) :: forall (n :: ErrorMessage) (n :: ErrorMessage). (Sing n) -> (Sing n) -> SErrorMessage ((:$$:) n n :: ErrorMessage) diff --git a/singletons-base/tests/compile-and-dump/Singletons/T209.golden b/singletons-base/tests/compile-and-dump/Singletons/T209.golden index 86ce1649..7605b0b6 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T209.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T209.golden @@ -77,7 +77,7 @@ Singletons/T209.hs:(0,0)-(0,0): Splicing declarations instance SingI2 (MSym2 :: a -> b -> (~>) Bool Bool) where liftSing2 (s :: Sing (d :: a)) (s :: Sing (d :: b)) = (singFun1 @(MSym2 (d :: a) (d :: b))) ((sM s) s) - data SHm :: Hm -> GHC.Types.Type where SHm :: SHm (Hm :: Hm) + data SHm :: Hm -> Type where SHm :: SHm (Hm :: Hm) type instance Sing @Hm = SHm instance SingKind Hm where type Demote Hm = Hm diff --git a/singletons-base/tests/compile-and-dump/Singletons/T271.golden b/singletons-base/tests/compile-and-dump/Singletons/T271.golden index 63421c37..b365a78d 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T271.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T271.golden @@ -157,8 +157,8 @@ 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 :: Type) (b :: Type)) 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) diff --git a/singletons-base/tests/compile-and-dump/Singletons/T326.golden b/singletons-base/tests/compile-and-dump/Singletons/T326.golden index 56325dc9..5bb6b514 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T326.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T326.golden @@ -23,8 +23,8 @@ Singletons/T326.hs:0:0:: Splicing declarations type family (<%>@#@$$$) (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: a where (<%>@#@$$$) a0123456789876543210 a0123456789876543210 = (<%>) a0123456789876543210 a0123456789876543210 infixl 9 <%>@#@$$$ - type PC1 :: GHC.Types.Type -> Constraint - class PC1 (a :: GHC.Types.Type) where + type PC1 :: Type -> Constraint + class PC1 (a :: Type) where type family (<%>) (arg :: a) (arg :: a) :: a infixl 9 <%> Singletons/T326.hs:0:0:: Splicing declarations @@ -52,15 +52,15 @@ Singletons/T326.hs:0:0:: Splicing declarations type family (<%%>@#@$$$) (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: a where (<%%>@#@$$$) a0123456789876543210 a0123456789876543210 = (<%%>) a0123456789876543210 a0123456789876543210 infixl 9 <%%>@#@$$$ - type PC2 :: GHC.Types.Type -> Constraint - class PC2 (a :: GHC.Types.Type) where + type PC2 :: Type -> Constraint + class PC2 (a :: Type) where type family (<%%>) (arg :: a) (arg :: a) :: a infixl 9 <%%> - class SC2 (a :: GHC.Types.Type) where + class SC2 (a :: Type) where (%<%%>) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (<%%>@#@$) t) t :: a) - type SC2 :: GHC.Types.Type -> Constraint + type SC2 :: Type -> Constraint infixl 9 %<%%> instance SC2 a => SingI ((<%%>@#@$) :: (~>) a ((~>) a a)) where sing = (singFun2 @(<%%>@#@$)) (%<%%>) diff --git a/singletons-base/tests/compile-and-dump/Singletons/T33.golden b/singletons-base/tests/compile-and-dump/Singletons/T33.golden index c1053c11..b7eb22a2 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T33.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T33.golden @@ -27,13 +27,13 @@ Singletons/T33.hs:(0,0)-(0,0): Splicing declarations sing = (singFun1 @FooSym0) sFoo Singletons/T33.hs:0:0: warning: - Lazy pattern converted into regular pattern in promotion + Lazy pattern converted into regular pattern during singleton generation. | 6 | $(singletons [d| | ^^^^^^^^^^^^^^^... Singletons/T33.hs:0:0: warning: - Lazy pattern converted into regular pattern during singleton generation. + Lazy pattern converted into regular pattern in promotion | 6 | $(singletons [d| | ^^^^^^^^^^^^^^^... diff --git a/singletons-base/tests/compile-and-dump/Singletons/T332.golden b/singletons-base/tests/compile-and-dump/Singletons/T332.golden index d3184753..1c68561d 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T332.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T332.golden @@ -56,8 +56,7 @@ Singletons/T332.hs:(0,0)-(0,0): Splicing declarations sB SMkBar = STuple0 instance SingI (BSym0 :: (~>) Bar ()) where sing = (singFun1 @BSym0) sB - data SBar :: Bar -> GHC.Types.Type - where SMkBar :: SBar (MkBar :: Bar) + data SBar :: Bar -> Type where SMkBar :: SBar (MkBar :: Bar) type instance Sing @Bar = SBar instance SingKind Bar where type Demote Bar = Bar diff --git a/singletons-base/tests/compile-and-dump/Singletons/T412.golden b/singletons-base/tests/compile-and-dump/Singletons/T412.golden index d2d535c3..db02d1db 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T412.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T412.golden @@ -160,7 +160,7 @@ Singletons/T412.hs:(0,0)-(0,0): Splicing declarations sing = (singFun1 @D1BSym0) sD1B instance SingI (D1ASym0 :: (~>) (D1 a b) a) where sing = (singFun1 @D1ASym0) sD1A - data SD1 :: forall a b. D1 a b -> GHC.Types.Type + data SD1 :: forall a b. D1 a b -> Type where SMkD1 :: forall a b (n :: a) (n :: b). (Sing n) -> (Sing n) -> SD1 (MkD1 n n :: D1 a b) @@ -223,16 +223,16 @@ Singletons/T412.hs:0:0:: Splicing declarations type family M2Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: Bool where M2Sym2 a0123456789876543210 a0123456789876543210 = M2 a0123456789876543210 a0123456789876543210 infix 6 `M2Sym2` - type PC2 :: GHC.Types.Type -> GHC.Types.Type -> Constraint - class PC2 (a :: GHC.Types.Type) (b :: GHC.Types.Type) where + type PC2 :: Type -> Type -> Constraint + class PC2 (a :: Type) (b :: Type) where type family M2 (arg :: a) (arg :: b) :: Bool infix 5 `PC2` infix 6 `M2` - class SC2 (a :: GHC.Types.Type) (b :: GHC.Types.Type) where + class SC2 (a :: Type) (b :: Type) where sM2 :: forall (t :: a) (t :: b). Sing t -> Sing t -> Sing (Apply (Apply M2Sym0 t) t :: Bool) - type SC2 :: GHC.Types.Type -> GHC.Types.Type -> Constraint + type SC2 :: Type -> Type -> Constraint infix 5 `SC2` infix 6 `sM2` instance SC2 a b => SingI (M2Sym0 :: (~>) a ((~>) b Bool)) where @@ -243,8 +243,8 @@ Singletons/T412.hs:0:0:: Splicing declarations instance SC2 a b => SingI1 (M2Sym1 :: a -> (~>) b Bool) where liftSing (s :: Sing (d :: a)) = (singFun1 @(M2Sym1 (d :: a))) (sM2 s) - type T2aSym0 :: (~>) GHC.Types.Type ((~>) GHC.Types.Type GHC.Types.Type) - data T2aSym0 :: (~>) GHC.Types.Type ((~>) GHC.Types.Type GHC.Types.Type) + type T2aSym0 :: (~>) Type ((~>) Type Type) + data T2aSym0 :: (~>) Type ((~>) Type Type) where T2aSym0KindInference :: SameKind (Apply T2aSym0 arg) (T2aSym1 arg) => T2aSym0 a0123456789876543210 @@ -252,9 +252,8 @@ Singletons/T412.hs:0:0:: Splicing declarations instance SuppressUnusedWarnings T2aSym0 where suppressUnusedWarnings = snd (((,) T2aSym0KindInference) ()) infixl 5 `T2aSym0` - type T2aSym1 :: GHC.Types.Type - -> (~>) GHC.Types.Type GHC.Types.Type - data T2aSym1 (a0123456789876543210 :: GHC.Types.Type) :: (~>) GHC.Types.Type GHC.Types.Type + type T2aSym1 :: Type -> (~>) Type Type + data T2aSym1 (a0123456789876543210 :: Type) :: (~>) Type Type where T2aSym1KindInference :: SameKind (Apply (T2aSym1 a0123456789876543210) arg) (T2aSym2 a0123456789876543210 arg) => T2aSym1 a0123456789876543210 a0123456789876543210 @@ -262,12 +261,12 @@ Singletons/T412.hs:0:0:: Splicing declarations instance SuppressUnusedWarnings (T2aSym1 a0123456789876543210) where suppressUnusedWarnings = snd (((,) T2aSym1KindInference) ()) infixl 5 `T2aSym1` - type T2aSym2 :: GHC.Types.Type -> GHC.Types.Type -> GHC.Types.Type - type family T2aSym2 (a0123456789876543210 :: GHC.Types.Type) (a0123456789876543210 :: GHC.Types.Type) :: GHC.Types.Type where + type T2aSym2 :: Type -> Type -> Type + type family T2aSym2 (a0123456789876543210 :: Type) (a0123456789876543210 :: Type) :: Type where T2aSym2 a0123456789876543210 a0123456789876543210 = T2a a0123456789876543210 a0123456789876543210 infixl 5 `T2aSym2` - type T2bSym0 :: (~>) GHC.Types.Type ((~>) GHC.Types.Type GHC.Types.Type) - data T2bSym0 :: (~>) GHC.Types.Type ((~>) GHC.Types.Type GHC.Types.Type) + type T2bSym0 :: (~>) Type ((~>) Type Type) + data T2bSym0 :: (~>) Type ((~>) Type Type) where T2bSym0KindInference :: SameKind (Apply T2bSym0 arg) (T2bSym1 arg) => T2bSym0 a0123456789876543210 @@ -275,9 +274,8 @@ Singletons/T412.hs:0:0:: Splicing declarations instance SuppressUnusedWarnings T2bSym0 where suppressUnusedWarnings = snd (((,) T2bSym0KindInference) ()) infixl 5 `T2bSym0` - type T2bSym1 :: GHC.Types.Type - -> (~>) GHC.Types.Type GHC.Types.Type - data T2bSym1 (a0123456789876543210 :: GHC.Types.Type) :: (~>) GHC.Types.Type GHC.Types.Type + type T2bSym1 :: Type -> (~>) Type Type + data T2bSym1 (a0123456789876543210 :: Type) :: (~>) Type Type where T2bSym1KindInference :: SameKind (Apply (T2bSym1 a0123456789876543210) arg) (T2bSym2 a0123456789876543210 arg) => T2bSym1 a0123456789876543210 a0123456789876543210 @@ -285,13 +283,13 @@ Singletons/T412.hs:0:0:: Splicing declarations instance SuppressUnusedWarnings (T2bSym1 a0123456789876543210) where suppressUnusedWarnings = snd (((,) T2bSym1KindInference) ()) infixl 5 `T2bSym1` - type T2bSym2 :: GHC.Types.Type -> GHC.Types.Type -> GHC.Types.Type - type family T2bSym2 (a0123456789876543210 :: GHC.Types.Type) (a0123456789876543210 :: GHC.Types.Type) :: GHC.Types.Type where + type T2bSym2 :: Type -> Type -> Type + type family T2bSym2 (a0123456789876543210 :: Type) (a0123456789876543210 :: Type) :: Type where T2bSym2 a0123456789876543210 a0123456789876543210 = T2b a0123456789876543210 a0123456789876543210 infixl 5 `T2bSym2` - type MkD2Sym0 :: forall (a :: GHC.Types.Type) - (b :: GHC.Types.Type). (~>) a ((~>) b (D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type))) - data MkD2Sym0 :: (~>) a ((~>) b (D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type))) + type MkD2Sym0 :: forall (a :: Type) + (b :: Type). (~>) a ((~>) b (D2 (a :: Type) (b :: Type))) + data MkD2Sym0 :: (~>) a ((~>) b (D2 (a :: Type) (b :: Type))) where MkD2Sym0KindInference :: SameKind (Apply MkD2Sym0 arg) (MkD2Sym1 arg) => MkD2Sym0 a0123456789876543210 @@ -299,10 +297,9 @@ Singletons/T412.hs:0:0:: Splicing declarations instance SuppressUnusedWarnings MkD2Sym0 where suppressUnusedWarnings = snd (((,) MkD2Sym0KindInference) ()) infixr 5 `MkD2Sym0` - type MkD2Sym1 :: forall (a :: GHC.Types.Type) - (b :: GHC.Types.Type). a - -> (~>) b (D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type)) - data MkD2Sym1 (a0123456789876543210 :: a) :: (~>) b (D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type)) + type MkD2Sym1 :: forall (a :: Type) (b :: Type). a + -> (~>) b (D2 (a :: Type) (b :: Type)) + data MkD2Sym1 (a0123456789876543210 :: a) :: (~>) b (D2 (a :: Type) (b :: Type)) where MkD2Sym1KindInference :: SameKind (Apply (MkD2Sym1 a0123456789876543210) arg) (MkD2Sym2 a0123456789876543210 arg) => MkD2Sym1 a0123456789876543210 a0123456789876543210 @@ -310,81 +307,70 @@ Singletons/T412.hs:0:0:: Splicing declarations instance SuppressUnusedWarnings (MkD2Sym1 a0123456789876543210) where suppressUnusedWarnings = snd (((,) MkD2Sym1KindInference) ()) infixr 5 `MkD2Sym1` - type MkD2Sym2 :: forall (a :: GHC.Types.Type) - (b :: GHC.Types.Type). a - -> b - -> D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type) - type family MkD2Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type) where + 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 MkD2Sym2 a0123456789876543210 a0123456789876543210 = 'MkD2 a0123456789876543210 a0123456789876543210 infixr 5 `MkD2Sym2` infixr 5 `D2A` infixr 5 `D2B` - type D2BSym0 :: forall (a :: GHC.Types.Type) - (b :: GHC.Types.Type). (~>) (D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type)) b - data D2BSym0 :: (~>) (D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type)) b + type D2BSym0 :: forall (a :: Type) + (b :: Type). (~>) (D2 (a :: Type) (b :: Type)) b + data D2BSym0 :: (~>) (D2 (a :: Type) (b :: Type)) 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 :: GHC.Types.Type) - (b :: GHC.Types.Type). D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type) - -> b - type family D2BSym1 (a0123456789876543210 :: D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type)) :: b where + type D2BSym1 :: forall (a :: Type) + (b :: Type). D2 (a :: Type) (b :: Type) -> b + type family D2BSym1 (a0123456789876543210 :: D2 (a :: Type) (b :: Type)) :: b where D2BSym1 a0123456789876543210 = D2B a0123456789876543210 - type D2ASym0 :: forall (a :: GHC.Types.Type) - (b :: GHC.Types.Type). (~>) (D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type)) a - data D2ASym0 :: (~>) (D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type)) a + type D2ASym0 :: forall (a :: Type) + (b :: Type). (~>) (D2 (a :: Type) (b :: Type)) a + data D2ASym0 :: (~>) (D2 (a :: Type) (b :: Type)) 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 :: GHC.Types.Type) - (b :: GHC.Types.Type). D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type) - -> a - type family D2ASym1 (a0123456789876543210 :: D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type)) :: a where + type D2ASym1 :: forall (a :: Type) + (b :: Type). D2 (a :: Type) (b :: Type) -> a + type family D2ASym1 (a0123456789876543210 :: D2 (a :: Type) (b :: Type)) :: a where D2ASym1 a0123456789876543210 = D2A a0123456789876543210 - type D2B :: forall (a :: GHC.Types.Type) - (b :: GHC.Types.Type). D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type) - -> b - type family D2B (a :: D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type)) :: b where + 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 ('MkD2 _ field) = field - type D2A :: forall (a :: GHC.Types.Type) - (b :: GHC.Types.Type). D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type) - -> a - type family D2A (a :: D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type)) :: a where + 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 ('MkD2 field _) = field sD2B :: - forall (a :: GHC.Types.Type) - (b :: GHC.Types.Type) - (t :: D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type)). Sing t - -> Sing (Apply D2BSym0 t :: b) + forall (a :: Type) + (b :: Type) + (t :: D2 (a :: Type) (b :: Type)). Sing t + -> Sing (Apply D2BSym0 t :: b) sD2A :: - forall (a :: GHC.Types.Type) - (b :: GHC.Types.Type) - (t :: D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type)). Sing t - -> Sing (Apply D2ASym0 t :: a) + forall (a :: Type) + (b :: Type) + (t :: D2 (a :: Type) (b :: Type)). Sing t + -> Sing (Apply D2ASym0 t :: a) sD2B (SMkD2 _ (sField :: Sing field)) = sField sD2A (SMkD2 (sField :: Sing field) _) = sField - instance SingI (D2BSym0 :: (~>) (D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type)) b) where + instance SingI (D2BSym0 :: (~>) (D2 (a :: Type) (b :: Type)) b) where sing = (singFun1 @D2BSym0) sD2B - instance SingI (D2ASym0 :: (~>) (D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type)) a) where + instance SingI (D2ASym0 :: (~>) (D2 (a :: Type) (b :: Type)) a) where sing = (singFun1 @D2ASym0) sD2A - type SD2 :: forall (a :: GHC.Types.Type) - (b :: GHC.Types.Type). D2 a b -> GHC.Types.Type - data SD2 :: forall (a :: GHC.Types.Type) (b :: GHC.Types.Type). - D2 a b -> GHC.Types.Type + 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 :: GHC.Types.Type) - (b :: GHC.Types.Type) - (n :: a) - (n :: b). - (Sing n) - -> (Sing n) - -> SD2 ('MkD2 n n :: D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type)) + SMkD2 :: forall (a :: Type) (b :: Type) (n :: a) (n :: b). + (Sing n) -> + (Sing n) -> + SD2 ('MkD2 n n :: D2 (a :: Type) (b :: Type)) 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) @@ -402,12 +388,12 @@ Singletons/T412.hs:0:0:: Splicing declarations liftSing = SMkD2 sing instance SingI2 'MkD2 where liftSing2 = SMkD2 - instance SingI (MkD2Sym0 :: (~>) a ((~>) b (D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type)))) where + instance SingI (MkD2Sym0 :: (~>) a ((~>) b (D2 (a :: Type) (b :: Type)))) where sing = (singFun2 @MkD2Sym0) SMkD2 instance SingI d => - SingI (MkD2Sym1 (d :: a) :: (~>) b (D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type))) where + SingI (MkD2Sym1 (d :: a) :: (~>) b (D2 (a :: Type) (b :: Type))) where sing = (singFun1 @(MkD2Sym1 (d :: a))) (SMkD2 (sing @d)) instance SingI1 (MkD2Sym1 :: a - -> (~>) b (D2 (a :: GHC.Types.Type) (b :: GHC.Types.Type))) where + -> (~>) b (D2 (a :: Type) (b :: Type))) 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 ea58511e..83daeb90 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T450.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T450.golden @@ -47,8 +47,8 @@ Singletons/T450.hs:(0,0)-(0,0): Splicing declarations type PMkMessageSym1 :: Symbol -> PMessage type family PMkMessageSym1 (a0123456789876543210 :: Symbol) :: PMessage where PMkMessageSym1 a0123456789876543210 = 'PMkMessage a0123456789876543210 - type SMessage :: PMessage -> GHC.Types.Type - data SMessage :: PMessage -> GHC.Types.Type + type SMessage :: PMessage -> Type + data SMessage :: PMessage -> Type where SMkMessage :: forall (n :: Symbol). (Sing n) -> SMessage ('PMkMessage n :: PMessage) @@ -116,9 +116,9 @@ Singletons/T450.hs:(0,0)-(0,0): Splicing declarations liftSing (s :: Sing (d :: PMessage)) = (singFun1 @(AppendMessageSym1 (d :: PMessage))) (sAppendMessage s) - type PMkFunctionSym0 :: forall (a :: GHC.Types.Type) - (b :: GHC.Types.Type). (~>) ((~>) a b) (PFunction (a :: GHC.Types.Type) (b :: GHC.Types.Type)) - data PMkFunctionSym0 :: (~>) ((~>) a b) (PFunction (a :: GHC.Types.Type) (b :: GHC.Types.Type)) + type PMkFunctionSym0 :: forall (a :: Type) + (b :: Type). (~>) ((~>) a b) (PFunction (a :: Type) (b :: Type)) + data PMkFunctionSym0 :: (~>) ((~>) a b) (PFunction (a :: Type) (b :: Type)) where PMkFunctionSym0KindInference :: SameKind (Apply PMkFunctionSym0 arg) (PMkFunctionSym1 arg) => PMkFunctionSym0 a0123456789876543210 @@ -126,22 +126,18 @@ Singletons/T450.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings PMkFunctionSym0 where suppressUnusedWarnings = snd (((,) PMkFunctionSym0KindInference) ()) - type PMkFunctionSym1 :: forall (a :: GHC.Types.Type) - (b :: GHC.Types.Type). (~>) a b - -> PFunction (a :: GHC.Types.Type) (b :: GHC.Types.Type) - type family PMkFunctionSym1 (a0123456789876543210 :: (~>) a b) :: PFunction (a :: GHC.Types.Type) (b :: GHC.Types.Type) where + 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 PMkFunctionSym1 a0123456789876543210 = 'PMkFunction a0123456789876543210 - type SFunction :: forall (a :: GHC.Types.Type) - (b :: GHC.Types.Type). PFunction a b -> GHC.Types.Type - data SFunction :: forall (a :: GHC.Types.Type) - (b :: GHC.Types.Type). - PFunction a b -> GHC.Types.Type + type SFunction :: forall (a :: Type) (b :: Type). PFunction a b + -> Type + data SFunction :: forall (a :: Type) (b :: Type). + PFunction a b -> Type where - SMkFunction :: forall (a :: GHC.Types.Type) - (b :: GHC.Types.Type) - (n :: (~>) a b). - (Sing n) - -> SFunction ('PMkFunction n :: PFunction (a :: GHC.Types.Type) (b :: GHC.Types.Type)) + SMkFunction :: forall (a :: Type) (b :: Type) (n :: (~>) a b). + (Sing n) -> + SFunction ('PMkFunction n :: PFunction (a :: Type) (b :: Type)) 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) @@ -153,7 +149,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 :: GHC.Types.Type) (b :: GHC.Types.Type))) where + instance SingI (PMkFunctionSym0 :: (~>) ((~>) a b) (PFunction (a :: Type) (b :: Type))) 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/TopLevelPatterns.golden b/singletons-base/tests/compile-and-dump/Singletons/TopLevelPatterns.golden index 476d136e..f8d1b396 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/TopLevelPatterns.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/TopLevelPatterns.golden @@ -32,7 +32,7 @@ Singletons/TopLevelPatterns.hs:(0,0)-(0,0): Splicing declarations type BarSym2 :: Bool -> Bool -> Foo type family BarSym2 (a0123456789876543210 :: Bool) (a0123456789876543210 :: Bool) :: Foo where BarSym2 a0123456789876543210 a0123456789876543210 = Bar a0123456789876543210 a0123456789876543210 - data SBool :: Bool -> GHC.Types.Type + data SBool :: Bool -> Type where SFalse :: SBool (False :: Bool) STrue :: SBool (True :: Bool) @@ -43,7 +43,7 @@ Singletons/TopLevelPatterns.hs:(0,0)-(0,0): Splicing declarations fromSing STrue = True toSing False = SomeSing SFalse toSing True = SomeSing STrue - data SFoo :: Foo -> GHC.Types.Type + data SFoo :: Foo -> Type where SBar :: forall (n :: Bool) (n :: Bool). (Sing n) -> (Sing n) -> SFoo (Bar n n :: Foo) diff --git a/singletons-th/CHANGES.md b/singletons-th/CHANGES.md index e66b5f56..67ae7cf8 100644 --- a/singletons-th/CHANGES.md +++ b/singletons-th/CHANGES.md @@ -1,6 +1,12 @@ Changelog for the `singletons-th` project ========================================= +3.1.1 [????.??.??] +------------------ +* Require building with GHC 9.4. +* Improve error messages when attempting to promote a partial application of + a function arrow `(->)`, which is not currently supported. + 3.1 [2021.10.30] ---------------- * Require building with GHC 9.2. diff --git a/singletons-th/README.md b/singletons-th/README.md index fa7c91e7..306a5f9d 100644 --- a/singletons-th/README.md +++ b/singletons-th/README.md @@ -14,7 +14,7 @@ which describes how promotion works in greater detail. `singletons-th` generates code that relies on bleeding-edge GHC language extensions. As such, `singletons-th` only supports the latest major version -of GHC (currently GHC 9.2). For more information, +of GHC (currently GHC 9.4). For more information, consult the `singletons` [`README`](https://github.com/goldfirere/singletons/blob/master/README.md). diff --git a/singletons-th/singletons-th.cabal b/singletons-th/singletons-th.cabal index f5b6f425..f8384070 100644 --- a/singletons-th/singletons-th.cabal +++ b/singletons-th/singletons-th.cabal @@ -1,5 +1,5 @@ name: singletons-th -version: 3.1 +version: 3.1.1 cabal-version: 1.24 synopsis: A framework for generating singleton types homepage: http://www.github.com/goldfirere/singletons @@ -8,7 +8,7 @@ author: Richard Eisenberg , Jan Stolarek bug-reports: https://github.com/goldfirere/singletons/issues stability: experimental -tested-with: GHC == 9.2.1 +tested-with: GHC == 9.4.1 extra-source-files: README.md, CHANGES.md license: BSD3 license-file: LICENSE @@ -26,7 +26,7 @@ description: . @singletons-th@ generates code that relies on bleeding-edge GHC language extensions. As such, @singletons-th@ only supports the latest major version - of GHC (currently GHC 9.2). For more information, + of GHC (currently GHC 9.4). For more information, consult the @singletons@ @@. . @@ -52,14 +52,14 @@ source-repository head library hs-source-dirs: src - build-depends: base >= 4.16 && < 4.17, + build-depends: base >= 4.17 && < 4.18, containers >= 0.5, mtl >= 2.2.1, ghc-boot-th, - singletons == 3.0.1, + singletons == 3.0.*, syb >= 0.4, - template-haskell >= 2.18 && < 2.19, - th-desugar >= 1.13 && < 1.14, + template-haskell >= 2.19 && < 2.20, + th-desugar >= 1.14 && < 1.15, th-orphans >= 0.13.11 && < 0.14, transformers >= 0.5.2 default-language: GHC2021 diff --git a/singletons/CHANGES.md b/singletons/CHANGES.md index 11f2559a..0252f44d 100644 --- a/singletons/CHANGES.md +++ b/singletons/CHANGES.md @@ -1,6 +1,14 @@ Changelog for the `singletons` project ====================================== +3.0.2 [????.??.??] +------------------ +* Allow building with GHC 9.4. +* When building with GHC 9.4 or later, use the new + [`withDict`](https://hackage.haskell.org/package/ghc-prim-0.9.0/docs/GHC-Magic-Dict.html#v:withDict) + primitive to implement `withSingI` instead of `unsafeCoerce`. This change + should not have any consequences for user-facing code. + 3.0.1 [2021.10.30] ------------------ * Add `SingI1` and `SingI2`, higher-order versions of `SingI`, to diff --git a/singletons/singletons.cabal b/singletons/singletons.cabal index cb374476..0bbf2a8d 100644 --- a/singletons/singletons.cabal +++ b/singletons/singletons.cabal @@ -1,5 +1,5 @@ name: singletons -version: 3.0.1 +version: 3.0.2 cabal-version: 1.24 synopsis: Basic singleton types and definitions homepage: http://www.github.com/goldfirere/singletons @@ -14,8 +14,9 @@ tested-with: GHC == 8.0.2 , GHC == 8.6.5 , GHC == 8.8.4 , GHC == 8.10.7 - , GHC == 9.0.1 - , GHC == 9.2.1 + , GHC == 9.0.2 + , GHC == 9.2.4 + , GHC == 9.4.1 , GHCJS==8.4 extra-source-files: README.md, CHANGES.md license: BSD3 @@ -57,7 +58,7 @@ source-repository head library hs-source-dirs: src - build-depends: base >= 4.9 && < 4.17 + build-depends: base >= 4.9 && < 4.18 default-language: Haskell2010 exposed-modules: Data.Singletons Data.Singletons.Decide @@ -74,5 +75,5 @@ test-suite singletons-test-suite other-modules: ByHand ByHand2 - build-depends: base >= 4.9 && < 4.17, + build-depends: base >= 4.9 && < 4.18, singletons