Sharpen range approximation for applied types with capture set ranges

[odersky]

This is a stopgap to avoid approximating the core type to Nothing. It can probably be dropped once we have capture set ranges that we can keep as inference results. The problem is, what should be the approximation of the range

C[{cs1} A .. {cs2} A]

where the type constructor C is non-variant? If the variance of the enclosing map is positive, this is C[? >: {cs1} A <: {cs2} A], which is a supertype of both range end points C[{cs1} A] and C[{cs2} A]. But if the variance is negative, we would normally fall back to Nothing, since that is the only known subtype of both range end points. This reasoning seems too strict for capture checking. In a sense, we have already inferred C[A] before; now we just need to find out what the set should be. What we are after is a notion of a capture set range. I.e. something like

C[{cs1}..{cs2} A]

with the meaning that the capture set of C is an unknown set between cs1 and cs2. We don't have that abstraction yet, so for now we approximate by the bounds, which avoids the failures, even though its soundness status is currently a bit unclear.

[Linyxus]

LGTM!

[Linyxus]

Agree that this is an effective solution to this issue; but I am also thinking about whether it is possible to do avoidance for capturing types without the concept of capture set range. It would be a simpler solution while the validity of the assumption behind it remains unknown. Consider a block expression:

{
  val x: {*} Cap = ???
  res
}

where res is typed as Inv[C S] => T and Inv has an invariant type parameter. There are two cases for avoid(C S):

• First case: C contains reference to x, e.g. {x} S. Since Inv is invariant on the type argument, and it is impossible to get a capability subcapturing the local reference x outside the block expression, we can avoid Inv[{x} S] => T to Nothing => T. This is what we are doing before.
• The second case, where the incompleteness issue this PR fixes comes from: C does not contain reference to x. Ideally we avoid(C S) should be C S'. Now it is a range C1 S' ... C2 S' where C1 and C2 are Mapped capture set from C. This is because we are afraid that x may be pushed to C after we do avoidance, so C1 and C2 basically avoids x from C by mapping it to empty set or {*}. This would not be necessary if the following assumption holds:

Assumption: x can only be pushed into C before we call avoidance on the result type Inv[C S] => T.

This assumption looks reasonable, since we do avoidance only when we finish typing a block expression. The local reference should not appear in the expected type, so it would not flow into the capture set of the result type any more. If this assumption holds, we know that if there is no x in C when we do avoidance on C, then C will not receive x afterwards. Therefore, we return a range {} S ... {*} S' for avoid({x} S), but returns C S if x does not appear in C instead of creating two Mapped instances and returning a Range.

However, since capture set inference is quite complicated, I am not sure if this assumption is valid or not. It would be good if we have some theoretical groundings for the implementation of capture set inference (like what we are doing for box inference), so that we could understand the results of capture set inference better and predict what will be going on.

[odersky]

@Linyxus I agree with your observations. That will lead to a clearer solution. I am revising the PR.

[Linyxus]

LGTM!