Refinement with instanceof and generic unions is unsound

[wchargin]

If x: T | MyClass<T>, then Flow infers from x instanceof MyClass
that x: MyClass<T>. This is unsound: T could be MyClass<U> for
some other U, so that in fact x: MyClass<MyClass<U>>.

Here is an example of how this can go wrong:

// @flow
class Box<T> {
  +field: T;
  constructor(x) {
    this.field = x;
  }
}

function asBox<T>(x: T | Box<T>): Box<T> {
  if (x instanceof Box) {
    // Here, `x` is refined to be `Box<T>`. This is unsound: `T` could
    // well be `Box<U>` for some other `U`. Example below.
    return x;
  } else {
    // whatever
    return new Box(x);
  }
}

const stringStringBox: Box<Box<string>> = asBox(new Box("wat"));  // unsound!
stringStringBox.field.field.substr(0);  // runtime error

[wchargin]

Needless to say, this yields coerce:

// @flow
function coerce<T, U>(t: T): U {
  class B<X> {
    x: X;
    constructor(x) {
      this.x = x;
    }
  }
  function b<X>(x: X | B<X>): B<X> {
    if (x instanceof B) return x;
    else throw new Error("Unreachable.");
  }
  const bb: B<B<{t: T}>> = b(new B({t}));
  if (!(bb.x instanceof B)) {
    return bb.x.t;
  }
  throw new Error("Unreachable.");
}
const twelve: number = coerce("twelve");

[jbrown215]

cc @samwgoldman

[jbrown215]

After speaking to @samwgoldman , we think it's possible that we are refining x to Box<any>. I'll take a look at this!

Thank you for reporting, @wchargin!

[samwgoldman]

Yeah, see

flow/src/typing/flow_js.ml

Line 3995 in 7057f04

| PredicateT ((RightP (InstanceofTest, _) | NotP (RightP (InstanceofTest, _))), _) ->

Worth experimenting with using instantiate_poly instead, which creates an implicit type argument (i.e., some fresh tvar instead of any). But I haven't thought about this very hard and I wonder about perf.

[wchargin]

Worth experimenting with using instantiate_poly instead, which creates an implicit type argument (i.e., some fresh tvar instead of any).

Makes sense; this sounds like the right semantics.

It would be nice for string | Box<T> to be refined to Box<T> instead of Box<?> under an instanceof check; it’s not clear to me whether instantiate_poly would admit that. But if it’s a tradeoff between that incompleteness and this unsoundness, I’d happily take the incompleteness.