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 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
    instance PEq Occ where
      type (==) a a = TFHelper_0123456789876543210 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
    instance POrd Occ where
      type Compare a a = Compare_0123456789876543210 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
    instance PShow Occ where
      type ShowsPrec a a a = ShowsPrec_0123456789876543210 a a a
    sEmpty :: (Sing (Empty :: [(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
      (%==) 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 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
        _
        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 (\case)
      (%~) SStr SMany = Disproved (\case)
      (%~) SOpt SStr = Disproved (\case)
      (%~) SOpt SOpt = Proved Refl
      (%~) SOpt SMany = Disproved (\case)
      (%~) SMany SStr = Disproved (\case)
      (%~) SMany SOpt = Disproved (\case)
      (%~) SMany SMany = Proved Refl
    instance Eq (SOcc (z :: Occ)) where
      (==) _ _ = True
    instance GHC.Internal.Data.Type.Equality.TestEquality (SOcc :: Occ
                                                                   -> Type) where
      GHC.Internal.Data.Type.Equality.testEquality
        = Data.Singletons.Decide.decideEquality
    instance GHC.Internal.Data.Type.Coercion.TestCoercion (SOcc :: Occ
                                                                   -> Type) where
      GHC.Internal.Data.Type.Coercion.testCoercion
        = Data.Singletons.Decide.decideCoercion
    instance Ord (SOcc (z :: Occ)) where
      compare _ _ = EQ
    deriving instance Show (SOcc (z :: Occ))
    instance SingI Str where
      sing = SStr
    instance SingI Opt where
      sing = SOpt
    instance SingI Many where
      sing = SMany