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