fasta strong mode: strange type inference with ?? and function types

[mraleph]

When compiling the code below with fasta in strong mode:

void foo<E>(C<E> c, int cmp(E a, E b)) {}

class C<E> {
  void barA([int cmp(E a, E b)]) {
    foo(this, cmp ?? _default);
  }

  void barB([int cmp(E a, E b)]) {
    foo(this, cmp ?? (_default as int Function(E, E)));
  }

  void barC([int cmp(E a, E b)]) {
    int Function(E, E) v = _default;
    foo(this, cmp ?? v);
  }

  void barD([int cmp(E a, E b)]) {
    foo<E>(this, cmp ?? _default);
  }

  void barE([int cmp(E a, E b)]) {
    foo(this, cmp == null ? _default : cmp);
  }

  void barF([int cmp(E a, E b)]) {
    foo(this, cmp != null ? cmp : _default);
  }

  static int _default(a, b) {
    return -1;
  }
}

main() {}

I get

class C<E extends core::Object> extends core::Object {
  default constructor •() → void
    : super core::Object::•()
    ;
  method barA([(t::C::E, t::C::E) → core::int cmp = null]) → void {
    t::foo<t::C::E>(this, let final (t::C::E, t::C::E) → core::int #t1 = cmp in 
                              #t1.==(null) ?{(core::Null, core::Null) → core::int} t::C::_default :
                              #t1);
  }
  method barB([(t::C::E, t::C::E) → core::int cmp = null]) → void {
    t::foo<t::C::E>(this, let final (t::C::E, t::C::E) → core::int #t2 = cmp in
                              #t2.==(null) ?{(core::Null, core::Null) → core::int} t::C::_default as (t::C::E, t::C::E) → core::int :
                              #t2);
  }
  method barC([(t::C::E, t::C::E) → core::int cmp = null]) → void {
    (t::C::E, t::C::E) → core::int v = t::C::_default;
    t::foo<t::C::E>(this, let final (t::C::E, t::C::E) → core::int #t3 = cmp in
                              #t3.==(null) ?{(core::Null, core::Null) → core::int} v :
                              #t3);
  }
  method barD([(t::C::E, t::C::E) → core::int cmp = null]) → void {
    t::foo<t::C::E>(this, let final (t::C::E, t::C::E) → core::int #t4 = cmp in 
                              #t4.==(null) ?{(t::C::E, t::C::E) → core::int} t::C::_default :
                              #t4);
  }
  method barE([(t::C::E, t::C::E) → core::int cmp = null]) → void {
    t::foo<t::C::E>(this, cmp.==(null) ?{(t::C::E, t::C::E) → core::int} t::C::_default : cmp);
  }
  method barF([(t::C::E, t::C::E) → core::int cmp = null]) → void {
    t::foo<t::C::E>(this, !cmp.==(null) ?{(t::C::E, t::C::E) → core::int} cmp : t::C::_default);
  }
  static method _default(dynamic a, dynamic b) → core::int {
    return 1.{core::int::unary-}();
  }
}

Notice that in

• barA, barB, barC the ternary has type (core::Null, core::Null) → core::int
• barD it has type (C::E, C::E) → int as I would expect.
• Notice that cases barE and barF are different from barA - even though I would expect a ?? b and a != null ? a : b have the same inferred type.

/cc @leafpetersen @floitschG

[stereotype441]

I believe barA, barB, and barC are behaving correctly according to the informal spec (https://github.com/dart-lang/sdk/pull/29371/files). When inferring the type of a ?? expression, if there is a non-empty context (as there is in this case), the type of the resulting expression is supposed to be inferred as the greatest closure of the context with respect to ?. So in this case the context is (?, ?) -> int, therefore the type is inferred as (Null, Null) -> int.

I also believe barD is behaving correctly. In this case, the presence of the explicit <E> in the call to foo means that the context is (E, E) -> int, so therefore the type is inferred as (Null, Null) -> int.

I believe the front end is doing the wrong thing for barE and barF. According to the informal spec, the behavior should be similar to ??; since there is a non-empty context, the type of the resulting expression should again be the greatest closure of the context with respect to ?. So the type should be (Null, Null) -> int, matching barA, barB, and barC.

I'll work on a fix ASAP.

[leafpetersen]

A couple of notes:

Strong mode inference treats a ?? b and a != null ? a : b slightly differently, despite the equivalence. The reason is that in practice it works out better to use the type of a as a downwards context in a ?? b. This is because:

• The expression "prefers" a in a certain sense. The intent is "use a, unless it's not there, in which case use b instead". So usually the type of b is intended to be a subtype of the type of a.
• In practice, b is often a default literal: a ?? [].

There is no equivalent user intent to guide a choice of sides to prefer for the ternary operator case.

The use of greatest closure on the context is probably not the most useful thing we could do here. I'll try to make a bit of time to think about this.

[mraleph]

Sorry maybe I am not following the reasoning entirely, but when I look at expression a ?? b where a and b have exactly the same type T without any ? in them I don't really expect the type of a ?? b to be anything but T. Anything else is counter intuitive. I think if users start look at inferred types they will be confused just as I am.

What is the motivation for that?

Also another concern of mine is that while every (t::C::E, t::C::E) → core::int is a (Null, Null) → core::int, this does not work the other way around (Null, Null) → core::int is not a (t::C::E, t::C::E) → core::int (unless I am misunderstanding how our type lattice works).

Which means that in the code above we need a dynamic check somewhere, because t::foo<t::C::E>(...) expects (t::C::E, t::C::E) → core::int and gets (Null, Null) → core::int instead.

[leafpetersen]

cc @jmesserly

[leafpetersen]

Sorry maybe I am not following the reasoning entirely, but when I look at expression a ?? b where a and b have exactly the same type T without any ? in them I don't really expect the type of a ?? b to be anything but T. Anything else is counter intuitive. I think if users start look at inferred types they will be confused just as I am.

If a and b both have type T then:

• If a ?? b is used in a context where a concrete type T is expected, then the question is irrelevant: the user doesn't know what type is inferred there, and doesn't care.
• If a ?? b is used in a context without a type expectation, then we will infer T for the type of the ?? expression, as you find intuitive.

The interesting cases are when the types of a, b and the context differ in some way, as in your example. In your example, we have:

a : (E, E) -> int
b : (dynamic, dynamic) -> int
K : (?, ?) -> int

where K is the type context in which the expression appears.

So what do we infer? The context says that a ?? b must be assignable to (?, ?) -> int. We can just ignore the context type, and take the least upper bound as we do in the case that we have no context. This is what the analyzer currently does, and it is the reason that this code is currently strong mode clean:

List x = (true) ? 3 : "hello";

In this case though, it would give us the answer that you presumably want: (E, E) -> int. So that's the tradeoff: good results for your example, bad results for the other example above.

Another choice we can make is to say that we always prefer the context type, and if the context type is partial, we fill in the missing bits using dynamic and Null as appropriate. In this case, this results in a ?? b being inferred to have type (Null, Null) -> int, with an implicit downcast to (E, E) -> int. The advantage of this choice is that it makes

List x = (true) ? 3 : "hello";

into an error, as we would like. So worse results for your case, better results for the bad case above.

:(

I do think there is a better approach that gets the best of both of these approaches by essentially matching the context type against LUB(a, b) to fill in the ? with something more meaningful than Null. Here, that would result in (E, E) -> int as desired. I'll try to make some time to write this up.

Which means that in the code above we need a dynamic check somewhere, because t::foo(...) expects (t::C::E, t::C::E) → core::int and gets (Null, Null) → core::int instead.

Yes there should be an implied implicit cast around the ?? expression, since it is only assignable to its surrounding context (not a subtype of it).

[stereotype441]

After discussion with @leafpetersen and @jmesserly we decided that for the short term we should match the behavior of analyzer (which is to use LUB); this should ease the transition to the new front end. At a later date we can change to the behavior in the informal spec.

CL to do this is out for review: https://dart-review.googlesource.com/c/sdk/+/3421

[stereotype441]

The fix in 068c78e9d72e713b6d2b045f240e62af4f7ccf4d changes the types of all these conditionals to (self::C::E, self::C::E) → core::int. Even though there's still an open question as to whether we want to make the inference more sophisticated in the future, this particular corner case now works as expected, so I'm closing the issue.