fate of the union (a.k.a. the roads not taken)

Summary:
This diff re-implements how union (and intersection) types are checked in Flow,
fixing serious bugs in the current system.

The problem
===========

Flow's inference engine is designed to find more errors over time as constraints
are added...but it is not designed to backtrack. Unfortunately, checking the
type of an expression against a union type does need backtracking: if some
branch of the union doesn't work out, the next branch must be tried, and so
on. The situation is further complicated by the fact that the type of the
expression may be unknown at the point of checking, so that a branch that looks
promising now might turn out to be incorrect later.

The solution
============

The basic idea is to delay trying a branch until a point where we can decide
whether the branch will definitely fail or succeed, without adding
constraints. If trying the branch results in failure, we can move on to the next
branch without needing to backtrack. If the branch succeeds, we are done. The
final case is where the branch looks promising, but we cannot be sure without
adding constraints: in this case we try other branches, and *bail* when we run
into ambiguities...requesting additional annotations to decide which branch to
select. Overall, this means that (1) we never commit to a branch that might turn
out to be incorrect and (2) can always select a correct branch (if such exists)
given enough annotations.

As a matter of implementation, we need to distinguish between annotations and
inferred types for this scheme to work: in particular, we fully resolve
annotations before branches are tried, and then use whatever partial information
we can obtain from inferred types to disambiguate those branches.

Fixes #1759
Fixes #1664
Fixes #1663
Fixes #1462
Fixes #1455
Fixes #1371
Fixes #1349
Fixes #824
Fixes #815

Reviewed By: bhosmer

Differential Revision: D3229344

fbshipit-source-id: 64da005f4a7eaa4b6a8c74c535b27ab24c7b80bc

lib/core.js

