module Singleraeh.Maybe where

import Data.Kind ( Type, Constraint )
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

class SingMaybe (ca :: ak -> Constraint) (sa :: ak -> Type) (ma :: Maybe ak) where
    singMaybe'
        :: (forall a. ca a => sa a)
        -> SMaybe sa ma

singMaybe
    :: forall ca sa ma. SingMaybe ca sa ma
    => (forall a. ca a => sa a)
    -> SMaybe sa ma
singMaybe :: forall {a} (ca :: a -> Constraint) (sa :: a -> Type)
       (ma :: Maybe a).
SingMaybe ca sa ma =>
(forall (a :: a). ca a => sa a) -> SMaybe sa ma
singMaybe = forall {a} (ca :: a -> Constraint) (sa :: a -> Type)
       (ma :: Maybe a).
SingMaybe ca sa ma =>
(forall (a :: a). ca a => sa a) -> SMaybe sa ma
singMaybe' @_ @ca

instance ca a => SingMaybe ca sa (Just a) where
    singMaybe' :: (forall (a :: a). ca a => sa a) -> SMaybe sa ('Just a)
singMaybe' forall (a :: a). ca a => sa a
sa = sa a -> SMaybe sa ('Just a)
forall {a} (sa :: a -> Type) (a :: a). sa a -> SMaybe sa ('Just a)
SJust sa a
forall (a :: a). ca a => sa a
sa

instance SingMaybe ca sa Nothing where
    singMaybe' :: (forall (a :: ak). ca a => sa a) -> SMaybe sa 'Nothing
singMaybe' forall (a :: ak). ca a => sa a
_  = SMaybe sa 'Nothing
forall {a} (sa :: a -> Type). SMaybe sa 'Nothing
SNothing