T163.ghc84.template

Singletons/T163.hs:0:0:: Splicing declarations
    singletons [d| data a + b = L a | R b |]
  ======>
    data (+) a b = L a | R b
    type LSym1 (t :: a0123456789876543210) = L t
    instance SuppressUnusedWarnings LSym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) LSym0KindInference) GHC.Tuple.())
    data LSym0 (l :: TyFun a0123456789876543210 ((+) a0123456789876543210 b0123456789876543210))
      = forall arg. SameKind (Apply LSym0 arg) (LSym1 arg) =>
        LSym0KindInference
    type instance Apply LSym0 l = L l
    type RSym1 (t :: b0123456789876543210) = R t
    instance SuppressUnusedWarnings RSym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) RSym0KindInference) GHC.Tuple.())
    data RSym0 (l :: TyFun b0123456789876543210 ((+) a0123456789876543210 b0123456789876543210))
      = forall arg. SameKind (Apply RSym0 arg) (RSym1 arg) =>
        RSym0KindInference
    type instance Apply RSym0 l = R l
    data instance Sing (z :: (+) a b)
      where
        SL :: forall (n :: a). (Sing (n :: a)) -> Sing (L n)
        SR :: forall (n :: b). (Sing (n :: b)) -> Sing (R n)
    type %+ = (Sing :: (+) a b -> GHC.Types.Type)
    instance (SingKind a, SingKind b) => SingKind ((+) a b) where
      type Demote ((+) a b) = (+) (Demote a) (Demote b)
      fromSing (SL b) = L (fromSing b)
      fromSing (SR b) = R (fromSing b)
      toSing (L (b :: Demote a))
        = case toSing b :: SomeSing a of { SomeSing c -> SomeSing (SL c) }
      toSing (R (b :: Demote b))
        = case toSing b :: SomeSing b of { SomeSing c -> SomeSing (SR c) }
    instance SingI n => SingI (L (n :: a)) where
      sing = SL sing
    instance SingI n => SingI (R (n :: b)) where
      sing = SR sing