T178.ghc82.template

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 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 (a :: Occ) (b :: Occ) = FalseSym0
    instance PEq Occ where
      type (:==) (a :: Occ) (b :: Occ) = Equals_0123456789876543210 a b
    type StrSym0 = Str
    type OptSym0 = Opt
    type ManySym0 = Many
    type EmptySym0 = Empty
    type family Empty :: [(Symbol, Occ)] where
      = '[]
    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 :: Occ) (a :: Occ) = Apply (Apply Compare_0123456789876543210Sym0 a) a
    sEmpty :: Sing (EmptySym0 :: [(Symbol, Occ)])
    sEmpty = SNil
    data instance Sing (z :: Occ)
      = z ~ Str => SStr | z ~ Opt => SOpt | z ~ Many => SMany
    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 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 {
                    _ -> error "Empty case reached -- this should be impossible" })
      (%~) SStr SMany
        = Disproved
            (\ x
               -> case x of {
                    _ -> error "Empty case reached -- this should be impossible" })
      (%~) SOpt SStr
        = Disproved
            (\ x
               -> case x of {
                    _ -> error "Empty case reached -- this should be impossible" })
      (%~) SOpt SOpt = Proved Refl
      (%~) SOpt SMany
        = Disproved
            (\ x
               -> case x of {
                    _ -> error "Empty case reached -- this should be impossible" })
      (%~) SMany SStr
        = Disproved
            (\ x
               -> case x of {
                    _ -> error "Empty case reached -- this should be impossible" })
      (%~) SMany SOpt
        = Disproved
            (\ x
               -> case x of {
                    _ -> error "Empty case reached -- this should be impossible" })
      (%~) SMany SMany = Proved Refl
    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 :: TyFun Occ Ordering
                                                                          -> GHC.Types.Type) t2 :: Ordering)
      sCompare SStr SStr
        = (applySing
             ((applySing
                 ((applySing ((singFun3 @FoldlSym0) sFoldl))
                    ((singFun2 @ThenCmpSym0) sThenCmp)))
                SEQ))
            SNil
      sCompare SOpt SOpt
        = (applySing
             ((applySing
                 ((applySing ((singFun3 @FoldlSym0) sFoldl))
                    ((singFun2 @ThenCmpSym0) sThenCmp)))
                SEQ))
            SNil
      sCompare SMany SMany
        = (applySing
             ((applySing
                 ((applySing ((singFun3 @FoldlSym0) sFoldl))
                    ((singFun2 @ThenCmpSym0) sThenCmp)))
                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 SingI Str where
      sing = SStr
    instance SingI Opt where
      sing = SOpt
    instance SingI Many where
      sing = SMany