singletons-2.5: tests/compile-and-dump/Singletons/T178.ghc86.template
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 USym0 = U
type StrSym0 = Str
type OptSym0 = Opt
type ManySym0 = Many
type EmptySym0 = Empty
type family Empty :: [(Symbol, Occ)] where
Empty = '[]
type family Compare_0123456789876543210 (a :: Occ) (a :: Occ) :: Ordering where
Compare_0123456789876543210 Str Str = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) '[]
Compare_0123456789876543210 Opt Opt = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) '[]
Compare_0123456789876543210 Many Many = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) '[]
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_0123456789876543210Sym2 (a0123456789876543210 :: Occ) (a0123456789876543210 :: Occ) =
Compare_0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (Compare_0123456789876543210Sym1 a0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Compare_0123456789876543210Sym1KindInference) ())
data Compare_0123456789876543210Sym1 (a0123456789876543210 :: Occ) :: (~>) Occ Ordering
where
Compare_0123456789876543210Sym1KindInference :: forall a0123456789876543210
a0123456789876543210
arg. 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_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd (((,) Compare_0123456789876543210Sym0KindInference) ())
data Compare_0123456789876543210Sym0 :: (~>) Occ ((~>) Occ Ordering)
where
Compare_0123456789876543210Sym0KindInference :: forall a0123456789876543210
arg. SameKind (Apply Compare_0123456789876543210Sym0 arg) (Compare_0123456789876543210Sym1 arg) =>
Compare_0123456789876543210Sym0 a0123456789876543210
type instance Apply Compare_0123456789876543210Sym0 a0123456789876543210 = Compare_0123456789876543210Sym1 a0123456789876543210
instance POrd Occ where
type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a
type family ShowsPrec_0123456789876543210 (a :: Nat) (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_0123456789876543210Sym3 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Occ) (a0123456789876543210 :: Symbol) =
ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) where
suppressUnusedWarnings
= snd (((,) ShowsPrec_0123456789876543210Sym2KindInference) ())
data ShowsPrec_0123456789876543210Sym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Occ) :: (~>) Symbol 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 :: Nat) :: (~>) Occ ((~>) Symbol 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 :: (~>) Nat ((~>) Occ ((~>) Symbol 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 Occ where
type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
type family Equals_0123456789876543210 (a :: Occ) (b :: Occ) :: Bool where
Equals_0123456789876543210 Str Str = TrueSym0
Equals_0123456789876543210 Opt Opt = TrueSym0
Equals_0123456789876543210 Many Many = TrueSym0
Equals_0123456789876543210 (_ :: Occ) (_ :: Occ) = FalseSym0
instance PEq Occ where
type (==) a b = Equals_0123456789876543210 a b
sEmpty :: Sing (EmptySym0 :: [(Symbol, Occ)])
sEmpty = Data.Singletons.Prelude.Instances.SNil
data instance Sing :: Occ -> GHC.Types.Type
where
SStr :: Sing Str
SOpt :: Sing Opt
SMany :: Sing Many
type SOcc = (Sing :: Occ -> GHC.Types.Type)
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 SOrd Occ where
sCompare ::
forall (t1 :: Occ) (t2 :: Occ).
Sing t1
-> Sing t2
-> Sing (Apply (Apply (CompareSym0 :: TyFun Occ ((~>) Occ Ordering)
-> GHC.Types.Type) t1) t2)
sCompare SStr SStr
= (applySing
((applySing
((applySing ((singFun3 @FoldlSym0) sFoldl))
((singFun2 @ThenCmpSym0) sThenCmp)))
SEQ))
Data.Singletons.Prelude.Instances.SNil
sCompare SOpt SOpt
= (applySing
((applySing
((applySing ((singFun3 @FoldlSym0) sFoldl))
((singFun2 @ThenCmpSym0) sThenCmp)))
SEQ))
Data.Singletons.Prelude.Instances.SNil
sCompare SMany SMany
= (applySing
((applySing
((applySing ((singFun3 @FoldlSym0) sFoldl))
((singFun2 @ThenCmpSym0) sThenCmp)))
SEQ))
Data.Singletons.Prelude.Instances.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 :: Nat) (t2 :: Occ) (t3 :: Symbol).
Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun Nat ((~>) Occ ((~>) Symbol Symbol))
-> GHC.Types.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 SEq Occ where
(%==) 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 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
deriving instance Show (Sing (z :: Occ))
instance SingI Str where
sing = SStr
instance SingI Opt where
sing = SOpt
instance SingI Many where
sing = SMany