You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Given an applied function `f[cs A](g)`, where the type of `f` is `[T] -> (x: {*}
C) -> T` and the type of `g` is dependent, e.g. `(x: {*} Cap) -> {x} A`, the
reference `x` may be propagate to cs.
But this makes `cs A` ill-formed since it is not allowed to mention `{x}`. This
sometimes cause soundness problems.
We heal this by pushing the capture set of `{x}` into cs.
0 commit comments