Singletons/Star.hs:0:0:: Splicing declarations singletonStar [''Nat, ''Int, ''String, ''Maybe, ''Vec] ======> data Rep = Singletons.Star.Nat | Singletons.Star.Int | Singletons.Star.String | Singletons.Star.Maybe Rep | Singletons.Star.Vec Rep Nat deriving (Eq, Ord, Read, Show) type NatSym0 = Nat type IntSym0 = Int type StringSym0 = String type MaybeSym1 (t :: Type) = Maybe t instance SuppressUnusedWarnings MaybeSym0 where suppressUnusedWarnings = snd ((GHC.Tuple.(,) MaybeSym0KindInference) GHC.Tuple.()) data MaybeSym0 (l :: TyFun Type Type) = forall arg. SameKind (Apply MaybeSym0 arg) (MaybeSym1 arg) => MaybeSym0KindInference type instance Apply MaybeSym0 l = Maybe l type VecSym2 (t :: Type) (t :: Nat) = Vec t t instance SuppressUnusedWarnings VecSym1 where suppressUnusedWarnings = snd ((GHC.Tuple.(,) VecSym1KindInference) GHC.Tuple.()) data VecSym1 (l :: Type) (l :: TyFun Nat Type) = forall arg. SameKind (Apply (VecSym1 l) arg) (VecSym2 l arg) => VecSym1KindInference type instance Apply (VecSym1 l) l = Vec l l instance SuppressUnusedWarnings VecSym0 where suppressUnusedWarnings = snd ((GHC.Tuple.(,) VecSym0KindInference) GHC.Tuple.()) data VecSym0 (l :: TyFun Type (TyFun Nat Type -> Type)) = forall arg. SameKind (Apply VecSym0 arg) (VecSym1 arg) => VecSym0KindInference type instance Apply VecSym0 l = VecSym1 l type family Equals_0123456789876543210 (a :: Type) (b :: Type) :: Bool where Equals_0123456789876543210 Nat Nat = TrueSym0 Equals_0123456789876543210 Int Int = TrueSym0 Equals_0123456789876543210 String String = TrueSym0 Equals_0123456789876543210 (Maybe a) (Maybe b) = (==) a b Equals_0123456789876543210 (Vec a a) (Vec b b) = (&&) ((==) a b) ((==) a b) Equals_0123456789876543210 (_ :: Type) (_ :: Type) = FalseSym0 instance PEq Type where type (==) a b = Equals_0123456789876543210 a b type family Compare_0123456789876543210 (a :: Type) (a :: Type) :: Ordering where Compare_0123456789876543210 Nat Nat = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) '[] Compare_0123456789876543210 Int Int = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) '[] Compare_0123456789876543210 String String = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) '[] Compare_0123456789876543210 (Maybe a_0123456789876543210) (Maybe b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) '[]) Compare_0123456789876543210 (Vec a_0123456789876543210 a_0123456789876543210) (Vec 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)) '[])) Compare_0123456789876543210 Nat Int = LTSym0 Compare_0123456789876543210 Nat String = LTSym0 Compare_0123456789876543210 Nat (Maybe _) = LTSym0 Compare_0123456789876543210 Nat (Vec _ _) = LTSym0 Compare_0123456789876543210 Int Nat = GTSym0 Compare_0123456789876543210 Int String = LTSym0 Compare_0123456789876543210 Int (Maybe _) = LTSym0 Compare_0123456789876543210 Int (Vec _ _) = LTSym0 Compare_0123456789876543210 String Nat = GTSym0 Compare_0123456789876543210 String Int = GTSym0 Compare_0123456789876543210 String (Maybe _) = LTSym0 Compare_0123456789876543210 String (Vec _ _) = LTSym0 Compare_0123456789876543210 (Maybe _) Nat = GTSym0 Compare_0123456789876543210 (Maybe _) Int = GTSym0 Compare_0123456789876543210 (Maybe _) String = GTSym0 Compare_0123456789876543210 (Maybe _) (Vec _ _) = LTSym0 Compare_0123456789876543210 (Vec _ _) Nat = GTSym0 Compare_0123456789876543210 (Vec _ _) Int = GTSym0 Compare_0123456789876543210 (Vec _ _) String = GTSym0 Compare_0123456789876543210 (Vec _ _) (Maybe _) = GTSym0 type Compare_0123456789876543210Sym2 (t :: Type) (t :: Type) = Compare_0123456789876543210 t t instance SuppressUnusedWarnings Compare_0123456789876543210Sym1 where suppressUnusedWarnings = snd ((GHC.Tuple.(,) Compare_0123456789876543210Sym1KindInference) GHC.Tuple.()) data Compare_0123456789876543210Sym1 (l :: Type) (l :: TyFun Type Ordering) = forall arg. SameKind (Apply (Compare_0123456789876543210Sym1 l) arg) (Compare_0123456789876543210Sym2 l arg) => Compare_0123456789876543210Sym1KindInference type instance Apply (Compare_0123456789876543210Sym1 l) l = Compare_0123456789876543210 l l instance SuppressUnusedWarnings Compare_0123456789876543210Sym0 where suppressUnusedWarnings = snd ((GHC.Tuple.(,) Compare_0123456789876543210Sym0KindInference) GHC.Tuple.()) data Compare_0123456789876543210Sym0 (l :: TyFun Type (TyFun Type Ordering -> Type)) = forall arg. SameKind (Apply Compare_0123456789876543210Sym0 arg) (Compare_0123456789876543210Sym1 arg) => Compare_0123456789876543210Sym0KindInference type instance Apply Compare_0123456789876543210Sym0 l = Compare_0123456789876543210Sym1 l instance POrd Type where type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a type family ShowsPrec_0123456789876543210 (a :: GHC.Types.Nat) (a :: Type) (a :: Symbol) :: Symbol where ShowsPrec_0123456789876543210 _ Nat a_0123456789876543210 = Apply (Apply ShowStringSym0 "Nat") a_0123456789876543210 ShowsPrec_0123456789876543210 _ Int a_0123456789876543210 = Apply (Apply ShowStringSym0 "Int") a_0123456789876543210 ShowsPrec_0123456789876543210 _ String a_0123456789876543210 = Apply (Apply ShowStringSym0 "String") a_0123456789876543210 ShowsPrec_0123456789876543210 p_0123456789876543210 (Maybe arg_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "Maybe ")) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210))) a_0123456789876543210 ShowsPrec_0123456789876543210 p_0123456789876543210 (Vec arg_0123456789876543210 arg_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "Vec ")) (Apply (Apply (.@#@$) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210)) (Apply (Apply (.@#@$) ShowSpaceSym0) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210))))) a_0123456789876543210 type ShowsPrec_0123456789876543210Sym3 (t :: GHC.Types.Nat) (t :: Type) (t :: Symbol) = ShowsPrec_0123456789876543210 t t t instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym2 where suppressUnusedWarnings = snd ((GHC.Tuple.(,) ShowsPrec_0123456789876543210Sym2KindInference) GHC.Tuple.()) data ShowsPrec_0123456789876543210Sym2 (l :: GHC.Types.Nat) (l :: Type) (l :: TyFun Symbol Symbol) = forall arg. SameKind (Apply (ShowsPrec_0123456789876543210Sym2 l l) arg) (ShowsPrec_0123456789876543210Sym3 l l arg) => ShowsPrec_0123456789876543210Sym2KindInference type instance Apply (ShowsPrec_0123456789876543210Sym2 l l) l = ShowsPrec_0123456789876543210 l l l instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym1 where suppressUnusedWarnings = snd ((GHC.Tuple.(,) ShowsPrec_0123456789876543210Sym1KindInference) GHC.Tuple.()) data ShowsPrec_0123456789876543210Sym1 (l :: GHC.Types.Nat) (l :: TyFun Type (TyFun Symbol Symbol -> Type)) = forall arg. SameKind (Apply (ShowsPrec_0123456789876543210Sym1 l) arg) (ShowsPrec_0123456789876543210Sym2 l arg) => ShowsPrec_0123456789876543210Sym1KindInference type instance Apply (ShowsPrec_0123456789876543210Sym1 l) l = ShowsPrec_0123456789876543210Sym2 l l instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym0 where suppressUnusedWarnings = snd ((GHC.Tuple.(,) ShowsPrec_0123456789876543210Sym0KindInference) GHC.Tuple.()) data ShowsPrec_0123456789876543210Sym0 (l :: TyFun GHC.Types.Nat (TyFun Type (TyFun Symbol Symbol -> Type) -> Type)) = forall arg. SameKind (Apply ShowsPrec_0123456789876543210Sym0 arg) (ShowsPrec_0123456789876543210Sym1 arg) => ShowsPrec_0123456789876543210Sym0KindInference type instance Apply ShowsPrec_0123456789876543210Sym0 l = ShowsPrec_0123456789876543210Sym1 l instance PShow Type where type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a data instance Sing (z :: Type) where SNat :: Sing Nat SInt :: Sing Int SString :: Sing String SMaybe :: forall (n :: Type). (Sing (n :: Type)) -> Sing (Maybe n) SVec :: forall (n :: Type) (n :: Nat). (Sing (n :: Type)) -> (Sing (n :: Nat)) -> Sing (Vec n n) type SRep = (Sing :: Type -> Type) instance SingKind Type where type Demote Type = Rep fromSing SNat = Singletons.Star.Nat fromSing SInt = Singletons.Star.Int fromSing SString = Singletons.Star.String fromSing (SMaybe b) = Singletons.Star.Maybe (fromSing b) fromSing (SVec b b) = (Singletons.Star.Vec (fromSing b)) (fromSing b) toSing Singletons.Star.Nat = SomeSing SNat toSing Singletons.Star.Int = SomeSing SInt toSing Singletons.Star.String = SomeSing SString toSing (Singletons.Star.Maybe (b :: Demote Type)) = case toSing b :: SomeSing Type of { SomeSing c -> SomeSing (SMaybe c) } toSing (Singletons.Star.Vec (b :: Demote Type) (b :: Demote Nat)) = case (GHC.Tuple.(,) (toSing b :: SomeSing Type)) (toSing b :: SomeSing Nat) of { GHC.Tuple.(,) (SomeSing c) (SomeSing c) -> SomeSing ((SVec c) c) } instance (SEq Type, SEq Nat) => SEq Type where (%==) SNat SNat = STrue (%==) SNat SInt = SFalse (%==) SNat SString = SFalse (%==) SNat (SMaybe _) = SFalse (%==) SNat (SVec _ _) = SFalse (%==) SInt SNat = SFalse (%==) SInt SInt = STrue (%==) SInt SString = SFalse (%==) SInt (SMaybe _) = SFalse (%==) SInt (SVec _ _) = SFalse (%==) SString SNat = SFalse (%==) SString SInt = SFalse (%==) SString SString = STrue (%==) SString (SMaybe _) = SFalse (%==) SString (SVec _ _) = SFalse (%==) (SMaybe _) SNat = SFalse (%==) (SMaybe _) SInt = SFalse (%==) (SMaybe _) SString = SFalse (%==) (SMaybe a) (SMaybe b) = ((%==) a) b (%==) (SMaybe _) (SVec _ _) = SFalse (%==) (SVec _ _) SNat = SFalse (%==) (SVec _ _) SInt = SFalse (%==) (SVec _ _) SString = SFalse (%==) (SVec _ _) (SMaybe _) = SFalse (%==) (SVec a a) (SVec b b) = ((%&&) (((%==) a) b)) (((%==) a) b) instance (SDecide Type, SDecide Nat) => SDecide Type where (%~) SNat SNat = Proved Refl (%~) SNat SInt = Disproved (\ x -> case x of) (%~) SNat SString = Disproved (\ x -> case x of) (%~) SNat (SMaybe _) = Disproved (\ x -> case x of) (%~) SNat (SVec _ _) = Disproved (\ x -> case x of) (%~) SInt SNat = Disproved (\ x -> case x of) (%~) SInt SInt = Proved Refl (%~) SInt SString = Disproved (\ x -> case x of) (%~) SInt (SMaybe _) = Disproved (\ x -> case x of) (%~) SInt (SVec _ _) = Disproved (\ x -> case x of) (%~) SString SNat = Disproved (\ x -> case x of) (%~) SString SInt = Disproved (\ x -> case x of) (%~) SString SString = Proved Refl (%~) SString (SMaybe _) = Disproved (\ x -> case x of) (%~) SString (SVec _ _) = Disproved (\ x -> case x of) (%~) (SMaybe _) SNat = Disproved (\ x -> case x of) (%~) (SMaybe _) SInt = Disproved (\ x -> case x of) (%~) (SMaybe _) SString = Disproved (\ x -> case x of) (%~) (SMaybe a) (SMaybe b) = case ((%~) a) b of Proved Refl -> Proved Refl Disproved contra -> Disproved (\ refl -> case refl of { Refl -> contra Refl }) (%~) (SMaybe _) (SVec _ _) = Disproved (\ x -> case x of) (%~) (SVec _ _) SNat = Disproved (\ x -> case x of) (%~) (SVec _ _) SInt = Disproved (\ x -> case x of) (%~) (SVec _ _) SString = Disproved (\ x -> case x of) (%~) (SVec _ _) (SMaybe _) = Disproved (\ x -> case x of) (%~) (SVec a a) (SVec b b) = case (GHC.Tuple.(,) (((%~) a) b)) (((%~) a) b) of GHC.Tuple.(,) (Proved Refl) (Proved Refl) -> Proved Refl GHC.Tuple.(,) (Disproved contra) _ -> Disproved (\ refl -> case refl of { Refl -> contra Refl }) GHC.Tuple.(,) _ (Disproved contra) -> Disproved (\ refl -> case refl of { Refl -> contra Refl }) instance (SOrd Type, SOrd Nat) => SOrd Type where sCompare :: forall (t1 :: Type) (t2 :: Type). Sing t1 -> Sing t2 -> Sing (Apply (Apply (CompareSym0 :: TyFun Type (TyFun Type Ordering -> Type) -> Type) t1) t2) sCompare SNat SNat = (applySing ((applySing ((applySing ((singFun3 @FoldlSym0) sFoldl)) ((singFun2 @ThenCmpSym0) sThenCmp))) SEQ)) SNil sCompare SInt SInt = (applySing ((applySing ((applySing ((singFun3 @FoldlSym0) sFoldl)) ((singFun2 @ThenCmpSym0) sThenCmp))) SEQ)) SNil sCompare SString SString = (applySing ((applySing ((applySing ((singFun3 @FoldlSym0) sFoldl)) ((singFun2 @ThenCmpSym0) sThenCmp))) SEQ)) SNil sCompare (SMaybe (sA_0123456789876543210 :: Sing a_0123456789876543210)) (SMaybe (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))) SNil) sCompare (SVec (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210)) (SVec (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)) sCompare SNat SInt = SLT sCompare SNat SString = SLT sCompare SNat (SMaybe _) = SLT sCompare SNat (SVec _ _) = SLT sCompare SInt SNat = SGT sCompare SInt SString = SLT sCompare SInt (SMaybe _) = SLT sCompare SInt (SVec _ _) = SLT sCompare SString SNat = SGT sCompare SString SInt = SGT sCompare SString (SMaybe _) = SLT sCompare SString (SVec _ _) = SLT sCompare (SMaybe _) SNat = SGT sCompare (SMaybe _) SInt = SGT sCompare (SMaybe _) SString = SGT sCompare (SMaybe _) (SVec _ _) = SLT sCompare (SVec _ _) SNat = SGT sCompare (SVec _ _) SInt = SGT sCompare (SVec _ _) SString = SGT sCompare (SVec _ _) (SMaybe _) = SGT instance (SShow Type, SShow Nat) => SShow Type where sShowsPrec :: forall (t1 :: GHC.Types.Nat) (t2 :: Type) (t3 :: Symbol). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Types.Nat (TyFun Type (TyFun Symbol Symbol -> Type) -> Type) -> Type) t1) t2) t3) sShowsPrec _ SNat (sA_0123456789876543210 :: Sing a_0123456789876543210) = (applySing ((applySing ((singFun2 @ShowStringSym0) sShowString)) (sing :: Sing "Nat"))) sA_0123456789876543210 sShowsPrec _ SInt (sA_0123456789876543210 :: Sing a_0123456789876543210) = (applySing ((applySing ((singFun2 @ShowStringSym0) sShowString)) (sing :: Sing "Int"))) sA_0123456789876543210 sShowsPrec _ SString (sA_0123456789876543210 :: Sing a_0123456789876543210) = (applySing ((applySing ((singFun2 @ShowStringSym0) sShowString)) (sing :: Sing "String"))) sA_0123456789876543210 sShowsPrec (sP_0123456789876543210 :: Sing p_0123456789876543210) (SMaybe (sArg_0123456789876543210 :: Sing arg_0123456789876543210)) (sA_0123456789876543210 :: Sing a_0123456789876543210) = (applySing ((applySing ((applySing ((singFun3 @ShowParenSym0) sShowParen)) ((applySing ((applySing ((singFun2 @(>@#@$)) (%>))) sP_0123456789876543210)) (sFromInteger (sing :: Sing 10))))) ((applySing ((applySing ((singFun3 @(.@#@$)) (%.))) ((applySing ((singFun2 @ShowStringSym0) sShowString)) (sing :: Sing "Maybe ")))) ((applySing ((applySing ((singFun3 @ShowsPrecSym0) sShowsPrec)) (sFromInteger (sing :: Sing 11)))) sArg_0123456789876543210)))) sA_0123456789876543210 sShowsPrec (sP_0123456789876543210 :: Sing p_0123456789876543210) (SVec (sArg_0123456789876543210 :: Sing arg_0123456789876543210) (sArg_0123456789876543210 :: Sing arg_0123456789876543210)) (sA_0123456789876543210 :: Sing a_0123456789876543210) = (applySing ((applySing ((applySing ((singFun3 @ShowParenSym0) sShowParen)) ((applySing ((applySing ((singFun2 @(>@#@$)) (%>))) sP_0123456789876543210)) (sFromInteger (sing :: Sing 10))))) ((applySing ((applySing ((singFun3 @(.@#@$)) (%.))) ((applySing ((singFun2 @ShowStringSym0) sShowString)) (sing :: Sing "Vec ")))) ((applySing ((applySing ((singFun3 @(.@#@$)) (%.))) ((applySing ((applySing ((singFun3 @ShowsPrecSym0) sShowsPrec)) (sFromInteger (sing :: Sing 11)))) sArg_0123456789876543210))) ((applySing ((applySing ((singFun3 @(.@#@$)) (%.))) ((singFun1 @ShowSpaceSym0) sShowSpace))) ((applySing ((applySing ((singFun3 @ShowsPrecSym0) sShowsPrec)) (sFromInteger (sing :: Sing 11)))) sArg_0123456789876543210)))))) sA_0123456789876543210 instance SingI Nat where sing = SNat instance SingI Int where sing = SInt instance SingI String where sing = SString instance SingI n => SingI (Maybe (n :: Type)) where sing = SMaybe sing instance (SingI n, SingI n) => SingI (Vec (n :: Type) (n :: Nat)) where sing = (SVec sing) sing