Maybe.ghc76.template

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 instance (:==) Nothing Nothing = True
    type instance (:==) Nothing (Just b) = False
    type instance (:==) (Just a) Nothing = False
    type instance (:==) (Just a) (Just b) = :== a b
    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 instance 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
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      %~ (SJust _) SNothing
        = Disproved
            (\case {
               _ -> error "Empty case reached -- this should be impossible" })
      %~ (SJust a) (SJust b)
        = case (%~) a b of {
            Proved Refl -> Proved Refl
            Disproved contra -> Disproved (\ Refl -> contra Refl) }
    instance SingI Nothing where
      sing = SNothing
    instance SingI n => SingI (Just (n :: a)) where
      sing = SJust sing