module Singleraeh.Maybe where

import Data.Kind ( Type )
import Singleraeh.Demote

-- | Singleton 'Maybe'.
type SMaybe :: (a -> Type) -> Maybe a -> Type
data SMaybe sa ma 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

instance Demotable sa => Demotable (SMaybe sa) where
    type Demote (SMaybe sa) = Maybe (Demote sa)
    demote :: forall (k1 :: Maybe a). SMaybe sa k1 -> Demote (SMaybe sa)
demote = (forall (a :: a). sa a -> Demote sa)
-> SMaybe sa k1 -> Maybe (Demote sa)
forall {a} da (sa :: a -> Type) (ma :: Maybe a).
(forall (a :: a). sa a -> da) -> SMaybe sa ma -> Maybe da
demoteSMaybe sa a -> Demote sa
forall (a :: a). sa a -> Demote sa
forall k (sk :: k -> Type) (k1 :: k).
Demotable sk =>
sk k1 -> Demote sk
demote