module Singleraeh.Maybe where

-- | Singleton 'Maybe'.
data SMaybe sa (ma :: Maybe a) where
    SJust    :: sa a -> SMaybe sa (Just a)
    SNothing ::         SMaybe sa Nothing

demoteSMaybe
    :: forall da sa ma
    .  (forall a. sa a -> da)
    -> SMaybe sa ma
    -> Maybe da
demoteSMaybe :: forall {a} da (sa :: a -> Type) (ma :: Maybe a).
(forall (a :: a). sa a -> da) -> SMaybe sa ma -> Maybe da
demoteSMaybe forall (a :: a). sa a -> da
demoteSA = \case
  SJust sa a
sa -> da -> Maybe da
forall a. a -> Maybe a
Just (da -> Maybe da) -> da -> Maybe da
forall a b. (a -> b) -> a -> b
$ sa a -> da
forall (a :: a). sa a -> da
demoteSA sa a
sa
  SMaybe sa ma
SNothing -> Maybe da
forall a. Maybe a
Nothing