Dependent sessions

[np]

Two kinds of dependencies should be supported at first.

Simple dependencies: indexing

(this is supported since 5657a0a)

Example:

dep_fun_server =
  \(A : Type)
   (B : (x : A)-> Type)
   (f : (x : A)-> B x)->
   proc(c : ?(x : A). !B x)
   recv c (x : A).
   send c (f x)

Large-elimination over finite data types

Example:

case_fun_server =
  proc(c : ?(x : Bool). case x of { `true -> !String, `false -> {!String,!String} })
  recv c (x : Bool).
  case x of
    `true -> send c "Hello World!"
    `false ->
       c{d,e}
       send d "Hello".
       send e "World"

However since case is not part of process but of terms the example above is rejected, instead one can write:

case_fun_server =
  proc(c : ?(x : Bool). (case x of { `true -> !String, `false -> {!String,!String} }))
  recv c (x : Bool).
  @(case x of
    `true -> proc (c) send c "Hello World!"
    `false ->
       proc (c)
       c{d,e}
       send d "Hello".
       send e "World"
  )(c)

Which is rejected so far with the following message:

Expected a protocol type, not:
case x of {
  `false -> < {!String, !String}> ,
  `true -> < !String >
}

Here the fix seems straightforward the type above should be equivalent to:

< case x of { `false -> {!String, !String} , `true -> !String } >