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 (:*:@#@$$$) (t0123456789876543210 :: a0123456789876543210) (t0123456789876543210 :: b0123456789876543210) = (:*:) t0123456789876543210 t0123456789876543210 instance SuppressUnusedWarnings ((:*:@#@$$) t0123456789876543210) where suppressUnusedWarnings = snd (((,) (::*:@#@$$###)) ()) data (:*:@#@$$) (t0123456789876543210 :: a0123456789876543210) :: forall b0123456789876543210. (~>) b0123456789876543210 (T a0123456789876543210 b0123456789876543210) where (::*:@#@$$###) :: forall t0123456789876543210 t0123456789876543210 arg. SameKind (Apply ((:*:@#@$$) t0123456789876543210) arg) ((:*:@#@$$$) t0123456789876543210 arg) => (:*:@#@$$) t0123456789876543210 t0123456789876543210 type instance Apply ((:*:@#@$$) t0123456789876543210) t0123456789876543210 = (:*:) t0123456789876543210 t0123456789876543210 infixl 6 :*:@#@$$ instance SuppressUnusedWarnings (:*:@#@$) where suppressUnusedWarnings = snd (((,) (::*:@#@$###)) ()) data (:*:@#@$) :: forall a0123456789876543210 b0123456789876543210. (~>) a0123456789876543210 ((~>) b0123456789876543210 (T a0123456789876543210 b0123456789876543210)) where (::*:@#@$###) :: forall t0123456789876543210 arg. SameKind (Apply (:*:@#@$) arg) ((:*:@#@$$) arg) => (:*:@#@$) t0123456789876543210 type instance Apply (:*:@#@$) t0123456789876543210 = (:*:@#@$$) t0123456789876543210 infixl 6 :*:@#@$ type S1Sym0 = S1 type S2Sym0 = S2 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 ThenCmpSym0) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) '[])) type Compare_0123456789876543210Sym2 (a0123456789876543210 :: T a0123456789876543210 ()) (a0123456789876543210 :: T a0123456789876543210 ()) = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (Compare_0123456789876543210Sym1 a0123456789876543210) where suppressUnusedWarnings = snd (((,) Compare_0123456789876543210Sym1KindInference) ()) data Compare_0123456789876543210Sym1 (a0123456789876543210 :: T a0123456789876543210 ()) :: (~>) (T a0123456789876543210 ()) 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 :: forall a0123456789876543210. (~>) (T a0123456789876543210 ()) ((~>) (T a0123456789876543210 ()) 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 (T a ()) where type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a type family ShowsPrec_0123456789876543210 (a :: GHC.Types.Nat) (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_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: T a0123456789876543210 ()) (a0123456789876543210 :: 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 :: T a0123456789876543210 ()) :: (~>) 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 :: GHC.Types.Nat) :: forall a0123456789876543210. (~>) (T a0123456789876543210 ()) ((~>) 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 :: forall a0123456789876543210. (~>) GHC.Types.Nat ((~>) (T a0123456789876543210 ()) ((~>) 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 (T a ()) where type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a type family Compare_0123456789876543210 (a :: S) (a :: S) :: Ordering where Compare_0123456789876543210 S1 S1 = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) '[] Compare_0123456789876543210 S2 S2 = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) '[] Compare_0123456789876543210 S1 S2 = LTSym0 Compare_0123456789876543210 S2 S1 = GTSym0 type Compare_0123456789876543210Sym2 (a0123456789876543210 :: S) (a0123456789876543210 :: S) = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (Compare_0123456789876543210Sym1 a0123456789876543210) where suppressUnusedWarnings = snd (((,) Compare_0123456789876543210Sym1KindInference) ()) data Compare_0123456789876543210Sym1 (a0123456789876543210 :: S) :: (~>) S 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 :: (~>) S ((~>) S 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 S where type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a type family ShowsPrec_0123456789876543210 (a :: GHC.Types.Nat) (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_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: S) (a0123456789876543210 :: 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 :: S) :: (~>) 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 :: GHC.Types.Nat) :: (~>) S ((~>) 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 :: (~>) GHC.Types.Nat ((~>) S ((~>) 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 S where type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a type family MinBound_0123456789876543210 :: S where MinBound_0123456789876543210 = S1Sym0 type MinBound_0123456789876543210Sym0 = MinBound_0123456789876543210 type family MaxBound_0123456789876543210 :: S where MaxBound_0123456789876543210 = S2Sym0 type 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 family ToEnum_0123456789876543210 (a :: GHC.Types.Nat) :: S where ToEnum_0123456789876543210 n = Case_0123456789876543210 n (Apply (Apply (==@#@$) n) (FromInteger 0)) type ToEnum_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Types.Nat) = ToEnum_0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings ToEnum_0123456789876543210Sym0 where suppressUnusedWarnings = snd (((,) ToEnum_0123456789876543210Sym0KindInference) ()) data ToEnum_0123456789876543210Sym0 :: (~>) GHC.Types.Nat S where ToEnum_0123456789876543210Sym0KindInference :: forall a0123456789876543210 arg. SameKind (Apply ToEnum_0123456789876543210Sym0 arg) (ToEnum_0123456789876543210Sym1 arg) => ToEnum_0123456789876543210Sym0 a0123456789876543210 type instance Apply ToEnum_0123456789876543210Sym0 a0123456789876543210 = ToEnum_0123456789876543210 a0123456789876543210 type family FromEnum_0123456789876543210 (a :: S) :: GHC.Types.Nat where FromEnum_0123456789876543210 S1 = FromInteger 0 FromEnum_0123456789876543210 S2 = FromInteger 1 type FromEnum_0123456789876543210Sym1 (a0123456789876543210 :: S) = FromEnum_0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings FromEnum_0123456789876543210Sym0 where suppressUnusedWarnings = snd (((,) FromEnum_0123456789876543210Sym0KindInference) ()) data FromEnum_0123456789876543210Sym0 :: (~>) S GHC.Types.Nat where FromEnum_0123456789876543210Sym0KindInference :: forall a0123456789876543210 arg. SameKind (Apply FromEnum_0123456789876543210Sym0 arg) (FromEnum_0123456789876543210Sym1 arg) => FromEnum_0123456789876543210Sym0 a0123456789876543210 type instance Apply FromEnum_0123456789876543210Sym0 a0123456789876543210 = FromEnum_0123456789876543210 a0123456789876543210 instance PEnum S where type ToEnum a = Apply ToEnum_0123456789876543210Sym0 a type FromEnum a = Apply FromEnum_0123456789876543210Sym0 a type family Equals_0123456789876543210 (a :: T a ()) (b :: T a ()) :: Bool where Equals_0123456789876543210 ((:*:) a a) ((:*:) b b) = (&&) ((==) a b) ((==) a b) Equals_0123456789876543210 (_ :: T a ()) (_ :: T a ()) = FalseSym0 instance PEq (T a ()) where type (==) a b = Equals_0123456789876543210 a b type family Equals_0123456789876543210 (a :: S) (b :: S) :: Bool where Equals_0123456789876543210 S1 S1 = TrueSym0 Equals_0123456789876543210 S2 S2 = TrueSym0 Equals_0123456789876543210 (_ :: S) (_ :: S) = FalseSym0 instance PEq S where type (==) a b = Equals_0123456789876543210 a b infixl 6 :%*: data ST :: forall a b. T a b -> GHC.Types.Type where (:%*:) :: forall a b (n :: a) (n :: b). (Sing (n :: a)) -> (Sing (n :: b)) -> ST ((:*:) n n) 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 -> GHC.Types.Type where SS1 :: SS S1 SS2 :: SS S2 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 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) -> GHC.Types.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 @ThenCmpSym0) sThenCmp))) 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.Types.Nat) (t2 :: T a ()) (t3 :: Symbol). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Types.Nat ((~>) (T a ()) ((~>) Symbol Symbol)) -> GHC.Types.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 SOrd S where sCompare :: forall (t1 :: S) (t2 :: S). Sing t1 -> Sing t2 -> Sing (Apply (Apply (CompareSym0 :: TyFun S ((~>) S Ordering) -> GHC.Types.Type) t1) t2) sCompare SS1 SS1 = (applySing ((applySing ((applySing ((singFun3 @FoldlSym0) sFoldl)) ((singFun2 @ThenCmpSym0) sThenCmp))) SEQ)) SNil sCompare SS2 SS2 = (applySing ((applySing ((applySing ((singFun3 @FoldlSym0) sFoldl)) ((singFun2 @ThenCmpSym0) sThenCmp))) SEQ)) SNil sCompare SS1 SS2 = SLT sCompare SS2 SS1 = SGT instance SShow S where sShowsPrec :: forall (t1 :: GHC.Types.Nat) (t2 :: S) (t3 :: Symbol). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Types.Nat ((~>) S ((~>) Symbol Symbol)) -> GHC.Types.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.Types.Nat). Sing t -> Sing (Apply (ToEnumSym0 :: TyFun GHC.Types.Nat S -> GHC.Types.Type) t) sFromEnum :: forall (t :: S). Sing t -> Sing (Apply (FromEnumSym0 :: TyFun S GHC.Types.Nat -> GHC.Types.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 SEq a => SEq (T a ()) where (%==) ((:%*:) a a) ((:%*:) b b) = ((%&&) (((%==) a) b)) (((%==) a) b) 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 () -> GHC.Types.Type) where Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality instance SDecide a => Data.Type.Coercion.TestCoercion (ST :: T a () -> GHC.Types.Type) where Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion instance SEq S where (%==) SS1 SS1 = STrue (%==) SS1 SS2 = SFalse (%==) SS2 SS1 = SFalse (%==) SS2 SS2 = STrue 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 -> GHC.Types.Type) where Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality instance Data.Type.Coercion.TestCoercion (SS :: S -> GHC.Types.Type) where Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion instance Data.Singletons.ShowSing.ShowSing a => Show (ST (z :: T a ())) where showsPrec p_0123456789876543210 ((:%*:) (argL_0123456789876543210 :: Sing argTyL_0123456789876543210) (argR_0123456789876543210 :: Sing argTyR_0123456789876543210)) = (showParen (((>) p_0123456789876543210) 9)) (((.) ((showsPrec 10) argL_0123456789876543210)) (((.) (showString " :%*: ")) ((showsPrec 10) argR_0123456789876543210))) :: (Data.Singletons.ShowSing.ShowSing' argTyL_0123456789876543210, Data.Singletons.ShowSing.ShowSing' argTyR_0123456789876543210) => ShowS instance Show (SS (z :: S)) where showsPrec _ SS1 = showString "SS1" showsPrec _ SS2 = showString "SS2" instance (SingI n, SingI n) => SingI ((:*:) (n :: a) (n :: b)) where sing = ((:%*:) sing) sing 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 SingI S1 where sing = SS1 instance SingI S2 where sing = SS2