Parameter's type not promoted after `is`-check when it has a type parameter.

[spkersten]

In the following snippet, the type of the foo argument isn't promoted to FooImpl in the if-statement's clause while it does work in several related versions of the code (e.g. the the parameter type is Foo instead of Foo<T>):

void bar<T>(Foo<T> foo) {
  if (foo is FooImpl) {
    print(foo.impl);  // error: The getter 'impl' isn't defined for the type 'Foo<T>'.
  }
}

class Foo<T> {}

class FooImpl extends Foo<int> {
  String get impl => "";
}

[eernstg]

The reason why you get no promotion here is that FooImpl isn't a subtype of Foo<T> for all T, and promotion can only give a variable v a type T in the case where the declared type of v is a supertype of T.

The rationale behind that behavior is that we shouldn't promote a variable in such ways that it drops some members from its interface:

class A { void aMethod() {}}
mixin B { void bMethod() {}}
class C extends A with B {}

void f(A a) {
  if (a is B) a.bMethod(); // Compile-time error, because `a` is not promoted to `B`.
}

If we had promoted a to have the type B then the interface of a would change from having aMethod to having bMethod (and dropping aMethod), and the ability to drop some members by promotion was deemed to be inconvenient and surprising, so we don't do that.

[eernstg]

@stereotype441, we have a special case here where the actual value of T is guaranteed to be a supertype of int at the point where we have succeeded in the test foo is FooImpl (because no class can implement Foo<T> and Foo<S> at the same time when T and S are mutually unrelated type-, and we do know that the run-time type of foo implements Foo<int>).

Does this mean that we could refine the promotion machinery to recognize that a promotion from Foo<T> to FooImpl is actually allowed, because FooImpl <: Foo<T> is guaranteed to hold?

[lrhn]

In general, we do promote in some cases where the type is not statically a subtype, when we introduce type variable intersection types:

void foo<T>(List<T> values) {
  var value = values.first;
  if (value is int) { // `int` is not subtype of `T`
    // Promoted to `T & int`, is subtype of `T`
    print(value.toRadixString(16));
  }
  if (values is List<int>) { 
    // Not promoted to List<T & int> :(
    print(values.first.toRadixString(16));
  }
}

We don't allow those intersection types to occur as type arguments. Probably with good reason. (At some, probably very early, point we're going to have to project back to either int or T, because the intersection type doesn't actually exist. If that's too unpredictable, then it's not a good feature to expose.)

If the second example above could potentially be made to work, so you could promote List<T> to List<T&int>, that still wouldn't be enough for this issue's problem.

Even if we could promote Foo<T> to Foo<T&int>, that's not the same type as FooImpl, and FooImpl is still not a subtype of Foo<T&int> (which is satisfied by T being Never). The is FooImpl check actually provides a lower bound on T, not just an upper bound. T is int, otherwise it couldn't be a FooImpl. We'd need a kind of promotion for T itself, "promoting" T to int, not just promoting a variable to T&int.

[eernstg]

we do promote in some cases where the type is not statically a subtype

I think we should stick to the characterization: We do not promote a local variable v with declared type T to any type S where S is not a subtype of T.

In the case where we promote a variable from a type variable type X to an intersection type like X & int, the promoted type is still, as you mention, a subtype of the declared type.

The special property of the situation in this issue is that we can prove that FooImpl <: Foo<T> because FooImpl implements Foo, and hence we know that FooImpl implements Foo<S> for some S, and (by soundness) that's only possible in the case where S <: T.

It wouldn't be sound to promote T to int, because the actual value of T could be, say, a top type, and it would still be true that FooImpl <: Foo<T>. But at the location in the promotion machinery where we check whether we're testing for a subtype of the declared type, we could say yes in the true continuation of foo is FooImpl, and that would allow us to promote foo to fooImpl.

The novelty here is that we have a subtype judgment which is known statically to hold, but only in the true continuation of the given subtype test.

[lrhn]

It's still the case that FooImpl is not a subtype of Foo<T>. We may deduce that T must have a value such that it's the case, but we are not promoting T, we don't have any machinery to do so (we can't promote T to int, that concept doesn't exist in our type inference, we only promote normal variables). Which means that if we do promote the variable from Foo<T> to FooImpl, we can no longer assign it back to Foo<T>.

