{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}

module Control.Monad.Stateless
  ( MonadStateless (..),
  )
where

import Control.Monad.Trans.Control
import Data.Type.Equality
import Prelude

class (MonadBaseControl b m, forall a. StatelessProof m a) => MonadStateless b m | m -> b where
  liftWithStateless :: ((forall a. m a -> b a) -> b c) -> m c

instance (MonadBaseControl b m, forall a. StatelessProof m a) => MonadStateless b m where
  liftWithStateless :: forall c. ((forall a. m a -> b a) -> b c) -> m c
liftWithStateless (forall a. m a -> b a) -> b c
f = (RunInBase m b -> b c) -> m c
forall a. (RunInBase m b -> b a) -> m a
forall (b :: * -> *) (m :: * -> *) a.
MonadBaseControl b m =>
(RunInBase m b -> b a) -> m a
liftBaseWith ((RunInBase m b -> b c) -> m c) -> (RunInBase m b -> b c) -> m c
forall a b. (a -> b) -> a -> b
$ \RunInBase m b
lowerBase ->
    let lowerBasePure :: forall a. m a -> b a
        lowerBasePure :: forall a. m a -> b a
lowerBasePure m a
m = case forall (m :: * -> *) a. StatelessProof m a => StM m a :~: a
statelessProof @m @a of
          StM m a :~: a
Refl -> m a -> b (StM m a)
RunInBase m b
lowerBase m a
m
     in (forall a. m a -> b a) -> b c
f m a -> b a
forall a. m a -> b a
lowerBasePure

class (StM m a ~ a) => StatelessProof m a where
  statelessProof :: StM m a :~: a

instance (StM m a ~ a) => StatelessProof m a where
  statelessProof :: StM m a :~: a
statelessProof = a :~: a
StM m a :~: a
forall {k} (a :: k). a :~: a
Refl