Yichen Xu

Another soundness issue found: ```scala import language.experimental.captureChecking def runOps(ops: List[() => Unit]): Unit = ops.foreach(op => op()) def app[T, U](x: T, op: T => U): () ->{op} U = ()...

How is the second one sharing the root cause with the first? My idea behind that example was that given (x:T) where T is a type parameter with no upper...

I see that in `reachCanSubsumeDcs` a special case is made for `cap`, but `cap` might well represent something outlives the reach. For instance, the following compiles again: ```scala import language.experimental.captureChecking...

Also, the error in the second example depends on the fact that `runOps` is eta-expanded when passed to `app` on the last line. See the tree: ``` def unsafeRunOps(ops: List[box...

IMO, the root cause of the second issue is in: ```scala def app[T, U](x: T, op: T => U): () ->{op} U = () => op(x) ``` The closure returned...

> I see that in `reachCanSubsumeDcs` a special case is made for `cap`, but `cap` might well represent something outlives the reach. For instance, the following compiles again: > >...

I think the kernel of the first issue: ```scala def delayedRunOps1(ops: List[() => Unit]): () ->{} Unit = () => val ops1: List[() ->{ops*} Unit] = ops runOps(ops1) ``` is...

And when the dcs of the type of `ops1` contains `cap`, we should error, like in the revised snippet: ```scala def delayedRunOps1(ops: List[() => Unit]): () ->{} Unit = ()...

If we instead adopt the above mechanism in place of `reachCanSubsumeDcs`, it could also save us from the nightmare of parametric reasoning, since very often given `x: X` where X...

For `app`, since now we assumed `dcs(T)` can be `cap`, it will not typecheck. It only typechecks if we do: ```scala def app[T, U](x: T, op: T => U): ()...