singletons-2.3: tests/compile-and-dump/Singletons/Star.ghc82.template
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, Show, Read)
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 (a :: Type) (b :: Type) = FalseSym0
instance PEq Type where
type (:==) (a :: Type) (b :: Type) = Equals_0123456789876543210 a b
type NatSym0 = Nat
type IntSym0 = Int
type StringSym0 = String
type MaybeSym1 (t :: Type) = Maybe t
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings MaybeSym0 where
Data.Singletons.SuppressUnusedWarnings.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 Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings VecSym1 where
Data.Singletons.SuppressUnusedWarnings.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 Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings VecSym0 where
Data.Singletons.SuppressUnusedWarnings.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 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 _z_0123456789876543210) = LTSym0
Compare_0123456789876543210 Nat (Vec _z_0123456789876543210 _z_0123456789876543210) = LTSym0
Compare_0123456789876543210 Int Nat = GTSym0
Compare_0123456789876543210 Int String = LTSym0
Compare_0123456789876543210 Int (Maybe _z_0123456789876543210) = LTSym0
Compare_0123456789876543210 Int (Vec _z_0123456789876543210 _z_0123456789876543210) = LTSym0
Compare_0123456789876543210 String Nat = GTSym0
Compare_0123456789876543210 String Int = GTSym0
Compare_0123456789876543210 String (Maybe _z_0123456789876543210) = LTSym0
Compare_0123456789876543210 String (Vec _z_0123456789876543210 _z_0123456789876543210) = LTSym0
Compare_0123456789876543210 (Maybe _z_0123456789876543210) Nat = GTSym0
Compare_0123456789876543210 (Maybe _z_0123456789876543210) Int = GTSym0
Compare_0123456789876543210 (Maybe _z_0123456789876543210) String = GTSym0
Compare_0123456789876543210 (Maybe _z_0123456789876543210) (Vec _z_0123456789876543210 _z_0123456789876543210) = LTSym0
Compare_0123456789876543210 (Vec _z_0123456789876543210 _z_0123456789876543210) Nat = GTSym0
Compare_0123456789876543210 (Vec _z_0123456789876543210 _z_0123456789876543210) Int = GTSym0
Compare_0123456789876543210 (Vec _z_0123456789876543210 _z_0123456789876543210) String = GTSym0
Compare_0123456789876543210 (Vec _z_0123456789876543210 _z_0123456789876543210) (Maybe _z_0123456789876543210) = GTSym0
type Compare_0123456789876543210Sym2 (t :: Type) (t :: Type) =
Compare_0123456789876543210 t t
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Compare_0123456789876543210Sym1 where
Data.Singletons.SuppressUnusedWarnings.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 Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Compare_0123456789876543210Sym0 where
Data.Singletons.SuppressUnusedWarnings.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 :: Type) (a :: Type) = Apply (Apply Compare_0123456789876543210Sym0 a) a
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 :: TyFun Type Ordering
-> Type) t2 :: Ordering)
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
data instance Sing (z :: Type)
= z ~ Nat => SNat |
z ~ Int => SInt |
z ~ String => SString |
forall (n :: Type). z ~ Maybe n => SMaybe (Sing (n :: Type)) |
forall (n :: Type) (n :: Nat). z ~ Vec n n =>
SVec (Sing (n :: Type)) (Sing (n :: Nat))
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)
= case toSing b :: SomeSing Type of {
SomeSing c -> SomeSing (SMaybe c) }
toSing (Singletons.Star.Vec b b)
= 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 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 where
(%~) SNat SNat = Proved Refl
(%~) SNat SInt
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) SNat SString
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) SNat (SMaybe _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) SNat (SVec _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) SInt SNat
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) SInt SInt = Proved Refl
(%~) SInt SString
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) SInt (SMaybe _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) SInt (SVec _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) SString SNat
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) SString SInt
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) SString SString = Proved Refl
(%~) SString (SMaybe _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) SString (SVec _ _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SMaybe _) SNat
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SMaybe _) SInt
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SMaybe _) SString
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (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 {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SVec _ _) SNat
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SVec _ _) SInt
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SVec _ _) SString
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (SVec _ _) (SMaybe _)
= Disproved
(\ x
-> case x of {
_ -> error "Empty case reached -- this should be impossible" })
(%~) (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 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