singletons 2.5 → 2.5.1
raw patch · 12 files changed
+355/−16 lines, 12 files
Files
- CHANGES.md +9/−0
- README.md +6/−3
- singletons.cabal +3/−3
- src/Data/Singletons.hs +6/−1
- src/Data/Singletons/Prelude/Monoid.hs +0/−2
- src/Data/Singletons/Prelude/Semigroup.hs +0/−1
- src/Data/Singletons/ShowSing.hs +77/−3
- tests/SingletonsTestSuite.hs +1/−0
- tests/SingletonsTestSuiteUtils.hs +0/−1
- tests/compile-and-dump/Singletons/T358.ghc86.template +4/−2
- tests/compile-and-dump/Singletons/T371.ghc86.template +233/−0
- tests/compile-and-dump/Singletons/T371.hs +16/−0
CHANGES.md view
@@ -1,6 +1,15 @@ Changelog for singletons project ================================ +2.5.1+-----+* `ShowSing` is now a type class (with a single instance) instead of a type+ synonym. This was changed because defining `ShowSing` as a type synonym+ prevents it from working well with recursive types due to an unfortunate GHC+ bug. For more information, see+ [issue #371](https://github.com/goldfirere/singletons/issues/371).+* Add an `IsString` instance for `SomeSing`.+ 2.5 --- * The `Data.Promotion.Prelude.*` namespace has been removed. Use the
README.md view
@@ -1,5 +1,5 @@-singletons 2.5-==============+singletons 2.5.1+================ [](http://hackage.haskell.org/package/singletons) [](https://travis-ci.org/goldfirere/singletons)@@ -33,6 +33,10 @@ `Data.Maybe`, `Data.Either`, `Data.Tuple` and `Data.List`. See the promotion paper for a more thorough introduction. +[This blog series](https://blog.jle.im/entry/introduction-to-singletons-1.html),+authored by Justin Le, offers a tutorial for this library that assumes no+knowledge of dependent types.+ Compatibility ------------- @@ -52,7 +56,6 @@ * `KindSignatures` * `NoStarIsType` * `PolyKinds`-* `QuantifiedConstraints` * `RankNTypes` * `ScopedTypeVariables` * `StandaloneDeriving`
singletons.cabal view
@@ -1,5 +1,5 @@ name: singletons-version: 2.5+version: 2.5.1 -- Remember to bump version in the Makefile as well cabal-version: >= 1.10 synopsis: A framework for generating singleton types@@ -9,7 +9,7 @@ maintainer: Ryan Scott <ryan.gl.scott@gmail.com> bug-reports: https://github.com/goldfirere/singletons/issues stability: experimental-tested-with: GHC == 8.6.1+tested-with: GHC == 8.6.2 extra-source-files: README.md, CHANGES.md, tests/compile-and-dump/buildGoldenFiles.awk, tests/compile-and-dump/GradingClient/*.hs,@@ -38,7 +38,7 @@ source-repository this type: git location: https://github.com/goldfirere/singletons.git- tag: v2.5+ tag: v2.5.1 source-repository head type: git
src/Data/Singletons.hs view
@@ -5,7 +5,6 @@ {-# LANGUAGE MagicHash #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE PolyKinds #-}-{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-}@@ -86,12 +85,15 @@ import Data.Singletons.Internal import Data.Singletons.Prelude.Enum import Data.Singletons.Prelude.Eq+import Data.Singletons.Prelude.IsString import Data.Singletons.Prelude.Monoid import Data.Singletons.Prelude.Num import Data.Singletons.Prelude.Ord import Data.Singletons.Prelude.Semigroup import Data.Singletons.Promote import Data.Singletons.ShowSing+import Data.String+import qualified Data.Text as T (pack) ---------------------------------------------------------------------- ---- SomeSing instances ----------------------------------------------@@ -138,6 +140,9 @@ instance SMonoid k => Monoid (SomeSing k) where mempty = SomeSing sMempty++instance SIsString k => IsString (SomeSing k) where+ fromString s = withSomeSing (T.pack s) (SomeSing . sFromString) ---------------------------------------------------------------------- ---- Defunctionalization symbols -------------------------------------
src/Data/Singletons/Prelude/Monoid.hs view
@@ -4,7 +4,6 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE PolyKinds #-}-{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-}@@ -174,7 +173,6 @@ -- deriving newtype instance Monoid a => Monoid (Down a) instance Monoid a => Monoid (Down a) where mempty = Down mempty- Down a `mappend` Down b = Down (a `mappend` b) -- deriving newtype instance Applicative First instance Applicative First where
src/Data/Singletons/Prelude/Semigroup.hs view
@@ -4,7 +4,6 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE PolyKinds #-}-{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-}
src/Data/Singletons/ShowSing.hs view
@@ -29,7 +29,6 @@ ShowSing ) where -import Data.Kind import Data.Singletons.Internal import Data.Singletons.Prelude.Instances import Data.Singletons.Single@@ -70,7 +69,7 @@ -- @ -- -- Because that quantified constraint is somewhat lengthy, we provide the--- 'ShowSing' type synonym as a convenient shorthand. Thus, the above instance+-- 'ShowSing' class synonym as a convenient shorthand. Thus, the above instance -- is equivalent to: -- -- @@@ -87,7 +86,82 @@ -- * A 'Show' instance for the singleton type -- -- What a bargain!-type ShowSing k = (forall z. Show (Sing (z :: k)) :: Constraint)+class (forall (z :: k). Show (Sing z)) => ShowSing k+instance (forall (z :: k). Show (Sing z)) => ShowSing k++{-+Note [Define ShowSing as a class, not a type synonym]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+In an ideal world, we would simply define ShowSing as an ordinary type synonym,+like this:++ type ShowSing k = (forall (z :: k). Show (Sing z) :: Constraint)++In fact, I used to assume that we lived in an ideal world, so I defined+ShowSing as a type synonym in version 2.5 of this library. However, I realized+some time after 2.5's release that the world is far from ideal, unfortunately,+and that this approach is unfeasible at the time being due to GHC Trac #15888.++To be more precise, the exact issue involves an infelicity in the way+QuantifiedConstraints interacts with recursive type class instances.+Consider the following example (from #371):++ $(singletons [d|+ data X a = X1 | X2 (Y a) deriving Show+ data Y a = Y1 | Y2 (X a) deriving Show+ |])++This will generate the following instances:++ deriving instance ShowSing (Y a) => Show (Sing (z :: X a))+ deriving instance ShowSing (X a) => Show (Sing (z :: Y a))++So far, so good. Now, suppose you try to actually `show` a singleton for X.+For example:++ show (sing @(X1 :: X Bool))++Somewhat surprisingly, this will be rejected by the typechecker with the+following error:++ • Reduction stack overflow; size = 201+ When simplifying the following type: Show (Sing z)++To see why this happens, observe what goes on if we expand the occurrences of+the ShowSing type synonym in the generated instances:++ deriving instance (forall z. Show (Sing (z :: Y a))) => Show (Sing (z :: X a))+ deriving instance (forall z. Show (Sing (z :: X a))) => Show (Sing (z :: Y a))++Due to the way QuantifiedConstraints currently works (as surmised in Trac+#15888), when GHC has a Wanted `Show (Sing X1 :: X Bool)` constraint, it+chooses the appropriate instance and emits a Wanted+`forall z. Show (Sing (z :: Y Bool))` constraint (from the instance context).+GHC skolemizes the `z` to `z1` and tries to solve a Wanted+`Show (Sing (z1 :: Y Bool))` constraint. GHC chooses the appropriate instance+and emits a Wanted `forall z. Show (Sing (z :: X Bool))` constraint. GHC+skolemizes the `z` to `z2` and tries to solve a Wanted+`Show (Sing (z2 :: X Bool))` constraint... we repeat the process and find+ourselves in an infinite loop that eventually overflows the reduction stack.+Eep.++Until Trac #15888 is fixed, there are two possible ways to work around this+problem:++1. Make derived instances' type inference more clever. If you look closely,+ you'll notice that the `ShowSing (X a)`/`ShowSing (Y a)` constraints in+ the generated instances are entirely redundant and could safely be left+ off. But determining this would require significantly improving singletons'+ Template Haskell capabilities for type inference, which is a path that we+ usually spurn in favor of keeping the generated code dumb but predictable.+2. Define `ShowSing` as a class (with a single instance) instead of a type+ synonym. `ShowSing`-as-a-class ties the recursive knot during instance+ resolution and thus avoids the problems that the type synonym version+ currently suffers from.++Given the two options, (2) is by far the easier option, so that is what we+ultimately went with.+-} ------------------------------------------------------------ -- TypeLits instances
tests/SingletonsTestSuite.hs view
@@ -102,6 +102,7 @@ , compileAndDumpStdTest "FunctorLikeDeriving" , compileAndDumpStdTest "T353" , compileAndDumpStdTest "T358"+ , compileAndDumpStdTest "T371" ], testCompileAndDumpGroup "Promote" [ compileAndDumpStdTest "Constructors"
tests/SingletonsTestSuiteUtils.hs view
@@ -69,7 +69,6 @@ , "-XTypeApplications" , "-XEmptyCase" , "-XNoStarIsType"- , "-XQuantifiedConstraints" ] -- Compile a test using specified GHC options. Save output to file, filter with
tests/compile-and-dump/Singletons/T358.ghc86.template view
@@ -108,8 +108,10 @@ forall b (t :: b). Sing t -> Sing (Apply Method2aSym0 t :: [a]) sMethod2b :: forall b (t :: b). Sing t -> Sing (Apply Method2bSym0 t :: [a])- sMethod2a _ = Data.Singletons.Prelude.Instances.SNil- sMethod2b _ = Data.Singletons.Prelude.Instances.SNil+ sMethod2a _+ = Data.Singletons.Prelude.Instances.SNil+ sMethod2b _+ = Data.Singletons.Prelude.Instances.SNil instance SC2 a => SingI (Method2aSym0 :: (~>) b a) where sing = (singFun1 @Method2aSym0) sMethod2a instance SC2 a => SingI (Method2bSym0 :: (~>) b a) where
+ tests/compile-and-dump/Singletons/T371.ghc86.template view
@@ -0,0 +1,233 @@+Singletons/T371.hs:(0,0)-(0,0): Splicing declarations+ singletons+ [d| data Y (a :: Type)+ = Y1 | Y2 (X a)+ deriving Show+ data X (a :: Type)+ = X1 | X2 (Y a)+ deriving Show |]+ ======>+ data X (a :: Type)+ = X1 | X2 (Y a)+ deriving Show+ data Y (a :: Type)+ = Y1 | Y2 (X a)+ deriving Show+ type X1Sym0 = X1+ type X2Sym1 (t0123456789876543210 :: Y a0123456789876543210) =+ X2 t0123456789876543210+ instance SuppressUnusedWarnings X2Sym0 where+ suppressUnusedWarnings = snd (((,) X2Sym0KindInference) ())+ data X2Sym0 :: forall (a0123456789876543210 :: Type).+ (~>) (Y a0123456789876543210) (X (a0123456789876543210 :: Type))+ where+ X2Sym0KindInference :: forall t0123456789876543210+ arg. SameKind (Apply X2Sym0 arg) (X2Sym1 arg) =>+ X2Sym0 t0123456789876543210+ type instance Apply X2Sym0 t0123456789876543210 = X2 t0123456789876543210+ type Y1Sym0 = Y1+ type Y2Sym1 (t0123456789876543210 :: X a0123456789876543210) =+ Y2 t0123456789876543210+ instance SuppressUnusedWarnings Y2Sym0 where+ suppressUnusedWarnings = snd (((,) Y2Sym0KindInference) ())+ data Y2Sym0 :: forall (a0123456789876543210 :: Type).+ (~>) (X a0123456789876543210) (Y (a0123456789876543210 :: Type))+ where+ Y2Sym0KindInference :: forall t0123456789876543210+ arg. SameKind (Apply Y2Sym0 arg) (Y2Sym1 arg) =>+ Y2Sym0 t0123456789876543210+ type instance Apply Y2Sym0 t0123456789876543210 = Y2 t0123456789876543210+ type family ShowsPrec_0123456789876543210 (a :: GHC.Types.Nat) (a :: X a) (a :: GHC.Types.Symbol) :: GHC.Types.Symbol where+ ShowsPrec_0123456789876543210 _ X1 a_0123456789876543210 = Apply (Apply ShowStringSym0 "X1") a_0123456789876543210+ ShowsPrec_0123456789876543210 p_0123456789876543210 (X2 arg_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (Data.Singletons.Prelude.Num.FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "X2 ")) (Apply (Apply ShowsPrecSym0 (Data.Singletons.Prelude.Num.FromInteger 11)) arg_0123456789876543210))) a_0123456789876543210+ type ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: X a0123456789876543210) (a0123456789876543210 :: GHC.Types.Symbol) =+ ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210+ instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) where+ suppressUnusedWarnings+ = snd (((,) ShowsPrec_0123456789876543210Sym2KindInference) ())+ data ShowsPrec_0123456789876543210Sym2 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: X a0123456789876543210) :: (~>) GHC.Types.Symbol GHC.Types.Symbol+ where+ ShowsPrec_0123456789876543210Sym2KindInference :: forall a0123456789876543210+ a0123456789876543210+ a0123456789876543210+ arg. SameKind (Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 arg) =>+ ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 a0123456789876543210+ type instance Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210+ instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) where+ suppressUnusedWarnings+ = snd (((,) ShowsPrec_0123456789876543210Sym1KindInference) ())+ data ShowsPrec_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Types.Nat) :: forall a0123456789876543210.+ (~>) (X a0123456789876543210) ((~>) GHC.Types.Symbol GHC.Types.Symbol)+ where+ ShowsPrec_0123456789876543210Sym1KindInference :: forall a0123456789876543210+ a0123456789876543210+ arg. SameKind (Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 arg) =>+ ShowsPrec_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210+ type instance Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210+ instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym0 where+ suppressUnusedWarnings+ = snd (((,) ShowsPrec_0123456789876543210Sym0KindInference) ())+ data ShowsPrec_0123456789876543210Sym0 :: forall a0123456789876543210.+ (~>) GHC.Types.Nat ((~>) (X a0123456789876543210) ((~>) GHC.Types.Symbol GHC.Types.Symbol))+ where+ ShowsPrec_0123456789876543210Sym0KindInference :: forall a0123456789876543210+ arg. SameKind (Apply ShowsPrec_0123456789876543210Sym0 arg) (ShowsPrec_0123456789876543210Sym1 arg) =>+ ShowsPrec_0123456789876543210Sym0 a0123456789876543210+ type instance Apply ShowsPrec_0123456789876543210Sym0 a0123456789876543210 = ShowsPrec_0123456789876543210Sym1 a0123456789876543210+ instance PShow (X a) where+ type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a+ type family ShowsPrec_0123456789876543210 (a :: GHC.Types.Nat) (a :: Y a) (a :: GHC.Types.Symbol) :: GHC.Types.Symbol where+ ShowsPrec_0123456789876543210 _ Y1 a_0123456789876543210 = Apply (Apply ShowStringSym0 "Y1") a_0123456789876543210+ ShowsPrec_0123456789876543210 p_0123456789876543210 (Y2 arg_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (Data.Singletons.Prelude.Num.FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "Y2 ")) (Apply (Apply ShowsPrecSym0 (Data.Singletons.Prelude.Num.FromInteger 11)) arg_0123456789876543210))) a_0123456789876543210+ type ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: Y a0123456789876543210) (a0123456789876543210 :: GHC.Types.Symbol) =+ ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210+ instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) where+ suppressUnusedWarnings+ = snd (((,) ShowsPrec_0123456789876543210Sym2KindInference) ())+ data ShowsPrec_0123456789876543210Sym2 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: Y a0123456789876543210) :: (~>) GHC.Types.Symbol GHC.Types.Symbol+ where+ ShowsPrec_0123456789876543210Sym2KindInference :: forall a0123456789876543210+ a0123456789876543210+ a0123456789876543210+ arg. SameKind (Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 arg) =>+ ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 a0123456789876543210+ type instance Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210+ instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) where+ suppressUnusedWarnings+ = snd (((,) ShowsPrec_0123456789876543210Sym1KindInference) ())+ data ShowsPrec_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Types.Nat) :: forall a0123456789876543210.+ (~>) (Y a0123456789876543210) ((~>) GHC.Types.Symbol GHC.Types.Symbol)+ where+ ShowsPrec_0123456789876543210Sym1KindInference :: forall a0123456789876543210+ a0123456789876543210+ arg. SameKind (Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 arg) =>+ ShowsPrec_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210+ type instance Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210+ instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym0 where+ suppressUnusedWarnings+ = snd (((,) ShowsPrec_0123456789876543210Sym0KindInference) ())+ data ShowsPrec_0123456789876543210Sym0 :: forall a0123456789876543210.+ (~>) GHC.Types.Nat ((~>) (Y a0123456789876543210) ((~>) GHC.Types.Symbol GHC.Types.Symbol))+ where+ ShowsPrec_0123456789876543210Sym0KindInference :: forall a0123456789876543210+ arg. SameKind (Apply ShowsPrec_0123456789876543210Sym0 arg) (ShowsPrec_0123456789876543210Sym1 arg) =>+ ShowsPrec_0123456789876543210Sym0 a0123456789876543210+ type instance Apply ShowsPrec_0123456789876543210Sym0 a0123456789876543210 = ShowsPrec_0123456789876543210Sym1 a0123456789876543210+ instance PShow (Y a) where+ type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a+ data instance Sing :: X a -> Type+ where+ SX1 :: Sing X1+ SX2 :: forall a (n :: Y a). (Sing (n :: Y a)) -> Sing (X2 n)+ type SX = (Sing :: X a -> Type)+ instance SingKind a => SingKind (X a) where+ type Demote (X a) = X (Demote a)+ fromSing SX1 = X1+ fromSing (SX2 b) = X2 (fromSing b)+ toSing X1 = SomeSing SX1+ toSing (X2 (b :: Demote (Y a)))+ = case toSing b :: SomeSing (Y a) of {+ SomeSing c -> SomeSing (SX2 c) }+ data instance Sing :: Y a -> Type+ where+ SY1 :: Sing Y1+ SY2 :: forall a (n :: X a). (Sing (n :: X a)) -> Sing (Y2 n)+ type SY = (Sing :: Y a -> Type)+ instance SingKind a => SingKind (Y a) where+ type Demote (Y a) = Y (Demote a)+ fromSing SY1 = Y1+ fromSing (SY2 b) = Y2 (fromSing b)+ toSing Y1 = SomeSing SY1+ toSing (Y2 (b :: Demote (X a)))+ = case toSing b :: SomeSing (X a) of {+ SomeSing c -> SomeSing (SY2 c) }+ instance SShow (Y a) => SShow (X a) where+ sShowsPrec ::+ forall (t1 :: GHC.Types.Nat) (t2 :: X a) (t3 :: GHC.Types.Symbol).+ Sing t1+ -> Sing t2+ -> Sing t3+ -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Types.Nat ((~>) (X a) ((~>) GHC.Types.Symbol GHC.Types.Symbol))+ -> Type) t1) t2) t3)+ sShowsPrec+ _+ SX1+ (sA_0123456789876543210 :: Sing a_0123456789876543210)+ = (applySing+ ((applySing ((singFun2 @ShowStringSym0) sShowString))+ (sing :: Sing "X1")))+ sA_0123456789876543210+ sShowsPrec+ (sP_0123456789876543210 :: Sing p_0123456789876543210)+ (SX2 (sArg_0123456789876543210 :: Sing arg_0123456789876543210))+ (sA_0123456789876543210 :: Sing a_0123456789876543210)+ = (applySing+ ((applySing+ ((applySing ((singFun3 @ShowParenSym0) sShowParen))+ ((applySing+ ((applySing ((singFun2 @(>@#@$)) (%>))) sP_0123456789876543210))+ (Data.Singletons.Prelude.Num.sFromInteger (sing :: Sing 10)))))+ ((applySing+ ((applySing ((singFun3 @(.@#@$)) (%.)))+ ((applySing ((singFun2 @ShowStringSym0) sShowString))+ (sing :: Sing "X2 "))))+ ((applySing+ ((applySing ((singFun3 @ShowsPrecSym0) sShowsPrec))+ (Data.Singletons.Prelude.Num.sFromInteger (sing :: Sing 11))))+ sArg_0123456789876543210))))+ sA_0123456789876543210+ instance SShow (X a) => SShow (Y a) where+ sShowsPrec ::+ forall (t1 :: GHC.Types.Nat) (t2 :: Y a) (t3 :: GHC.Types.Symbol).+ Sing t1+ -> Sing t2+ -> Sing t3+ -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Types.Nat ((~>) (Y a) ((~>) GHC.Types.Symbol GHC.Types.Symbol))+ -> Type) t1) t2) t3)+ sShowsPrec+ _+ SY1+ (sA_0123456789876543210 :: Sing a_0123456789876543210)+ = (applySing+ ((applySing ((singFun2 @ShowStringSym0) sShowString))+ (sing :: Sing "Y1")))+ sA_0123456789876543210+ sShowsPrec+ (sP_0123456789876543210 :: Sing p_0123456789876543210)+ (SY2 (sArg_0123456789876543210 :: Sing arg_0123456789876543210))+ (sA_0123456789876543210 :: Sing a_0123456789876543210)+ = (applySing+ ((applySing+ ((applySing ((singFun3 @ShowParenSym0) sShowParen))+ ((applySing+ ((applySing ((singFun2 @(>@#@$)) (%>))) sP_0123456789876543210))+ (Data.Singletons.Prelude.Num.sFromInteger (sing :: Sing 10)))))+ ((applySing+ ((applySing ((singFun3 @(.@#@$)) (%.)))+ ((applySing ((singFun2 @ShowStringSym0) sShowString))+ (sing :: Sing "Y2 "))))+ ((applySing+ ((applySing ((singFun3 @ShowsPrecSym0) sShowsPrec))+ (Data.Singletons.Prelude.Num.sFromInteger (sing :: Sing 11))))+ sArg_0123456789876543210))))+ sA_0123456789876543210+ deriving instance Data.Singletons.ShowSing.ShowSing (Y a) =>+ Show (Sing (z :: X a))+ deriving instance Data.Singletons.ShowSing.ShowSing (X a) =>+ Show (Sing (z :: Y a))+ instance SingI X1 where+ sing = SX1+ instance SingI n => SingI (X2 (n :: Y a)) where+ sing = SX2 sing+ instance SingI (X2Sym0 :: (~>) (Y a) (X (a :: Type))) where+ sing = (singFun1 @X2Sym0) SX2+ instance SingI (TyCon1 X2 :: (~>) (Y a) (X (a :: Type))) where+ sing = (singFun1 @(TyCon1 X2)) SX2+ instance SingI Y1 where+ sing = SY1+ instance SingI n => SingI (Y2 (n :: X a)) where+ sing = SY2 sing+ instance SingI (Y2Sym0 :: (~>) (X a) (Y (a :: Type))) where+ sing = (singFun1 @Y2Sym0) SY2+ instance SingI (TyCon1 Y2 :: (~>) (X a) (Y (a :: Type))) where+ sing = (singFun1 @(TyCon1 Y2)) SY2
+ tests/compile-and-dump/Singletons/T371.hs view
@@ -0,0 +1,16 @@+module T371 where++import Data.Kind+import Data.Singletons.TH++$(singletons [d|+ data X (a :: Type) = X1 | X2 (Y a) deriving Show+ data Y (a :: Type) = Y1 | Y2 (X a) deriving Show+ |])++main :: IO ()+main = do+ print (sing :: Sing ('[] :: [Bool]))+ print (sing :: Sing '[True])+ print (sing :: Sing (X1 :: X Bool))+ print (sing :: Sing (Y2 X1 :: Y Bool))