singletons-1.1: tests/compile-and-dump/Singletons/Star.ghc78.template
Singletons/Star.hs:0:0: Splicing declarations
singletonStar [''Nat, ''Int, ''String, ''Maybe, ''Vec]
======>
Singletons/Star.hs:0:0:
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_0123456789 (a :: *) (b :: *) :: Bool where
Equals_0123456789 Nat Nat = TrueSym0
Equals_0123456789 Int Int = TrueSym0
Equals_0123456789 String String = TrueSym0
Equals_0123456789 (Maybe a) (Maybe b) = (:==) a b
Equals_0123456789 (Vec a a) (Vec b b) = (:&&) ((:==) a b) ((:==) a b)
Equals_0123456789 (a :: *) (b :: *) = FalseSym0
instance PEq (KProxy :: KProxy *) where
type (:==) (a :: *) (b :: *) = Equals_0123456789 a b
instance POrd (KProxy :: KProxy *) where
type Compare Nat Nat = EQ
type Compare Nat Int = LT
type Compare Nat String = LT
type Compare Nat (Maybe rhs) = LT
type Compare Nat (Vec rhs rhs) = LT
type Compare Int Nat = GT
type Compare Int Int = EQ
type Compare Int String = LT
type Compare Int (Maybe rhs) = LT
type Compare Int (Vec rhs rhs) = LT
type Compare String Nat = GT
type Compare String Int = GT
type Compare String String = EQ
type Compare String (Maybe rhs) = LT
type Compare String (Vec rhs rhs) = LT
type Compare (Maybe lhs) Nat = GT
type Compare (Maybe lhs) Int = GT
type Compare (Maybe lhs) String = GT
type Compare (Maybe lhs) (Maybe rhs) = ThenCmp EQ (Compare lhs rhs)
type Compare (Maybe lhs) (Vec rhs rhs) = LT
type Compare (Vec lhs lhs) Nat = GT
type Compare (Vec lhs lhs) Int = GT
type Compare (Vec lhs lhs) String = GT
type Compare (Vec lhs lhs) (Maybe rhs) = GT
type Compare (Vec lhs lhs) (Vec rhs rhs) = ThenCmp (ThenCmp EQ (Compare lhs rhs)) (Compare lhs rhs)
type NatSym0 = Nat
type IntSym0 = Int
type StringSym0 = String
type MaybeSym1 (t :: *) = Maybe t
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings MaybeSym0 where
Data.Singletons.SuppressUnusedWarnings.suppressUnusedWarnings _
= snd (GHC.Tuple.(,) MaybeSym0KindInference GHC.Tuple.())
data MaybeSym0 (l :: TyFun * *)
= forall arg. KindOf (Apply MaybeSym0 arg) ~ KindOf (MaybeSym1 arg) =>
MaybeSym0KindInference
type instance Apply MaybeSym0 l = MaybeSym1 l
type VecSym2 (t :: *) (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 :: *) (l :: TyFun Nat *)
= forall arg. KindOf (Apply (VecSym1 l) arg) ~ KindOf (VecSym2 l arg) =>
VecSym1KindInference
type instance Apply (VecSym1 l) l = VecSym2 l l
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings VecSym0 where
Data.Singletons.SuppressUnusedWarnings.suppressUnusedWarnings _
= snd (GHC.Tuple.(,) VecSym0KindInference GHC.Tuple.())
data VecSym0 (l :: TyFun * (TyFun Nat * -> *))
= forall arg. KindOf (Apply VecSym0 arg) ~ KindOf (VecSym1 arg) =>
VecSym0KindInference
type instance Apply VecSym0 l = VecSym1 l
data instance Sing (z :: *)
= z ~ Nat => SNat |
z ~ Int => SInt |
z ~ String => SString |
forall (n :: *). z ~ Maybe n => SMaybe (Sing n) |
forall (n :: *) (n :: Nat). z ~ Vec n n => SVec (Sing n) (Sing n)
type SRep (z :: *) = Sing z
instance SingKind (KProxy :: KProxy *) where
type DemoteRep (KProxy :: KProxy *) = 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 (KProxy :: KProxy *) of {
SomeSing c -> SomeSing (SMaybe c) }
toSing (Singletons.Star.Vec b b)
= case
GHC.Tuple.(,)
(toSing b :: SomeSing (KProxy :: KProxy *))
(toSing b :: SomeSing (KProxy :: KProxy Nat))
of {
GHC.Tuple.(,) (SomeSing c) (SomeSing c) -> SomeSing (SVec c c) }
instance SEq (KProxy :: KProxy *) 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 (KProxy :: KProxy *) 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 :: *)) where
sing = SMaybe sing
instance (SingI n, SingI n) =>
SingI (Vec (n :: *) (n :: Nat)) where
sing = SVec sing sing