Yes, that would be nice, but unfortunately there are some fine distinctions that we need to make for soundness. The issue arises when we would call oneOf in a lambda like this:
val xs: List[A^{b, c}] = List(b, c)
() => oneOf(a, xs*)
Do we charge the deep capture set of the type of xs* to the closure, which would be {b, c}, or just the capture set, which would be empty? I.e. Should this expression have type () ->{a} A or () ->{a, b, c} A? The answer is that we always charge the capture set, not the deep set, so it would be () ->{a} A. But that means we cannot access a reach capability of a parameter unless we immediately box it again.
If you replace the reach capability with a capset variable B it’s the other way round. We always charge the deep capture set of the type argument passed to B, so referring to B anywhere in the function result is sound.
This is admittedly very tricky, and the best thiung to do here is follow the compiler’s advice. Maybe we should simply drop reach capabilities and always rely on capset variables for these cases. Then these issues would not arise, but we’d get some expressiveness issues elsewhere.
Yes, that’s correct. Inference is done with a constraint solver that effectively unions the argument sets passed into a capset variable.