Front-end UP of promoted type variables does not behave correctly.

[lrhn]

Example:

void main() { foo<Object>(false, D(), D()); }
void foo<X>(bool not, X b, X c) {
  if (b is! B) return;
  // Promoted to X&B. Proof:
  {
    X v1 = b;
    B v2 = b;  
  }
  if (c is! C) return;
  // Promoted to X&C
  { 
    X v1 = c;
    C v2 = c;
  }
  var bc = not ? b : c;
  // BY THE RULES, UP(X&B, X&C) which is X.
  // THE RULES are:
  //
  // UP(X1 & B1, T2) =
  // * T2 if X1 <: T2
  // * otherwise X1 if T2 <: X1
  // * otherwise UP(B1a, T2) where B1a is the greatest closure of B1 with respect to
  //    X1, as defined in inference.md.
  //
  //  Here X1 is X, B1 is B, T2 is (X & C)
  //     * X <: X&C  - not true,
  //     * X&C <: X - true!, so result is X.  
  //        (Analyzer fails here, goes on to next step, computes UP(B, T&C) and gets A).
  // So declared and static type of bc is `X`, with no further promotion.

  // Front-end *agrees*
  {
    X v1 = bc; // bc assignable to X.
    // B v2 = bc; // Error in front-end
    // C v3 = bc; // Error in front-end
    if (not) {
      // BUT!
      bc = 0 as X;  // X assignable to bc.
      // Get error here saying that X is nullable and X is not. 
      throw "never got here, never go back"; // Don't flow demotion back.
    }
  }
  // But it's not the X you expect?

  bc.st<E<X>>; // Requires (reified as type argument) static type of `v` to be exactly X.
  St(bc).st<E<X>>; 
  Rt(bc).rt<E<X>>;
}

// Diamond hierarchy
class A {}
class B implements A {}
class C implements A {}
class D implements B, C {}

// Static type-checking helper.
typedef E<T> = T Function(T);
extension St<T> on T {
  void st<T2 extends E<T>>(){}
}
// Non-extension based static type checker.
// (In case we thought it was just extensions being wrong.)
class Rt<T> { 
  Rt(T t);
  void rt<T2 extends E<T>>() {}
}

When compiled in DartPad, I get the following errors:

Error: A value of type 'X' can't be assigned to a variable of type 'X' because 'X' is nullable and 'X' isn't.
      bc = 0 as X;  // X assignable to bc.
             ^
lib/main.dart:45:8:
Error: Type argument 'X Function(X)' doesn't conform to the bound 'X Function(X)' of the type variable 'T2' on 'void Function<T2 extends X Function(X)>()'.
  bc.st<E<X>>; // Requires (reified as type argument) static type of `v` to be exactly X.
       ^
lib/main.dart:46:12:
Error: Type argument 'X Function(X)' doesn't conform to the bound 'X Function(X)' of the type variable 'T2' on 'void Function<T2 extends X Function(X)>()'.
  St(bc).st<E<X>>; 
           ^
lib/main.dart:47:12:
Error: Type argument 'X Function(X)' doesn't conform to the bound 'X Function(X)' of the type variable 'T2' on 'void Function<T2 extends X Function(X)>()'.
  Rt(bc).rt<E<X>>;
           ^

This suggests that the result of UP(X&B, X&C) is a kind of "X & Object", with the "may be nullable" flag turned off (which makes a kind of sense because X&B and X&C are both non-nullable), without it actually being an intersection type.
It differs from the real X type.

Now add to the above:

void bar<X>(bool not, X b, X c) { // Or a `?` to one of the `X`s, shoudn't change anything.
  if (b is! B) return;
  {
     X v1 = b;
     B v2 = b; 
  }
  if (c is! B) return; // Sames as above.
  {
     X v1 = c;
     B v2 = c; 
  }
  var bc = not ? b : c;  // Type is UP(X&B,X&B) = X&B.
  // RULE THE FIRST of UP:
  //  UP(T, T) = T
  // Here we do UP(X&B, X&B), which is *the same type*, so we should
  // get X&B as result.
  X v1 = bc; // Allowed
  B v2 = bc; // Fails on front-end. Seems to use X as type.
  // C v3 = bc; // Not allowed. Correct.
  
  bc.st<E<X>>; // Stull fails with X != X
  St(bc).st<E<X>>;
  Rt(bc).rt<E<X>>;
}

and we get the same errors of X is not X,
and the UP(X&B, X&B) appears to X, not X&B, which it should be by the (very first) reflexivity rule of UP: "UP(T, T) = T":

lib/main.dart:85:10:
Error: A value of type 'X' can't be assigned to a variable of type 'B'.
 - 'B' is from 'package:dartpad_sample/main.dart' ('lib/main.dart').
  B v2 = bc; // Fails on front-end. Seems to use X as type.
         ^
lib/main.dart:88:8:
Error: Type argument 'X Function(X)' doesn't conform to the bound 'X Function(X)' of the type variable 'T2' on 'void Function<T2 extends X Function(X)>()'.
  bc.st<E<X>>; // Stull fails with X != X
       ^
lib/main.dart:89:12:
Error: Type argument 'X Function(X)' doesn't conform to the bound 'X Function(X)' of the type variable 'T2' on 'void Function<T2 extends X Function(X)>()'.
  St(bc).st<E<X>>;
           ^
lib/main.dart:90:12:
Error: Type argument 'X Function(X)' doesn't conform to the bound 'X Function(X)' of the type variable 'T2' on 'void Function<T2 extends X Function(X)>()'.
  Rt(bc).rt<E<X>>;
           ^

So, UP of promoted type variables is not doing the right thing, in two ways:

• UP(X&B, X&B) does not become X&B
• UP(X&B, X&C) does yield "X", but an "X" that the real X is not a assignable to, because the latter may be null and the former not. It's like a NON_NULL(X) type, which is not an intersection type X&Object, because it's reified as type argument.

[eernstg]

It looks like the X which is obtained as the declared type of b or c has a different nullability than the X which is the result obtained from UP(X&B, X&C). Perhaps the former is undetermined and the latter is nonNullable, because null has been ruled out by the tests that gave rise to the type X&B and the type X&C.

This seems to be consistent with the behavior of the CFE when we change bc = 0 as X; to bc = (0 as X)!;. When other errors have been commented out (the static type checks using E<X> below), the VM runs the program with no issues.

An underlying difficulty here could be that the nullability of types has been modeled using a bit on the DartType. So what's the correct way to compute the nullability bit in this case? We want X to be considered potentially nullable in the first place, but X & B as well as X & C should be non-nullable. So if a TypeParameterType turns out to be an intersection type (is that the way it's modeled?), the nullability should probably be computed based on the right operand of the intersection. If that's a non-nullable type then the intersection type is non-nullable, even in the case where the nullability value of the type is undetermined.

(If the type variable X is already non-nullable because it has a bound which is Object or a subtype thereof then it will never be promoted to X & T for any type T which isn't non-nullable.)

[lrhn]

Sounds reasonable.

There is only one X type, which has undetermined nullability. The type of bc should be X, since that's UP(X&B, X&C), and it should be the one X type, and any X should be assignable to or from bc.

(Even if we got smarter and inferred X & UP(B, C), aka. X & A, the declared type of bc would still be X. It would just be immediately assignment promoted to X & A again.)

[chloestefantsova]

if a TypeParameterType turns out to be an intersection type (is that the way it's modeled?)

That was the way we represented intersection types before. We have a dedicated IntersectionType for that now, but the left-hand side of it can only be a TypeParameterType.