T178.golden

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 USym0 = U
    type StrSym0 = Str :: Occ
    type OptSym0 = Opt :: Occ
    type ManySym0 = Many :: Occ
    type EmptySym0 = Empty :: [(Symbol, Occ)]
    type Empty :: [(Symbol, Occ)]
    type family Empty where
      Empty = NilSym0
    type Compare_0123456789876543210 :: Occ -> Occ -> Ordering
    type family Compare_0123456789876543210 a a where
      Compare_0123456789876543210 Str Str = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) NilSym0
      Compare_0123456789876543210 Opt Opt = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) EQSym0) NilSym0
      Compare_0123456789876543210 Many Many = Apply (Apply (Apply FoldlSym0 ThenCmpSym0) 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 a0123456789876543210
      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 a0123456789876543210
      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_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (Compare_0123456789876543210Sym1 a0123456789876543210) where
      suppressUnusedWarnings
        = snd (((,) Compare_0123456789876543210Sym1KindInference) ())
    type Compare_0123456789876543210Sym2 (a0123456789876543210 :: Occ) (a0123456789876543210 :: Occ) =
        Compare_0123456789876543210 a0123456789876543210 a0123456789876543210 :: Ordering
    instance POrd Occ where
      type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a
    type ShowsPrec_0123456789876543210 :: Nat
                                          -> Occ -> Symbol -> Symbol
    type family ShowsPrec_0123456789876543210 a a a 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 :: (~>) Nat ((~>) Occ ((~>) Symbol Symbol))
    data ShowsPrec_0123456789876543210Sym0 a0123456789876543210
      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 :: Nat
                                              -> (~>) Occ ((~>) Symbol Symbol)
    data ShowsPrec_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
      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 :: Nat
                                              -> Occ -> (~>) Symbol Symbol
    data ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 a0123456789876543210
      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_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) where
      suppressUnusedWarnings
        = snd (((,) ShowsPrec_0123456789876543210Sym2KindInference) ())
    type ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Occ) (a0123456789876543210 :: Symbol) =
        ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 :: Symbol
    instance PShow Occ where
      type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
    type Equals_0123456789876543210 :: Occ -> Occ -> Bool
    type family Equals_0123456789876543210 a b 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 SOcc :: Occ -> GHC.Types.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 SOrd Occ where
      sCompare ::
        forall (t1 :: Occ) (t2 :: Occ).
        Sing t1
        -> Sing t2
           -> Sing (Apply (Apply (CompareSym0 :: TyFun Occ ((~>) Occ Ordering)
                                                 -> 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 ((~>) Occ ((~>) Symbol Symbol))
                                                             -> 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.Type.Equality.TestEquality (SOcc :: Occ
                                                      -> GHC.Types.Type) where
      Data.Type.Equality.testEquality
        = Data.Singletons.Decide.decideEquality
    instance Data.Type.Coercion.TestCoercion (SOcc :: Occ
                                                      -> GHC.Types.Type) where
      Data.Type.Coercion.testCoercion
        = Data.Singletons.Decide.decideCoercion
    instance Show (SOcc (z :: Occ)) where
      showsPrec _ SStr = showString "SStr"
      showsPrec _ SOpt = showString "SOpt"
      showsPrec _ SMany = showString "SMany"
    instance SingI Str where
      sing = SStr
    instance SingI Opt where
      sing = SOpt
    instance SingI Many where
      sing = SMany