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 = TrueSym0
    type instance (:==) Nat Int = FalseSym0
    type instance (:==) Nat String = FalseSym0
    type instance (:==) Nat (Maybe b) = FalseSym0
    type instance (:==) Nat (Vec b b) = FalseSym0
    type instance (:==) Int Nat = FalseSym0
    type instance (:==) Int Int = TrueSym0
    type instance (:==) Int String = FalseSym0
    type instance (:==) Int (Maybe b) = FalseSym0
    type instance (:==) Int (Vec b b) = FalseSym0
    type instance (:==) String Nat = FalseSym0
    type instance (:==) String Int = FalseSym0
    type instance (:==) String String = TrueSym0
    type instance (:==) String (Maybe b) = FalseSym0
    type instance (:==) String (Vec b b) = FalseSym0
    type instance (:==) (Maybe a) Nat = FalseSym0
    type instance (:==) (Maybe a) Int = FalseSym0
    type instance (:==) (Maybe a) String = FalseSym0
    type instance (:==) (Maybe a) (Maybe b) = :== a b
    type instance (:==) (Maybe a) (Vec b b) = FalseSym0
    type instance (:==) (Vec a a) Nat = FalseSym0
    type instance (:==) (Vec a a) Int = FalseSym0
    type instance (:==) (Vec a a) String = FalseSym0
    type instance (:==) (Vec a a) (Maybe b) = FalseSym0
    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