Soundness issue with intersection types

[eernstg]

The document subtyping.md states that 'Promoted type variable types will only appear as top level types: that is, they can never appear as sub-components of other types, in bounds, or as part of other promoted type variables.'

However, that property is not enforced consistently by the current static analysis. Consider the following program:

class A { void bar() => print("Doing bar stuff!"); }

List<Y> typedResult<Y extends A>(Y y) => ["Hello world!" as Y];

foo<X>(final X x) {
  if (x is A) {
    var v = typedResult(x);
    a = v[0];
    print("Just assigned a string to a variable of type A, still running.");
  }
}

A a;

main() {
  foo<Object>(A());
  a.bar();
}

This program produces a 'No issues!' response with dartanalyzer and with dartanalyzer --no-implicit-casts (version 2.1.0-dev.8.0 as well as a fresh one from commit 55f3cc9), it has no compile-time errors with dart (same versions), and it throws as follows at a.bar():

Just assigned a string to a variable of type A, still running.
Unhandled exception:
NoSuchMethodError: Class 'String' has no instance method 'bar'.
Receiver: "Hello world!"
Tried calling: bar()
#0      Object.noSuchMethod (dart:core/runtime/libobject_patch.dart:50:5)
#1      main (file:///usr/local/google/home/eernst/lang/dart/scratch/201811/n014.dart:20:5)
#2      _startIsolate.<anonymous closure> (dart:isolate/runtime/libisolate_patch.dart:289:19)
#3      _RawReceivePortImpl._handleMessage (dart:isolate/runtime/libisolate_patch.dart:171:12)

Note that before the dynamic error occurs, the program prints 'Just assigned a string to a variable of type A, still running', which shows that a heap invariant violation has taken place (we assigned an instance of String to the variable a of type A) and no dynamic errors were incurred when we did that.

The underlying issue is that the static analysis allows the static type of the variable x at the invocation of typedResult to propagate into the type of the invocation: Presumably, the actual type argument passed to typedResult is considered (by the static analysis) to be X & A, and the returned value is considered to have type List<X & A>, because that's the reason why dartanalyzer --no-implicit-casts considers the assignment of v[0] to a to be type correct.

If the static analysis had considered the type argument to typedResult to be a plain X then the type of v would have been List<X>, and a = v[0] would have been a compile-time error (with or without --no-implicit-casts).

If the static analysis had considered the type argument to be a plain A then v would have had type List<A> and a = v[0] would be OK, but we just need to add in X v2 = v[0];: That would then have been a compile-time error, and it is not (and the fact that it still isn't an error with --no-implicit-casts shows that the type of v[0] is not a supertype of X or a supertype of A).

The soundness issue arises because the static analysis fails to track the dynamic semantics faithfully: The actual actual type argument passed to typedResult is Object, that is, code is generated to pass X (vary it a bit and print it), but the static analysis thinks that the type argument is X & A, and when they are not the same type we cannot trust various kinds of code (say, type casts, or newly created objects with Y in their reified type, or invocations of other generic functions receiving Y as an actual type argument or as part of one).

Apart from the obvious soundness issue that we get to assign a String to a variable of type A, we also have the issue that the type argument passed to typedResult has bound A, but we get to actually pass Object (no static error, no dynamic error), and it seems impossible to avoid the conclusion that the inferred type of v is List<X & A>, which is a shape of type that shouldn't occur anywhere at all.

So we definitely need to avoid the split where a type argument passed to a generic function call is considered to have one value during static analysis and actually gets another value at run time. It's hard to tell what this means for existing code, but it might be necessary to pass type arguments explicitly in some situations where the inferred type argument now cannot be an intersection type.

[lrhn]

This is great news. We can now write unsafe code! 😈 😁

void main() {
  int i = unsafe("X", 2);
  print(i); // X
  String s = unsafe(42, "a");
  print(s); // 42
  Null n = unsafe("not null", null);
  print(n); // not null
}

/// Return [value] as type [T]. 
/// You need to prove that [T] exists by giving a [helper] instance.
T unsafe<T>(Object value, T helper) {
  T unsafe<R>(R value, R x) {
    if (x is T) { // x promoted to "R extends T"
      var y = x; // Infer type "R extends T".
      y = value; // R  =?= R extends T
      T z = y; // Upcast from (R extends T) to T
      return z;
    }
    return null;
  }
  return unsafe(value, helper);
}

You just need to prove that you have a value of a type, then we can make any value have that static type.

The analyzer is quiet, so is the front-end. The code runs on both VM and dart2js.

If you start doing more things with the value, like print(i.runtimeType), dart2js may start showing why type unsoundness is not good for tree shaking. I have had examples where String.toString$0 did not exist.

[leafpetersen]

I think this is basically this issue: #30832 . Obviously still needs fixed.

[lrhn]

I'll use this issue as the front-end bug then, we can use #30832 as the analyzer bug.