Singletons/T178.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| empty :: U
          empty = []
          
          data Occ
            = Str | Opt | Many
            deriving (Eq, Ord, Show)
          type U = [(Symbol, Occ)] |]
  ======>
    data Occ
      = Str | Opt | Many
      deriving (Eq, Ord, Show)
    type U = [(Symbol, Occ)]
    empty :: U
    empty = []
    type family USym0 where
      USym0 = U
    type StrSym0 :: Occ
    type family StrSym0 :: Occ where
      StrSym0 = Str
    type OptSym0 :: Occ
    type family OptSym0 :: Occ where
      OptSym0 = Opt
    type ManySym0 :: Occ
    type family ManySym0 :: Occ where
      ManySym0 = Many
    type EmptySym0 :: [(Symbol, Occ)]
    type family EmptySym0 :: [(Symbol, Occ)] where
      EmptySym0 = Empty
    type Empty :: [(Symbol, Occ)]
    type family Empty :: [(Symbol, Occ)] where
      Empty = NilSym0
    type TFHelper_0123456789876543210 :: Occ -> Occ -> Bool
    type family TFHelper_0123456789876543210 (a :: Occ) (a :: Occ) :: Bool where
      TFHelper_0123456789876543210 Str Str = TrueSym0
      TFHelper_0123456789876543210 Str Opt = FalseSym0
      TFHelper_0123456789876543210 Str Many = FalseSym0
      TFHelper_0123456789876543210 Opt Str = FalseSym0
      TFHelper_0123456789876543210 Opt Opt = TrueSym0
      TFHelper_0123456789876543210 Opt Many = FalseSym0
      TFHelper_0123456789876543210 Many Str = FalseSym0
      TFHelper_0123456789876543210 Many Opt = FalseSym0
      TFHelper_0123456789876543210 Many Many = TrueSym0
    type TFHelper_0123456789876543210Sym0 :: (~>) Occ ((~>) Occ Bool)
    data TFHelper_0123456789876543210Sym0 :: (~>) Occ ((~>) Occ Bool)
      where
        TFHelper_0123456789876543210Sym0KindInference :: SameKind (Apply TFHelper_0123456789876543210Sym0 arg) (TFHelper_0123456789876543210Sym1 arg) =>
                                                         TFHelper_0123456789876543210Sym0 a0123456789876543210
    type instance Apply TFHelper_0123456789876543210Sym0 a0123456789876543210 = TFHelper_0123456789876543210Sym1 a0123456789876543210
    instance SuppressUnusedWarnings TFHelper_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd ((,) TFHelper_0123456789876543210Sym0KindInference ())
    type TFHelper_0123456789876543210Sym1 :: Occ -> (~>) Occ Bool
    data TFHelper_0123456789876543210Sym1 (a0123456789876543210 :: Occ) :: (~>) Occ Bool
      where
        TFHelper_0123456789876543210Sym1KindInference :: SameKind (Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) arg) (TFHelper_0123456789876543210Sym2 a0123456789876543210 arg) =>
                                                         TFHelper_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
    type instance Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (TFHelper_0123456789876543210Sym1 a0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) TFHelper_0123456789876543210Sym1KindInference ())
    type TFHelper_0123456789876543210Sym2 :: Occ -> Occ -> Bool
    type family TFHelper_0123456789876543210Sym2 (a0123456789876543210 :: Occ) (a0123456789876543210 :: Occ) :: Bool where
      TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210
    instance PEq Occ where
      type (==) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a
    type Compare_0123456789876543210 :: Occ -> Occ -> Ordering
    type family Compare_0123456789876543210 (a :: Occ) (a :: Occ) :: Ordering where
      Compare_0123456789876543210 Str Str = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) NilSym0
      Compare_0123456789876543210 Opt Opt = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) NilSym0
      Compare_0123456789876543210 Many Many = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) NilSym0
      Compare_0123456789876543210 Str Opt = LTSym0
      Compare_0123456789876543210 Str Many = LTSym0
      Compare_0123456789876543210 Opt Str = GTSym0
      Compare_0123456789876543210 Opt Many = LTSym0
      Compare_0123456789876543210 Many Str = GTSym0
      Compare_0123456789876543210 Many Opt = GTSym0
    type Compare_0123456789876543210Sym0 :: (~>) Occ ((~>) Occ Ordering)
    data Compare_0123456789876543210Sym0 :: (~>) Occ ((~>) Occ Ordering)
      where
        Compare_0123456789876543210Sym0KindInference :: SameKind (Apply Compare_0123456789876543210Sym0 arg) (Compare_0123456789876543210Sym1 arg) =>
                                                        Compare_0123456789876543210Sym0 a0123456789876543210
    type instance Apply Compare_0123456789876543210Sym0 a0123456789876543210 = Compare_0123456789876543210Sym1 a0123456789876543210
    instance SuppressUnusedWarnings Compare_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd ((,) Compare_0123456789876543210Sym0KindInference ())
    type Compare_0123456789876543210Sym1 :: Occ -> (~>) Occ Ordering
    data Compare_0123456789876543210Sym1 (a0123456789876543210 :: Occ) :: (~>) Occ Ordering
      where
        Compare_0123456789876543210Sym1KindInference :: SameKind (Apply (Compare_0123456789876543210Sym1 a0123456789876543210) arg) (Compare_0123456789876543210Sym2 a0123456789876543210 arg) =>
                                                        Compare_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
    type instance Apply (Compare_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (Compare_0123456789876543210Sym1 a0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) Compare_0123456789876543210Sym1KindInference ())
    type Compare_0123456789876543210Sym2 :: Occ -> Occ -> Ordering
    type family Compare_0123456789876543210Sym2 (a0123456789876543210 :: Occ) (a0123456789876543210 :: Occ) :: Ordering where
      Compare_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210
    instance POrd Occ where
      type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a
    type ShowsPrec_0123456789876543210 :: Natural
                                          -> Occ -> Symbol -> Symbol
    type family ShowsPrec_0123456789876543210 (a :: Natural) (a :: Occ) (a :: Symbol) :: Symbol where
      ShowsPrec_0123456789876543210 _ Str a_0123456789876543210 = Apply (Apply ShowStringSym0 "Str") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ Opt a_0123456789876543210 = Apply (Apply ShowStringSym0 "Opt") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ Many a_0123456789876543210 = Apply (Apply ShowStringSym0 "Many") a_0123456789876543210
    type ShowsPrec_0123456789876543210Sym0 :: (~>) Natural ((~>) Occ ((~>) Symbol Symbol))
    data ShowsPrec_0123456789876543210Sym0 :: (~>) Natural ((~>) Occ ((~>) Symbol Symbol))
      where
        ShowsPrec_0123456789876543210Sym0KindInference :: SameKind (Apply ShowsPrec_0123456789876543210Sym0 arg) (ShowsPrec_0123456789876543210Sym1 arg) =>
                                                          ShowsPrec_0123456789876543210Sym0 a0123456789876543210
    type instance Apply ShowsPrec_0123456789876543210Sym0 a0123456789876543210 = ShowsPrec_0123456789876543210Sym1 a0123456789876543210
    instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd ((,) ShowsPrec_0123456789876543210Sym0KindInference ())
    type ShowsPrec_0123456789876543210Sym1 :: Natural
                                              -> (~>) Occ ((~>) Symbol Symbol)
    data ShowsPrec_0123456789876543210Sym1 (a0123456789876543210 :: Natural) :: (~>) Occ ((~>) Symbol Symbol)
      where
        ShowsPrec_0123456789876543210Sym1KindInference :: SameKind (Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 arg) =>
                                                          ShowsPrec_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
    type instance Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) ShowsPrec_0123456789876543210Sym1KindInference ())
    type ShowsPrec_0123456789876543210Sym2 :: Natural
                                              -> Occ -> (~>) Symbol Symbol
    data ShowsPrec_0123456789876543210Sym2 (a0123456789876543210 :: Natural) (a0123456789876543210 :: Occ) :: (~>) Symbol Symbol
      where
        ShowsPrec_0123456789876543210Sym2KindInference :: SameKind (Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 arg) =>
                                                          ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 a0123456789876543210
    type instance Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) ShowsPrec_0123456789876543210Sym2KindInference ())
    type ShowsPrec_0123456789876543210Sym3 :: Natural
                                              -> Occ -> Symbol -> Symbol
    type family ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: Natural) (a0123456789876543210 :: Occ) (a0123456789876543210 :: Symbol) :: Symbol where
      ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
    instance PShow Occ where
      type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
    sEmpty :: (Sing (EmptySym0 :: [(Symbol, Occ)]) :: Type)
    sEmpty = SNil
    data SOcc :: Occ -> Type
      where
        SStr :: SOcc (Str :: Occ)
        SOpt :: SOcc (Opt :: Occ)
        SMany :: SOcc (Many :: Occ)
    type instance Sing @Occ = SOcc
    instance SingKind Occ where
      type Demote Occ = Occ
      fromSing SStr = Str
      fromSing SOpt = Opt
      fromSing SMany = Many
      toSing Str = SomeSing SStr
      toSing Opt = SomeSing SOpt
      toSing Many = SomeSing SMany
    instance SEq Occ where
      (%==) ::
        forall (t1 :: Occ) (t2 :: Occ). Sing t1
                                        -> Sing t2
                                           -> Sing (Apply (Apply ((==@#@$) :: TyFun Occ ((~>) Occ Bool)
                                                                              -> Type) t1) t2)
      (%==) SStr SStr = STrue
      (%==) SStr SOpt = SFalse
      (%==) SStr SMany = SFalse
      (%==) SOpt SStr = SFalse
      (%==) SOpt SOpt = STrue
      (%==) SOpt SMany = SFalse
      (%==) SMany SStr = SFalse
      (%==) SMany SOpt = SFalse
      (%==) SMany SMany = STrue
    instance SOrd Occ where
      sCompare ::
        forall (t1 :: Occ) (t2 :: Occ). Sing t1
                                        -> Sing t2
                                           -> Sing (Apply (Apply (CompareSym0 :: TyFun Occ ((~>) Occ Ordering)
                                                                                 -> Type) t1) t2)
      sCompare SStr SStr
        = applySing
            (applySing
               (applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>)))
               SEQ)
            SNil
      sCompare SOpt SOpt
        = applySing
            (applySing
               (applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>)))
               SEQ)
            SNil
      sCompare SMany SMany
        = applySing
            (applySing
               (applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>)))
               SEQ)
            SNil
      sCompare SStr SOpt = SLT
      sCompare SStr SMany = SLT
      sCompare SOpt SStr = SGT
      sCompare SOpt SMany = SLT
      sCompare SMany SStr = SGT
      sCompare SMany SOpt = SGT
    instance SShow Occ where
      sShowsPrec ::
        forall (t1 :: Natural) (t2 :: Occ) (t3 :: Symbol). Sing t1
                                                           -> Sing t2
                                                              -> Sing t3
                                                                 -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun Natural ((~>) Occ ((~>) Symbol Symbol))
                                                                                                                -> Type) t1) t2) t3)
      sShowsPrec
        _
        SStr
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = applySing
            (applySing
               (singFun2 @ShowStringSym0 sShowString) (sing :: Sing "Str"))
            sA_0123456789876543210
      sShowsPrec
        _
        SOpt
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = applySing
            (applySing
               (singFun2 @ShowStringSym0 sShowString) (sing :: Sing "Opt"))
            sA_0123456789876543210
      sShowsPrec
        _
        SMany
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = applySing
            (applySing
               (singFun2 @ShowStringSym0 sShowString) (sing :: Sing "Many"))
            sA_0123456789876543210
    instance SDecide Occ where
      (%~) SStr SStr = Proved Refl
      (%~) SStr SOpt = Disproved (\ x -> case x of {})
      (%~) SStr SMany = Disproved (\ x -> case x of {})
      (%~) SOpt SStr = Disproved (\ x -> case x of {})
      (%~) SOpt SOpt = Proved Refl
      (%~) SOpt SMany = Disproved (\ x -> case x of {})
      (%~) SMany SStr = Disproved (\ x -> case x of {})
      (%~) SMany SOpt = Disproved (\ x -> case x of {})
      (%~) SMany SMany = Proved Refl
    instance Data.Type.Equality.TestEquality (SOcc :: Occ
                                                      -> Type) where
      Data.Type.Equality.testEquality
        = Data.Singletons.Decide.decideEquality
    instance Data.Type.Coercion.TestCoercion (SOcc :: Occ
                                                      -> Type) where
      Data.Type.Coercion.testCoercion
        = Data.Singletons.Decide.decideCoercion
    deriving instance Show (SOcc (z :: Occ))
    instance SingI Str where
      sing = SStr
    instance SingI Opt where
      sing = SOpt
    instance SingI Many where
      sing = SMany