@@ -196,20 +196,22 @@ declare class Array<T> {
     map<U>(callbackfn: (value: T, index: number, array: Array<T>) => U, thisArg?: any): Array<U>;
     pop(): T;
     push(...items: Array<T>): number;
+    reduce(
+      callbackfn: (previousValue: T, currentValue: T, currentIndex: number, array: Array<T>) => T,
+      initialValue: void
+    ): T;
     reduce<U>(
       callbackfn: (previousValue: U, currentValue: T, currentIndex: number, array: Array<T>) => U,
       initialValue: U
     ): U;
-    reduce<U>(
-      callbackfn: (previousValue: T|U, currentValue: T, currentIndex: number, array: Array<T>) => U
-    ): U;
+    reduceRight(
+      callbackfn: (previousValue: T, currentValue: T, currentIndex: number, array: Array<T>) => T,
+      initialValue: void
+    ): T;
     reduceRight<U>(
       callbackfn: (previousValue: U, currentValue: T, currentIndex: number, array: Array<T>) => U,
       initialValue: U
     ): U;
-    reduceRight<U>(
-      callbackfn: (previousValue: T|U, currentValue: T, currentIndex: number, array: Array<T>) => U
-    ): U;
     reverse(): Array<T>;
     shift(): T;
     slice(start?: number, end?: number): Array<T>;
@@ -421,10 +423,7 @@ interface Generator<+Yield,+Return,-Next> {
 
 declare class Map<K, V> {
     @@iterator(): Iterator<[K, V]>;
-    constructor<Key, Value>(_: void): Map<Key, Value>;
-    constructor<Key, Value>(_: null): Map<Key, Value>;
-    constructor<Key, Value>(iterable: Array<[Key, Value]>): Map<Key, Value>;
-    constructor<Key, Value>(iterable: Iterable<[Key, Value]>): Map<Key, Value>;
+    constructor(iterable: ?Iterable<[K, V]>): void;
     clear(): void;
     delete(key: K): boolean;
     entries(): Iterator<[K, V]>;
@@ -462,9 +461,7 @@ declare class Set<T> {
 }
 
 declare class WeakSet<T: Object> {
-    constructor<V: Object>(_: void): WeakSet<V>;
-    constructor<V: Object>(iterable: Array<V>): WeakSet<V>;
-    constructor<V: Object>(iterable: Iterable<V>): WeakSet<V>;
+    constructor(iterable?: Iterable<T>): void;
     add(value: T): WeakSet<T>;
     delete(value: T): boolean;
     has(value: T): boolean;
@@ -549,22 +546,22 @@ declare class $TypedArray {
     keys(): Array<number>;
     lastIndexOf(searchElement: number, fromIndex?: number): number; // -1 if not present
     map(callback: (currentValue: number, index: number, array: this) => number, thisArg?: any): this;
+    reduce(
+      callback: (previousValue: number, currentValue: number, index: number, array: this) => number,
+      initialValue: void
+    ): number;
     reduce<U>(
       callback: (previousValue: U, currentValue: number, index: number, array: this) => U,
       initialValue: U
     ): U;
-    reduce<U>(
-      callback: (previousValue: number|U, currentValue: number, index: number, array: this) => U,
+    reduceRight(
+      callback: (previousValue: number, currentValue: number, index: number, array: this) => number,
       initialValue: void
-    ): U;
+    ): number;
     reduceRight<U>(
       callback: (previousValue: U, currentValue: number, index: number, array: this) => U,
       initialValue: U
     ): U;
-    reduceRight<U>(
-      callback: (previousValue: number|U, currentValue: number, index: number, array: this) => U,
-      initialValue: void
-    ): U;
     reverse(): this;
     set(array: Array<number> | $TypedArray, offset?: number): void;
     slice(begin?: number, end?: number): this;

src/common/reason_js.ml

@@ -216,6 +216,54 @@ let is_internal_module_name name =
 let internal_pattern_name loc =
   spf ".$pattern__%s" (string_of_loc loc)
 
+let typeparam_prefix s =
+  spf "type parameter%s" s
+
+let has_typeparam_prefix s =
+  Utils.str_starts_with s "type parameter"
+
+let thistype_desc = "`this` type"
+let existential_desc = "existential"
+
+(* Instantiable reasons identify tvars that are created for the purpose of
+   instantiation: they are fresh rather than shared, and should become types
+   that flow to them. We assume these characteristics when performing
+   speculative matching (even though we don't yet enforce them). *)
+let is_instantiable_reason r =
+  let desc = desc_of_reason r in
+  has_typeparam_prefix desc
+  || desc = thistype_desc
+  || desc = existential_desc
+
+(* TODO: Property accesses create unresolved tvars to hold results, even when
+   the object(s) on which the property accesses happen may be resolved. This can
+   and should be fixed, for various benefits including but not limited to more
+   precise type inference. But meanwhile we need to consider results of property
+   accesses that might result in sentinel property values as constants to decide
+   membership in disjoint unions, instead of asking for unnecessary annotations
+   to make progress. According to Facebook's style guide, constant properties
+   should have names like CONSTANT_PROPERTY, so we bet that when properties with
+   such names are accessed, their types have the 0->1 property.
+
+   As an example, suppose that we have an object `Tags` that stores tags of a
+   disjoint union, e.g. { ACTION_FOO: 'foo', ACTION_BAR: 'bar' }.
+
+   Then the types of Tags.ACTION_FOO and Tags.ACTION_BAR are assumed to be 0->1.
+*)
+let is_constant_property_reason r =
+  let desc = desc_of_reason r in
+  let property_prefix = "property `" in
+  Utils.str_starts_with desc property_prefix &&
+    let i = String.length property_prefix in
+    let j = String.index_from desc (i+1) '`' in
+    let property_name = String.sub desc i (j-i) in
+    try
+      String.iter (fun c ->
+        assert (c = '_' || Char.uppercase c = c)
+      ) property_name;
+      true
+    with _ -> false
+
 let is_derivable_reason r =
   r.derivable
 
@@ -243,10 +291,6 @@ let is_blamable_reason r =
 let reasons_overlap r1 r2 =
   Loc.(contains r1.loc r2.loc)
 
-(* reasons compare on their locations *)
-let compare r1 r2 =
-  Pervasives.compare (loc_of_reason r1) (loc_of_reason r2)
-
 (* reason transformers: *)
 
 (* returns reason whose description is prefix-extension of original *)
@@ -270,7 +314,7 @@ let replace_reason replacement reason =
 
 (* returns reason with new location and description of original *)
 let repos_reason loc reason =
-  mk_reason (desc_of_reason reason) loc
+  mk_reason_with_test_id reason.test_id (desc_of_reason reason) loc
 
 (* helper: strip root from positions *)
 let strip_root_from_loc root loc = Loc.(

src/common/reason_js.mli

@@ -39,6 +39,14 @@ val internal_module_name: string -> string
 
 val internal_pattern_name: Loc.t -> string
 
+val typeparam_prefix: string -> string
+val has_typeparam_prefix: string -> bool
+val thistype_desc: string
+val existential_desc: string
+val is_instantiable_reason: reason -> bool
+
+val is_constant_property_reason: reason -> bool
+
 val derivable_reason: reason -> reason
 val is_derivable_reason: reason -> bool
 
@@ -71,8 +79,6 @@ val replace_reason: string -> reason -> reason
 
 val repos_reason: Loc.t -> reason -> reason
 
-val compare: reason -> reason -> int
-
 val do_patch: string list -> (int * int * string) list -> string
 
 val strip_root: Path.t -> reason -> reason

src/services/inference/infer_service.ml

@@ -48,10 +48,11 @@ let infer_module ~options ~metadata filename =
 let infer_job ~options (inferred, errsets, errsuppressions) files =
   let metadata = Context.metadata_of_options options in
   List.fold_left (fun (inferred, errsets, errsuppressions) file ->
+    let file_str = string_of_filename file in
     try Profile_utils.checktime ~options 1.0
-      (fun t -> spf "perf: inferred %s in %f" (string_of_filename file) t)
+      (fun t -> spf "perf: inferred %s in %f" file_str t)
       (fun () ->
-        (*prerr_endlinef "[%d] INFER: %s" (Unix.getpid()) file;*)
+        (* prerr_endlinef "[%d] INFER: %s" (Unix.getpid()) file_str; *)
 
         (* infer produces a context for this module *)
         let cx = infer_module ~options ~metadata file in

src/services/inference/merge_service.ml

@@ -170,7 +170,7 @@ let merge_strict_job ~options (merged, errsets) (components: filename list list)
     try Profile_utils.checktime ~options 1.0
       (fun t -> spf "[%d] perf: merged %s in %f" (Unix.getpid()) files t)
       (fun () ->
-        (*prerr_endlinef "[%d] MERGE: %s" (Unix.getpid()) file;*)
+        (* prerr_endlinef "[%d] MERGE: %s" (Unix.getpid()) files; *)
         let file, errors = merge_strict_component ~options component in
         file :: merged, errors :: errsets
       )

src/services/inference/types_js.ml

@@ -210,7 +210,6 @@ let typecheck_contents ~options ?verbose contents filename =
       (* should never happen *)
       timing, None, errors, info
 
-
 (* commit newly inferred and removed modules, collect errors. *)
 let commit_modules workers ~options inferred removed =
   let errmap = Module_js.commit_modules workers ~options inferred removed in

src/typing/class_sig.ml

@@ -264,7 +264,7 @@ let add_this self cx reason tparams tparams_map =
   in
   let this_tp = { Type.
     name = "this";
-    reason = replace_reason "`this` type" reason;
+    reason = replace_reason thistype_desc reason;
     bound = rec_instance_type;
     polarity = Type.Positive;
     default = None;

src/typing/context.ml

@@ -51,6 +51,12 @@ type t = {
   (* map from evaluation ids to types *)
   mutable evaluated: Type.t IMap.t;
 
+  (* graph tracking full resolution of types *)
+  mutable type_graph: Graph_explorer.graph;
+
+  (* map of speculation ids to sets of unresolved tvars *)
+  mutable all_unresolved: Type.TypeSet.t IMap.t;
+
   (* map from frame ids to env snapshots *)
   mutable envs: env IMap.t;
 
@@ -114,6 +120,8 @@ let make metadata file module_name = {
   envs = IMap.empty;
   property_maps = IMap.empty;
   evaluated = IMap.empty;
+  type_graph = Graph_explorer.new_graph ISet.empty;
+  all_unresolved = IMap.empty;
   modulemap = SMap.empty;
 
   errors = Errors_js.ErrorSet.empty;
@@ -128,6 +136,7 @@ let make metadata file module_name = {
 }
 
 (* accessors *)
+let all_unresolved cx = cx.all_unresolved
 let annot_table cx = cx.annot_table
 let envs cx = cx.envs
 let enable_const_params cx = cx.metadata.enable_const_params
@@ -167,6 +176,7 @@ let should_munge_underscores cx  = cx.metadata.munge_underscores
 let should_strip_root cx = cx.metadata.strip_root
 let suppress_comments cx = cx.metadata.suppress_comments
 let suppress_types cx = cx.metadata.suppress_types
+let type_graph cx = cx.type_graph
 let type_table cx = cx.type_table
 let verbose cx = cx.metadata.verbose
 
@@ -200,6 +210,8 @@ let remove_all_error_suppressions cx =
   cx.error_suppressions <- Errors_js.ErrorSuppressions.empty
 let remove_tvar cx id =
   cx.graph <- IMap.remove id cx.graph
+let set_all_unresolved cx all_unresolved =
+  cx.all_unresolved <- all_unresolved
 let set_envs cx envs =
   cx.envs <- envs
 let set_evaluated cx evaluated =
@@ -214,6 +226,8 @@ let set_module_exports_type cx module_exports_type =
   cx.module_exports_type <- module_exports_type
 let set_property_maps cx property_maps =
   cx.property_maps <- property_maps
+let set_type_graph cx type_graph =
+  cx.type_graph <- type_graph
 let set_tvar cx id node =
   cx.graph <- IMap.add id node cx.graph
 
@@ -235,5 +249,7 @@ let merge_into cx cx_other =
   set_envs cx (IMap.union (envs cx_other) (envs cx));
   set_property_maps cx (IMap.union (property_maps cx_other) (property_maps cx));
   set_evaluated cx (IMap.union (evaluated cx_other) (evaluated cx));
+  set_type_graph cx (Graph_explorer.union_finished (type_graph cx_other) (type_graph cx));
+  set_all_unresolved cx (IMap.union (all_unresolved cx_other) (all_unresolved cx));
   set_globals cx (SSet.union (globals cx_other) (globals cx));
   set_graph cx (IMap.union (graph cx_other) (graph cx))

src/typing/context.mli

@@ -39,6 +39,7 @@ val make: metadata -> Loc.filename -> Modulename.t -> t
 val metadata_of_options: Options.t -> metadata
 
 (* accessors *)
+val all_unresolved: t -> Type.TypeSet.t IMap.t
 val annot_table: t -> (Loc.t, Type.t) Hashtbl.t
 val enable_const_params: t -> bool
 val enable_unsafe_getters_and_setters: t -> bool
@@ -74,6 +75,7 @@ val should_munge_underscores: t -> bool
 val should_strip_root: t -> bool
 val suppress_comments: t -> Str.regexp list
 val suppress_types: t -> SSet.t
+val type_graph: t -> Graph_explorer.graph
 val type_table: t -> (Loc.t, Type.t) Hashtbl.t
 val verbose: t -> int option
 
@@ -94,6 +96,8 @@ val remove_all_error_suppressions: t -> unit
 val remove_tvar: t -> Constraint_js.ident -> unit
 val set_envs: t -> env IMap.t -> unit
 val set_evaluated: t  -> Type.t IMap.t -> unit
+val set_type_graph: t  -> Graph_explorer.graph -> unit
+val set_all_unresolved: t  -> Type.TypeSet.t IMap.t -> unit
 val set_globals: t -> SSet.t -> unit
 val set_graph: t -> Constraint_js.node IMap.t -> unit
 val set_in_declare_module: t -> bool -> unit