No error in CFE for promoted type variable of wrong type

[sgrekhov]

The code below produces compile-time error in analyzer and no issues in CFE

test<X>(X? x) {
  if (x is String?) {
    Object o = x; // Error in analyzer. A value of type 'X?' can't be assigned to a variable of type 'Object'
  }
}

main() {
  test<String>("");
}

If to remove if (x is String?) { from function test then CFE starts produce an error as well

Dart VM version: 2.9.0-11.0.dev (dev) (Tue May 26 12:14:57 2020 +0200) on "windows_x64"

[eernstg]

Interesting.

@johnniwinther, it looks like the CFE might create types of the form X? & T where X is a type variable. That may be a small step in the CFE, but it is not currently supported by https://github.com/dart-lang/language/blob/master/resources/type-system/subtyping.md, and it would presumably be a non-trivial change to the treatment of types.

[Edit: Some kind of promotion seems to happen, otherwise it shouldn't make a difference to remove if (x is String?); but if x is promoted to X? & String? then it's still an error to assign it to Object. So that can't be it. But it is not obvious what the CFE is doing.]

[vsmenon]

@eernstg - should we file this as a CFE issue or a language one?

[eernstg]

I suspect that it would be too big for a language issue (the implications could be substantial if we start generalizing promoted types to have other forms than X & T), so that would make it a CFE issue. I've mentioned this for the language team, so if there is a strong desire to go down that way then we can do that, but right now I think it should be CFE.

[lrhn]

I see no need for a language change.
The only thing that can be on the left of a & is a type variable, so X? & T is not a type, and there should be nothing in the specification introducing it.
The type (X & T)? seems more likely to be what you need. I even believe that is what promoting X? by is String? should do - although I admit I don't know where it's specified.

[leafpetersen]

The relevant portion of the spec is in flow-analysis.md:

- `promote(E, T, M)` where `E` is an expression, `T` is a type which it may be
  promoted to, and `M = FlowModel(r, VI)` is the flow model in which to promote,
  is defined as follows:
  - If `E` is not a promotion target, then `M`
  - If `E` is a promotion target `x`, then
    - Let `VM = VariableModel(declared, promoted, tested, assigned, unassigned,
      captured)` be the variable model for `x` in `VI`
    - If `x` is not promotable via type test to `T` given `VM`, then return `M`
    - Else
      - Let `S` be the current type of `x` in `VM`
      - If `T <: S` then let `T1` = `T`
      - Else if `S` is `X extends R` then let `T1` = `X & T`
      - Else If `S` is `X & R` then let `T1` = `X & T`
      - Else `x` is not promotable (shouldn't happen since we checked above)
      - Let `VM2 = VariableModel(declared, T1::promoted, T1::tested, assigned,
      unassigned, captured)`
      - Return `FlowModel(r, VI[x -> VM2])`

There is no promotion specified to happen in this case, and in fact, the CFE seems to be going completely off the rails here. The following program runs in the CFE and calls .length on null.

test<X>(X? x) {
  if (x is String?) {
    Object o = x; // Error in analyzer. A value of type 'X?' can't be assigned to a variable of type 'Object'
    x.length;
  }
}

main() {
  test<String>(null);
}

[lrhn]

Would we want to be able to promote Something<X> to Something<X & SpecificType> (where Something is a type constructor, not limited to generic classes)?

That could account for

foo<X extends Object>(X? x) { 
   if (x is String?) ... /* x is (X & String)? */ 
}

(There are probably lots of issues with that, but it looks so plausible that users might expect it to work).

[leafpetersen]

Would we want to be able to promote Something<X> to Something<X & SpecificType> (where Something is a type constructor, not limited to generic classes)?

We could push on it. It hasn't come up in migrations yet, and the ship is sailing, so I think this is probably not making it into v1.