[adrianratnapala]

If "val1" and "val2" are really things that have to be used exactly once, then the above code is already in error (unless they are provably the same object), and a compiler with linear types will correctly complain about it.

This is indeed "pain", but of a good kind (at least it if the error message is decent).

I admit there are harder cases:

    if(foo)
      func(val1)
    else
      func(val2)

    ... do something that doesn't change foo or use val1, val2 
    ...  

    if(!foo)
      func(val1)
    else
      func(val2)

Is correct, if strange, code which I assume is hard for a compiler to understand. But then it is hard for humans too.