singletons-2.1: tests/compile-and-dump/Singletons/Star.ghc80.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_0123456789 (a :: Type) (b :: Type) :: 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 :: Type) (b :: Type) = FalseSym0
instance PEq (KProxy :: KProxy Type) where
type (:==) (a :: Type) (b :: Type) = Equals_0123456789 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. KindOf (Apply MaybeSym0 arg) ~ KindOf (MaybeSym1 arg) =>
MaybeSym0KindInference
type instance Apply MaybeSym0 l = MaybeSym1 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. 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 Type (TyFun Nat Type -> Type))
= forall arg. KindOf (Apply VecSym0 arg) ~ KindOf (VecSym1 arg) =>
VecSym0KindInference
type instance Apply VecSym0 l = VecSym1 l
type family Compare_0123456789 (a :: Type)
(a :: Type) :: Ordering where
Compare_0123456789 Nat Nat = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) '[]
Compare_0123456789 Int Int = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) '[]
Compare_0123456789 String String = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) '[]
Compare_0123456789 (Maybe a_0123456789) (Maybe b_0123456789) = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) (Apply (Apply (:$) (Apply (Apply CompareSym0 a_0123456789) b_0123456789)) '[])
Compare_0123456789 (Vec a_0123456789 a_0123456789) (Vec b_0123456789 b_0123456789) = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) (Apply (Apply (:$) (Apply (Apply CompareSym0 a_0123456789) b_0123456789)) (Apply (Apply (:$) (Apply (Apply CompareSym0 a_0123456789) b_0123456789)) '[]))
Compare_0123456789 Nat Int = LTSym0
Compare_0123456789 Nat String = LTSym0
Compare_0123456789 Nat (Maybe _z_0123456789) = LTSym0
Compare_0123456789 Nat (Vec _z_0123456789 _z_0123456789) = LTSym0
Compare_0123456789 Int Nat = GTSym0
Compare_0123456789 Int String = LTSym0
Compare_0123456789 Int (Maybe _z_0123456789) = LTSym0
Compare_0123456789 Int (Vec _z_0123456789 _z_0123456789) = LTSym0
Compare_0123456789 String Nat = GTSym0
Compare_0123456789 String Int = GTSym0
Compare_0123456789 String (Maybe _z_0123456789) = LTSym0
Compare_0123456789 String (Vec _z_0123456789 _z_0123456789) = LTSym0
Compare_0123456789 (Maybe _z_0123456789) Nat = GTSym0
Compare_0123456789 (Maybe _z_0123456789) Int = GTSym0
Compare_0123456789 (Maybe _z_0123456789) String = GTSym0
Compare_0123456789 (Maybe _z_0123456789) (Vec _z_0123456789 _z_0123456789) = LTSym0
Compare_0123456789 (Vec _z_0123456789 _z_0123456789) Nat = GTSym0
Compare_0123456789 (Vec _z_0123456789 _z_0123456789) Int = GTSym0
Compare_0123456789 (Vec _z_0123456789 _z_0123456789) String = GTSym0
Compare_0123456789 (Vec _z_0123456789 _z_0123456789) (Maybe _z_0123456789) = GTSym0
type Compare_0123456789Sym2 (t :: Type) (t :: Type) =
Compare_0123456789 t t
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Compare_0123456789Sym1 where
Data.Singletons.SuppressUnusedWarnings.suppressUnusedWarnings _
= snd
(GHC.Tuple.(,) Compare_0123456789Sym1KindInference GHC.Tuple.())
data Compare_0123456789Sym1 (l :: Type) (l :: TyFun Type Ordering)
= forall arg. KindOf (Apply (Compare_0123456789Sym1 l) arg) ~ KindOf (Compare_0123456789Sym2 l arg) =>
Compare_0123456789Sym1KindInference
type instance Apply (Compare_0123456789Sym1 l) l = Compare_0123456789Sym2 l l
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Compare_0123456789Sym0 where
Data.Singletons.SuppressUnusedWarnings.suppressUnusedWarnings _
= snd
(GHC.Tuple.(,) Compare_0123456789Sym0KindInference GHC.Tuple.())
data Compare_0123456789Sym0 (l :: TyFun Type (TyFun Type Ordering
-> Type))
= forall arg. KindOf (Apply Compare_0123456789Sym0 arg) ~ KindOf (Compare_0123456789Sym1 arg) =>
Compare_0123456789Sym0KindInference
type instance Apply Compare_0123456789Sym0 l = Compare_0123456789Sym1 l
instance POrd (KProxy :: KProxy Type) where
type Compare (a :: Type) (a :: Type) = Apply (Apply Compare_0123456789Sym0 a) a
instance (SOrd (KProxy :: KProxy Type),
SOrd (KProxy :: KProxy Nat)) =>
SOrd (KProxy :: KProxy Type) where
sCompare ::
forall (t0 :: Type) (t1 :: Type).
Sing t0
-> Sing t1
-> Sing (Apply (Apply (CompareSym0 :: TyFun Type (TyFun Type Ordering
-> Type)
-> Type) t0 :: TyFun Type Ordering
-> Type) t1 :: Ordering)
sCompare SNat SNat
= let
lambda ::
(t0 ~ NatSym0, t1 ~ NatSym0) =>
Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
lambda
= applySing
(applySing
(applySing
(singFun3 (Data.Proxy.Proxy :: Data.Proxy.Proxy FoldlSym0) sFoldl)
(singFun2
(Data.Proxy.Proxy :: Data.Proxy.Proxy ThenCmpSym0) sThenCmp))
SEQ)
SNil
in lambda
sCompare SInt SInt
= let
lambda ::
(t0 ~ IntSym0, t1 ~ IntSym0) =>
Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
lambda
= applySing
(applySing
(applySing
(singFun3 (Data.Proxy.Proxy :: Data.Proxy.Proxy FoldlSym0) sFoldl)
(singFun2
(Data.Proxy.Proxy :: Data.Proxy.Proxy ThenCmpSym0) sThenCmp))
SEQ)
SNil
in lambda
sCompare SString SString
= let
lambda ::
(t0 ~ StringSym0, t1 ~ StringSym0) =>
Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
lambda
= applySing
(applySing
(applySing
(singFun3 (Data.Proxy.Proxy :: Data.Proxy.Proxy FoldlSym0) sFoldl)
(singFun2
(Data.Proxy.Proxy :: Data.Proxy.Proxy ThenCmpSym0) sThenCmp))
SEQ)
SNil
in lambda
sCompare (SMaybe sA_0123456789) (SMaybe sB_0123456789)
= let
lambda ::
forall a_0123456789 b_0123456789.
(t0 ~ Apply MaybeSym0 a_0123456789,
t1 ~ Apply MaybeSym0 b_0123456789) =>
Sing a_0123456789
-> Sing b_0123456789
-> Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
lambda a_0123456789 b_0123456789
= applySing
(applySing
(applySing
(singFun3 (Data.Proxy.Proxy :: Data.Proxy.Proxy FoldlSym0) sFoldl)
(singFun2
(Data.Proxy.Proxy :: Data.Proxy.Proxy ThenCmpSym0) sThenCmp))
SEQ)
(applySing
(applySing
(singFun2 (Data.Proxy.Proxy :: Data.Proxy.Proxy (:$)) SCons)
(applySing
(applySing
(singFun2
(Data.Proxy.Proxy :: Data.Proxy.Proxy CompareSym0) sCompare)
a_0123456789)
b_0123456789))
SNil)
in lambda sA_0123456789 sB_0123456789
sCompare
(SVec sA_0123456789 sA_0123456789)
(SVec sB_0123456789 sB_0123456789)
= let
lambda ::
forall a_0123456789 a_0123456789 b_0123456789 b_0123456789.
(t0 ~ Apply (Apply VecSym0 a_0123456789) a_0123456789,
t1 ~ Apply (Apply VecSym0 b_0123456789) b_0123456789) =>
Sing a_0123456789
-> Sing a_0123456789
-> Sing b_0123456789
-> Sing b_0123456789
-> Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
lambda a_0123456789 a_0123456789 b_0123456789 b_0123456789
= applySing
(applySing
(applySing
(singFun3 (Data.Proxy.Proxy :: Data.Proxy.Proxy FoldlSym0) sFoldl)
(singFun2
(Data.Proxy.Proxy :: Data.Proxy.Proxy ThenCmpSym0) sThenCmp))
SEQ)
(applySing
(applySing
(singFun2 (Data.Proxy.Proxy :: Data.Proxy.Proxy (:$)) SCons)
(applySing
(applySing
(singFun2
(Data.Proxy.Proxy :: Data.Proxy.Proxy CompareSym0) sCompare)
a_0123456789)
b_0123456789))
(applySing
(applySing
(singFun2 (Data.Proxy.Proxy :: Data.Proxy.Proxy (:$)) SCons)
(applySing
(applySing
(singFun2
(Data.Proxy.Proxy :: Data.Proxy.Proxy CompareSym0) sCompare)
a_0123456789)
b_0123456789))
SNil))
in lambda sA_0123456789 sA_0123456789 sB_0123456789 sB_0123456789
sCompare SNat SInt
= let
lambda ::
(t0 ~ NatSym0, t1 ~ IntSym0) =>
Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
lambda = SLT
in lambda
sCompare SNat SString
= let
lambda ::
(t0 ~ NatSym0, t1 ~ StringSym0) =>
Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
lambda = SLT
in lambda
sCompare SNat (SMaybe _s_z_0123456789)
= let
lambda ::
forall _z_0123456789.
(t0 ~ NatSym0, t1 ~ Apply MaybeSym0 _z_0123456789) =>
Sing _z_0123456789
-> Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
lambda _z_0123456789 = SLT
in lambda _s_z_0123456789
sCompare SNat (SVec _s_z_0123456789 _s_z_0123456789)
= let
lambda ::
forall _z_0123456789 _z_0123456789.
(t0 ~ NatSym0,
t1 ~ Apply (Apply VecSym0 _z_0123456789) _z_0123456789) =>
Sing _z_0123456789
-> Sing _z_0123456789
-> Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
lambda _z_0123456789 _z_0123456789 = SLT
in lambda _s_z_0123456789 _s_z_0123456789
sCompare SInt SNat
= let
lambda ::
(t0 ~ IntSym0, t1 ~ NatSym0) =>
Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
lambda = SGT
in lambda
sCompare SInt SString
= let
lambda ::
(t0 ~ IntSym0, t1 ~ StringSym0) =>
Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
lambda = SLT
in lambda
sCompare SInt (SMaybe _s_z_0123456789)
= let
lambda ::
forall _z_0123456789.
(t0 ~ IntSym0, t1 ~ Apply MaybeSym0 _z_0123456789) =>
Sing _z_0123456789
-> Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
lambda _z_0123456789 = SLT
in lambda _s_z_0123456789
sCompare SInt (SVec _s_z_0123456789 _s_z_0123456789)
= let
lambda ::
forall _z_0123456789 _z_0123456789.
(t0 ~ IntSym0,
t1 ~ Apply (Apply VecSym0 _z_0123456789) _z_0123456789) =>
Sing _z_0123456789
-> Sing _z_0123456789
-> Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
lambda _z_0123456789 _z_0123456789 = SLT
in lambda _s_z_0123456789 _s_z_0123456789
sCompare SString SNat
= let
lambda ::
(t0 ~ StringSym0, t1 ~ NatSym0) =>
Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
lambda = SGT
in lambda
sCompare SString SInt
= let
lambda ::
(t0 ~ StringSym0, t1 ~ IntSym0) =>
Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
lambda = SGT
in lambda
sCompare SString (SMaybe _s_z_0123456789)
= let
lambda ::
forall _z_0123456789.
(t0 ~ StringSym0, t1 ~ Apply MaybeSym0 _z_0123456789) =>
Sing _z_0123456789
-> Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
lambda _z_0123456789 = SLT
in lambda _s_z_0123456789
sCompare SString (SVec _s_z_0123456789 _s_z_0123456789)
= let
lambda ::
forall _z_0123456789 _z_0123456789.
(t0 ~ StringSym0,
t1 ~ Apply (Apply VecSym0 _z_0123456789) _z_0123456789) =>
Sing _z_0123456789
-> Sing _z_0123456789
-> Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
lambda _z_0123456789 _z_0123456789 = SLT
in lambda _s_z_0123456789 _s_z_0123456789
sCompare (SMaybe _s_z_0123456789) SNat
= let
lambda ::
forall _z_0123456789.
(t0 ~ Apply MaybeSym0 _z_0123456789, t1 ~ NatSym0) =>
Sing _z_0123456789
-> Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
lambda _z_0123456789 = SGT
in lambda _s_z_0123456789
sCompare (SMaybe _s_z_0123456789) SInt
= let
lambda ::
forall _z_0123456789.
(t0 ~ Apply MaybeSym0 _z_0123456789, t1 ~ IntSym0) =>
Sing _z_0123456789
-> Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
lambda _z_0123456789 = SGT
in lambda _s_z_0123456789
sCompare (SMaybe _s_z_0123456789) SString
= let
lambda ::
forall _z_0123456789.
(t0 ~ Apply MaybeSym0 _z_0123456789, t1 ~ StringSym0) =>
Sing _z_0123456789
-> Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
lambda _z_0123456789 = SGT
in lambda _s_z_0123456789
sCompare
(SMaybe _s_z_0123456789)
(SVec _s_z_0123456789 _s_z_0123456789)
= let
lambda ::
forall _z_0123456789 _z_0123456789 _z_0123456789.
(t0 ~ Apply MaybeSym0 _z_0123456789,
t1 ~ Apply (Apply VecSym0 _z_0123456789) _z_0123456789) =>
Sing _z_0123456789
-> Sing _z_0123456789
-> Sing _z_0123456789
-> Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
lambda _z_0123456789 _z_0123456789 _z_0123456789 = SLT
in lambda _s_z_0123456789 _s_z_0123456789 _s_z_0123456789
sCompare (SVec _s_z_0123456789 _s_z_0123456789) SNat
= let
lambda ::
forall _z_0123456789 _z_0123456789.
(t0 ~ Apply (Apply VecSym0 _z_0123456789) _z_0123456789,
t1 ~ NatSym0) =>
Sing _z_0123456789
-> Sing _z_0123456789
-> Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
lambda _z_0123456789 _z_0123456789 = SGT
in lambda _s_z_0123456789 _s_z_0123456789
sCompare (SVec _s_z_0123456789 _s_z_0123456789) SInt
= let
lambda ::
forall _z_0123456789 _z_0123456789.
(t0 ~ Apply (Apply VecSym0 _z_0123456789) _z_0123456789,
t1 ~ IntSym0) =>
Sing _z_0123456789
-> Sing _z_0123456789
-> Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
lambda _z_0123456789 _z_0123456789 = SGT
in lambda _s_z_0123456789 _s_z_0123456789
sCompare (SVec _s_z_0123456789 _s_z_0123456789) SString
= let
lambda ::
forall _z_0123456789 _z_0123456789.
(t0 ~ Apply (Apply VecSym0 _z_0123456789) _z_0123456789,
t1 ~ StringSym0) =>
Sing _z_0123456789
-> Sing _z_0123456789
-> Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
lambda _z_0123456789 _z_0123456789 = SGT
in lambda _s_z_0123456789 _s_z_0123456789
sCompare
(SVec _s_z_0123456789 _s_z_0123456789)
(SMaybe _s_z_0123456789)
= let
lambda ::
forall _z_0123456789 _z_0123456789 _z_0123456789.
(t0 ~ Apply (Apply VecSym0 _z_0123456789) _z_0123456789,
t1 ~ Apply MaybeSym0 _z_0123456789) =>
Sing _z_0123456789
-> Sing _z_0123456789
-> Sing _z_0123456789
-> Sing (Apply (Apply CompareSym0 t0) t1 :: Ordering)
lambda _z_0123456789 _z_0123456789 _z_0123456789 = SGT
in lambda _s_z_0123456789 _s_z_0123456789 _s_z_0123456789
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 (KProxy :: KProxy Type) where
type DemoteRep (KProxy :: KProxy 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 (KProxy :: KProxy Type) of {
SomeSing c -> SomeSing (SMaybe c) }
toSing (Singletons.Star.Vec b b)
= case
GHC.Tuple.(,)
(toSing b :: SomeSing (KProxy :: KProxy Type))
(toSing b :: SomeSing (KProxy :: KProxy Nat))
of {
GHC.Tuple.(,) (SomeSing c) (SomeSing c) -> SomeSing (SVec c c) }
instance SEq (KProxy :: KProxy 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 (KProxy :: KProxy 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