content: {-@ LIQUID "--noclasscheck"    @-}
  module T385 where
  
  import Prelude hiding (Functor, Monad, (>>))
  
  data ST s a = ST {runState :: s -> (a,s)}
  
  {-@ data ST s a <p :: s -> Bool, q :: s -> s -> Bool, r :: s -> a -> Bool> 
        = ST (runState :: x:s<p> -> (a<r x>, s<q x>)) @-}
  
  {-@ runState :: forall <p :: s -> Bool, q :: s -> s -> Bool, r :: s -> a -> Bool>. ST <p, q, r> s a -> x:s<p> -> (a<r x>, s<q x>) @-}
  
  class Functor f where
    fmap :: (a -> b) -> f a -> f b
  
  instance Functor (ST s) where
    fmap f (ST g) = ST (\s -> let (a, s') = g s in (f a, s'))
  
  class Functor m => Monad m where
    (>>) :: m a -> m b -> m b
  
  instance Monad (ST s) where
    {-@ instance Monad ST s where
          >>  :: forall s a b  < pref :: s -> Bool, postf :: s -> s -> Bool
                      , pre  :: s -> Bool, postg :: s -> s -> Bool
                      , post :: s -> s -> Bool
                      , rg   :: s -> a -> Bool
                      , rf   :: s -> b -> Bool
                      , r    :: s -> b -> Bool
                      >. 
               {x::s<pre>, y::s<postg x> |- b<rf y> <: b<r x>}
               {xx::s<pre>, w::s<postg xx> |- s<postf w> <: s<post xx>}
               {ww::s<pre> |- s<postg ww> <: s<pref>}
               (ST <pre, postg, rg> s a)
            -> (ST <pref, postf, rf> s b)
            -> (ST <pre, post, r> s b)
      @-}
    (ST g) >>  f = ST (\x -> case g x of {(y, s) -> (runState f) s})    
  