avoid creating too many type variables in expand_type_and_narrow

Summary:
This diff is all about using Typing_union.simplify_unions instead of get_union_elements.

Why does it make things better ?
Suppose you have type variables like:
```
vec<int> <: #1 <: #2
```
Since we transitively close, we'll get a constraint graph like:
```
vec<int> <: #1
vec<int>, #1 <: #2
```
get_union_elements was implemented in such a way that calling in on #2 would get vec<int> twice, resulting in the widened type being (vec<#3> | vec<#4). You can see how this causes a explosion of type variables for bigger, transitively closed, constraint graphs.

Reviewed By: andrewjkennedy

Differential Revision: D15149670

fbshipit-source-id: d74e3f0cc35de755025da087bda7606376206531

hphp/hack/src/typing/typing_subtype.ml

@@ -2711,56 +2711,34 @@ let expand_type_and_solve env ~description_of_expected p ty =
  * The `widen` function extends this to nullables and abstract types.
  * General unions have been dealt with already.
  *)
-let rec widen env widen_concrete_type ty =
-  let env, ty = Env.expand_type env ty in
-  match ty with
-   | r, Toption ty ->
-    begin match widen env widen_concrete_type ty with
-    | env, Some ty -> env, Some (r, Toption ty)
-    | env, None -> env, None
-    end
-  (* Don't widen the `this` type, because the field type changes up the hierarchy
-   * so we lose precision
-   *)
-  | _, Tabstract (AKdependent (`this, _), _) ->
-    env, Some ty
-  (* For other abstract types, just widen to the bound, if possible *)
-  | _, Tabstract (_, Some ty) ->
-    widen env widen_concrete_type ty
-  | _ ->
-    widen_concrete_type env ty
-
-(* Deconstruct a type into its union elements, if it's a union or nullable.
- * If any elements are type variables, take their lower bounds.
- * Return (has_var, nullable_reason, elements) where
- *   has_var = true if any union elements are type variables
- *   nullable_reason = Some r if there is a nullable/null element with reason r
- *   elements are the de-duplicated elements of the union
- *)
-let get_union_elements env ty =
-  let rec aux env tyl (has_var, nullable_reason, res) =
-  match tyl with
-  | [] -> env, has_var,
-      begin match nullable_reason with
-      | None -> res
-      | Some r -> MakeType.null r::res
-      end
-  | ty::tyl ->
-    let env, ety = Env.expand_type env ty in
-    match ety with
-    | _, Tunresolved tyl' ->
-      aux env (tyl' @ tyl) (has_var, nullable_reason, res)
+let widen env widen_concrete_type ty =
+  let rec widen env ty =
+    let env, ty = Env.expand_type env ty in
+    match ty with
+    | r, Tunresolved tyl ->
+      widen_all env r tyl
     | r, Toption ty ->
-      aux env (ty::tyl) (has_var, Some r, res)
-    | _, Tvar var ->
-      let tyvar_info = Env.get_tyvar_info env var in
-      (* Lower bounds of type variable, excluding itself *)
-      let lower_bounds = Typing_set.remove ety tyvar_info.Env.lower_bounds in
-      aux env tyl (true, nullable_reason, Typing_set.elements lower_bounds @ res)
+      widen_all env r [(r, Tprim Nast.Tnull); ty]
+    (* Don't widen the `this` type, because the field type changes up the hierarchy
+     * so we lose precision
+     *)
+    | _, Tabstract (AKdependent (`this, _), _) ->
+      env, ty
+    (* For other abstract types, just widen to the bound, if possible *)
+    | _, Tabstract (_, Some ty) ->
+      widen env ty
     | _ ->
-      aux env tyl (has_var, nullable_reason, ety::res)
-  in
-    aux env [ty] (false, None, [])
+      begin match widen_concrete_type env ty with
+      | env, Some ty -> env, ty
+      | env, None -> env, (Reason.none, Tunresolved [])
+      end
+  and widen_all env r tyl =
+    let env, tyl = List.fold_map tyl ~init:env ~f:widen in
+    Typing_union.union_list env r tyl in
+  widen env ty
+
+let is_nothing env ty =
+  is_sub_type_alt env ty (Reason.none, Tunresolved []) ~no_top_bottom:true = Some true
 
 (* Using the `widen_concrete_type` function to compute an upper bound,
  * narrow the constraints on a type that are valid for an operation.
@@ -2786,29 +2764,26 @@ let expand_type_and_narrow env ~description_of_expected widen_concrete_type p ty
    * take the lower bounds. If there are no variables, then we have a concrete
    * type so just return expanded type
    *)
-  let env, has_var, tys = get_union_elements env ty in
-  if not has_var
+  let has_tyvar = ref false in
+  let seen_tyvars = ref ISet.empty in
+  (* Simplify unions in ty, but when we encounter a type variable in the process,
+  recursively replace it with the union of its lower bounds, effectively getting
+  rid of all unsolved type variables in the union. *)
+  let env, concretized_ty = Typing_union.simplify_unions env ty ~on_tyvar:(fun env r v ->
+    has_tyvar := true;
+    if ISet.mem v !seen_tyvars then env, (r, Tunresolved []) else
+    let () = seen_tyvars := ISet.add v !seen_tyvars in
+    let lower_bounds = TySet.elements (Env.get_tyvar_lower_bounds env v) in
+    Typing_union.union_list env r lower_bounds) in
+  if not !has_tyvar
   then Typing_utils.simplify_unions env ty
   else
-  (* Now for each union element, use widen_concrete_type to suggest a concrete
-   * upper bound. *)
-    let rec widen_tys env tyl res =
-      match tyl with
-      | [] ->
-        env, res
-
-      | ty :: tyl ->
-        let env, opt_upper = widen env widen_concrete_type ty in
-        let res = match opt_upper with None -> res | Some ty -> ty :: res in
-        widen_tys env tyl res in
-
-    let env, widened_tys = widen_tys env tys [] in
+    let env, widened_ty = widen env widen_concrete_type concretized_ty in
     (* We really don't want to just guess `nothing` if none of the types can be widened *)
-    if List.is_empty widened_tys
+    if is_nothing env widened_ty
     (* Default behaviour is currently to force solve *)
     then expand_type_and_solve env ~description_of_expected p ty
     else
-    let env, widened_ty = TUtils.union_list env (fst ty) widened_tys in
       Errors.try_
         (fun () ->
           let env = sub_type env ty widened_ty in

hphp/hack/test/typecheck/append_blow.php

@@ -0,0 +1,15 @@
+<?hh // strict
+// Copyright 2004-present Facebook. All Rights Reserved.
+
+function test2(int $id): void {
+  $res = Map {};
+  $res[$id] = vec[1];
+  $res[$id][0] += 0;
+  $res[$id][1] += 0;
+  $res[$id][2] += 0;
+  $res[$id][3] += 0;
+  $res[$id][4] += 0;
+  $res[$id][5] += 0;
+  hh_force_solve();
+  hh_show($res);
+}

hphp/hack/test/typecheck/append_blow.php.exp

@@ -0,0 +1,3 @@
+File "append_blow.php", line 14, characters 3-15:
+  Map<int, vec<(int | int)>>
+No errors

hphp/hack/test/typecheck/append_blow.php.legacy.exp

@@ -0,0 +1,3 @@
+File "append_blow.php", line 14, characters 3-15:
+  Map<int, vec<int>>
+No errors