better detection of early solve failure

Summary: In expand_type_and_solve, we detect whether we solve invariant type variables to nothing. The logic however is brittle. For example, if the type at hand is (#1 & nonnull) and #1 gets solved to nothing, it would fail to detect it, and therefore fail to fail. Same goes if the type at hand is (#1 | #2).

Reviewed By: andrewjkennedy

Differential Revision: D18635991

fbshipit-source-id: 33ce9d1b0630b1a8bf01ecdccf8d05363ce16072

hphp/hack/src/typing/typing_solver.ml

@@ -725,6 +725,33 @@ let solve_all_unsolved_tyvars_gi env make_on_error =
     env.tvenv
     env
 
+let unsolved_invariant_tyvars_under_union_and_intersection env ty =
+  let rec find_tyvars (env, tyvars) ty =
+    let (env, ty) = Env.expand_type env ty in
+    match ty with
+    | (r, Tvar v) ->
+      let tyvars =
+        if
+          Env.get_tyvar_appears_invariantly env v
+          || TypecheckerOptions.new_inference_lambda (Env.get_tcopt env)
+        then
+          (r, v) :: tyvars
+        else
+          tyvars
+      in
+      (env, tyvars)
+    | (_, Toption ty) -> find_tyvars (env, tyvars) ty
+    | (_, Tunion tyl)
+    | (_, Tintersection tyl) ->
+      List.fold tyl ~init:(env, tyvars) ~f:find_tyvars
+    | ( _,
+        ( Terr | Tany _ | Tdynamic | Tnonnull | Tprim _ | Tclass _ | Tobject
+        | Tabstract _ | Tarraykind _ | Ttuple _ | Tshape _ | Tfun _ | Tanon _
+        | Tpu _ | Tpu_access _ ) ) ->
+      (env, tyvars)
+  in
+  find_tyvars (env, []) ty
+
 (* Expand an already-solved type variable, and solve an unsolved type variable
  * by binding it to the union of its lower bounds, with covariant and contravariant
  * components of the type suitably "freshened". For example,
@@ -733,22 +760,25 @@ let solve_all_unsolved_tyvars_gi env make_on_error =
  *    #1 := vec<#2>  where C <: #2
  *)
 let expand_type_and_solve env ~description_of_expected p ty on_error =
+  let (env, unsolved_invariant_tyvars) =
+    unsolved_invariant_tyvars_under_union_and_intersection env ty
+  in
   let (env', ety) =
     Typing_utils.simplify_unions env ty ~on_tyvar:(fun env r v ->
         let env = always_solve_tyvar ~freshen:true env r v on_error in
         Env.expand_var env r v)
   in
   let (env', ety) = Env.expand_type env' ety in
-  match (ty, ety) with
-  | ((r, Tvar v), (_, Tunion []))
-    when (not (Env.tyvar_is_solved env v))
-         && ( Env.get_tyvar_appears_invariantly env v
-            || TypecheckerOptions.new_inference_lambda (Env.get_tcopt env) ) ->
-    Errors.unknown_type
-      description_of_expected
-      p
-      (Reason.to_string "It is unknown" r);
-    let env = Env.set_tyvar_eager_solve_fail env v in
+  match (unsolved_invariant_tyvars, ety) with
+  | (_ :: _, (_, Tunion [])) ->
+    let env =
+      List.fold unsolved_invariant_tyvars ~init:env ~f:(fun env (r, v) ->
+          Errors.unknown_type
+            description_of_expected
+            p
+            (Reason.to_string "It is unknown" r);
+          Env.set_tyvar_eager_solve_fail env v)
+    in
     (env, (Reason.Rsolve_fail p, TUtils.terr env))
   | _ -> (env', ety)
 

hphp/hack/test/typecheck/early_solve_inter.php

@@ -0,0 +1,16 @@
+<?hh
+
+function test(Vector<int> $v): void {
+  $m = Map {};
+
+  foreach ($v as $i) {
+    if ($m->containsKey("a")) {
+      $current_m = $m->get("a");
+      if ($current_m !== null) {
+        $current_m->add($i);
+      }
+    } else {
+      $m["a"] = Vector {$i};
+    }
+  }
+}

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

@@ -0,0 +1,6 @@
+File "early_solve_inter.php", line 10, characters 9-18:
+Was expecting an object but type is unknown (Typing[4297])
+File "early_solve_inter.php", line 4, characters 8-13:
+It is unknown because type parameter Tv of HH\Map could not be determined. Please add explicit type parameters to the invocation of HH\Map
+File "collections/Map.hhi", line 475, characters 32-33:
+  via this generic Tv

hphp/hack/test/typecheck/early_solve_inter.php.like_types.exp

@@ -0,0 +1,8 @@
+File "early_solve_inter.php", line 13, characters 7-27:
+Invalid assignment (Typing[4110])
+File "early_solve_inter.php", line 4, characters 8-13:
+Expected nothing because type parameter Tv of HH\Map could not be determined. Please add explicit type parameters to the invocation of HH\Map
+File "collections/Map.hhi", line 475, characters 32-33:
+  via this generic Tv
+File "early_solve_inter.php", line 13, characters 17-27:
+But got Vector<[unresolved]>

hphp/hack/test/typecheck/early_solve_inter2.php

@@ -0,0 +1,16 @@
+<?hh
+
+function test(Vector<int> $v): void {
+  $m = Map {};
+
+  foreach ($v as $i) {
+    if ($m->containsKey("a")) {
+      $current_m = $m->get("a");
+      if ($current_m is nonnull) {
+        $current_m->add($i);
+      }
+    } else {
+      $m["a"] = Vector {$i};
+    }
+  }
+}

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

@@ -0,0 +1,6 @@
+File "early_solve_inter2.php", line 10, characters 9-18:
+Was expecting an object but type is unknown (Typing[4297])
+File "early_solve_inter2.php", line 4, characters 8-13:
+It is unknown because type parameter Tv of HH\Map could not be determined. Please add explicit type parameters to the invocation of HH\Map
+File "collections/Map.hhi", line 475, characters 32-33:
+  via this generic Tv

hphp/hack/test/typecheck/early_solve_inter2.php.like_types.exp

@@ -0,0 +1,8 @@
+File "early_solve_inter2.php", line 13, characters 7-27:
+Invalid assignment (Typing[4110])
+File "early_solve_inter2.php", line 4, characters 8-13:
+Expected nothing because type parameter Tv of HH\Map could not be determined. Please add explicit type parameters to the invocation of HH\Map
+File "collections/Map.hhi", line 475, characters 32-33:
+  via this generic Tv
+File "early_solve_inter2.php", line 13, characters 17-27:
+But got Vector<[unresolved]>