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
Capture set healing happens at the end of capture checking (in the `postCheck`
function), which checks the capture set in each type argument and widen the
ill-formed `TermParamRef`s by widening them. However, it is possible that a
capture set is healed first, and then get a `TermParamRef` propagated into it
later when we are healing another capture set. This lead to unsoundness.
This commit installs an handler on capture sets when healing them and will
inspect the newly added elements and heal these new elements as well.
0 commit comments