Missing annotations about whether synchronizations occure in a function

[bastian-koepcke]

Function signatures must represent whether the function contains a barrier synchronization or which execution resource accessed place expressions that are arguments of the function.

Example

fn f(in: T1, out: T2) -[x: ExecLevel]-> T3 where unsync(x -> out)

The exact details of what the annotation should contain, especially what the accessed place expression should look like, must still be determined.

The information is then used to type check function application, where the annotation is substitued with the values for the calling execution resource and the input arguments (how to deal with non-place expressions as input arguments?)