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