Kernel needs a way to represent a type variable with a promoted bound

[stereotype441]

In strong mode type inference (see https://github.com/dart-lang/sdk/pull/29371/files), we need to be able to handle type promotions like this:

class A {}
class B extends A {
  void foo() { ... }
}
class C<T extends A> {
  f(T t) { ... }
  h(T t) {
    if (t is B) {
      f(t); // ok because t has type T
      t.foo(); // ok because t extends B
    }
  }
}

In order for this to work, we need to be able to represent the type of t within the "if" block as "T extends B". Currently kernel can't do this, because currently a TypeParameterType just points to the type parameter, which can only have a single bound.

Note that we need to be able to recognize the difference between a type that has a promoted bound and a type that has its original bound, so what we probably want to do is add a nullable bound field to TypeParameterType--we'll use null to represent the (typical) case of a type variable with a non-promoted bound, and a non-null value to represent the case of a type variable with a promoted bound.

[lrhn]

Is this actually allowed by the current type promotion specification?

The static type of the variable t is T. The type B is not more specific than either T or A, so there is no promotion from an t is B test.

[stereotype441]

@lrhn whoops, there were two errors in my example:

• I meant to say class B extends A instead of simply class B
• I meant for the "if" test inside of h to be if (t is B), not if (t is int)

Sorry about that--I've fixed my example above.

Since the spec for strong mode is still being written, and is based on the de facto implementation of strong mode in analyzer, there are several ways to answer your question:

• For the current Dart 1.0 spec (non-strong-mode), B is more specific than A but not more specific than T (taking into account the corrections I mentioned above). So no type promotion happens and t.foo() gives a warning. Analyzer's non-strong-mode behavior is consistent with this.

• If we made no change to type promotion for strong mode, then t.foo() would be an error.

• The de facto implementation of strong mode in analyzer considers if (t is B) to promote t to type T extends B (this is possible to represent in analyzer). Therefore t.foo() is ok and no errors are reported.

• The current proposal for strong mode type inference (https://github.com/dart-lang/sdk/pull/29371/files) doesn't specifically mention any changes to type promotion, but on line 225 it says "A type variable T not in L with bound P is a subtype match for the same type variable T with bound Q with respect to L under constraints C...", which presumes that it's possible for a single type variable to have one bound in one situation and a different bound in a different situation. When I asked @leafpetersen how this could happen, he brought up the type promotion example (see the review thread on that PR). So while the current strong mode spec proposal doesn't call for T to be promoted, we should probably think of that as an oversight rather than an intention :)

I'm happy to defer to you folks on the language team to decide how we want things to work in Dart 2.0. However, for now, I'd prefer to make Fasta/kernel match the behavior of analyzer in strong mode, so that we will be free to transition tools over to Fasta without having to change any client code. If we decide that we don't want promotion to work this way, it would be nice to be able to roll that change out independently of the Fasta transition.

[eernstg]

.. the current strong mode spec proposal doesn't call for T to be promoted ..

It might be useful to restate explicitly what we are doing here. Of course, there is no way we can actually promote T as such (other expressions could have type T, too, but the type test was only applied to t), but we are somehow coming up with an entity that looks like a "promoted version of T". So here's a way to describe the situation which doesn't create that illusion:

When the given expression (here: the formal parameter t) has been checked and found promotable, we may conclude that its value has type T (from the declaration) and type B (from the type test), and we also know that T <: A (from the bound). What we really know is that t has the intersection type (exists T<=A. T) & B, and that just happens (because B <: A) to be equivalent to "T where the bound has been changed to B", that is, exists T<=B. T.

In other words, we're expressing a non-trivial intersection type for this particular special case, just because we can. ;-)

I think we should model these finite intersection types (say, as simple finite sets of other types), such that we give developers the improved service of preserving everything we know in a promotion.

Also, we should be careful when creating artificial type parameters like exists T<=B. T: they might cause incorrect information to flow back to the developer (say, if there is an error message involving the bound of T and we print B for that, the developer would rightly say "but the bound of T is A, not B!").

So maybe we should aim for supporting those finite intersections in general, and stop exploiting this special case?

[leafpetersen]

Yes, I have been thinking about these as an intersection type. Supporting these in the general case might be great, but concretely this limited use of them addresses a big class of problems.