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 :: *) (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
    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
    type family Compare_0123456789 (a :: *) (a :: *) :: 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 :: *) (t :: *) =
        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 :: *) (l :: TyFun * 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 * (TyFun * Ordering -> *))
      = 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 *) where
      type Compare (a :: *) (a :: *) = Apply (Apply Compare_0123456789Sym0 a) a
    instance (SOrd (KProxy :: KProxy *),
              SOrd (KProxy :: KProxy Nat)) =>
             SOrd (KProxy :: KProxy *) where
      sCompare ::
        forall (t0 :: *) (t1 :: *).
        Sing t0
        -> Sing t1
           -> Sing (Apply (Apply (CompareSym0 :: TyFun * (TyFun * Ordering
                                                          -> *)
                                                 -> *) t0 :: TyFun * Ordering -> *) t1 :: Ordering)
      sCompare SNat SNat
        = let
            lambda ::
              (t0 ~ NatSym0, t1 ~ NatSym0) =>
              Sing (Apply (Apply CompareSym0 NatSym0) NatSym0 :: 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 IntSym0) IntSym0 :: 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 StringSym0) StringSym0 :: 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 (Apply MaybeSym0 a_0123456789)) (Apply MaybeSym0 b_0123456789) :: 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 (Apply (Apply VecSym0 a_0123456789) a_0123456789)) (Apply (Apply VecSym0 b_0123456789) b_0123456789) :: 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 NatSym0) IntSym0 :: Ordering)
            lambda = SLT
          in lambda
      sCompare SNat SString
        = let
            lambda ::
              (t0 ~ NatSym0, t1 ~ StringSym0) =>
              Sing (Apply (Apply CompareSym0 NatSym0) StringSym0 :: 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 NatSym0) (Apply MaybeSym0 _z_0123456789) :: 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 NatSym0) (Apply (Apply VecSym0 _z_0123456789) _z_0123456789) :: 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 IntSym0) NatSym0 :: Ordering)
            lambda = SGT
          in lambda
      sCompare SInt SString
        = let
            lambda ::
              (t0 ~ IntSym0, t1 ~ StringSym0) =>
              Sing (Apply (Apply CompareSym0 IntSym0) StringSym0 :: 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 IntSym0) (Apply MaybeSym0 _z_0123456789) :: 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 IntSym0) (Apply (Apply VecSym0 _z_0123456789) _z_0123456789) :: 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 StringSym0) NatSym0 :: Ordering)
            lambda = SGT
          in lambda
      sCompare SString SInt
        = let
            lambda ::
              (t0 ~ StringSym0, t1 ~ IntSym0) =>
              Sing (Apply (Apply CompareSym0 StringSym0) IntSym0 :: 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 StringSym0) (Apply MaybeSym0 _z_0123456789) :: 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 StringSym0) (Apply (Apply VecSym0 _z_0123456789) _z_0123456789) :: 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 (Apply MaybeSym0 _z_0123456789)) NatSym0 :: 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 (Apply MaybeSym0 _z_0123456789)) IntSym0 :: 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 (Apply MaybeSym0 _z_0123456789)) StringSym0 :: 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 (Apply MaybeSym0 _z_0123456789)) (Apply (Apply VecSym0 _z_0123456789) _z_0123456789) :: 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 (Apply (Apply VecSym0 _z_0123456789) _z_0123456789)) NatSym0 :: 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 (Apply (Apply VecSym0 _z_0123456789) _z_0123456789)) IntSym0 :: 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 (Apply (Apply VecSym0 _z_0123456789) _z_0123456789)) StringSym0 :: 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 (Apply (Apply VecSym0 _z_0123456789) _z_0123456789)) (Apply MaybeSym0 _z_0123456789) :: Ordering)
            lambda _z_0123456789 _z_0123456789 _z_0123456789 = SGT
          in lambda _s_z_0123456789 _s_z_0123456789 _s_z_0123456789
    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 :: Nat))
    type SRep = (Sing :: * -> *)
    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