Maybe.golden

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 :: forall a. Maybe a
    type family NothingSym0 @a :: Maybe a where
      NothingSym0 = Nothing
    type JustSym0 :: forall a. (~>) a (Maybe a)
    data JustSym0 :: (~>) a (Maybe a)
      where
        JustSym0KindInference :: SameKind (Apply JustSym0 arg) (JustSym1 arg) =>
                                 JustSym0 a0123456789876543210
    type instance Apply @a @(Maybe a) JustSym0 a0123456789876543210 = Just a0123456789876543210
    instance SuppressUnusedWarnings JustSym0 where
      suppressUnusedWarnings = snd ((,) JustSym0KindInference ())
    type JustSym1 :: forall a. a -> Maybe a
    type family JustSym1 @a (a0123456789876543210 :: a) :: Maybe a where
      JustSym1 a0123456789876543210 = Just a0123456789876543210
    type TFHelper_0123456789876543210 :: forall a. Maybe a
                                                   -> Maybe a -> Bool
    type family TFHelper_0123456789876543210 @a (a :: Maybe a) (a :: Maybe a) :: Bool where
      TFHelper_0123456789876543210 @a (Nothing :: Maybe a) (Nothing :: Maybe a) = TrueSym0
      TFHelper_0123456789876543210 @a (Nothing :: Maybe a) (Just _ :: Maybe a) = FalseSym0
      TFHelper_0123456789876543210 @a (Just _ :: Maybe a) (Nothing :: Maybe a) = FalseSym0
      TFHelper_0123456789876543210 @a (Just a_0123456789876543210 :: Maybe a) (Just b_0123456789876543210 :: Maybe a) = Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210
    instance PEq (Maybe a) where
      type (==) a a = TFHelper_0123456789876543210 a a
    type ShowsPrec_0123456789876543210 :: forall a. GHC.Num.Natural.Natural
                                                    -> Maybe a
                                                       -> GHC.Types.Symbol -> GHC.Types.Symbol
    type family ShowsPrec_0123456789876543210 @a (a :: GHC.Num.Natural.Natural) (a :: Maybe a) (a :: GHC.Types.Symbol) :: GHC.Types.Symbol where
      ShowsPrec_0123456789876543210 @a (_ :: GHC.Num.Natural.Natural) (Nothing :: Maybe a) (a_0123456789876543210 :: GHC.Types.Symbol) = Apply (Apply ShowStringSym0 "Nothing") a_0123456789876543210
      ShowsPrec_0123456789876543210 @a (p_0123456789876543210 :: GHC.Num.Natural.Natural) (Just arg_0123456789876543210 :: Maybe a) (a_0123456789876543210 :: GHC.Types.Symbol) = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "Just ")) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210))) a_0123456789876543210
    instance PShow (Maybe a) where
      type ShowsPrec a a a = ShowsPrec_0123456789876543210 a a a
    data SMaybe :: forall a. Maybe a -> Type
      where
        SNothing :: forall a. SMaybe (Nothing :: Maybe a)
        SJust :: forall a (n :: a). (Sing n) -> SMaybe (Just n :: Maybe a)
    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))
        = (\cases (SomeSing c) -> SomeSing (SJust c))
            (toSing b :: SomeSing a)
    instance SEq a => SEq (Maybe a) where
      (%==) SNothing SNothing = STrue
      (%==) SNothing (SJust _) = SFalse
      (%==) (SJust _) SNothing = SFalse
      (%==)
        (SJust (sA_0123456789876543210 :: Sing a_0123456789876543210))
        (SJust (sB_0123456789876543210 :: Sing b_0123456789876543210))
        = applySing
            (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210)
            sB_0123456789876543210
    instance SShow a => SShow (Maybe a) where
      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)
                     (sFromInteger (sing :: Sing 10))))
               (applySing
                  (applySing
                     (singFun3 @(.@#@$) (%.))
                     (applySing
                        (singFun2 @ShowStringSym0 sShowString) (sing :: Sing "Just ")))
                  (applySing
                     (applySing
                        (singFun3 @ShowsPrecSym0 sShowsPrec)
                        (sFromInteger (sing :: Sing 11)))
                     sArg_0123456789876543210)))
            sA_0123456789876543210
    instance SDecide a => SDecide (Maybe a) where
      (%~) SNothing SNothing = Proved Refl
      (%~) SNothing (SJust _) = Disproved (\case)
      (%~) (SJust _) SNothing = Disproved (\case)
      (%~) (SJust a) (SJust b)
        = (\cases
             (Proved Refl) -> Proved Refl
             (Disproved contra) -> Disproved (\cases Refl -> contra Refl))
            ((%~) a b)
    instance Eq (SMaybe (z :: Maybe a)) where
      (==) _ _ = True
    instance SDecide a =>
             GHC.Internal.Data.Type.Equality.TestEquality (SMaybe :: Maybe a
                                                                     -> Type) where
      GHC.Internal.Data.Type.Equality.testEquality
        = Data.Singletons.Decide.decideEquality
    instance SDecide a =>
             GHC.Internal.Data.Type.Coercion.TestCoercion (SMaybe :: Maybe a
                                                                     -> Type) where
      GHC.Internal.Data.Type.Coercion.testCoercion
        = Data.Singletons.Decide.decideCoercion
    deriving instance Data.Singletons.ShowSing.ShowSing a =>
                      Show (SMaybe (z :: Maybe a))
    instance SingI Nothing where
      sing = SNothing
    instance SingI n => SingI (Just (n :: a)) where
      sing = SJust sing
    instance SingI1 Just where
      liftSing = SJust
    instance SingI (JustSym0 :: (~>) a (Maybe a)) where
      sing = singFun1 @JustSym0 SJust