Singletons/Star.hs:0:0:: Splicing declarations singletonStar [''Nat, ''Int, ''String, ''Maybe, ''Vec] ======> data Rep :: Type where Singletons.Star.Nat :: Rep Singletons.Star.Int :: Rep Singletons.Star.String :: Rep Singletons.Star.Maybe :: Rep -> Rep Singletons.Star.Vec :: Rep -> Nat -> Rep deriving (Eq, Ord, Read, Show) type NatSym0 :: Type type family NatSym0 :: Type where NatSym0 = Nat type IntSym0 :: Type type family IntSym0 :: Type where IntSym0 = Int type StringSym0 :: Type type family StringSym0 :: Type where StringSym0 = String type MaybeSym0 :: (~>) Type Type data MaybeSym0 :: (~>) Type Type where MaybeSym0KindInference :: SameKind (Apply MaybeSym0 arg) (MaybeSym1 arg) => MaybeSym0 a0123456789876543210 type instance Apply MaybeSym0 a0123456789876543210 = Maybe a0123456789876543210 instance SuppressUnusedWarnings MaybeSym0 where suppressUnusedWarnings = snd ((,) MaybeSym0KindInference ()) type MaybeSym1 :: Type -> Type type family MaybeSym1 (a0123456789876543210 :: Type) :: Type where MaybeSym1 a0123456789876543210 = Maybe a0123456789876543210 type VecSym0 :: (~>) Type ((~>) Nat Type) data VecSym0 :: (~>) Type ((~>) Nat Type) where VecSym0KindInference :: SameKind (Apply VecSym0 arg) (VecSym1 arg) => VecSym0 a0123456789876543210 type instance Apply VecSym0 a0123456789876543210 = VecSym1 a0123456789876543210 instance SuppressUnusedWarnings VecSym0 where suppressUnusedWarnings = snd ((,) VecSym0KindInference ()) type VecSym1 :: Type -> (~>) Nat Type data VecSym1 (a0123456789876543210 :: Type) :: (~>) Nat Type where VecSym1KindInference :: SameKind (Apply (VecSym1 a0123456789876543210) arg) (VecSym2 a0123456789876543210 arg) => VecSym1 a0123456789876543210 a0123456789876543210 type instance Apply (VecSym1 a0123456789876543210) a0123456789876543210 = Vec a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (VecSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) VecSym1KindInference ()) type VecSym2 :: Type -> Nat -> Type type family VecSym2 (a0123456789876543210 :: Type) (a0123456789876543210 :: Nat) :: Type where VecSym2 a0123456789876543210 a0123456789876543210 = Vec a0123456789876543210 a0123456789876543210 type TFHelper_0123456789876543210 :: Type -> Type -> Bool type family TFHelper_0123456789876543210 (a :: Type) (a :: Type) :: Bool where TFHelper_0123456789876543210 Nat Nat = TrueSym0 TFHelper_0123456789876543210 Nat Int = FalseSym0 TFHelper_0123456789876543210 Nat String = FalseSym0 TFHelper_0123456789876543210 Nat (Maybe _) = FalseSym0 TFHelper_0123456789876543210 Nat (Vec _ _) = FalseSym0 TFHelper_0123456789876543210 Int Nat = FalseSym0 TFHelper_0123456789876543210 Int Int = TrueSym0 TFHelper_0123456789876543210 Int String = FalseSym0 TFHelper_0123456789876543210 Int (Maybe _) = FalseSym0 TFHelper_0123456789876543210 Int (Vec _ _) = FalseSym0 TFHelper_0123456789876543210 String Nat = FalseSym0 TFHelper_0123456789876543210 String Int = FalseSym0 TFHelper_0123456789876543210 String String = TrueSym0 TFHelper_0123456789876543210 String (Maybe _) = FalseSym0 TFHelper_0123456789876543210 String (Vec _ _) = FalseSym0 TFHelper_0123456789876543210 (Maybe _) Nat = FalseSym0 TFHelper_0123456789876543210 (Maybe _) Int = FalseSym0 TFHelper_0123456789876543210 (Maybe _) String = FalseSym0 TFHelper_0123456789876543210 (Maybe a_0123456789876543210) (Maybe b_0123456789876543210) = Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210 TFHelper_0123456789876543210 (Maybe _) (Vec _ _) = FalseSym0 TFHelper_0123456789876543210 (Vec _ _) Nat = FalseSym0 TFHelper_0123456789876543210 (Vec _ _) Int = FalseSym0 TFHelper_0123456789876543210 (Vec _ _) String = FalseSym0 TFHelper_0123456789876543210 (Vec _ _) (Maybe _) = FalseSym0 TFHelper_0123456789876543210 (Vec a_0123456789876543210 a_0123456789876543210) (Vec b_0123456789876543210 b_0123456789876543210) = Apply (Apply (&&@#@$) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210) type TFHelper_0123456789876543210Sym0 :: (~>) Type ((~>) Type Bool) data TFHelper_0123456789876543210Sym0 :: (~>) Type ((~>) Type 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 :: Type -> (~>) Type Bool data TFHelper_0123456789876543210Sym1 (a0123456789876543210 :: Type) :: (~>) Type 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 :: Type -> Type -> Bool type family TFHelper_0123456789876543210Sym2 (a0123456789876543210 :: Type) (a0123456789876543210 :: Type) :: Bool where TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210 instance PEq Type where type (==) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a type Compare_0123456789876543210 :: Type -> Type -> Ordering type family Compare_0123456789876543210 (a :: Type) (a :: Type) :: Ordering where Compare_0123456789876543210 Nat Nat = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) NilSym0 Compare_0123456789876543210 Int Int = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) NilSym0 Compare_0123456789876543210 String String = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) NilSym0 Compare_0123456789876543210 (Maybe a_0123456789876543210) (Maybe b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0) Compare_0123456789876543210 (Vec a_0123456789876543210 a_0123456789876543210) (Vec b_0123456789876543210 b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0)) 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_0123456789876543210Sym0 :: (~>) Type ((~>) Type Ordering) data Compare_0123456789876543210Sym0 :: (~>) Type ((~>) Type 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 :: Type -> (~>) Type Ordering data Compare_0123456789876543210Sym1 (a0123456789876543210 :: Type) :: (~>) Type 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 :: Type -> Type -> Ordering type family Compare_0123456789876543210Sym2 (a0123456789876543210 :: Type) (a0123456789876543210 :: Type) :: Ordering where Compare_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210 instance POrd Type where type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a type ShowsPrec_0123456789876543210 :: GHC.Num.Natural.Natural -> Type -> Symbol -> Symbol type family ShowsPrec_0123456789876543210 (a :: GHC.Num.Natural.Natural) (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_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) Type ((~>) Symbol Symbol)) data ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) Type ((~>) 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 -> (~>) Type ((~>) Symbol Symbol) data ShowsPrec_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Num.Natural.Natural) :: (~>) Type ((~>) 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 -> Type -> (~>) Symbol Symbol data ShowsPrec_0123456789876543210Sym2 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: Type) :: (~>) 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 -> Type -> Symbol -> Symbol type family ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: Type) (a0123456789876543210 :: Symbol) :: Symbol where ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance PShow Type where type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a data SRep :: Type -> Type where SNat :: SRep (Nat :: Type) SInt :: SRep (Int :: Type) SString :: SRep (String :: Type) SMaybe :: forall (n :: Type). (Sing n) -> SRep (Maybe n :: Type) SVec :: forall (n :: Type) (n :: Nat). (Sing n) -> (Sing n) -> SRep (Vec n n :: Type) type instance Sing @Type = SRep 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 (,) (toSing b :: SomeSing Type) (toSing b :: SomeSing Nat) of (,) (SomeSing c) (SomeSing c) -> SomeSing (SVec c c) 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 (,) ((%~) 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 Type, SDecide Nat) => Data.Type.Equality.TestEquality (SRep :: Type -> Type) where Data.Type.Equality.testEquality = decideEquality instance (SDecide Type, SDecide Nat) => Data.Type.Coercion.TestCoercion (SRep :: Type -> Type) where Data.Type.Coercion.testCoercion = decideCoercion instance (SEq Type, SEq Nat) => SEq Type where (%==) :: forall (t1 :: Type) (t2 :: Type). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun Type ((~>) Type Bool) -> Type) t1) t2) (%==) 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 (sA_0123456789876543210 :: Sing a_0123456789876543210)) (SMaybe (sB_0123456789876543210 :: Sing b_0123456789876543210)) = applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210 (%==) (SMaybe _) (SVec _ _) = SFalse (%==) (SVec _ _) SNat = SFalse (%==) (SVec _ _) SInt = SFalse (%==) (SVec _ _) SString = SFalse (%==) (SVec _ _) (SMaybe _) = SFalse (%==) (SVec (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210)) (SVec (sB_0123456789876543210 :: Sing b_0123456789876543210) (sB_0123456789876543210 :: Sing b_0123456789876543210)) = applySing (applySing (singFun2 @(&&@#@$) (%&&)) (applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210)) (applySing (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210) instance (SOrd Type, SOrd Nat) => SOrd Type where sCompare :: forall (t1 :: Type) (t2 :: Type). Sing t1 -> Sing t2 -> Sing (Apply (Apply (CompareSym0 :: TyFun Type ((~>) Type Ordering) -> Type) t1) t2) sCompare SNat SNat = applySing (applySing (applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>))) SEQ) SNil sCompare SInt SInt = applySing (applySing (applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>))) SEQ) SNil sCompare SString SString = applySing (applySing (applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>))) SEQ) SNil sCompare (SMaybe (sA_0123456789876543210 :: Sing a_0123456789876543210)) (SMaybe (sB_0123456789876543210 :: Sing b_0123456789876543210)) = applySing (applySing (applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>))) 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 @(<>@#@$) (%<>))) 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.Num.Natural.Natural) (t2 :: Type) (t3 :: Symbol). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) Type ((~>) Symbol Symbol)) -> 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 SingI1 Maybe where liftSing = SMaybe instance SingI (MaybeSym0 :: (~>) Type Type) where sing = singFun1 @MaybeSym0 SMaybe instance (SingI n, SingI n) => SingI (Vec (n :: Type) (n :: Nat)) where sing = SVec sing sing instance SingI n => SingI1 (Vec (n :: Type)) where liftSing = SVec sing instance SingI2 Vec where liftSing2 = SVec instance SingI (VecSym0 :: (~>) Type ((~>) Nat Type)) where sing = singFun2 @VecSym0 SVec instance SingI d => SingI (VecSym1 (d :: Type) :: (~>) Nat Type) where sing = singFun1 @(VecSym1 (d :: Type)) (SVec (sing @d)) instance SingI1 (VecSym1 :: Type -> (~>) Nat Type) where liftSing (s :: Sing (d :: Type)) = singFun1 @(VecSym1 (d :: Type)) (SVec s)