singletons-2.7: 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 = Nat :: Type
type IntSym0 = Int :: Type
type StringSym0 = String :: Type
type MaybeSym0 :: (~>) Type Type
data MaybeSym0 a0123456789876543210
where
MaybeSym0KindInference :: SameKind (Apply MaybeSym0 arg) (MaybeSym1 arg) =>
MaybeSym0 a0123456789876543210
type instance Apply MaybeSym0 a0123456789876543210 = MaybeSym1 a0123456789876543210
instance SuppressUnusedWarnings MaybeSym0 where
suppressUnusedWarnings = snd (((,) MaybeSym0KindInference) ())
type MaybeSym1 (a0123456789876543210 :: Type) =
Maybe a0123456789876543210 :: Type
type VecSym0 :: (~>) Type ((~>) Nat Type)
data VecSym0 a0123456789876543210
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 a0123456789876543210
where
VecSym1KindInference :: SameKind (Apply (VecSym1 a0123456789876543210) arg) (VecSym2 a0123456789876543210 arg) =>
VecSym1 a0123456789876543210 a0123456789876543210
type instance Apply (VecSym1 a0123456789876543210) a0123456789876543210 = VecSym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (VecSym1 a0123456789876543210) where
suppressUnusedWarnings = snd (((,) VecSym1KindInference) ())
type VecSym2 (a0123456789876543210 :: Type) (a0123456789876543210 :: Nat) =
Vec a0123456789876543210 a0123456789876543210 :: Type
type Equals_0123456789876543210 :: Type -> Type -> Bool
type family Equals_0123456789876543210 a b 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 Compare_0123456789876543210 :: Type -> Type -> Ordering
type family Compare_0123456789876543210 a a where
Compare_0123456789876543210 Nat Nat = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) NilSym0
Compare_0123456789876543210 Int Int = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) NilSym0
Compare_0123456789876543210 String String = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) NilSym0
Compare_0123456789876543210 (Maybe a_0123456789876543210) (Maybe b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) 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 ThenCmpSym0) 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 a0123456789876543210
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 a0123456789876543210
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_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (Compare_0123456789876543210Sym1 a0123456789876543210) where
suppressUnusedWarnings
= snd (((,) Compare_0123456789876543210Sym1KindInference) ())
type Compare_0123456789876543210Sym2 (a0123456789876543210 :: Type) (a0123456789876543210 :: Type) =
Compare_0123456789876543210 a0123456789876543210 a0123456789876543210 :: Ordering
instance POrd Type where
type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a
type ShowsPrec_0123456789876543210 :: GHC.Types.Nat
-> Type -> Symbol -> Symbol
type family ShowsPrec_0123456789876543210 a a a 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.Types.Nat ((~>) Type ((~>) Symbol Symbol))
data ShowsPrec_0123456789876543210Sym0 a0123456789876543210
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.Types.Nat
-> (~>) Type ((~>) Symbol Symbol)
data ShowsPrec_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
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.Types.Nat
-> Type -> (~>) Symbol Symbol
data ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 a0123456789876543210
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_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) where
suppressUnusedWarnings
= snd (((,) ShowsPrec_0123456789876543210Sym2KindInference) ())
type ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: Type) (a0123456789876543210 :: Symbol) =
ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 :: Symbol
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 (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 ((,) (((%~) 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 (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 @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 ((~>) 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 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 (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))