T1697A.hs

-------------------------------------------------------------------------------------------
-- | Fixed User (WORKING)
-------------------------------------------------------------------------------------------

module T1697A where

data User = U

{-@ measure currentUser :: User @-}

{-@ data TaggedT m a <label :: User -> Bool, clear :: User -> Bool> = TaggedT _ @-}
data TaggedT m a = TaggedT { unTag :: m a }
{-@ data variance TaggedT invariant covariant contravariant covariant @-}

instance Functor m => Functor (TaggedT m) where
  fmap f = TaggedT . fmap f . unTag

instance Applicative m => Applicative (TaggedT m) where
  pure = TaggedT . pure
  f <*> x = TaggedT $ unTag f <*> unTag x

{-@
instance Monad m => Monad (TaggedT m) where
  >>= :: forall < p :: User -> Bool
                , q :: User -> Bool
                , r :: User -> Bool
                , s :: User -> Bool
                , t :: User -> Bool
                , u :: User -> Bool
                , rx :: a -> Bool
                , rf :: a -> b -> Bool
                , ro :: b -> Bool
                >.
    {content :: a<rx> |- b<rf content> <: b<ro>}
    {content :: a<rx> |- b<ro> <: b<rf content>}
    {{v : (User<s>) | True} <: {v : (User<p>) | True}}
    {{v : (User<t>) | True} <: {v : (User<p>) | True}}
    {{v : (User<t>) | True} <: {v : (User<r>) | True}}
    {{v : (User<q>) | True} <: {v : (User<u>) | True}}
    {{v : (User<s>) | True} <: {v : (User<u>) | True}}
    x:TaggedT<p, q> m (a<rx>)
    -> (y:a -> TaggedT<r, s> m (b<rf y>))
    -> TaggedT<t, u> m (b<ro>);

  return :: a -> TaggedT<{\_ -> True}, {\_ -> False}> m a
@-}
instance Monad m => Monad (TaggedT m) where
  x >>= f = TaggedT $ unTag x >>= \y -> unTag (f y)
  
-------------------------------------------------------------------------------------------
-- | Test
-------------------------------------------------------------------------------------------

{-@ assume respondT :: String -> TaggedT<{\_ -> True}, {\v -> v == currentUser}> m () @-}
respondT :: String -> TaggedT m ()
respondT = undefined

{-@ test :: TaggedT<{\_ -> True}, {\v -> v == currentUser}> m () @-}
test :: Monad m => TaggedT m ()
test = return "a" >>= respondT