singletons-base-3.2: tests/compile-and-dump/Singletons/T555.golden
Singletons/T555.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| data MyPropKind
= Location | Quaternion
deriving (Eq, Ord, Show) |]
======>
data MyPropKind
= Location | Quaternion
deriving (Eq, Ord, Show)
type LocationSym0 :: MyPropKind
type family LocationSym0 :: MyPropKind where
LocationSym0 = Location
type QuaternionSym0 :: MyPropKind
type family QuaternionSym0 :: MyPropKind where
QuaternionSym0 = Quaternion
type TFHelper_0123456789876543210 :: MyPropKind
-> MyPropKind -> Bool
type family TFHelper_0123456789876543210 (a :: MyPropKind) (a :: MyPropKind) :: Bool where
TFHelper_0123456789876543210 Location Location = TrueSym0
TFHelper_0123456789876543210 Location Quaternion = FalseSym0
TFHelper_0123456789876543210 Quaternion Location = FalseSym0
TFHelper_0123456789876543210 Quaternion Quaternion = TrueSym0
type TFHelper_0123456789876543210Sym0 :: (~>) MyPropKind ((~>) MyPropKind Bool)
data TFHelper_0123456789876543210Sym0 :: (~>) MyPropKind ((~>) MyPropKind 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 :: MyPropKind
-> (~>) MyPropKind Bool
data TFHelper_0123456789876543210Sym1 (a0123456789876543210 :: MyPropKind) :: (~>) MyPropKind 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 :: MyPropKind
-> MyPropKind -> Bool
type family TFHelper_0123456789876543210Sym2 (a0123456789876543210 :: MyPropKind) (a0123456789876543210 :: MyPropKind) :: Bool where
TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210
instance PEq MyPropKind where
type (==) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a
type Compare_0123456789876543210 :: MyPropKind
-> MyPropKind -> Ordering
type family Compare_0123456789876543210 (a :: MyPropKind) (a :: MyPropKind) :: Ordering where
Compare_0123456789876543210 Location Location = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) NilSym0
Compare_0123456789876543210 Quaternion Quaternion = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) NilSym0
Compare_0123456789876543210 Location Quaternion = LTSym0
Compare_0123456789876543210 Quaternion Location = GTSym0
type Compare_0123456789876543210Sym0 :: (~>) MyPropKind ((~>) MyPropKind Ordering)
data Compare_0123456789876543210Sym0 :: (~>) MyPropKind ((~>) MyPropKind 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 :: MyPropKind
-> (~>) MyPropKind Ordering
data Compare_0123456789876543210Sym1 (a0123456789876543210 :: MyPropKind) :: (~>) MyPropKind 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 :: MyPropKind
-> MyPropKind -> Ordering
type family Compare_0123456789876543210Sym2 (a0123456789876543210 :: MyPropKind) (a0123456789876543210 :: MyPropKind) :: Ordering where
Compare_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210
instance POrd MyPropKind where
type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a
type ShowsPrec_0123456789876543210 :: GHC.Num.Natural.Natural
-> MyPropKind -> Symbol -> Symbol
type family ShowsPrec_0123456789876543210 (a :: GHC.Num.Natural.Natural) (a :: MyPropKind) (a :: Symbol) :: Symbol where
ShowsPrec_0123456789876543210 _ Location a_0123456789876543210 = Apply (Apply ShowStringSym0 "Location") a_0123456789876543210
ShowsPrec_0123456789876543210 _ Quaternion a_0123456789876543210 = Apply (Apply ShowStringSym0 "Quaternion") a_0123456789876543210
type ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) MyPropKind ((~>) Symbol Symbol))
data ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) MyPropKind ((~>) 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
-> (~>) MyPropKind ((~>) Symbol Symbol)
data ShowsPrec_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Num.Natural.Natural) :: (~>) MyPropKind ((~>) 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
-> MyPropKind -> (~>) Symbol Symbol
data ShowsPrec_0123456789876543210Sym2 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: MyPropKind) :: (~>) 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
-> MyPropKind -> Symbol -> Symbol
type family ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: MyPropKind) (a0123456789876543210 :: Symbol) :: Symbol where
ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
instance PShow MyPropKind where
type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
data SMyPropKind :: MyPropKind -> Type
where
SLocation :: SMyPropKind (Location :: MyPropKind)
SQuaternion :: SMyPropKind (Quaternion :: MyPropKind)
type instance Sing @MyPropKind = SMyPropKind
instance SingKind MyPropKind where
type Demote MyPropKind = MyPropKind
fromSing SLocation = Location
fromSing SQuaternion = Quaternion
toSing Location = SomeSing SLocation
toSing Quaternion = SomeSing SQuaternion
instance SEq MyPropKind where
(%==) ::
forall (t1 :: MyPropKind) (t2 :: MyPropKind). Sing t1
-> Sing t2
-> Sing (Apply (Apply ((==@#@$) :: TyFun MyPropKind ((~>) MyPropKind Bool)
-> Type) t1) t2)
(%==) SLocation SLocation = STrue
(%==) SLocation SQuaternion = SFalse
(%==) SQuaternion SLocation = SFalse
(%==) SQuaternion SQuaternion = STrue
instance SOrd MyPropKind where
sCompare ::
forall (t1 :: MyPropKind) (t2 :: MyPropKind). Sing t1
-> Sing t2
-> Sing (Apply (Apply (CompareSym0 :: TyFun MyPropKind ((~>) MyPropKind Ordering)
-> Type) t1) t2)
sCompare SLocation SLocation
= applySing
(applySing
(applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>)))
SEQ)
SNil
sCompare SQuaternion SQuaternion
= applySing
(applySing
(applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>)))
SEQ)
SNil
sCompare SLocation SQuaternion = SLT
sCompare SQuaternion SLocation = SGT
instance SShow MyPropKind where
sShowsPrec ::
forall (t1 :: GHC.Num.Natural.Natural)
(t2 :: MyPropKind)
(t3 :: Symbol). Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) MyPropKind ((~>) Symbol Symbol))
-> Type) t1) t2) t3)
sShowsPrec
_
SLocation
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "Location"))
sA_0123456789876543210
sShowsPrec
_
SQuaternion
(sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "Quaternion"))
sA_0123456789876543210
instance SDecide MyPropKind where
(%~) SLocation SLocation = Proved Refl
(%~) SLocation SQuaternion = Disproved (\ x -> case x of {})
(%~) SQuaternion SLocation = Disproved (\ x -> case x of {})
(%~) SQuaternion SQuaternion = Proved Refl
instance Data.Type.Equality.TestEquality (SMyPropKind :: MyPropKind
-> Type) where
Data.Type.Equality.testEquality
= Data.Singletons.Decide.decideEquality
instance Data.Type.Coercion.TestCoercion (SMyPropKind :: MyPropKind
-> Type) where
Data.Type.Coercion.testCoercion
= Data.Singletons.Decide.decideCoercion
deriving instance Show (SMyPropKind (z :: MyPropKind))
instance SingI Location where
sing = SLocation
instance SingI Quaternion where
sing = SQuaternion