singletons-base-3.2: tests/compile-and-dump/Singletons/Star.golden
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)