singletons-base-3.2: tests/compile-and-dump/Singletons/StandaloneDeriving.golden
Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| infixl 6 :*:
data T a b = a :*: b
data S = S1 | S2
deriving instance Enum S
deriving instance Bounded S
deriving instance Show S
deriving instance Ord S
deriving instance Eq S
deriving instance Show a => Show (T a ())
deriving instance Ord a => Ord (T a ())
deriving instance Eq a => Eq (T a ()) |]
======>
infixl 6 :*:
data T a b = a :*: b
data S = S1 | S2
deriving instance Eq a => Eq (T a ())
deriving instance Ord a => Ord (T a ())
deriving instance Show a => Show (T a ())
deriving instance Eq S
deriving instance Ord S
deriving instance Show S
deriving instance Bounded S
deriving instance Enum S
type (:*:@#@$) :: forall a b. (~>) a ((~>) b (T a b))
data (:*:@#@$) :: (~>) a ((~>) b (T a b))
where
(::*:@#@$###) :: SameKind (Apply (:*:@#@$) arg) ((:*:@#@$$) arg) =>
(:*:@#@$) a0123456789876543210
type instance Apply (:*:@#@$) a0123456789876543210 = (:*:@#@$$) a0123456789876543210
instance SuppressUnusedWarnings (:*:@#@$) where
suppressUnusedWarnings = snd ((,) (::*:@#@$###) ())
infixl 6 :*:@#@$
type (:*:@#@$$) :: forall a b. a -> (~>) b (T a b)
data (:*:@#@$$) (a0123456789876543210 :: a) :: (~>) b (T a b)
where
(::*:@#@$$###) :: SameKind (Apply ((:*:@#@$$) a0123456789876543210) arg) ((:*:@#@$$$) a0123456789876543210 arg) =>
(:*:@#@$$) a0123456789876543210 a0123456789876543210
type instance Apply ((:*:@#@$$) a0123456789876543210) a0123456789876543210 = (:*:) a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings ((:*:@#@$$) a0123456789876543210) where
suppressUnusedWarnings = snd ((,) (::*:@#@$$###) ())
infixl 6 :*:@#@$$
type (:*:@#@$$$) :: forall a b. a -> b -> T a b
type family (:*:@#@$$$) (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: T a b where
(:*:@#@$$$) a0123456789876543210 a0123456789876543210 = (:*:) a0123456789876543210 a0123456789876543210
infixl 6 :*:@#@$$$
type S1Sym0 :: S
type family S1Sym0 :: S where
S1Sym0 = S1
type S2Sym0 :: S
type family S2Sym0 :: S where
S2Sym0 = S2
type TFHelper_0123456789876543210 :: T a () -> T a () -> Bool
type family TFHelper_0123456789876543210 (a :: T a ()) (a :: T a ()) :: Bool where
TFHelper_0123456789876543210 ((:*:) a_0123456789876543210 a_0123456789876543210) ((:*:) b_0123456789876543210 b_0123456789876543210) = Apply (Apply (&&@#@$) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)
type TFHelper_0123456789876543210Sym0 :: (~>) (T a ()) ((~>) (T a ()) Bool)
data TFHelper_0123456789876543210Sym0 :: (~>) (T a ()) ((~>) (T a ()) Bool)
where
TFHelper_0123456789876543210Sym0KindInference :: SameKind (Apply TFHelper_0123456789876543210Sym0 arg) (TFHelper_0123456789876543210Sym1 arg) =>
TFHelper_0123456789876543210Sym0 a0123456789876543210
type instance Apply TFHelper_0123456789876543210Sym0 a0123456789876543210 = TFHelper_0123456789876543210Sym1 a0123456789876543210
instance SuppressUnusedWarnings TFHelper_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd ((,) TFHelper_0123456789876543210Sym0KindInference ())
type TFHelper_0123456789876543210Sym1 :: T a ()
-> (~>) (T a ()) Bool
data TFHelper_0123456789876543210Sym1 (a0123456789876543210 :: T a ()) :: (~>) (T a ()) Bool
where
TFHelper_0123456789876543210Sym1KindInference :: SameKind (Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) arg) (TFHelper_0123456789876543210Sym2 a0123456789876543210 arg) =>
TFHelper_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
type instance Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (TFHelper_0123456789876543210Sym1 a0123456789876543210) where
suppressUnusedWarnings
= snd ((,) TFHelper_0123456789876543210Sym1KindInference ())
type TFHelper_0123456789876543210Sym2 :: T a () -> T a () -> Bool
type family TFHelper_0123456789876543210Sym2 (a0123456789876543210 :: T a ()) (a0123456789876543210 :: T a ()) :: Bool where
TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210
instance PEq (T a ()) where
type (==) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a
type Compare_0123456789876543210 :: T a () -> T a () -> Ordering
type family Compare_0123456789876543210 (a :: T a ()) (a :: T a ()) :: Ordering where
Compare_0123456789876543210 ((:*:) a_0123456789876543210 a_0123456789876543210) ((:*:) b_0123456789876543210 b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0))
type Compare_0123456789876543210Sym0 :: (~>) (T a ()) ((~>) (T a ()) Ordering)
data Compare_0123456789876543210Sym0 :: (~>) (T a ()) ((~>) (T a ()) Ordering)
where
Compare_0123456789876543210Sym0KindInference :: SameKind (Apply Compare_0123456789876543210Sym0 arg) (Compare_0123456789876543210Sym1 arg) =>
Compare_0123456789876543210Sym0 a0123456789876543210
type instance Apply Compare_0123456789876543210Sym0 a0123456789876543210 = Compare_0123456789876543210Sym1 a0123456789876543210
instance SuppressUnusedWarnings Compare_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd ((,) Compare_0123456789876543210Sym0KindInference ())
type Compare_0123456789876543210Sym1 :: T a ()
-> (~>) (T a ()) Ordering
data Compare_0123456789876543210Sym1 (a0123456789876543210 :: T a ()) :: (~>) (T a ()) Ordering
where
Compare_0123456789876543210Sym1KindInference :: SameKind (Apply (Compare_0123456789876543210Sym1 a0123456789876543210) arg) (Compare_0123456789876543210Sym2 a0123456789876543210 arg) =>
Compare_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
type instance Apply (Compare_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (Compare_0123456789876543210Sym1 a0123456789876543210) where
suppressUnusedWarnings
= snd ((,) Compare_0123456789876543210Sym1KindInference ())
type Compare_0123456789876543210Sym2 :: T a ()
-> T a () -> Ordering
type family Compare_0123456789876543210Sym2 (a0123456789876543210 :: T a ()) (a0123456789876543210 :: T a ()) :: Ordering where
Compare_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210
instance POrd (T a ()) where
type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a
type ShowsPrec_0123456789876543210 :: GHC.Num.Natural.Natural
-> T a () -> Symbol -> Symbol
type family ShowsPrec_0123456789876543210 (a :: GHC.Num.Natural.Natural) (a :: T a ()) (a :: Symbol) :: Symbol where
ShowsPrec_0123456789876543210 p_0123456789876543210 ((:*:) argL_0123456789876543210 argR_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 6))) (Apply (Apply (.@#@$) (Apply (Apply ShowsPrecSym0 (FromInteger 7)) argL_0123456789876543210)) (Apply (Apply (.@#@$) (Apply ShowStringSym0 " :*: ")) (Apply (Apply ShowsPrecSym0 (FromInteger 7)) argR_0123456789876543210)))) a_0123456789876543210
type ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) (T a ()) ((~>) Symbol Symbol))
data ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) (T a ()) ((~>) Symbol Symbol))
where
ShowsPrec_0123456789876543210Sym0KindInference :: SameKind (Apply ShowsPrec_0123456789876543210Sym0 arg) (ShowsPrec_0123456789876543210Sym1 arg) =>
ShowsPrec_0123456789876543210Sym0 a0123456789876543210
type instance Apply ShowsPrec_0123456789876543210Sym0 a0123456789876543210 = ShowsPrec_0123456789876543210Sym1 a0123456789876543210
instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd ((,) ShowsPrec_0123456789876543210Sym0KindInference ())
type ShowsPrec_0123456789876543210Sym1 :: GHC.Num.Natural.Natural
-> (~>) (T a ()) ((~>) Symbol Symbol)
data ShowsPrec_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Num.Natural.Natural) :: (~>) (T a ()) ((~>) Symbol Symbol)
where
ShowsPrec_0123456789876543210Sym1KindInference :: 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_0123456789876543210Sym1 a0123456789876543210) where
suppressUnusedWarnings
= snd ((,) ShowsPrec_0123456789876543210Sym1KindInference ())
type ShowsPrec_0123456789876543210Sym2 :: GHC.Num.Natural.Natural
-> T a () -> (~>) Symbol Symbol
data ShowsPrec_0123456789876543210Sym2 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: T a ()) :: (~>) Symbol Symbol
where
ShowsPrec_0123456789876543210Sym2KindInference :: 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_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) where
suppressUnusedWarnings
= snd ((,) ShowsPrec_0123456789876543210Sym2KindInference ())
type ShowsPrec_0123456789876543210Sym3 :: GHC.Num.Natural.Natural
-> T a () -> Symbol -> Symbol
type family ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: T a ()) (a0123456789876543210 :: Symbol) :: Symbol where
ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
instance PShow (T a ()) where
type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
type TFHelper_0123456789876543210 :: S -> S -> Bool
type family TFHelper_0123456789876543210 (a :: S) (a :: S) :: Bool where
TFHelper_0123456789876543210 S1 S1 = TrueSym0
TFHelper_0123456789876543210 S1 S2 = FalseSym0
TFHelper_0123456789876543210 S2 S1 = FalseSym0
TFHelper_0123456789876543210 S2 S2 = TrueSym0
type TFHelper_0123456789876543210Sym0 :: (~>) S ((~>) S Bool)
data TFHelper_0123456789876543210Sym0 :: (~>) S ((~>) S Bool)
where
TFHelper_0123456789876543210Sym0KindInference :: SameKind (Apply TFHelper_0123456789876543210Sym0 arg) (TFHelper_0123456789876543210Sym1 arg) =>
TFHelper_0123456789876543210Sym0 a0123456789876543210
type instance Apply TFHelper_0123456789876543210Sym0 a0123456789876543210 = TFHelper_0123456789876543210Sym1 a0123456789876543210
instance SuppressUnusedWarnings TFHelper_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd ((,) TFHelper_0123456789876543210Sym0KindInference ())
type TFHelper_0123456789876543210Sym1 :: S -> (~>) S Bool
data TFHelper_0123456789876543210Sym1 (a0123456789876543210 :: S) :: (~>) S Bool
where
TFHelper_0123456789876543210Sym1KindInference :: SameKind (Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) arg) (TFHelper_0123456789876543210Sym2 a0123456789876543210 arg) =>
TFHelper_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
type instance Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (TFHelper_0123456789876543210Sym1 a0123456789876543210) where
suppressUnusedWarnings
= snd ((,) TFHelper_0123456789876543210Sym1KindInference ())
type TFHelper_0123456789876543210Sym2 :: S -> S -> Bool
type family TFHelper_0123456789876543210Sym2 (a0123456789876543210 :: S) (a0123456789876543210 :: S) :: Bool where
TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210
instance PEq S where
type (==) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a
type Compare_0123456789876543210 :: S -> S -> Ordering
type family Compare_0123456789876543210 (a :: S) (a :: S) :: Ordering where
Compare_0123456789876543210 S1 S1 = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) NilSym0
Compare_0123456789876543210 S2 S2 = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) NilSym0
Compare_0123456789876543210 S1 S2 = LTSym0
Compare_0123456789876543210 S2 S1 = GTSym0
type Compare_0123456789876543210Sym0 :: (~>) S ((~>) S Ordering)
data Compare_0123456789876543210Sym0 :: (~>) S ((~>) S Ordering)
where
Compare_0123456789876543210Sym0KindInference :: SameKind (Apply Compare_0123456789876543210Sym0 arg) (Compare_0123456789876543210Sym1 arg) =>
Compare_0123456789876543210Sym0 a0123456789876543210
type instance Apply Compare_0123456789876543210Sym0 a0123456789876543210 = Compare_0123456789876543210Sym1 a0123456789876543210
instance SuppressUnusedWarnings Compare_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd ((,) Compare_0123456789876543210Sym0KindInference ())
type Compare_0123456789876543210Sym1 :: S -> (~>) S Ordering
data Compare_0123456789876543210Sym1 (a0123456789876543210 :: S) :: (~>) S Ordering
where
Compare_0123456789876543210Sym1KindInference :: SameKind (Apply (Compare_0123456789876543210Sym1 a0123456789876543210) arg) (Compare_0123456789876543210Sym2 a0123456789876543210 arg) =>
Compare_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
type instance Apply (Compare_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (Compare_0123456789876543210Sym1 a0123456789876543210) where
suppressUnusedWarnings
= snd ((,) Compare_0123456789876543210Sym1KindInference ())
type Compare_0123456789876543210Sym2 :: S -> S -> Ordering
type family Compare_0123456789876543210Sym2 (a0123456789876543210 :: S) (a0123456789876543210 :: S) :: Ordering where
Compare_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210
instance POrd S where
type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a
type ShowsPrec_0123456789876543210 :: GHC.Num.Natural.Natural
-> S -> Symbol -> Symbol
type family ShowsPrec_0123456789876543210 (a :: GHC.Num.Natural.Natural) (a :: S) (a :: Symbol) :: Symbol where
ShowsPrec_0123456789876543210 _ S1 a_0123456789876543210 = Apply (Apply ShowStringSym0 "S1") a_0123456789876543210
ShowsPrec_0123456789876543210 _ S2 a_0123456789876543210 = Apply (Apply ShowStringSym0 "S2") a_0123456789876543210
type ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) S ((~>) Symbol Symbol))
data ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) S ((~>) Symbol Symbol))
where
ShowsPrec_0123456789876543210Sym0KindInference :: SameKind (Apply ShowsPrec_0123456789876543210Sym0 arg) (ShowsPrec_0123456789876543210Sym1 arg) =>
ShowsPrec_0123456789876543210Sym0 a0123456789876543210
type instance Apply ShowsPrec_0123456789876543210Sym0 a0123456789876543210 = ShowsPrec_0123456789876543210Sym1 a0123456789876543210
instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd ((,) ShowsPrec_0123456789876543210Sym0KindInference ())
type ShowsPrec_0123456789876543210Sym1 :: GHC.Num.Natural.Natural
-> (~>) S ((~>) Symbol Symbol)
data ShowsPrec_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Num.Natural.Natural) :: (~>) S ((~>) Symbol Symbol)
where
ShowsPrec_0123456789876543210Sym1KindInference :: 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_0123456789876543210Sym1 a0123456789876543210) where
suppressUnusedWarnings
= snd ((,) ShowsPrec_0123456789876543210Sym1KindInference ())
type ShowsPrec_0123456789876543210Sym2 :: GHC.Num.Natural.Natural
-> S -> (~>) Symbol Symbol
data ShowsPrec_0123456789876543210Sym2 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: S) :: (~>) Symbol Symbol
where
ShowsPrec_0123456789876543210Sym2KindInference :: 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_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) where
suppressUnusedWarnings
= snd ((,) ShowsPrec_0123456789876543210Sym2KindInference ())
type ShowsPrec_0123456789876543210Sym3 :: GHC.Num.Natural.Natural
-> S -> Symbol -> Symbol
type family ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: S) (a0123456789876543210 :: Symbol) :: Symbol where
ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
instance PShow S where
type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
type MinBound_0123456789876543210 :: S
type family MinBound_0123456789876543210 :: S where
MinBound_0123456789876543210 = S1Sym0
type MinBound_0123456789876543210Sym0 :: S
type family MinBound_0123456789876543210Sym0 :: S where
MinBound_0123456789876543210Sym0 = MinBound_0123456789876543210
type MaxBound_0123456789876543210 :: S
type family MaxBound_0123456789876543210 :: S where
MaxBound_0123456789876543210 = S2Sym0
type MaxBound_0123456789876543210Sym0 :: S
type family MaxBound_0123456789876543210Sym0 :: S where
MaxBound_0123456789876543210Sym0 = MaxBound_0123456789876543210
instance PBounded S where
type MinBound = MinBound_0123456789876543210Sym0
type MaxBound = MaxBound_0123456789876543210Sym0
type family Case_0123456789876543210 n t where
Case_0123456789876543210 n 'True = S2Sym0
Case_0123456789876543210 n 'False = Apply ErrorSym0 "toEnum: bad argument"
type family Case_0123456789876543210 n t where
Case_0123456789876543210 n 'True = S1Sym0
Case_0123456789876543210 n 'False = Case_0123456789876543210 n (Apply (Apply (==@#@$) n) (FromInteger 1))
type ToEnum_0123456789876543210 :: GHC.Num.Natural.Natural -> S
type family ToEnum_0123456789876543210 (a :: GHC.Num.Natural.Natural) :: S where
ToEnum_0123456789876543210 n = Case_0123456789876543210 n (Apply (Apply (==@#@$) n) (FromInteger 0))
type ToEnum_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural S
data ToEnum_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural S
where
ToEnum_0123456789876543210Sym0KindInference :: SameKind (Apply ToEnum_0123456789876543210Sym0 arg) (ToEnum_0123456789876543210Sym1 arg) =>
ToEnum_0123456789876543210Sym0 a0123456789876543210
type instance Apply ToEnum_0123456789876543210Sym0 a0123456789876543210 = ToEnum_0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings ToEnum_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd ((,) ToEnum_0123456789876543210Sym0KindInference ())
type ToEnum_0123456789876543210Sym1 :: GHC.Num.Natural.Natural -> S
type family ToEnum_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Num.Natural.Natural) :: S where
ToEnum_0123456789876543210Sym1 a0123456789876543210 = ToEnum_0123456789876543210 a0123456789876543210
type FromEnum_0123456789876543210 :: S -> GHC.Num.Natural.Natural
type family FromEnum_0123456789876543210 (a :: S) :: GHC.Num.Natural.Natural where
FromEnum_0123456789876543210 S1 = FromInteger 0
FromEnum_0123456789876543210 S2 = FromInteger 1
type FromEnum_0123456789876543210Sym0 :: (~>) S GHC.Num.Natural.Natural
data FromEnum_0123456789876543210Sym0 :: (~>) S GHC.Num.Natural.Natural
where
FromEnum_0123456789876543210Sym0KindInference :: SameKind (Apply FromEnum_0123456789876543210Sym0 arg) (FromEnum_0123456789876543210Sym1 arg) =>
FromEnum_0123456789876543210Sym0 a0123456789876543210
type instance Apply FromEnum_0123456789876543210Sym0 a0123456789876543210 = FromEnum_0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings FromEnum_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd ((,) FromEnum_0123456789876543210Sym0KindInference ())
type FromEnum_0123456789876543210Sym1 :: S
-> GHC.Num.Natural.Natural
type family FromEnum_0123456789876543210Sym1 (a0123456789876543210 :: S) :: GHC.Num.Natural.Natural where
FromEnum_0123456789876543210Sym1 a0123456789876543210 = FromEnum_0123456789876543210 a0123456789876543210
instance PEnum S where
type ToEnum a = Apply ToEnum_0123456789876543210Sym0 a
type FromEnum a = Apply FromEnum_0123456789876543210Sym0 a
infixl 6 :%*:
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)
type instance Sing @(T a b) = ST
instance (SingKind a, SingKind b) => SingKind (T a b) where
type Demote (T a b) = T (Demote a) (Demote b)
fromSing ((:%*:) b b) = (:*:) (fromSing b) (fromSing b)
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 -> Type
where
SS1 :: SS (S1 :: S)
SS2 :: SS (S2 :: S)
type instance Sing @S = SS
instance SingKind S where
type Demote S = S
fromSing SS1 = S1
fromSing SS2 = S2
toSing S1 = SomeSing SS1
toSing S2 = SomeSing SS2
instance SEq a => SEq (T a ()) where
(%==) ::
forall (t1 :: T a ()) (t2 :: T a ()). Sing t1
-> Sing t2
-> Sing (Apply (Apply ((==@#@$) :: TyFun (T a ()) ((~>) (T a ()) Bool)
-> Type) t1) t2)
(%==)
((:%*:) (sA_0123456789876543210 :: Sing a_0123456789876543210)
(sA_0123456789876543210 :: Sing a_0123456789876543210))
((:%*:) (sB_0123456789876543210 :: Sing b_0123456789876543210)
(sB_0123456789876543210 :: Sing b_0123456789876543210))
= applySing
(applySing
(singFun2 @(&&@#@$) (%&&))
(applySing
(applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210)
sB_0123456789876543210))
(applySing
(applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210)
sB_0123456789876543210)
instance SOrd a => SOrd (T a ()) where
sCompare ::
forall (t1 :: T a ()) (t2 :: T a ()). Sing t1
-> Sing t2
-> Sing (Apply (Apply (CompareSym0 :: TyFun (T a ()) ((~>) (T a ()) Ordering)
-> Type) t1) t2)
sCompare
((:%*:) (sA_0123456789876543210 :: Sing a_0123456789876543210)
(sA_0123456789876543210 :: Sing a_0123456789876543210))
((:%*:) (sB_0123456789876543210 :: Sing b_0123456789876543210)
(sB_0123456789876543210 :: Sing b_0123456789876543210))
= applySing
(applySing
(applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>)))
SEQ)
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
(applySing
(applySing
(singFun2 @(:@#@$) SCons)
(applySing
(applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
sB_0123456789876543210))
SNil))
instance SShow a => SShow (T a ()) where
sShowsPrec ::
forall (t1 :: GHC.Num.Natural.Natural)
(t2 :: T a ())
(t3 :: Symbol). Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) (T a ()) ((~>) Symbol Symbol))
-> Type) t1) t2) t3)
sShowsPrec
(sP_0123456789876543210 :: Sing p_0123456789876543210)
((:%*:) (sArgL_0123456789876543210 :: Sing argL_0123456789876543210)
(sArgR_0123456789876543210 :: Sing argR_0123456789876543210))
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(applySing
(singFun3 @ShowParenSym0 sShowParen)
(applySing
(applySing (singFun2 @(>@#@$) (%>)) sP_0123456789876543210)
(sFromInteger (sing :: Sing 6))))
(applySing
(applySing
(singFun3 @(.@#@$) (%.))
(applySing
(applySing
(singFun3 @ShowsPrecSym0 sShowsPrec)
(sFromInteger (sing :: Sing 7)))
sArgL_0123456789876543210))
(applySing
(applySing
(singFun3 @(.@#@$) (%.))
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing " :*: ")))
(applySing
(applySing
(singFun3 @ShowsPrecSym0 sShowsPrec)
(sFromInteger (sing :: Sing 7)))
sArgR_0123456789876543210))))
sA_0123456789876543210
instance SEq S where
(%==) ::
forall (t1 :: S) (t2 :: S). Sing t1
-> Sing t2
-> Sing (Apply (Apply ((==@#@$) :: TyFun S ((~>) S Bool)
-> Type) t1) t2)
(%==) SS1 SS1 = STrue
(%==) SS1 SS2 = SFalse
(%==) SS2 SS1 = SFalse
(%==) SS2 SS2 = STrue
instance SOrd S where
sCompare ::
forall (t1 :: S) (t2 :: S). Sing t1
-> Sing t2
-> Sing (Apply (Apply (CompareSym0 :: TyFun S ((~>) S Ordering)
-> Type) t1) t2)
sCompare SS1 SS1
= applySing
(applySing
(applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>)))
SEQ)
SNil
sCompare SS2 SS2
= applySing
(applySing
(applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>)))
SEQ)
SNil
sCompare SS1 SS2 = SLT
sCompare SS2 SS1 = SGT
instance SShow S where
sShowsPrec ::
forall (t1 :: GHC.Num.Natural.Natural)
(t2 :: S)
(t3 :: Symbol). Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) S ((~>) Symbol Symbol))
-> Type) t1) t2) t3)
sShowsPrec
_
SS1
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "S1"))
sA_0123456789876543210
sShowsPrec
_
SS2
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "S2"))
sA_0123456789876543210
instance SBounded S where
sMinBound :: Sing (MinBoundSym0 :: S)
sMaxBound :: Sing (MaxBoundSym0 :: S)
sMinBound = SS1
sMaxBound = SS2
instance SEnum S where
sToEnum ::
forall (t :: GHC.Num.Natural.Natural). Sing t
-> Sing (Apply (ToEnumSym0 :: TyFun GHC.Num.Natural.Natural S
-> Type) t)
sFromEnum ::
forall (t :: S). Sing t
-> Sing (Apply (FromEnumSym0 :: TyFun S GHC.Num.Natural.Natural
-> Type) t)
sToEnum (sN :: Sing n)
= id
@(Sing (Case_0123456789876543210 n (Apply (Apply (==@#@$) n) (FromInteger 0))))
(case
applySing
(applySing (singFun2 @(==@#@$) (%==)) sN)
(sFromInteger (sing :: Sing 0))
of
STrue -> SS1
SFalse
-> id
@(Sing (Case_0123456789876543210 n (Apply (Apply (==@#@$) n) (FromInteger 1))))
(case
applySing
(applySing (singFun2 @(==@#@$) (%==)) sN)
(sFromInteger (sing :: Sing 1))
of
STrue -> SS2
SFalse -> sError (sing :: Sing "toEnum: bad argument")))
sFromEnum SS1 = sFromInteger (sing :: Sing 0)
sFromEnum SS2 = sFromInteger (sing :: Sing 1)
instance SDecide a => SDecide (T a ()) where
(%~) ((:%*:) a a) ((:%*:) b b)
= case (,) ((%~) a b) ((%~) a b) of
(,) (Proved Refl) (Proved Refl) -> Proved Refl
(,) (Disproved contra) _
-> Disproved (\ refl -> case refl of Refl -> contra Refl)
(,) _ (Disproved contra)
-> Disproved (\ refl -> case refl of Refl -> contra Refl)
instance SDecide a =>
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 () -> Type) where
Data.Type.Coercion.testCoercion
= Data.Singletons.Decide.decideCoercion
instance SDecide S where
(%~) SS1 SS1 = Proved Refl
(%~) 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 -> Type) where
Data.Type.Equality.testEquality
= Data.Singletons.Decide.decideEquality
instance Data.Type.Coercion.TestCoercion (SS :: S -> Type) where
Data.Type.Coercion.testCoercion
= Data.Singletons.Decide.decideCoercion
deriving instance Data.Singletons.ShowSing.ShowSing a =>
Show (ST (z :: T a ()))
deriving instance Show (SS (z :: S))
instance (SingI n, SingI n) =>
SingI ((:*:) (n :: a) (n :: b)) where
sing = (:%*:) sing sing
instance SingI n => SingI1 ((:*:) (n :: a)) where
liftSing = (:%*:) sing
instance SingI2 (:*:) where
liftSing2 = (:%*:)
instance SingI ((:*:@#@$) :: (~>) a ((~>) b (T a b))) where
sing = singFun2 @(:*:@#@$) (:%*:)
instance SingI d =>
SingI ((:*:@#@$$) (d :: a) :: (~>) b (T a b)) where
sing = singFun1 @((:*:@#@$$) (d :: a)) ((:%*:) (sing @d))
instance SingI1 ((:*:@#@$$) :: a -> (~>) b (T a b)) where
liftSing (s :: Sing (d :: a))
= singFun1 @((:*:@#@$$) (d :: a)) ((:%*:) s)
instance SingI S1 where
sing = SS1
instance SingI S2 where
sing = SS2