Delegation and the "remaining" channel at end type
This program compiles:
new x y: !integer.end if true then x!4 else x!5 | y?z
Now if one delegates channel x on one the branches:
def p z: !integer.end = z!5 new x y: !integer.end if true then x!4 else p!x | y?z
then program does not compile anymore. Instead the compiler outputs "The sets of linear channel end must be equal in branches: x".
Now, if we delegate x
on both branches, then the program compiles again:
def p z: !integer.end = z!5 new x y: !integer.end if true then p!x else p!x | y?z
I believe the problem has to do with the fact that on the then
branch the symbol table has x:end
, whereas on the else
branch it has no entry for for variable x
.
Can we not add an entry x:colon
to the symbol table when delegating a x
? There is no reason for the second program not to compile. And if "procedure" p
is a complex one and cannot be inlined, then the programmer is forced to write a procedure just to keep the compiler happy.