Maybe.ghc82.template

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 family Equals_0123456789876543210 (a :: Maybe k) (b :: Maybe k) :: Bool where
      Equals_0123456789876543210 Nothing Nothing = TrueSym0
      Equals_0123456789876543210 (Just a) (Just b) = (:==) a b
      Equals_0123456789876543210 (a :: Maybe k) (b :: Maybe k) = FalseSym0
    instance PEq (Maybe k) where
      type (:==) (a :: Maybe k) (b :: Maybe k) = Equals_0123456789876543210 a b
    type NothingSym0 = Nothing
    type JustSym1 (t :: a0123456789876543210) = Just t
    instance SuppressUnusedWarnings JustSym0 where
      suppressUnusedWarnings _
        = snd ((GHC.Tuple.(,) JustSym0KindInference) GHC.Tuple.())
    data JustSym0 (l :: TyFun a0123456789876543210 (Maybe a0123456789876543210))
      = forall arg. SameKind (Apply JustSym0 arg) (JustSym1 arg) =>
        JustSym0KindInference
    type instance Apply JustSym0 l = Just l
    data instance Sing (z :: Maybe a)
      = z ~ Nothing => SNothing |
        forall (n :: a). z ~ Just n => SJust (Sing (n :: a))
    type SMaybe = (Sing :: Maybe a -> GHC.Types.Type)
    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)
        = case toSing b :: SomeSing a of {
            SomeSing c -> SomeSing (SJust c) }
    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 {
                    _ -> 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