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 StrSym0 = Str
    type OptSym0 = Opt
    type ManySym0 = Many
    type EmptySym0 = Empty
    type family Empty :: [(Symbol, Occ)] where
      Empty = '[]
    type family Compare_0123456789876543210 (a :: Occ) (a :: Occ) :: Ordering where
      Compare_0123456789876543210 Str Str = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) '[]
      Compare_0123456789876543210 Opt Opt = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) '[]
      Compare_0123456789876543210 Many Many = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) '[]
      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_0123456789876543210Sym2 (t :: Occ) (t :: Occ) =
        Compare_0123456789876543210 t t
    instance SuppressUnusedWarnings Compare_0123456789876543210Sym1 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,) Compare_0123456789876543210Sym1KindInference)
               GHC.Tuple.())
    data Compare_0123456789876543210Sym1 (l :: Occ) (l :: TyFun Occ 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 SuppressUnusedWarnings Compare_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,) Compare_0123456789876543210Sym0KindInference)
               GHC.Tuple.())
    data Compare_0123456789876543210Sym0 (l :: TyFun Occ (TyFun Occ Ordering
                                                          -> GHC.Types.Type))
      = forall arg. SameKind (Apply Compare_0123456789876543210Sym0 arg) (Compare_0123456789876543210Sym1 arg) =>
        Compare_0123456789876543210Sym0KindInference
    type instance Apply Compare_0123456789876543210Sym0 l = Compare_0123456789876543210Sym1 l
    instance POrd Occ where
      type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a
    type family ShowsPrec_0123456789876543210 (a :: Nat) (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_0123456789876543210Sym3 (t :: Nat) (t :: Occ) (t :: Symbol) =
        ShowsPrec_0123456789876543210 t t t
    instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym2 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,) ShowsPrec_0123456789876543210Sym2KindInference)
               GHC.Tuple.())
    data ShowsPrec_0123456789876543210Sym2 (l :: Nat) (l :: Occ) (l :: TyFun Symbol Symbol)
      = forall arg. SameKind (Apply (ShowsPrec_0123456789876543210Sym2 l l) arg) (ShowsPrec_0123456789876543210Sym3 l l arg) =>
        ShowsPrec_0123456789876543210Sym2KindInference
    type instance Apply (ShowsPrec_0123456789876543210Sym2 l l) l = ShowsPrec_0123456789876543210 l l l
    instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym1 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,) ShowsPrec_0123456789876543210Sym1KindInference)
               GHC.Tuple.())
    data ShowsPrec_0123456789876543210Sym1 (l :: Nat) (l :: TyFun Occ (TyFun Symbol Symbol
                                                                       -> GHC.Types.Type))
      = forall arg. SameKind (Apply (ShowsPrec_0123456789876543210Sym1 l) arg) (ShowsPrec_0123456789876543210Sym2 l arg) =>
        ShowsPrec_0123456789876543210Sym1KindInference
    type instance Apply (ShowsPrec_0123456789876543210Sym1 l) l = ShowsPrec_0123456789876543210Sym2 l l
    instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,) ShowsPrec_0123456789876543210Sym0KindInference)
               GHC.Tuple.())
    data ShowsPrec_0123456789876543210Sym0 (l :: TyFun Nat (TyFun Occ (TyFun Symbol Symbol
                                                                       -> GHC.Types.Type)
                                                            -> GHC.Types.Type))
      = forall arg. SameKind (Apply ShowsPrec_0123456789876543210Sym0 arg) (ShowsPrec_0123456789876543210Sym1 arg) =>
        ShowsPrec_0123456789876543210Sym0KindInference
    type instance Apply ShowsPrec_0123456789876543210Sym0 l = ShowsPrec_0123456789876543210Sym1 l
    instance PShow Occ where
      type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
    type family Equals_0123456789876543210 (a :: Occ) (b :: Occ) :: Bool where
      Equals_0123456789876543210 Str Str = TrueSym0
      Equals_0123456789876543210 Opt Opt = TrueSym0
      Equals_0123456789876543210 Many Many = TrueSym0
      Equals_0123456789876543210 (_ :: Occ) (_ :: Occ) = FalseSym0
    instance PEq Occ where
      type (==) a b = Equals_0123456789876543210 a b
    sEmpty :: Sing (EmptySym0 :: [(Symbol, Occ)])
    sEmpty = Data.Singletons.Prelude.Instances.SNil
    data instance Sing (z :: Occ)
      where
        SStr :: Sing Str
        SOpt :: Sing Opt
        SMany :: Sing Many
    type SOcc = (Sing :: Occ -> GHC.Types.Type)
    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 SOrd Occ where
      sCompare ::
        forall (t1 :: Occ) (t2 :: Occ).
        Sing t1
        -> Sing t2
           -> Sing (Apply (Apply (CompareSym0 :: TyFun Occ (TyFun Occ Ordering
                                                            -> GHC.Types.Type)
                                                 -> GHC.Types.Type) t1) t2)
      sCompare SStr SStr
        = (applySing
             ((applySing
                 ((applySing ((singFun3 @FoldlSym0) sFoldl))
                    ((singFun2 @ThenCmpSym0) sThenCmp)))
                SEQ))
            Data.Singletons.Prelude.Instances.SNil
      sCompare SOpt SOpt
        = (applySing
             ((applySing
                 ((applySing ((singFun3 @FoldlSym0) sFoldl))
                    ((singFun2 @ThenCmpSym0) sThenCmp)))
                SEQ))
            Data.Singletons.Prelude.Instances.SNil
      sCompare SMany SMany
        = (applySing
             ((applySing
                 ((applySing ((singFun3 @FoldlSym0) sFoldl))
                    ((singFun2 @ThenCmpSym0) sThenCmp)))
                SEQ))
            Data.Singletons.Prelude.Instances.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 :: Nat) (t2 :: Occ) (t3 :: Symbol).
        Sing t1
        -> Sing t2
           -> Sing t3
              -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun Nat (TyFun Occ (TyFun Symbol Symbol
                                                                                   -> GHC.Types.Type)
                                                                        -> GHC.Types.Type)
                                                             -> GHC.Types.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 SEq Occ where
      (%==) 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 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.Singletons.ShowSing.ShowSing Occ where
      Data.Singletons.ShowSing.showsSingPrec _ SStr = showString "SStr"
      Data.Singletons.ShowSing.showsSingPrec _ SOpt = showString "SOpt"
      Data.Singletons.ShowSing.showsSingPrec _ SMany = showString "SMany"
    instance Show (Sing (z :: Occ)) where
      showsPrec = Data.Singletons.ShowSing.showsSingPrec
    instance SingI Str where
      sing = SStr
    instance SingI Opt where
      sing = SOpt
    instance SingI Many where
      sing = SMany