singletons-base 3.1 → 3.1.1
raw patch · 108 files changed
+422/−643 lines, 108 filesdep ~basedep ~singletonsdep ~template-haskell
Dependency ranges changed: base, singletons, template-haskell, th-desugar
Files
- CHANGES.md +4/−0
- README.md +3/−3
- singletons-base.cabal +15/−15
- src/Control/Applicative/Singletons.hs +0/−9
- src/Control/Monad/Fail/Singletons.hs +0/−5
- src/Control/Monad/Singletons.hs +0/−9
- src/Control/Monad/Singletons/Internal.hs +1/−9
- src/Control/Monad/Zip/Singletons.hs +0/−8
- src/Data/Bool/Singletons.hs +5/−3
- src/Data/Either/Singletons.hs +4/−3
- src/Data/Eq/Singletons.hs +5/−5
- src/Data/Foldable/Singletons.hs +2/−9
- src/Data/Function/Singletons.hs +5/−5
- src/Data/Functor/Compose/Singletons.hs +0/−7
- src/Data/Functor/Const/Singletons.hs +1/−8
- src/Data/Functor/Identity/Singletons.hs +1/−8
- src/Data/Functor/Product/Singletons.hs +0/−7
- src/Data/Functor/Singletons.hs +1/−10
- src/Data/Functor/Sum/Singletons.hs +0/−7
- src/Data/List/NonEmpty/Singletons.hs +4/−4
- src/Data/List/Singletons/Internal.hs +5/−4
- src/Data/List/Singletons/Internal/Disambiguation.hs +5/−4
- src/Data/Maybe/Singletons.hs +4/−3
- src/Data/Monoid/Singletons.hs +1/−10
- src/Data/Ord/Singletons.hs +5/−5
- src/Data/Ord/Singletons/Disambiguation.hs +0/−5
- src/Data/Proxy/Singletons.hs +0/−7
- src/Data/Semigroup/Singletons.hs +1/−11
- src/Data/Semigroup/Singletons/Internal.hs +1/−10
- src/Data/Semigroup/Singletons/Internal/Disambiguation.hs +0/−5
- src/Data/Singletons/Base/Enum.hs +5/−4
- src/Data/Singletons/Base/Instances.hs +6/−6
- src/Data/Singletons/Base/SomeSing.hs +0/−3
- src/Data/Singletons/Base/TypeError.hs +1/−8
- src/Data/Singletons/Base/TypeRepTYPE.hs +2/−4
- src/Data/Singletons/Base/Util.hs +2/−1
- src/Data/String/Singletons.hs +0/−6
- src/Data/Traversable/Singletons.hs +2/−9
- src/Data/Tuple/Singletons.hs +4/−3
- src/Data/Void/Singletons.hs +1/−6
- src/GHC/Base/Singletons.hs +4/−4
- src/GHC/Num/Singletons.hs +6/−5
- src/GHC/TypeLits/Singletons.hs +5/−5
- src/GHC/TypeLits/Singletons/Internal.hs +6/−6
- src/Prelude/Singletons.hs +3/−2
- src/Text/Show/Singletons.hs +0/−10
- tests/SingletonsBaseTestSuite.hs +1/−0
- tests/SingletonsBaseTestSuiteUtils.hs +39/−16
- tests/compile-and-dump/GradingClient/Database.hs +0/−6
- tests/compile-and-dump/GradingClient/Main.hs +0/−2
- tests/compile-and-dump/InsertionSort/InsertionSortImp.hs +0/−5
- tests/compile-and-dump/Singletons/AsPattern.golden +1/−1
- tests/compile-and-dump/Singletons/BoxUnBox.golden +1/−1
- tests/compile-and-dump/Singletons/Classes.golden +5/−5
- tests/compile-and-dump/Singletons/Classes2.golden +2/−2
- tests/compile-and-dump/Singletons/DataValues.golden +2/−2
- tests/compile-and-dump/Singletons/Empty.golden +1/−1
- tests/compile-and-dump/Singletons/EmptyShowDeriving.golden +2/−2
- tests/compile-and-dump/Singletons/EnumDeriving.golden +6/−6
- tests/compile-and-dump/Singletons/EqInstances.golden +2/−2
- tests/compile-and-dump/Singletons/FunctorLikeDeriving.golden +5/−5
- tests/compile-and-dump/Singletons/FunctorLikeDeriving.hs +0/−1
- tests/compile-and-dump/Singletons/HigherOrder.golden +1/−1
- tests/compile-and-dump/Singletons/Lambdas.golden +1/−1
- tests/compile-and-dump/Singletons/Lambdas.hs +0/−1
- tests/compile-and-dump/Singletons/Maybe.golden +5/−7
- tests/compile-and-dump/Singletons/Nat.golden +6/−8
- tests/compile-and-dump/Singletons/Natural.golden +1/−1
- tests/compile-and-dump/Singletons/NegativeLiterals.golden +1/−1
- tests/compile-and-dump/Singletons/NegativeLiterals.hs +1/−0
- tests/compile-and-dump/Singletons/Operators.golden +1/−1
- tests/compile-and-dump/Singletons/OrdDeriving.golden +40/−44
- tests/compile-and-dump/Singletons/OverloadedStrings.hs +1/−0
- tests/compile-and-dump/Singletons/PatternMatching.golden +2/−2
- tests/compile-and-dump/Singletons/Records.golden +1/−1
- tests/compile-and-dump/Singletons/ShowDeriving.golden +6/−7
- tests/compile-and-dump/Singletons/StandaloneDeriving.golden +14/−18
- tests/compile-and-dump/Singletons/T136.golden +4/−6
- tests/compile-and-dump/Singletons/T136.hs +0/−7
- tests/compile-and-dump/Singletons/T136b.golden +1/−1
- tests/compile-and-dump/Singletons/T153.hs +0/−3
- tests/compile-and-dump/Singletons/T159.golden +5/−5
- tests/compile-and-dump/Singletons/T163.golden +1/−1
- tests/compile-and-dump/Singletons/T166.golden +3/−3
- tests/compile-and-dump/Singletons/T166.hs +0/−8
- tests/compile-and-dump/Singletons/T167.hs +0/−10
- tests/compile-and-dump/Singletons/T172.hs +0/−8
- tests/compile-and-dump/Singletons/T175.hs +0/−10
- tests/compile-and-dump/Singletons/T176.hs +0/−8
- tests/compile-and-dump/Singletons/T178.golden +6/−6
- tests/compile-and-dump/Singletons/T184.hs +1/−0
- tests/compile-and-dump/Singletons/T187.golden +5/−5
- tests/compile-and-dump/Singletons/T190.golden +8/−10
- tests/compile-and-dump/Singletons/T190.hs +0/−7
- tests/compile-and-dump/Singletons/T197b.golden +2/−2
- tests/compile-and-dump/Singletons/T200.golden +1/−1
- tests/compile-and-dump/Singletons/T209.golden +1/−1
- tests/compile-and-dump/Singletons/T209.hs +1/−0
- tests/compile-and-dump/Singletons/T271.golden +2/−2
- tests/compile-and-dump/Singletons/T326.golden +6/−6
- tests/compile-and-dump/Singletons/T33.golden +2/−2
- tests/compile-and-dump/Singletons/T332.golden +1/−2
- tests/compile-and-dump/Singletons/T412.golden +63/−77
- tests/compile-and-dump/Singletons/T450.golden +16/−20
- tests/compile-and-dump/Singletons/T511.golden +13/−0
- tests/compile-and-dump/Singletons/T511.hs +9/−0
- tests/compile-and-dump/Singletons/TopLevelPatterns.golden +2/−2
- tests/compile-and-dump/Singletons/TypeRepTYPE.hs +1/−0
CHANGES.md view
@@ -1,6 +1,10 @@ Changelog for the `singletons-base` project =========================================== +3.1.1 [2022.08.23]+------------------+* Require building with GHC 9.4.+ 3.1 [2021.10.30] ---------------- * Require building with GHC 9.2.
README.md view
@@ -6,9 +6,9 @@ `singletons-base` uses `singletons-th` to define promoted and singled functions from the @base@ library, including the `Prelude`. This library was originally presented in-[_Dependently Typed Programming with Singletons_](https://cs.brynmawr.edu/~rae/papers/2012/singletons/paper.pdf),+[_Dependently Typed Programming with Singletons_](https://richarde.dev/papers/2012/singletons/paper.pdf), published at the Haskell Symposium, 2012. See also-[the paper published at Haskell Symposium, 2014](https://cs.brynmawr.edu/~rae/papers/2014/promotion/promotion.pdf),+[the paper published at Haskell Symposium, 2014](https://richarde.dev/papers/2014/promotion/promotion.pdf), which describes how promotion works in greater detail. WARNING: `singletons-base` defines orphan instances for `Sing`, `SingKind`, etc.@@ -18,7 +18,7 @@ `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).
singletons-base.cabal view
@@ -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 @@ maintainer: Ryan Scott <ryan.gl.scott@gmail.com> 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,@@ -26,10 +26,10 @@ functions from the @base@ library, including the "Prelude". This library was originally presented in /Dependently Typed Programming with Singletons/, published at the Haskell Symposium, 2012.- (<https://cs.brynmawr.edu/~rae/papers/2012/singletons/paper.pdf>)+ (<https://richarde.dev/papers/2012/singletons/paper.pdf>) See also the paper published at Haskell Symposium, 2014, which describes how promotion works in greater detail:- <https://cs.brynmawr.edu/~rae/papers/2014/promotion/promotion.pdf>.+ <https://richarde.dev/papers/2014/promotion/promotion.pdf>. . WARNING: @singletons-base@ defines orphan instances for @Sing@, @SingKind@, etc. for common types such as @Bool@, @[]@, @Maybe@, etc. If you define@@ -38,7 +38,7 @@ . @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@ @<https://github.com/goldfirere/singletons/blob/master/README.md README>@. .@@ -55,7 +55,7 @@ type: git location: https://github.com/goldfirere/singletons.git subdir: singletons-base- tag: v3.1+ tag: v3.1.1 source-repository head type: git@@ -65,21 +65,21 @@ 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- default-language: Haskell2010+ th-desugar >= 1.14 && < 1.15+ default-language: GHC2021 other-extensions: TemplateHaskell exposed-modules: Data.Singletons.Base.CustomStar Data.Singletons.Base.Enum@@ -149,11 +149,11 @@ type: exitcode-stdio-1.0 hs-source-dirs: tests ghc-options: -Wall -Wcompat -threaded -with-rtsopts=-maxN16- default-language: Haskell2010+ default-language: GHC2021 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,
src/Control/Applicative/Singletons.hs view
@@ -1,15 +1,6 @@ {-# LANGUAGE DataKinds #-}-{-# LANGUAGE DefaultSignatures #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-}
src/Control/Monad/Fail/Singletons.hs view
@@ -1,10 +1,5 @@ {-# LANGUAGE DataKinds #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-}
src/Control/Monad/Singletons.hs view
@@ -1,15 +1,6 @@ {-# LANGUAGE DataKinds #-}-{-# LANGUAGE DefaultSignatures #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-}
src/Control/Monad/Singletons/Internal.hs view
@@ -1,16 +1,8 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE NoNamedWildCards #-} {-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} -----------------------------------------------------------------------------
src/Control/Monad/Zip/Singletons.hs view
@@ -1,15 +1,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} -----------------------------------------------------------------------------
src/Data/Bool/Singletons.hs view
@@ -1,6 +1,8 @@-{-# LANGUAGE TemplateHaskell, TypeApplications, TypeFamilies, TypeOperators,- GADTs, ScopedTypeVariables, DeriveDataTypeable, UndecidableInstances,- DataKinds, PolyKinds, StandaloneKindSignatures #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE NoNamedWildCards #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-} ----------------------------------------------------------------------------- -- |
src/Data/Either/Singletons.hs view
@@ -1,6 +1,7 @@-{-# LANGUAGE TemplateHaskell, ScopedTypeVariables, TypeFamilies, GADTs,- RankNTypes, UndecidableInstances, DataKinds, PolyKinds,- TypeApplications, StandaloneKindSignatures #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-} ----------------------------------------------------------------------------- -- |
src/Data/Eq/Singletons.hs view
@@ -1,8 +1,8 @@-{-# LANGUAGE TypeOperators, DataKinds, PolyKinds, TypeFamilies,- RankNTypes, FlexibleContexts, TemplateHaskell,- UndecidableInstances, GADTs, DefaultSignatures,- ScopedTypeVariables, TypeApplications, StandaloneKindSignatures,- InstanceSigs #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-} ----------------------------------------------------------------------------- -- |
src/Data/Foldable/Singletons.hs view
@@ -1,17 +1,10 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE NoNamedWildCards #-} {-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-}+ ----------------------------------------------------------------------------- -- | -- Module : Data.Foldable.Singletons
src/Data/Function/Singletons.hs view
@@ -1,3 +1,8 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}+ ----------------------------------------------------------------------------- -- | -- Module : Data.Function.Singletons@@ -16,11 +21,6 @@ -- between Template Haskell and Haddock. -- ------------------------------------------------------------------------------{-# LANGUAGE TemplateHaskell, ScopedTypeVariables, TypeFamilies,- TypeOperators, UndecidableInstances, GADTs,- DataKinds, PolyKinds, TypeApplications,- StandaloneKindSignatures #-} module Data.Function.Singletons ( -- * "Prelude" re-exports
src/Data/Functor/Compose/Singletons.hs view
@@ -1,13 +1,6 @@ {-# LANGUAGE DataKinds #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-}
src/Data/Functor/Const/Singletons.hs view
@@ -1,14 +1,7 @@ {-# LANGUAGE DataKinds #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE NoNamedWildCards #-} {-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-}
src/Data/Functor/Identity/Singletons.hs view
@@ -1,13 +1,6 @@ {-# LANGUAGE DataKinds #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE MagicHash #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE NoNamedWildCards #-} {-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-}
src/Data/Functor/Product/Singletons.hs view
@@ -1,13 +1,6 @@ {-# LANGUAGE DataKinds #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-}
src/Data/Functor/Singletons.hs view
@@ -1,16 +1,7 @@ {-# LANGUAGE DataKinds #-}-{-# LANGUAGE DefaultSignatures #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE NoNamedWildCards #-} {-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-}
src/Data/Functor/Sum/Singletons.hs view
@@ -1,13 +1,6 @@ {-# LANGUAGE DataKinds #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-}
src/Data/List/NonEmpty/Singletons.hs view
@@ -1,7 +1,7 @@-{-# LANGUAGE TemplateHaskell, ScopedTypeVariables, TypeOperators,- TypeFamilies, GADTs, UndecidableInstances, InstanceSigs,- DataKinds, PolyKinds, TypeApplications,- StandaloneKindSignatures #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-} -----------------------------------------------------------------------------
src/Data/List/Singletons/Internal.hs view
@@ -1,7 +1,8 @@-{-# LANGUAGE TypeOperators, DataKinds, PolyKinds, TypeFamilies,- TemplateHaskell, GADTs, UndecidableInstances, RankNTypes,- ScopedTypeVariables, FlexibleContexts,- TypeApplications, StandaloneKindSignatures #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE NoNamedWildCards #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -O0 #-} -----------------------------------------------------------------------------
src/Data/List/Singletons/Internal/Disambiguation.hs view
@@ -1,3 +1,8 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}+ ----------------------------------------------------------------------------- -- | -- Module : Data.List.Singletons.Internal.Disambiguation@@ -11,10 +16,6 @@ -- names. :( -- ------------------------------------------------------------------------------{-# LANGUAGE TemplateHaskell, ScopedTypeVariables, TypeFamilies,- UndecidableInstances, GADTs, DataKinds, PolyKinds,- TypeApplications, StandaloneKindSignatures #-} module Data.List.Singletons.Internal.Disambiguation where
src/Data/Maybe/Singletons.hs view
@@ -1,6 +1,7 @@-{-# LANGUAGE TemplateHaskell, ScopedTypeVariables, TypeFamilies,- DataKinds, PolyKinds, UndecidableInstances, GADTs, RankNTypes,- TypeApplications, StandaloneKindSignatures #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-} ----------------------------------------------------------------------------- -- |
src/Data/Monoid/Singletons.hs view
@@ -1,17 +1,8 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE NoNamedWildCards #-} {-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-}
src/Data/Ord/Singletons.hs view
@@ -1,8 +1,8 @@-{-# LANGUAGE TemplateHaskell, DataKinds, PolyKinds, ScopedTypeVariables,- TypeFamilies, TypeOperators, GADTs, UndecidableInstances,- FlexibleContexts, DefaultSignatures, InstanceSigs,- StandaloneDeriving, FlexibleInstances, TypeApplications,- StandaloneKindSignatures #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-} -----------------------------------------------------------------------------
src/Data/Ord/Singletons/Disambiguation.hs view
@@ -1,10 +1,5 @@ {-# LANGUAGE DataKinds #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-}
src/Data/Proxy/Singletons.hs view
@@ -1,12 +1,5 @@ {-# LANGUAGE DataKinds #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-}
src/Data/Semigroup/Singletons.hs view
@@ -1,17 +1,7 @@ {-# LANGUAGE DataKinds #-}-{-# LANGUAGE DefaultSignatures #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE NoNamedWildCards #-} {-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-}
src/Data/Semigroup/Singletons/Internal.hs view
@@ -1,17 +1,8 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE NoNamedWildCards #-} {-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-}
src/Data/Semigroup/Singletons/Internal/Disambiguation.hs view
@@ -1,10 +1,5 @@ {-# LANGUAGE DataKinds #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-}
src/Data/Singletons/Base/Enum.hs view
@@ -1,7 +1,8 @@-{-# LANGUAGE TemplateHaskell, DataKinds, PolyKinds, ScopedTypeVariables,- TypeFamilies, TypeOperators, GADTs, UndecidableInstances,- FlexibleContexts, DefaultSignatures, BangPatterns,- InstanceSigs, TypeApplications, StandaloneKindSignatures #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-} ----------------------------------------------------------------------------- -- |
src/Data/Singletons/Base/Instances.hs view
@@ -1,3 +1,9 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wno-orphans #-}+ {- Data/Singletons/Base/Instances.hs (c) Richard Eisenberg 2013@@ -7,12 +13,6 @@ re-exported from various places. -}--{-# LANGUAGE DataKinds, PolyKinds, RankNTypes, GADTs, TypeFamilies, EmptyCase,- FlexibleContexts, TemplateHaskell, ScopedTypeVariables,- UndecidableInstances, TypeOperators, FlexibleInstances,- TypeApplications, StandaloneKindSignatures, StandaloneDeriving #-}-{-# OPTIONS_GHC -Wno-orphans #-} module Data.Singletons.Base.Instances ( module Data.Singletons.Base.Instances
src/Data/Singletons/Base/SomeSing.hs view
@@ -1,8 +1,5 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving #-} {-# OPTIONS_GHC -Wno-orphans #-} -----------------------------------------------------------------------------
src/Data/Singletons/Base/TypeError.hs view
@@ -1,15 +1,8 @@ {-# LANGUAGE DataKinds #-}-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-}+ ----------------------------------------------------------------------------- -- | -- Module : Data.Singletons.Base.TypeError
src/Data/Singletons/Base/TypeRepTYPE.hs view
@@ -1,7 +1,5 @@-{-# LANGUAGE RankNTypes, TypeFamilies, FlexibleInstances,- GADTs, UndecidableInstances, ScopedTypeVariables,- MagicHash, TypeOperators, PolyKinds, TypeApplications,- StandaloneKindSignatures #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-} -----------------------------------------------------------------------------
src/Data/Singletons/Base/Util.hs view
@@ -1,3 +1,5 @@+{-# LANGUAGE TemplateHaskellQuotes #-}+ {- Data/Singletons/Prelude/Util.hs (c) Richard Eisenberg 2013@@ -7,7 +9,6 @@ Users of the package should not need to consult this file. -} -{-# LANGUAGE TemplateHaskellQuotes #-} module Data.Singletons.Base.Util where import Data.Functor.Identity
src/Data/String/Singletons.hs view
@@ -1,11 +1,5 @@ {-# LANGUAGE DataKinds #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-}
src/Data/Traversable/Singletons.hs view
@@ -1,17 +1,10 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE NoNamedWildCards #-} {-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-}+ ----------------------------------------------------------------------------- -- | -- Module : Data.Traversable.Singletons
src/Data/Tuple/Singletons.hs view
@@ -1,6 +1,7 @@-{-# LANGUAGE TemplateHaskell, ScopedTypeVariables, DataKinds, PolyKinds,- RankNTypes, TypeFamilies, GADTs, UndecidableInstances,- TypeApplications, StandaloneKindSignatures #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-} ----------------------------------------------------------------------------- -- |
src/Data/Void/Singletons.hs view
@@ -1,13 +1,8 @@ {-# LANGUAGE DataKinds #-}-{-# LANGUAGE EmptyCase #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-}+ ----------------------------------------------------------------------------- -- | -- Module : Data.Void.Singletons
src/GHC/Base/Singletons.hs view
@@ -1,7 +1,7 @@-{-# LANGUAGE TemplateHaskell, TypeOperators, DataKinds, PolyKinds,- ScopedTypeVariables, TypeFamilies, GADTs,- UndecidableInstances, BangPatterns, TypeApplications,- StandaloneKindSignatures #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-} ----------------------------------------------------------------------------- -- |
src/GHC/Num/Singletons.hs view
@@ -1,8 +1,9 @@-{-# LANGUAGE TemplateHaskell, PolyKinds, DataKinds, TypeFamilies,- TypeOperators, GADTs, ScopedTypeVariables, UndecidableInstances,- DefaultSignatures, FlexibleContexts, InstanceSigs, NoStarIsType,- TypeApplications, StandaloneKindSignatures- #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE NoStarIsType #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-} ----------------------------------------------------------------------------- -- |
src/GHC/TypeLits/Singletons.hs view
@@ -1,6 +1,8 @@-{-# LANGUAGE TemplateHaskell, ScopedTypeVariables, ConstraintKinds,- GADTs, TypeApplications, TypeFamilies, UndecidableInstances,- DataKinds, PolyKinds, StandaloneKindSignatures #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wno-orphans #-} ----------------------------------------------------------------------------- -- |@@ -15,8 +17,6 @@ -- kinds. -- ------------------------------------------------------------------------------{-# OPTIONS_GHC -Wno-orphans #-} module GHC.TypeLits.Singletons ( Natural, Symbol, Char,
src/GHC/TypeLits/Singletons/Internal.hs view
@@ -1,3 +1,9 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wno-orphans #-}+ ----------------------------------------------------------------------------- -- | -- Module : GHC.TypeLits.Singletons.Internal@@ -12,12 +18,6 @@ -- "GHC.TypeLits.Singletons" for a safe interface. -- ------------------------------------------------------------------------------{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, FlexibleInstances,- UndecidableInstances, ScopedTypeVariables, RankNTypes,- GADTs, FlexibleContexts, TypeOperators, ConstraintKinds,- TemplateHaskell, TypeApplications, StandaloneKindSignatures #-}-{-# OPTIONS_GHC -Wno-orphans #-} module GHC.TypeLits.Singletons.Internal ( Sing,
src/Prelude/Singletons.hs view
@@ -1,3 +1,6 @@+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE NoStarIsType #-}+ ----------------------------------------------------------------------------- -- | -- Module : Prelude.Singletons@@ -17,8 +20,6 @@ -- ---------------------------------------------------------------------------- -{-# LANGUAGE ExplicitNamespaces #-}-{-# LANGUAGE NoStarIsType #-} module Prelude.Singletons ( -- * Basic singleton definitions module Data.Singletons,
src/Text/Show/Singletons.hs view
@@ -1,17 +1,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-}-{-# LANGUAGE EmptyCase #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} -----------------------------------------------------------------------------
tests/SingletonsBaseTestSuite.hs view
@@ -143,6 +143,7 @@ , compileAndDumpStdTest "T489" , compileAndDumpStdTest "T492" , compileAndDumpStdTest "Natural"+ , compileAndDumpStdTest "T511" ], testCompileAndDumpGroup "Promote" [ compileAndDumpStdTest "Constructors"
tests/SingletonsBaseTestSuiteUtils.hs view
@@ -1,8 +1,7 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DerivingStrategies #-}-{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE TypeApplications #-}+ module SingletonsBaseTestSuiteUtils ( compileAndDumpTest , compileAndDumpStdTest@@ -24,6 +23,7 @@ , callCommand ) import Test.Tasty ( TestTree, testGroup ) import Test.Tasty.Golden ( goldenVsFileDiff )+import qualified Data.Text as Text import qualified Turtle -- Some infractructure for handling external process errors@@ -46,31 +46,18 @@ , "-fprint-explicit-kinds" , "-O0" , "-i" ++ goldenPath+ , "-XGHC2021" , "-XTemplateHaskell" , "-XDataKinds"- , "-XKindSignatures" , "-XTypeFamilies"- , "-XTypeOperators"- , "-XMultiParamTypeClasses" , "-XGADTs"- , "-XFlexibleInstances" , "-XUndecidableInstances"- , "-XRankNTypes"- , "-XScopedTypeVariables"- , "-XPolyKinds"- , "-XFlexibleContexts" , "-XIncoherentInstances" , "-XLambdaCase" , "-XUnboxedTuples"- , "-XInstanceSigs" , "-XDefaultSignatures" , "-XCPP"- , "-XStandaloneDeriving"- , "-XTypeApplications"- , "-XEmptyCase" , "-XNoStarIsType"- , "-XStandaloneKindSignatures"- , "-XConstraintKinds" , "-XNoNamedWildCards" ] @@ -154,6 +141,38 @@ This allows inserting comments into test files without the need to modify the golden file to adjust line numbers.++Note [Normalizing Windows path separators]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+File paths are printed differently by GHC depending on which operating system+one uses:++* On Unix-like operating systems: Foo/Bar.hs+* On Windows: Foo\Bar.hs++This is annoying for golden testing, since it means that checking in output+that prints file paths will only work on some operating systems and not others.+To circumvent this problem, we normalize Windows-style path separators to+Unix-like ones.++One way to do this is to replace all occurrences of the '\' character with '/'.+This is a step too far, however, since this will normalize things like+(\x -> x) to (/x -> x). A reasonable middle ground is to require that the+characters before and after the '\' character are alphanumeric before+normalizing it. This just so happens to be the case for every path that is+checked into the singletons-base test suite. This approach isn't perfect, since+one could check in a golden file that prints a path with a non-alphanumeric+character. This seems very unlikely to happen, however, so we will only worry+about that issue should it ever arise in practice.++Moreover, this approach would normalize expressions like (id\x -> x)+to (id/x -> x), which could hypothetically happen with BlockArguments. However,+the vast majority of the expressions that we check into golden files arise from+-ddump-splices output, which puts surrounding whitespace after the backslashes+in lambda expressions. As a result, the expression above would be+pretty-printed as (id \ x -> x), which avoids the issue entirely. Again, we+will choose not to worry about this corner case unless it becomes an issue in+practice. -} normalizeOutput :: FilePath -> IO ()@@ -170,6 +189,10 @@ -- (e.g., turn `singletons-2.4.1:Sing` into `Sing`) to make the output -- more stable. , "" <$ "singletons-" <* verNum <* ":"+ , do x <- Turtle.alphaNum+ _ <- Turtle.char '\\'+ y <- Turtle.alphaNum+ pure $ Text.pack [x, '/', y] ] verNum = d `Turtle.sepBy` Turtle.char '.' numPair = () <$ "(" <* d <* "," <* d <* ")"
tests/compile-and-dump/GradingClient/Database.hs view
@@ -8,12 +8,6 @@ -} -{-# LANGUAGE PolyKinds, DataKinds, TemplateHaskell, TypeFamilies,- GADTs, TypeOperators, RankNTypes, FlexibleContexts, UndecidableInstances,- FlexibleInstances, ScopedTypeVariables, MultiParamTypeClasses,- ConstraintKinds, InstanceSigs #-}-{-# OPTIONS_GHC -Wno-warnings-deprecations #-}- -- The OverlappingInstances is needed only to allow the InC and SubsetC classes. -- This is simply a convenience so that GHC can infer the necessary proofs of -- schema inclusion. The library could easily be designed without this flag,
tests/compile-and-dump/GradingClient/Main.hs view
@@ -8,8 +8,6 @@ -} -{-# LANGUAGE TemplateHaskell, DataKinds #-}- module Main where import Data.List.Singletons
tests/compile-and-dump/InsertionSort/InsertionSortImp.hs view
@@ -27,11 +27,6 @@ -} -{-# LANGUAGE IncoherentInstances, ConstraintKinds, TypeFamilies,- TemplateHaskell, RankNTypes, ScopedTypeVariables, GADTs,- TypeOperators, DataKinds, PolyKinds, MultiParamTypeClasses,- FlexibleContexts, FlexibleInstances, UndecidableInstances #-}- module InsertionSort.InsertionSortImp where import Data.Kind (Type)
tests/compile-and-dump/Singletons/AsPattern.golden view
@@ -360,7 +360,7 @@ 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)
tests/compile-and-dump/Singletons/BoxUnBox.golden view
@@ -38,7 +38,7 @@ 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
tests/compile-and-dump/Singletons/Classes.golden view
@@ -324,7 +324,7 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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
tests/compile-and-dump/Singletons/Classes2.golden view
@@ -59,7 +59,7 @@ 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 @@ 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
tests/compile-and-dump/Singletons/DataValues.golden view
@@ -122,7 +122,7 @@ ((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 @@ -> 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)
tests/compile-and-dump/Singletons/Empty.golden view
@@ -2,7 +2,7 @@ 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
tests/compile-and-dump/Singletons/EmptyShowDeriving.golden view
@@ -46,7 +46,7 @@ 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 @@ -> 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)
tests/compile-and-dump/Singletons/EnumDeriving.golden view
@@ -70,7 +70,7 @@ 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 @@ 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 @@ 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 @@ 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)))))
tests/compile-and-dump/Singletons/EqInstances.golden view
@@ -35,7 +35,7 @@ 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 @@ 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
tests/compile-and-dump/Singletons/FunctorLikeDeriving.golden view
@@ -954,11 +954,11 @@ (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
tests/compile-and-dump/Singletons/FunctorLikeDeriving.hs view
@@ -1,4 +1,3 @@-{-# LANGUAGE DeriveTraversable #-} -- Ensure that we can derive Functor, Foldable, and Traversable using only -- an import of Data.Singletons.TH module FunctorLikeDeriving where
tests/compile-and-dump/Singletons/HigherOrder.golden view
@@ -476,7 +476,7 @@ 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)
tests/compile-and-dump/Singletons/Lambdas.golden view
@@ -752,7 +752,7 @@ 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)
tests/compile-and-dump/Singletons/Lambdas.hs view
@@ -1,6 +1,5 @@ {-# OPTIONS_GHC -Wno-unused-matches -Wno-name-shadowing #-} -{-# LANGUAGE UnboxedTuples #-} -- We expect unused binds and name shadowing in foo5 test. module Singletons.Lambdas where
tests/compile-and-dump/Singletons/Maybe.golden view
@@ -91,7 +91,7 @@ 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 @@ 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 @@ -> 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 @@ 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 =>
tests/compile-and-dump/Singletons/Nat.golden view
@@ -195,7 +195,7 @@ 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 @@ 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 @@ -> 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 @@ 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 @@ 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 =>
tests/compile-and-dump/Singletons/Natural.golden view
@@ -60,7 +60,7 @@ 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
tests/compile-and-dump/Singletons/NegativeLiterals.golden view
@@ -17,5 +17,5 @@ Singletons/NegativeLiterals.hs:0:0: warning: [-Woverflowed-literals] Literal -1 is negative but Natural only supports positive numbers |-7 | $(singletons [d|+8 | $(singletons [d| | ^^^^^^^^^^^^^^^...
tests/compile-and-dump/Singletons/NegativeLiterals.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE NegativeLiterals #-}+ module Singletons.NegativeLiterals where import Data.Singletons.Base.TH
tests/compile-and-dump/Singletons/Operators.golden view
@@ -103,7 +103,7 @@ = (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).
tests/compile-and-dump/Singletons/OrdDeriving.golden view
@@ -463,7 +463,7 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ (,,,) _ _ _ (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
tests/compile-and-dump/Singletons/OverloadedStrings.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE OverloadedStrings #-}+ module OverloadedStrings where import Data.Singletons.Base.TH
tests/compile-and-dump/Singletons/PatternMatching.golden view
@@ -122,7 +122,7 @@ ((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 @@ -> 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)
tests/compile-and-dump/Singletons/Records.golden view
@@ -61,7 +61,7 @@ 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)
tests/compile-and-dump/Singletons/ShowDeriving.golden view
@@ -292,14 +292,13 @@ 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 @@ 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 @@ -> 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 @@ -> 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 @@ -> 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)
tests/compile-and-dump/Singletons/StandaloneDeriving.golden view
@@ -302,7 +302,7 @@ 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 @@ 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 @@ 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 @@ 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 @@ -> 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 @@ 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 @@ 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 @@ -> 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 @@ 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 @@ (,) _ (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 @@ (%~) 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 =>
tests/compile-and-dump/Singletons/T136.golden view
@@ -115,20 +115,18 @@ 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))
tests/compile-and-dump/Singletons/T136.hs view
@@ -1,10 +1,3 @@-{-# LANGUAGE GADTs, DataKinds, PolyKinds, TypeFamilies, KindSignatures #-}-{-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}-{-# LANGUAGE InstanceSigs, DefaultSignatures #-}- module Binary where import Data.Singletons.Base.Enum
tests/compile-and-dump/Singletons/T136b.golden view
@@ -49,6 +49,6 @@ 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
tests/compile-and-dump/Singletons/T153.hs view
@@ -1,6 +1,3 @@-{-# LANGUAGE LambdaCase, GADTs, ScopedTypeVariables,- TypeApplications, RankNTypes #-}- module Singletons.T153 where import Data.Singletons
tests/compile-and-dump/Singletons/T159.golden view
@@ -19,8 +19,8 @@ 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 @@ 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 @@ 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).
tests/compile-and-dump/Singletons/T163.golden view
@@ -24,7 +24,7 @@ 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)
tests/compile-and-dump/Singletons/T166.golden view
@@ -144,6 +144,6 @@ -> Type’ • In the type ‘Apply Lambda_0123456789876543210Sym0 x’ In the type family declaration for ‘Foo_0123456789876543210’- |-14 | $(singletonsOnly [d|- | ^^^^^^^^^^^^^^^^^^^...+ |+6 | $(singletonsOnly [d|+ | ^^^^^^^^^^^^^^^^^^^...
tests/compile-and-dump/Singletons/T166.hs view
@@ -1,11 +1,3 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE DefaultSignatures #-}-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeFamilies #-} module SingletonsBug where import Data.Singletons.Base.TH
tests/compile-and-dump/Singletons/T167.hs view
@@ -1,13 +1,3 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE DefaultSignatures #-}-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE UndecidableInstances #-} module Singletons.T167 where import Data.Singletons.Base.TH
tests/compile-and-dump/Singletons/T172.hs view
@@ -1,11 +1,3 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-} module T172 where import Data.Singletons.TH
tests/compile-and-dump/Singletons/T175.hs view
@@ -1,13 +1,3 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE DefaultSignatures #-}-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE FlexibleContexts #-}- module T175 where import Data.Singletons.TH
tests/compile-and-dump/Singletons/T176.hs view
@@ -1,11 +1,3 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE DefaultSignatures #-}-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE UndecidableInstances #-} module T176 where import Data.Kind (Type)
tests/compile-and-dump/Singletons/T178.golden view
@@ -142,7 +142,7 @@ 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 @@ 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 @@ 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 @@ -> 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 @@ (%~) 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))
tests/compile-and-dump/Singletons/T184.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE ParallelListComp #-}+ module T184 where import Control.Monad
tests/compile-and-dump/Singletons/T187.golden view
@@ -61,7 +61,7 @@ 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 @@ 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
tests/compile-and-dump/Singletons/T190.golden view
@@ -153,7 +153,7 @@ 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 @@ 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 @@ 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 @@ -> 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 @@ 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))
tests/compile-and-dump/Singletons/T190.hs view
@@ -1,10 +1,3 @@-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE InstanceSigs #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE UndecidableInstances #-} module T190 where import Data.Singletons.Base.TH
tests/compile-and-dump/Singletons/T197b.golden view
@@ -51,7 +51,7 @@ 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 @@ 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)
tests/compile-and-dump/Singletons/T200.golden view
@@ -143,7 +143,7 @@ -> (~>) 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)
tests/compile-and-dump/Singletons/T209.golden view
@@ -77,7 +77,7 @@ 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
tests/compile-and-dump/Singletons/T209.hs view
@@ -1,5 +1,6 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DerivingStrategies #-}+ module T209 where import Data.Singletons.TH
tests/compile-and-dump/Singletons/T271.golden view
@@ -157,8 +157,8 @@ 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)
tests/compile-and-dump/Singletons/T326.golden view
@@ -23,8 +23,8 @@ 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 @@ 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 @(<%%>@#@$)) (%<%%>)
tests/compile-and-dump/Singletons/T33.golden view
@@ -27,13 +27,13 @@ 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| | ^^^^^^^^^^^^^^^...
tests/compile-and-dump/Singletons/T332.golden view
@@ -56,8 +56,7 @@ 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
tests/compile-and-dump/Singletons/T412.golden view
@@ -160,7 +160,7 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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)
tests/compile-and-dump/Singletons/T450.golden view
@@ -47,8 +47,8 @@ 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 @@ 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 @@ 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 @@ 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
+ tests/compile-and-dump/Singletons/T511.golden view
@@ -0,0 +1,13 @@++Singletons/T511.hs:0:0: error: Q monad failure+ |+7 | $(singletons [d|+ | ^^^^^^^^^^^^^^^...++Singletons/T511.hs:0:0: error:+ `singletons-th` does not support partial applications of (->)+ In the type: Data.Proxy.Proxy (->)++ |+7 | $(singletons [d|+ | ^^^^^^^^^^^^^^^...
+ tests/compile-and-dump/Singletons/T511.hs view
@@ -0,0 +1,9 @@+module T511 where++import Data.Proxy+import Data.Proxy.Singletons+import Data.Singletons.TH++$(singletons [d|+ data Foo = MkFoo (Proxy (->))+ |])
tests/compile-and-dump/Singletons/TopLevelPatterns.golden view
@@ -32,7 +32,7 @@ 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 @@ 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)
tests/compile-and-dump/Singletons/TypeRepTYPE.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE MagicHash #-}+ module TypeRepTYPE where import Data.Kind (Type)