Foo2.hs

module Foo where
import Language.Haskell.Liquid.Prelude

{-@
data Message = Ping { pingPid :: {v:Pid | validPid v} }
             | Pong { pongPid :: {v:Pid | validPid v} } 
@-}

data Message = Ping Pid
             | Pong Pid
instance ValidMsg Message where

class ValidMsg a where               

data Process a = P a
data Pid = Pid Int
         deriving Eq

instance Functor Process where
instance Applicative Process where
instance Monad Process where  

{-@ measure validPid @-}
validPid (Pid _) = True

{-@ assume send :: {v:Pid | validPid v} -> m:m -> Process () @-}
send :: Pid -> m -> Process ()
send p m = undefined

{-@ assume recv :: ValidMsg a => Process a @-}
recv :: ValidMsg a => Process a
recv = undefined

{-@ measure msgPid @-}               
msgPid :: Message -> Pid               
msgPid (Ping p) = p
msgPid (Pong p) = p

{-@ foo :: Process () @-}
foo :: Process ()
foo = do x <- recv
         let q = case x of
                   Ping q -> q
                   Pong q -> q
         send q x