singletons-base-3.3: tests/compile-and-dump/Singletons/T178.golden
Singletons/T178.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| empty :: U
empty = []
data Occ
= Str | Opt | Many
deriving (Eq, Ord, Show)
type U = [(Symbol, Occ)] |]
======>
data Occ
= Str | Opt | Many
deriving (Eq, Ord, Show)
type U = [(Symbol, Occ)]
empty :: U
empty = []
type family USym0 where
USym0 = U
type StrSym0 :: Occ
type family StrSym0 :: Occ where
StrSym0 = Str
type OptSym0 :: Occ
type family OptSym0 :: Occ where
OptSym0 = Opt
type ManySym0 :: Occ
type family ManySym0 :: Occ where
ManySym0 = Many
type EmptySym0 :: [(Symbol, Occ)]
type family EmptySym0 :: [(Symbol, Occ)] where
EmptySym0 = Empty
type Empty :: [(Symbol, Occ)]
type family Empty :: [(Symbol, Occ)] where
Empty = NilSym0
type TFHelper_0123456789876543210 :: Occ -> Occ -> Bool
type family TFHelper_0123456789876543210 (a :: Occ) (a :: Occ) :: Bool where
TFHelper_0123456789876543210 Str Str = TrueSym0
TFHelper_0123456789876543210 Str Opt = FalseSym0
TFHelper_0123456789876543210 Str Many = FalseSym0
TFHelper_0123456789876543210 Opt Str = FalseSym0
TFHelper_0123456789876543210 Opt Opt = TrueSym0
TFHelper_0123456789876543210 Opt Many = FalseSym0
TFHelper_0123456789876543210 Many Str = FalseSym0
TFHelper_0123456789876543210 Many Opt = FalseSym0
TFHelper_0123456789876543210 Many Many = TrueSym0
type TFHelper_0123456789876543210Sym0 :: (~>) Occ ((~>) Occ Bool)
data TFHelper_0123456789876543210Sym0 :: (~>) Occ ((~>) Occ 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 :: Occ -> (~>) Occ Bool
data TFHelper_0123456789876543210Sym1 (a0123456789876543210 :: Occ) :: (~>) Occ 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 :: Occ -> Occ -> Bool
type family TFHelper_0123456789876543210Sym2 (a0123456789876543210 :: Occ) (a0123456789876543210 :: Occ) :: Bool where
TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210
instance PEq Occ where
type (==) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a
type Compare_0123456789876543210 :: Occ -> Occ -> Ordering
type family Compare_0123456789876543210 (a :: Occ) (a :: Occ) :: Ordering where
Compare_0123456789876543210 Str Str = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) NilSym0
Compare_0123456789876543210 Opt Opt = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) NilSym0
Compare_0123456789876543210 Many Many = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) NilSym0
Compare_0123456789876543210 Str Opt = LTSym0
Compare_0123456789876543210 Str Many = LTSym0
Compare_0123456789876543210 Opt Str = GTSym0
Compare_0123456789876543210 Opt Many = LTSym0
Compare_0123456789876543210 Many Str = GTSym0
Compare_0123456789876543210 Many Opt = GTSym0
type Compare_0123456789876543210Sym0 :: (~>) Occ ((~>) Occ Ordering)
data Compare_0123456789876543210Sym0 :: (~>) Occ ((~>) Occ 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 :: Occ -> (~>) Occ Ordering
data Compare_0123456789876543210Sym1 (a0123456789876543210 :: Occ) :: (~>) Occ 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 :: Occ -> Occ -> Ordering
type family Compare_0123456789876543210Sym2 (a0123456789876543210 :: Occ) (a0123456789876543210 :: Occ) :: Ordering where
Compare_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210
instance POrd Occ where
type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a
type ShowsPrec_0123456789876543210 :: Natural
-> Occ -> Symbol -> Symbol
type family ShowsPrec_0123456789876543210 (a :: Natural) (a :: Occ) (a :: Symbol) :: Symbol where
ShowsPrec_0123456789876543210 _ Str a_0123456789876543210 = Apply (Apply ShowStringSym0 "Str") a_0123456789876543210
ShowsPrec_0123456789876543210 _ Opt a_0123456789876543210 = Apply (Apply ShowStringSym0 "Opt") a_0123456789876543210
ShowsPrec_0123456789876543210 _ Many a_0123456789876543210 = Apply (Apply ShowStringSym0 "Many") a_0123456789876543210
type ShowsPrec_0123456789876543210Sym0 :: (~>) Natural ((~>) Occ ((~>) Symbol Symbol))
data ShowsPrec_0123456789876543210Sym0 :: (~>) Natural ((~>) Occ ((~>) 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 :: Natural
-> (~>) Occ ((~>) Symbol Symbol)
data ShowsPrec_0123456789876543210Sym1 (a0123456789876543210 :: Natural) :: (~>) Occ ((~>) 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 :: Natural
-> Occ -> (~>) Symbol Symbol
data ShowsPrec_0123456789876543210Sym2 (a0123456789876543210 :: Natural) (a0123456789876543210 :: Occ) :: (~>) 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 :: Natural
-> Occ -> Symbol -> Symbol
type family ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: Natural) (a0123456789876543210 :: Occ) (a0123456789876543210 :: Symbol) :: Symbol where
ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
instance PShow Occ where
type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
sEmpty :: (Sing (EmptySym0 :: [(Symbol, Occ)]) :: Type)
sEmpty = SNil
data SOcc :: Occ -> Type
where
SStr :: SOcc (Str :: Occ)
SOpt :: SOcc (Opt :: Occ)
SMany :: SOcc (Many :: Occ)
type instance Sing @Occ = SOcc
instance SingKind Occ where
type Demote Occ = Occ
fromSing SStr = Str
fromSing SOpt = Opt
fromSing SMany = Many
toSing Str = SomeSing SStr
toSing Opt = SomeSing SOpt
toSing Many = SomeSing SMany
instance SEq Occ where
(%==) ::
forall (t1 :: Occ) (t2 :: Occ). Sing t1
-> Sing t2
-> Sing (Apply (Apply ((==@#@$) :: TyFun Occ ((~>) Occ Bool)
-> Type) t1) t2)
(%==) SStr SStr = STrue
(%==) SStr SOpt = SFalse
(%==) SStr SMany = SFalse
(%==) SOpt SStr = SFalse
(%==) SOpt SOpt = STrue
(%==) SOpt SMany = SFalse
(%==) SMany SStr = SFalse
(%==) SMany SOpt = SFalse
(%==) SMany SMany = STrue
instance SOrd Occ where
sCompare ::
forall (t1 :: Occ) (t2 :: Occ). Sing t1
-> Sing t2
-> Sing (Apply (Apply (CompareSym0 :: TyFun Occ ((~>) Occ Ordering)
-> Type) t1) t2)
sCompare SStr SStr
= applySing
(applySing
(applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>)))
SEQ)
SNil
sCompare SOpt SOpt
= applySing
(applySing
(applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>)))
SEQ)
SNil
sCompare SMany SMany
= applySing
(applySing
(applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>)))
SEQ)
SNil
sCompare SStr SOpt = SLT
sCompare SStr SMany = SLT
sCompare SOpt SStr = SGT
sCompare SOpt SMany = SLT
sCompare SMany SStr = SGT
sCompare SMany SOpt = SGT
instance SShow Occ where
sShowsPrec ::
forall (t1 :: Natural) (t2 :: Occ) (t3 :: Symbol). Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun Natural ((~>) Occ ((~>) Symbol Symbol))
-> Type) t1) t2) t3)
sShowsPrec
_
SStr
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "Str"))
sA_0123456789876543210
sShowsPrec
_
SOpt
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "Opt"))
sA_0123456789876543210
sShowsPrec
_
SMany
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "Many"))
sA_0123456789876543210
instance SDecide Occ where
(%~) SStr SStr = Proved Refl
(%~) SStr SOpt = Disproved (\ x -> case x of {})
(%~) SStr SMany = Disproved (\ x -> case x of {})
(%~) SOpt SStr = Disproved (\ x -> case x of {})
(%~) SOpt SOpt = Proved Refl
(%~) SOpt SMany = Disproved (\ x -> case x of {})
(%~) SMany SStr = Disproved (\ x -> case x of {})
(%~) SMany SOpt = Disproved (\ x -> case x of {})
(%~) SMany SMany = Proved Refl
instance Eq (SOcc (z :: Occ)) where
(==) _ _ = True
instance Data.Type.Equality.TestEquality (SOcc :: Occ
-> Type) where
Data.Type.Equality.testEquality
= Data.Singletons.Decide.decideEquality
instance Data.Type.Coercion.TestCoercion (SOcc :: Occ
-> Type) where
Data.Type.Coercion.testCoercion
= Data.Singletons.Decide.decideCoercion
instance Ord (SOcc (z :: Occ)) where
compare _ _ = EQ
deriving instance Show (SOcc (z :: Occ))
instance SingI Str where
sing = SStr
instance SingI Opt where
sing = SOpt
instance SingI Many where
sing = SMany