Intersection type soundness issue

[eernstg]

Consider the following program:

X id<X extends int>(X x) {
  print(x.isEven); // But `x` is `Object()`!
  return x;
}

void foo<Y>(Y y) {
  if (y is int) { // `y` has type `Y & int`.
    // This invocation is inferred as `id<Y & int>(y)`.
    id(y);
  }
}

void main() => foo<Object>(Object());

This program is accepted with no diagnostics by the analyzer. However, it violates soundness because foo is invoked with an argument of type Object which is passed on to id, and the body of id invokes isEven on that object.

The core reason for this soundness violation is that the invocation id(y) is inferred to have a type argument which is reified as Y, but we cannot prove Y <: int, and this means that the invocation of id is unsound.

It seems likely that this is allowed to happen because type inference of the invocation of id uses the static type of the actual argument, namely Y & int, and this yields an actual type argument that does satisfy the declared bound, as if the invocation had been of the form id<Y & int>(y). This explanation could be wrong, but in that case it is not easy to see why no bound violation error occurs at the invocation of id (or, rather, an error which reports that type inference for id(y) failed).

This is not possible, of course, because Y & int cannot be reified. So it is erased to Y, and that is what is passed as the actual type argument at run time. It is the erasure that introduces the type soundness violation (or, rather, the fact that no checks are performed after the erasure).

The CFE does not have this soundness issue, it correctly reports that inference of an actual type argument to id fails.

[eernstg]

Note this comment, too.