dynamicIsBottom not handled correctly by strong mode generic inference

[jmesserly]

In particular, this affects cases like:

// $ dartanalyzer --strong --no-implicit-casts test.dart
// Analyzing [test.dart]...
// No issues found
typedef R Func2<A, B, R>(A a, B b);
main() {
  List<int> o = [1, 2, 3];
  var a = o.fold(100, (x, y) => x + y);
  print(a);
  Func2<dynamic, int, dynamic> f = (x, y) => x + y;
  f = (String x, int y) => x + '$y';
  var b = o.fold/*will infer `<dynamic>`*/(100, f);
  print(b);
}

Note the two cases are different: in the first one, we have a definite function, vs the second one we don't. If we infer o.fold<dynamic> ... I don't think fold will end up doing the correct checks on invoking the callback (it would need to be a dcall), so this leads to a soundness problem at runtime.

I can't fix the soundness problem however, without breaking inference the var a = o.fold ... line, because we'd need to know the lambda is definite and thus inferring <dynamic> is sound for a but not for b

[jmesserly]

CC @leafpetersen ... hit this working on https://codereview.chromium.org/2456803004/ but the problem already exists in current code.

[leafpetersen]

I don't think this has anything to do with inference per se, unless I'm missing something. This came up in a language meeting a while back - @floitschG or someone pointed it out.

Basically, we have a soundness bug at the interaction of dynamic as bottom and covariant generics. If you have something like:

/// No analysis errors in this code
class A<T> {
  void oops(void f(T a), T x) {f(x);}
}

void main() {
  void takesInt(int x) { x.abs();}
  A a = new A<dynamic>();
  a.oops(takesInt, "hello");
}

there is no implied covariance check on the first parameter to oops, and there is no implied dcall on the call of f, since T is not known to be dynamic. But if T is replaced with dynamic (as it is in the body of main) then the argument type becomes a fuzzy arrow which accepts anything.

This has been on my TODO list for a while. I really just want to look into getting rid of fuzzy arrows, but to do that I need to evaluate the impact on internal code and fix anything that needs to be fixed there. I believe that there is a fallback position (or perhaps a first step?) that is based on only treating function types which syntactically mention dynamic as fuzzy (as opposed to those created via substitution). This potentially a little heavy to implement, but might work out fine. In the worst cast, we'd have to treat all calls of functions with generic parameters as potentially fuzzy, which would be very unfortunate.

[jmesserly]

The reason I mention inference, is given an argument type A: (dynamic) ~> dynamic where ~> is fuzzy arrow, passed to some parameter type P, strong mode will check that A <: P and will interpret A as (⊥) -> ⊤ ... however inference understands the type of A as (⊤) -> ⊤ because it does not implement fuzzy arrows. That seems like it could be problematic?

[leafpetersen]

Maybe? Is it clear that inferring dynamic is the wrong thing there? And I'm not sure that I understand why inferring anything else (e.g. presumably Null) would solve the soundness issue? I guess what you're saying is that in this case, inferring Null would turn this code into an error, so we would avoid generating the unsound code. The user can still explicitly instantiate with dynamic though, so the unsoundness doesn't go away.

That seems reasonable - we could certainly make inference recognize dynamic as bottom, and it might help us catch and fix places where people are currently taking advantage of dynamic as bottom to write unsound code. Really though, the my meta-goal is to get rid of the fuzzy arrows.

[jmesserly]

I think we can close this. It sounds like we're going to look at removing fuzzy arrows: #29299