singletons-0.10.0: tests/compile-and-dump/Singletons/Star.ghc76.template
Singletons/Star.hs:0:0: Splicing declarations
singletonStar [''Nat, ''Int, ''String, ''Maybe, ''Vec]
======>
Singletons/Star.hs:0:0:
data Rep
= Nat | Int | String | Maybe Rep | Vec Rep Nat
deriving (Eq, Show, Read)
type instance (:==) Nat Nat = True
type instance (:==) Nat Int = False
type instance (:==) Nat String = False
type instance (:==) Nat (Maybe b) = False
type instance (:==) Nat (Vec b b) = False
type instance (:==) Int Nat = False
type instance (:==) Int Int = True
type instance (:==) Int String = False
type instance (:==) Int (Maybe b) = False
type instance (:==) Int (Vec b b) = False
type instance (:==) String Nat = False
type instance (:==) String Int = False
type instance (:==) String String = True
type instance (:==) String (Maybe b) = False
type instance (:==) String (Vec b b) = False
type instance (:==) (Maybe a) Nat = False
type instance (:==) (Maybe a) Int = False
type instance (:==) (Maybe a) String = False
type instance (:==) (Maybe a) (Maybe b) = :== a b
type instance (:==) (Maybe a) (Vec b b) = False
type instance (:==) (Vec a a) Nat = False
type instance (:==) (Vec a a) Int = False
type instance (:==) (Vec a a) String = False
type instance (:==) (Vec a a) (Maybe b) = False
type instance (:==) (Vec a a) (Vec b b) = :&& (:== a b) (:== a b)
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 instance DemoteRep (KProxy :: KProxy *) = Rep
fromSing SNat = Nat
fromSing SInt = Int
fromSing SString = String
fromSing (SMaybe b) = Maybe (fromSing b)
fromSing (SVec b b) = Vec (fromSing b) (fromSing b)
toSing Nat = SomeSing SNat
toSing Int = SomeSing SInt
toSing String = SomeSing SString
toSing (Maybe b)
= case toSing b :: SomeSing (KProxy :: KProxy *) of {
SomeSing c -> SomeSing (SMaybe c) }
toSing (Vec b b)
= case
(toSing b :: SomeSing (KProxy :: KProxy *),
toSing b :: SomeSing (KProxy :: KProxy Nat))
of {
(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
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SNat SString
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SNat (SMaybe _)
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SNat (SVec _ _)
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SInt SNat
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SInt SInt = Proved Refl
%~ SInt SString
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SInt (SMaybe _)
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SInt (SVec _ _)
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SString SNat
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SString SInt
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SString SString = Proved Refl
%~ SString (SMaybe _)
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ SString (SVec _ _)
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ (SMaybe _) SNat
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ (SMaybe _) SInt
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ (SMaybe _) SString
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ (SMaybe a) (SMaybe b)
= case (%~) a b of {
Proved Refl -> Proved Refl
Disproved contra -> Disproved (\ Refl -> contra Refl) }
%~ (SMaybe _) (SVec _ _)
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ (SVec _ _) SNat
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ (SVec _ _) SInt
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ (SVec _ _) SString
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ (SVec _ _) (SMaybe _)
= Disproved
(\case {
_ -> error "Empty case reached -- this should be impossible" })
%~ (SVec a a) (SVec b b)
= case ((%~) a b, (%~) a b) of {
(Proved Refl, Proved Refl) -> Proved Refl
(Disproved contra, _) -> Disproved (\ Refl -> contra Refl)
(_, Disproved contra) -> Disproved (\ 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