Now, if we could promote type variables, then the is FooImpl could validly promote T to having int as a lower bound, and then FooImpl would (locally) be a subtype of Foo<T>.

[eernstg]

It's still the case that FooImpl is not a subtype of Foo<T>.

It is a novelty to be able to conclude FooImpl <: Foo<T> in the true continuation of the test foo is FooImpl, but it might actually be useful.

We did have other situations where a proposed language mechanism could give rise to a similar situation (where a "hand-crafted" edge is added to the subtype graph based on dynamic tests, not based on the subtype ruleset). For instance:

// Assume that https://github.com/dart-lang/language/issues/2090 has been adopted.

void f<X, Y>(X x, Y y) {
  if (X is Type<Y>) {
    // In this block it is known that `X <: Y`.
    Y y2 = someCondition ? x : y; // OK.
  }
}

So the intention is definitely that we'd be able to rely on FooImpl <: Foo<T> in the true continuation of foo is FooImpl, and there would be no exception to the rule that we only promote to a subtype of the declared type.

[lrhn]

Just hit this one again:

  ListSlice<E> slice(int start, [int? end]) {
    end = RangeError.checkValidRange(start, end, length);
    var self = this;
    if (self is ListSlice) return self.slice(start, end);  // should be `self is ListSlice<E>`
    return ListSlice<E>(this, start, end);
  }

This method is an extension method on List, the ListSlice subclass has an instance method. Because of the lack of promotion, it would do an infinite recursion of the extension method if the value is actually a ListSlice.

In this case, the promotion doesn't require extra features around type variables, it's just a matter of seeing that if something is a List<E> and it's a ListSlice<Object?>, where ListSlice<E> implements List<E>, then it's guranteed to be a ListSlice<E> too, so we can safely promote self to ListSlice<E>.

So: Given a value of type T<X>, a check that it's a S<Y> where S<Z> implements T<Z> for any type Z, and X <: Y (or any case where Y <!: X), we can promote the value to S<X>. If Y <: X we can promote to S<Y> as normal.

That only works if S is generic and passes the type variable directly to T. If its class S implements T<int>, we cannot find an instantiation of S that is guaranteed to be a subtype of T<X>.

[eernstg]

Note that today we do have support for a way to write the original example in this issue such that we get access to the given object with the desired type.

This works in the general case where the promotion doesn't take place because the variable isn't promotable (somebody writes to it in a function literal), or because the new type isn't a subtype (like FooImpl which isn't a subtype of Foo<T>, or because the tested expression isn't a local variable, e.g., if (a.b.c() is FooImpl) ... doesn't allow us to assume anything extra about a.b.c()).

Here is the original example again:

void bar<T>(Foo<T> foo) {
  if (foo is FooImpl) {
    print(foo.impl);  // Error: The getter 'impl' isn't defined for the type 'Foo<T>'.
  }
}

class Foo<T> {}

class FooImpl extends Foo<int> {
  String get impl => "";
}

The rewrite that allows us to access the value of foo with type FooImpl is as follows:

void bar<T>(Foo<T> foo) {
  if (foo case FooImpl foo1) {
    print(foo1.impl);  // OK.
  }
}

The point is that the type test that uses a variable pattern (case FooImpl someName) will introduce a fresh variable (someName) with the given type. This will work independently of the ability to promote the existing variable. You may want to use the same name (as in if (foo case FooImpl foo) ...) or a different name (such as if (foo case FooImpl foo1) ...), depending on your opinion about local shadowing.

Caveats apply, though (especially if we use the same name): The variable introduced by the case term is different from the original variable, so we can't do foo = aNewValue (same name) or foo1 = aNewValue (different name) and expect the original variable to be updated. Next, FooImpl is a non-generic class, but in the case where we are testing for a generic type it is quite possible that the semantics of leaving out the actual type arguments is surprising (see https://github.com/dart-lang/language/issues/2047. This is no worse than is FooImpl, by the way, it's just worth noting that case can be better than is when it comes to actual type arguments in other cases).

Of course, we always had the option to introduce a fresh local variable with the desired type explicitly:

