Singletons/Maybe.hs:0:0: Splicing declarations
    singletons
      [d| data Maybe a
            = Nothing | Just a
            deriving (Eq, Show) |]
  ======>
    Singletons/Maybe.hs:(0,0)-(0,0)
    data Maybe a
      = Nothing | Just a
      deriving (Eq, Show)
    type family Equals_0123456789 (a :: Maybe k)
                                  (b :: Maybe k) :: Bool where
      Equals_0123456789 Nothing Nothing = TrueSym0
      Equals_0123456789 (Just a) (Just b) = (:==) a b
      Equals_0123456789 (a :: Maybe k) (b :: Maybe k) = FalseSym0
    instance PEq (KProxy :: KProxy (Maybe k)) where
      type (:==) (a :: Maybe k) (b :: Maybe k) = Equals_0123456789 a b
    type NothingSym0 = Nothing
    type JustSym1 (t :: a) = Just t
    instance SuppressUnusedWarnings JustSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) JustSym0KindInference GHC.Tuple.())
    data JustSym0 (l :: TyFun a (Maybe a))
      = forall arg. KindOf (Apply JustSym0 arg) ~ KindOf (JustSym1 arg) =>
        JustSym0KindInference
    type instance Apply JustSym0 l = JustSym1 l
    data instance Sing (z :: Maybe a)
      = z ~ Nothing => SNothing |
        forall (n :: a). z ~ Just n => SJust (Sing n)
    type SMaybe (z :: Maybe a) = Sing z
    instance SingKind (KProxy :: KProxy a) =>
             SingKind (KProxy :: KProxy (Maybe a)) where
      type DemoteRep (KProxy :: KProxy (Maybe a)) = Maybe (DemoteRep (KProxy :: KProxy a))
      fromSing SNothing = Nothing
      fromSing (SJust b) = Just (fromSing b)
      toSing Nothing = SomeSing SNothing
      toSing (Just b)
        = case toSing b :: SomeSing (KProxy :: KProxy a) of {
            SomeSing c -> SomeSing (SJust c) }
    instance SEq (KProxy :: KProxy a) =>
             SEq (KProxy :: KProxy (Maybe a)) where
      (%:==) SNothing SNothing = STrue
      (%:==) SNothing (SJust _) = SFalse
      (%:==) (SJust _) SNothing = SFalse
      (%:==) (SJust a) (SJust b) = (%:==) a b
    instance SDecide (KProxy :: KProxy a) =>
             SDecide (KProxy :: KProxy (Maybe a)) where
      (%~) SNothing SNothing = Proved Refl
      (%~) SNothing (SJust _)
        = Disproved
            (\ x
               -> case x of {
                    _ -> error "Empty case reached -- this should be impossible" })
      (%~) (SJust _) SNothing
        = Disproved
            (\ x
               -> case x of {
                    _ -> error "Empty case reached -- this should be impossible" })
      (%~) (SJust a) (SJust b)
        = case (%~) a b of {
            Proved Refl -> Proved Refl
            Disproved contra
              -> Disproved (\ refl -> case refl of { Refl -> contra Refl }) }
    instance SingI Nothing where
      sing = SNothing
    instance SingI n => SingI (Just (n :: a)) where
      sing = SJust sing