Singletons/Maybe.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| data Maybe a
            = Nothing | Just a
            deriving (Eq, Show) |]
  ======>
    data Maybe a
      = Nothing | Just a
      deriving (Eq, Show)
    type NothingSym0 = Nothing
    type JustSym1 (t0123456789876543210 :: a0123456789876543210) =
        Just t0123456789876543210
    instance SuppressUnusedWarnings JustSym0 where
      suppressUnusedWarnings = snd (((,) JustSym0KindInference) ())
    data JustSym0 :: forall a0123456789876543210.
                     (~>) a0123456789876543210 (Maybe a0123456789876543210)
      where
        JustSym0KindInference :: forall t0123456789876543210
                                        arg. SameKind (Apply JustSym0 arg) (JustSym1 arg) =>
                                 JustSym0 t0123456789876543210
    type instance Apply JustSym0 t0123456789876543210 = Just t0123456789876543210
    type family ShowsPrec_0123456789876543210 (a :: GHC.Types.Nat) (a :: Maybe a) (a :: GHC.Types.Symbol) :: GHC.Types.Symbol where
      ShowsPrec_0123456789876543210 _ Nothing a_0123456789876543210 = Apply (Apply ShowStringSym0 "Nothing") a_0123456789876543210
      ShowsPrec_0123456789876543210 p_0123456789876543210 (Just arg_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (Data.Singletons.Prelude.Num.FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "Just ")) (Apply (Apply ShowsPrecSym0 (Data.Singletons.Prelude.Num.FromInteger 11)) arg_0123456789876543210))) a_0123456789876543210
    type ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: Maybe a0123456789876543210) (a0123456789876543210 :: GHC.Types.Symbol) =
        ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) where
      suppressUnusedWarnings
        = snd (((,) ShowsPrec_0123456789876543210Sym2KindInference) ())
    data ShowsPrec_0123456789876543210Sym2 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: Maybe a0123456789876543210) :: (~>) GHC.Types.Symbol GHC.Types.Symbol
      where
        ShowsPrec_0123456789876543210Sym2KindInference :: forall a0123456789876543210
                                                                 a0123456789876543210
                                                                 a0123456789876543210
                                                                 arg. 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_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) where
      suppressUnusedWarnings
        = snd (((,) ShowsPrec_0123456789876543210Sym1KindInference) ())
    data ShowsPrec_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Types.Nat) :: forall a0123456789876543210.
                                                                                      (~>) (Maybe a0123456789876543210) ((~>) GHC.Types.Symbol GHC.Types.Symbol)
      where
        ShowsPrec_0123456789876543210Sym1KindInference :: forall a0123456789876543210
                                                                 a0123456789876543210
                                                                 arg. 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_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd (((,) ShowsPrec_0123456789876543210Sym0KindInference) ())
    data ShowsPrec_0123456789876543210Sym0 :: forall a0123456789876543210.
                                              (~>) GHC.Types.Nat ((~>) (Maybe a0123456789876543210) ((~>) GHC.Types.Symbol GHC.Types.Symbol))
      where
        ShowsPrec_0123456789876543210Sym0KindInference :: forall a0123456789876543210
                                                                 arg. SameKind (Apply ShowsPrec_0123456789876543210Sym0 arg) (ShowsPrec_0123456789876543210Sym1 arg) =>
                                                          ShowsPrec_0123456789876543210Sym0 a0123456789876543210
    type instance Apply ShowsPrec_0123456789876543210Sym0 a0123456789876543210 = ShowsPrec_0123456789876543210Sym1 a0123456789876543210
    instance PShow (Maybe a) where
      type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
    type family Equals_0123456789876543210 (a :: Maybe a) (b :: Maybe a) :: Bool where
      Equals_0123456789876543210 Nothing Nothing = TrueSym0
      Equals_0123456789876543210 (Just a) (Just b) = (==) a b
      Equals_0123456789876543210 (_ :: Maybe a) (_ :: Maybe a) = FalseSym0
    instance PEq (Maybe a) where
      type (==) a b = Equals_0123456789876543210 a b
    data SMaybe :: forall a. Maybe a -> GHC.Types.Type
      where
        SNothing :: SMaybe Nothing
        SJust :: forall a (n :: a). (Sing (n :: a)) -> SMaybe (Just n)
    type instance Sing @(Maybe a) = SMaybe
    instance SingKind a => SingKind (Maybe a) where
      type Demote (Maybe a) = Maybe (Demote a)
      fromSing SNothing = Nothing
      fromSing (SJust b) = Just (fromSing b)
      toSing Nothing = SomeSing SNothing
      toSing (Just (b :: Demote a))
        = case toSing b :: SomeSing a of {
            SomeSing c -> SomeSing (SJust c) }
    instance SShow a => SShow (Maybe a) where
      sShowsPrec ::
        forall (t1 :: GHC.Types.Nat)
               (t2 :: Maybe a)
               (t3 :: GHC.Types.Symbol).
        Sing t1
        -> Sing t2
           -> Sing t3
              -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Types.Nat ((~>) (Maybe a) ((~>) GHC.Types.Symbol GHC.Types.Symbol))
                                                             -> GHC.Types.Type) t1) t2) t3)
      sShowsPrec
        _
        SNothing
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing ((singFun2 @ShowStringSym0) sShowString))
                (sing :: Sing "Nothing")))
            sA_0123456789876543210
      sShowsPrec
        (sP_0123456789876543210 :: Sing p_0123456789876543210)
        (SJust (sArg_0123456789876543210 :: Sing arg_0123456789876543210))
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = (applySing
             ((applySing
                 ((applySing ((singFun3 @ShowParenSym0) sShowParen))
                    ((applySing
                        ((applySing ((singFun2 @(>@#@$)) (%>))) sP_0123456789876543210))
                       (Data.Singletons.Prelude.Num.sFromInteger (sing :: Sing 10)))))
                ((applySing
                    ((applySing ((singFun3 @(.@#@$)) (%.)))
                       ((applySing ((singFun2 @ShowStringSym0) sShowString))
                          (sing :: Sing "Just "))))
                   ((applySing
                       ((applySing ((singFun3 @ShowsPrecSym0) sShowsPrec))
                          (Data.Singletons.Prelude.Num.sFromInteger (sing :: Sing 11))))
                      sArg_0123456789876543210))))
            sA_0123456789876543210
    instance SEq a => SEq (Maybe a) where
      (%==) SNothing SNothing = STrue
      (%==) SNothing (SJust _) = SFalse
      (%==) (SJust _) SNothing = SFalse
      (%==) (SJust a) (SJust b) = ((%==) a) b
    instance SDecide a => SDecide (Maybe a) where
      (%~) SNothing SNothing = Proved Refl
      (%~) SNothing (SJust _) = Disproved (\ x -> case x of)
      (%~) (SJust _) SNothing = Disproved (\ x -> case x of)
      (%~) (SJust a) (SJust b)
        = case ((%~) a) b of
            Proved Refl -> Proved Refl
            Disproved contra
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl })
    instance SDecide a =>
             Data.Type.Equality.TestEquality (SMaybe :: Maybe a
                                                        -> GHC.Types.Type) where
      Data.Type.Equality.testEquality
        = Data.Singletons.Decide.decideEquality
    instance SDecide a =>
             Data.Type.Coercion.TestCoercion (SMaybe :: Maybe a
                                                        -> GHC.Types.Type) where
      Data.Type.Coercion.testCoercion
        = Data.Singletons.Decide.decideCoercion
    instance Data.Singletons.ShowSing.ShowSing a =>
             Show (SMaybe (z :: Maybe a)) where
      showsPrec _ SNothing = showString "SNothing"
      showsPrec
        p_0123456789876543210
        (SJust (arg_0123456789876543210 :: Sing argTy_0123456789876543210))
        = (showParen (((>) p_0123456789876543210) 10))
            (((.) (showString "SJust "))
               ((showsPrec 11) arg_0123456789876543210)) ::
            Data.Singletons.ShowSing.ShowSing' argTy_0123456789876543210 =>
            ShowS
    instance SingI Nothing where
      sing = SNothing
    instance SingI n => SingI (Just (n :: a)) where
      sing = SJust sing
    instance SingI (JustSym0 :: (~>) a (Maybe a)) where
      sing = (singFun1 @JustSym0) SJust