void bar<T>(Foo<T> foo) {
  Foo<Object?> fooPromotable = foo; // Enable promotion to `fooImpl`.
  if (fooPromotable is FooImpl) {
    print(fooPromotable.impl);  // OK.
  }
}

The tricky part here is that we need to think about the subtype relationships (perhaps looking up the declaration of FooImpl) in order to understand why the normal promotion mechanism doesn't kick in with the original example, and why it helps to declare fooPromotable to have type Foo<Object?>. So the form using case may still be preferable, which is the reason why I thought it would be useful to add this comment. ;-)

[lrhn]

Or, as you pointed out, if (foo case FooImpl()) { ... } will promote foo to FooImpl<T>.

We could, safely and soundly, allow if (foo is FooImpl) to promote foo to FooImpl<T>. It's not even about special-casing raw types, if (foo is FooImpl<Object?>) would do the same. The logic would be that if foo is Foo<T> and foo is FooImpl<Object?> and FooImpl<S> implements Foo<S> for any S, then by uniqueness of implementation of an interface, foo must be a FooImpl<T>.

That does require that the link between FooImpl and Impl is fairly trivial, because we want to solve FooImpl<X> implements Foo<T> (or FooImpl<X> implements Foo<Y> && T <:> Y where <:> means mutual subtype) for X, to effectively find the intersection Foo<T> & FooImpl<Object?>. (And the precise intersection, no more or less.)

An example of a non-trivial relation could be:

class Super<X, Y> {}
class Sub<W> extends Super<W, W> {}
void main() {
  var v = Super<int, double>();
  if (v is Sub1) {
    // Cannot find a *single* W such that Super<W, W> 
    // includes all values that are both `Sub<Object?` and `Super<int, double>,
    // so no promotion.
  } 
}

It requires "solving backwards". We can trivially go from Sub<X> to Super<X, X>, directly by expanding type variables through the super-interface declaration chain. Solving in the other direction is effectively what we try to do for if (v is Sub()), so we should probably just use the same algorithm here, and then refuse to promote if the solution does not promote the static type of the variable.

That is, for a check v is T where v has static type S, then:

• If T \<: S, then a successful check promotes v to T.
• If S and T are both interface or extension types (or maybe S is a union type where one of the types are), the declaration of the type of T, D, has the declaration of S (or of a single union-part type of S), C, as a transitive declared super-interface, and both declarations are generic, then solve for type parameters to D in the same way as we would for v case D().
  • If we infer type arguments <T1,...,Tn> to D, D<T1,...,Tn> implements C<S1,..,Sk> and C<S1,...,Sk> \<:> S, then a successful check promotes v to D<T1,...,Tn>.
• Otherwise v is T does not promote v.

(We may also promote on the negative branch for a FutureOr typed S as usual.)

The <:> is needed because v case Sub() may infer a lower bound. Take the traditional diamond class hierarch: A <: (B | C) <: D, and do Super<B, C> s = Sub<D>(); if (s case Sub()) { print("Match"); }. The s case Sub() will be inferred to mean s case Sub<Never>(), because the DOWN algorithm is mostly useless, and it won't actually match the value at runtime (or exhaust Sub if it needed to). An s case Sub _ would match and exhaust, but not promote. If we want an non-pattern is Sub check to promote, we need to have it match all the cases it normally would, and the promotion must be sound in all those cases, so we need to infer type arguments that so that it implements exactly Super<A, B>. Which we never can for a Super<S, T> where S and T are not equivalent types.

The "single part type of S" is because of a static type like FutureOr<Future<String>> where D<..> implements Future<T1>, and solving for Future<T1> <: FutureOr<Future<String>> could yield either String and Future<String>, neither being more or less precise. If one of them is a supertype of the other (like for FutureOr<Future<Object>>), we could just normalize it to Future<Object>. Maybe we should normalize before solving?

Anyway, this might be a solution that doesn't imply inferring types for the raw type (which, as the diamond example shows, would change its meaning).

[eernstg]

Note that FooImpl is non-generic:

class FooImpl extends Foo<int> {...}

so we don't have anything like FooImpl<T> <: Foo<T>, and FooImpl <: Foo<T> is not provable. So that's already one of those non-trivial examples.