{-# 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 f = liftBaseWith $ \lowerBase ->
    let lowerBasePure :: forall a. m a -> b a
        lowerBasePure m = case statelessProof @m @a of
          Refl -> lowerBase m
     in f 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 = Refl