Flow doesn't detect exhaustive type refinement

[samwgoldman]

In the example below, flow infers ?string when the actual return type is string. This isn't so bad, because you can easily turn the last else if into an else and get the same refinement and the correct inferred return type.

There's no reason flow can't catch this, and even complain about subsequent code being dead. (Edit: There is a fairly good reason, which is that the type of abc might be something other than ABC at runtime, due to any or interaction with untyped code. It would be unfortunate if Flow told you to remove code which actually caused a runtime exception!)

This is a good issue for someone trying to get their hands dirty with the type checker internals. I'd be happy to help anyone get oriented around this code if they want to take it on, or else I'll look into it in a couple weeks.

class A {}
class B {}
class C {}

type ABC = A | B | C;

function f(abc: ABC): string {
    if (abc instanceof A) {
        return 'A result';
    } else if (abc instanceof B) {
        return 'B result';
    } else if (abc instanceof C) {
        return 'C result';
    }
}

[samwgoldman]

Looking into this, I also found a little related bug:

function f(abc: string): string {
  if (typeof abc === "string") {
    return 'A result';
  } else {
    abc.foobar() // should error! abc is UndefT!
    return 'B result';
  }
}

(Edit: I was wrong about this. abc is empty in the else clause, and any use of empty is not a type error.)

[osnr]

Thanks for the tip on 'else'. This hack seems to make sure the refinement stays exhaustive if you add more types to the union:

function f(abc: ABC): string {
    if (abc instanceof A) {
        return 'A result';
    } else if (abc instanceof B) {
        return 'B result';
    } else { (abc : C);
        return 'C result';
    }
}

I might be interested in looking into the type checker code for this -- pointers?

[samwgoldman]

@osnr Cool! You'll want to start looking there the type checker refines types within conditional blocks.

Look closely at Type_inference_js.predicate_of_condition and Env_js.refine_with_pred to see what is going on. At a very high level, predicate_of_condition returns information that a given binding is a specific type, and refine_with_pred installs that refined type into Env_js.env, some shared mutable state.

Note that returning from a block has type inference implications. If we return from then "then" block, then the rest of the function can assume the inverse of the predicate from the "test" condition. This is really where this issue comes in. Each time we return from a test block, we can refine the env with the inverse of each test's predicate. If all those inverse predicates add up to "nothing," then the code is dead from that point on (I think, it's probably more nuanced).