stacst v.s. datasort

sortdef role = {a:int|a==0||a==1}


datasort stype = 
| pmsg of (int, vt@ype)
// | pseq of (stype, stype) // please compare this line
| pend of (int)

stacst pseq: (stype, stype) -> stype // with this line, by running the code
#define :: pseq 

absvtype chan (int, stype) = ptr

extern fun create {r1,r2:role} {p:stype} {r1 != r2} (chan(r2,p) -<lincloptr1> void): chan(r1,p)

extern fun send   {r,r0:role}  {p:stype} {a:vt@ype} {r0 == r}  (!chan(r, pmsg(r0,a)::p) >> chan(r,p), a): void
extern fun recv   {r,r0:role}  {p:stype} {a:vt@ype} {r0 != r}  (!chan(r, pmsg(r0,a)::p) >> chan(r,p)): a

extern fun close  {r,r0:role}  {p:stype} (chan(r, pend r0)): void


stadef pi = pmsg(1,int)::pend(1)

extern fun server (chan(0,pi)): void
extern fun client (chan(1,pi)): void


implement server (chan) = let 
    val n = recv chan
    val _ = $showtype n
in 
    close chan
end

implement client (chan) = let 
    val _ = send (chan, 42)
in 
    close chan
end