[flow] negation consistency check for type guards

Summary:
Today’s [consistency check](https://flow.org/en/docs/types/type-guards/#predicate-type-is-consistent-with-refined-type) guarantees that the refinement happening in the then-branch is safe. It does not prove correct, however, the refinement in the else-branch. For example, consider
```
function isPositive(value: mixed): value is number {
  return typeof value === "number" && value > 0; // no error here
}
```
If we use this type guard in an if-then-else, we'll notice that `x` is refined in both the then- and else-branches:
```
function bar(x: number | string) {
  if (isPositive(x)) {
    // x is number here -- okay
  } else {
    // x is string here -- BUG
  }
}
```
Here we mistakenly infer that `x` is `string` in the else branch.

This diff implements a fix for this soundness hole: a check that ensures that the type guard after being applied the negation of the function predicate is refined down to the empty type.

For `isPositive` this check will fail because `number` refined with the negation of the predicate encoded in
```
typeof value === "number" && value > 0
```
is still `number` (`value` could just be a non-positive number).

For now this check is only enforced when the flowconfig option `one_sided_type_guards=true`, because using a one-sided type guard is typically the right way to fix this issue.

Credit to danvk for [bringing up this issue](https://twitter.com/danvdk/status/1765745099554668830) and suggesting this version of the complete consistency check.

Reviewed By: SamChou19815

Differential Revision: D56207325

fbshipit-source-id: 319f5b4d9fdc2bd24ff2dd0afd2fcb84cd9c6498

src/typing/debug_js.ml

@@ -1991,6 +1991,8 @@ let dump_error_message =
       spf "EUnionOptimizationOnNonUnion (%s)" (string_of_aloc loc)
     | ECannotCallReactComponent { reason } ->
       spf "ECannotCallReactComponent (%s)" (dump_reason cx reason)
+    | ENegativeTypeGuardConsistency { reason; _ } ->
+      spf "ENegativeTypeGuardConsistency (%s)" (dump_reason cx reason)
 
 module Verbose = struct
   let print_if_verbose_lazy

src/typing/errors/error_message.ml

@@ -260,6 +260,11 @@ and 'loc t' =
       loc: 'loc;
       kind: string;
     }
+  | ENegativeTypeGuardConsistency of {
+      reason: 'loc virtual_reason;
+      return_reason: 'loc virtual_reason;
+      type_reason: 'loc virtual_reason;
+    }
   | EInternal of 'loc * internal_error
   | EUnsupportedSyntax of 'loc * unsupported_syntax
   | EUseArrayLiteral of 'loc
@@ -1023,6 +1028,13 @@ let rec map_loc_of_error_message (f : 'a -> 'b) : 'a t' -> 'b t' =
       }
   | ETypeGuardIncompatibleWithFunctionKind { loc; kind } ->
     ETypeGuardIncompatibleWithFunctionKind { loc = f loc; kind }
+  | ENegativeTypeGuardConsistency { reason; return_reason; type_reason } ->
+    ENegativeTypeGuardConsistency
+      {
+        reason = map_reason reason;
+        return_reason = map_reason return_reason;
+        type_reason = map_reason type_reason;
+      }
   | EInternal (loc, i) -> EInternal (f loc, i)
   | EUnsupportedSyntax (loc, u) -> EUnsupportedSyntax (f loc, u)
   | EUseArrayLiteral loc -> EUseArrayLiteral (f loc)
@@ -1619,6 +1631,7 @@ let util_use_op_of_msg nope util = function
   | ETypeGuardFunctionParamHavoced _
   | ETypeGuardIncompatibleWithFunctionKind _
   | ETypeGuardFunctionInvalidWrites _
+  | ENegativeTypeGuardConsistency _
   | EDuplicateComponentProp _
   | ERefComponentProp _
   | EInvalidRendersTypeArgument _
@@ -1695,6 +1708,7 @@ let loc_of_msg : 'loc t' -> 'loc option = function
   | EPredicateInvalidParameter { pred_reason = reason; _ }
   | ETypeGuardParamUnbound reason
   | ETypeGuardFunctionInvalidWrites { reason; _ }
+  | ENegativeTypeGuardConsistency { reason; _ }
   | ETypeGuardFunctionParamHavoced { type_guard_reason = reason; _ } ->
     Some (loc_of_reason reason)
   | EExponentialSpread
@@ -2366,6 +2380,8 @@ let friendly_message_of_msg = function
   | ETypeGuardParamUnbound reason -> Normal (MessageInvalidTypeGuardParamUnbound reason)
   | ETypeGuardFunctionInvalidWrites { reason = _; type_guard_reason; write_locs } ->
     Normal (MessageInvalidTypeGuardFunctionWritten { type_guard_reason; write_locs })
+  | ENegativeTypeGuardConsistency { reason; return_reason; type_reason } ->
+    Normal (MessageNegativeTypeGuardConsistency { reason; return_reason; type_reason })
   | ETypeGuardFunctionParamHavoced { type_guard_reason; param_reason; call_locs } ->
     Normal
       (MessageCannotUseTypeGuardWithFunctionParamHavoced
@@ -2952,6 +2968,7 @@ let error_code_of_message err : error_code option =
   | ETypeGuardImpliesMismatch _
   | ETypeGuardParamUnbound _
   | ETypeGuardFunctionInvalidWrites _
+  | ENegativeTypeGuardConsistency _
   | ETypeGuardFunctionParamHavoced _
   | ETypeGuardIncompatibleWithFunctionKind _ ->
     Some FunctionPredicate

src/typing/errors/flow_intermediate_error.ml

@@ -3659,6 +3659,15 @@ let to_printable_error :
       [ref lower; text " does not appear in the same position as "; ref upper]
     | MessageTypeGuardImpliesMismatch { lower; upper } ->
       [text "one-sided "; ref lower; text " is incompatible with default "; ref upper]
+    | MessageNegativeTypeGuardConsistency { reason = _; return_reason; type_reason } ->
+      [
+        text "Inconsistent type guard declaration.";
+        text " The negation of the predicate encoded in return expression ";
+        ref return_reason;
+        text " needs to completely refine away the guard type ";
+        ref type_reason;
+        text ".";
+      ]
     | MessageUnexpectedTemporaryBaseType ->
       [text "The type argument of a temporary base type must be a compatible literal type"]
     | MessageUnexpectedUseOfThisType -> [text "Unexpected use of "; code "this"; text " type."]

src/typing/errors/flow_intermediate_error_types.ml

@@ -705,6 +705,11 @@ type 'loc message =
       type_guard_reason: 'loc virtual_reason;
       write_locs: 'loc list;
     }
+  | MessageNegativeTypeGuardConsistency of {
+      reason: 'loc virtual_reason;
+      return_reason: 'loc virtual_reason;
+      type_reason: 'loc virtual_reason;
+    }
   | MessageInvalidTypeGuardParamUnbound of 'loc virtual_reason
   | MessageInvalidUseOfFlowEnforceOptimized of 'loc virtual_reason
   | MessageLowerIsNotArray of 'loc virtual_reason

src/typing/statement.ml

@@ -7567,7 +7567,7 @@ module Make
     in
     (* This check to be performed after the function has been checked to ensure all
      * entries have been prepared for type checking. *)
-    let check_type_guard_consistency cx _one_sided param_loc tg_param tg_reason type_guard =
+    let check_type_guard_consistency cx reason one_sided param_loc tg_param tg_reason type_guard =
       let env = Context.environment cx in
       let { Loc_env.var_info; _ } = env in
       let { Env_api.type_guard_consistency_maps; _ } = var_info in
@@ -7590,7 +7590,9 @@ module Make
           )
       | Some (None, reads) ->
         (* Each read corresponds to a return expression. *)
-        Base.List.iter reads ~f:(fun (ret_expr, return_reason, { Env_api.write_locs; _ }, _) ->
+        Base.List.iter
+          reads
+          ~f:(fun (ret_expr, return_reason, { Env_api.write_locs = pos_write_locs; _ }, neg_refi) ->
             let is_return_false_statement =
               match ret_expr with
               | Some (_, Ast.Expression.BooleanLiteral { Ast.BooleanLiteral.value = false; _ }) ->
@@ -7599,17 +7601,45 @@ module Make
             in
             let return_loc = Reason.loc_of_reason return_reason in
             match
-              Type_env.type_guard_at_return cx param_reason ~param_loc ~return_loc write_locs
+              Type_env.type_guard_at_return
+                cx
+                param_reason
+                ~param_loc
+                ~return_loc
+                ~pos_write_locs
+                ~neg_refi:(neg_refi, param_loc, Pattern_helper.Root)
             with
-            | Ok t ->
+            | Ok (t, neg_pred) ->
+              (* Positive *)
               let use_op =
                 Frame
                   ( InferredTypeForTypeGuardParameter
                       { reason = tg_reason; is_return_false_statement },
                     Op (FunReturnStatement { value = return_reason })
                   )
               in
-              Flow.flow cx (t, UseT (use_op, type_guard))
+              Flow.flow cx (t, UseT (use_op, type_guard));
+              (* Negative *)
+              if Context.one_sided_type_guards cx && not one_sided then
+                let type_guard_with_neg_pred =
+                  Tvar_resolver.mk_tvar_and_fully_resolve_no_wrap_where cx tg_reason (fun tout ->
+                      Flow.flow cx (type_guard, PredicateT (neg_pred, tout))
+                  )
+                in
+                if
+                  not
+                    (Flow_js.FlowJs.speculative_subtyping_succeeds
+                       cx
+                       type_guard_with_neg_pred
+                       (EmptyT.at ALoc.none)
+                    )
+                then
+                  Flow_js_utils.add_output
+                    cx
+                    Error_message.(
+                      ENegativeTypeGuardConsistency
+                        { reason; return_reason; type_reason = TypeUtil.reason_of_t type_guard }
+                    )
             | Error write_locs ->
               Flow_js_utils.add_output
                 cx
@@ -7633,21 +7663,21 @@ module Make
         | (loc, Rest) -> err_with_desc (RRestParameter (Some name)) expr_reason loc
         | (loc, Select _) -> err_with_desc (RPatternParameter name) expr_reason loc
       in
-      let type_guard_based_checks one_sided tg_param type_guard binding_opt =
+      let type_guard_based_checks reason one_sided tg_param type_guard binding_opt =
         let (name_loc, name) = tg_param in
         let tg_reason = mk_reason (RTypeGuardParam name) name_loc in
         let open Pattern_helper in
         match binding_opt with
         | None -> Flow_js_utils.add_output cx Error_message.(ETypeGuardParamUnbound tg_reason)
         | Some (param_loc, Root) ->
-          check_type_guard_consistency cx one_sided param_loc tg_param tg_reason type_guard
+          check_type_guard_consistency cx reason one_sided param_loc tg_param tg_reason type_guard
         | Some binding -> error_on_non_root_binding name tg_reason binding
       in
       match pred with
-      | TypeGuardBased { reason = _; one_sided; param_name; type_guard } ->
+      | TypeGuardBased { reason; one_sided; param_name; type_guard } ->
         let bindings = Pattern_helper.bindings_of_params params in
         let matching_binding = SMap.find_opt (snd param_name) bindings in
-        type_guard_based_checks one_sided param_name type_guard matching_binding
+        type_guard_based_checks reason one_sided param_name type_guard matching_binding
       | PredBased (expr_reason, (lazy (p_map, _))) ->
         let required_bindings =
           Base.List.filter_map (Key_map.keys p_map) ~f:(function

src/typing/type_env.ml

@@ -557,28 +557,27 @@ let read_entry_exn ~lookup_mode cx loc reason =
       | Ok x -> x
   )
 
+let read_to_predicate cx var_info ({ Env_api.write_locs; _ }, _, _) =
+  let predicates =
+    Base.List.filter_map write_locs ~f:(function
+        | Env_api.With_ALoc.Refinement { refinement_id; _ } ->
+          Some (find_refi var_info refinement_id |> snd |> predicate_of_refinement cx)
+        | _ -> None
+        )
+  in
+  predicates
+  |> Nel.of_list
+  |> Base.Option.map ~f:(fun (p, rest) -> Base.List.fold rest ~init:p ~f:(fun acc p -> OrP (acc, p)))
+
 let predicate_refinement_maps cx loc =
   let { Loc_env.var_info; _ } = Context.environment cx in
   let { Env_api.predicate_refinement_maps; _ } = var_info in
-  let read_to_predicate ({ Env_api.write_locs; _ }, _, _) =
-    let predicates =
-      Base.List.filter_map write_locs ~f:(function
-          | Env_api.With_ALoc.Refinement { refinement_id; _ } ->
-            Some (find_refi var_info refinement_id |> snd |> predicate_of_refinement cx)
-          | _ -> None
-          )
-    in
-    predicates
-    |> Nel.of_list
-    |> Base.Option.map ~f:(fun (p, rest) ->
-           Base.List.fold rest ~init:p ~f:(fun acc p -> OrP (acc, p))
-       )
-  in
   let to_predicate_key_map map =
     map
     |> SMap.elements
     |> Base.List.filter_map ~f:(fun (name, read) ->
-           read_to_predicate read |> Base.Option.map ~f:(fun p -> ((OrdinaryName name, []), p))
+           read_to_predicate cx var_info read
+           |> Base.Option.map ~f:(fun p -> ((OrdinaryName name, []), p))
        )
     |> Key_map.of_list
   in
@@ -587,7 +586,8 @@ let predicate_refinement_maps cx loc =
   | Some (expr_reason, p_map, n_map) ->
     Some (expr_reason, lazy (to_predicate_key_map p_map, to_predicate_key_map n_map))
 
-let type_guard_at_return cx reason ~param_loc ~return_loc write_locs =
+let type_guard_at_return cx reason ~param_loc ~return_loc ~pos_write_locs ~neg_refi =
+  let ({ Loc_env.var_info; _ } as env) = Context.environment cx in
   let rec is_invalid (acc_result, acc_locs) write_loc =
     match write_loc with
     | Env_api.Write reason when ALoc.equal (Reason.loc_of_reason reason) param_loc ->
@@ -601,14 +601,16 @@ let type_guard_at_return cx reason ~param_loc ~return_loc write_locs =
       (true, acc_locs)
   in
   let (is_invalid, invalid_writes) =
-    Base.List.fold_left write_locs ~init:(false, []) ~f:is_invalid
+    Base.List.fold_left pos_write_locs ~init:(false, []) ~f:is_invalid
   in
-  let env = Context.environment cx in
   if is_invalid then
     Error invalid_writes
   else
     let lookup_mode = LookupMode.ForValue in
-    Ok (type_of_state ~lookup_mode cx env return_loc reason write_locs None None)
+    Ok
+      ( type_of_state ~lookup_mode cx env return_loc reason pos_write_locs None None,
+        Base.Option.value ~default:NoP (read_to_predicate cx var_info neg_refi)
+      )
 
 let ref_entry_exn ~lookup_mode cx loc reason =
   let t = read_entry_exn ~lookup_mode cx loc reason in

src/typing/type_env.mli

@@ -176,5 +176,6 @@ val type_guard_at_return :
   Reason.reason ->
   param_loc:ALoc.t ->
   return_loc:ALoc.t ->
-  Env_api.write_locs ->
-  (Type.t, ALoc.t list) result
+  pos_write_locs:Env_api.write_locs ->
+  neg_refi:Env_api.predicate_refinement ->
+  (Type.t * Type.predicate, ALoc.t list) result

tests/type_guards/classes.js

@@ -111,12 +111,12 @@ function declare_class_test() {
 
   class D2 extends C {
     m(x: mixed): x is mixed { // error mixed ~> number
-      return true;
+      return true; // error (negation) mixed ~> empty
     }
   }
   class D3 extends C {
     m(x: mixed): x is number {
-      return true; // error mixed ~> number
+      return true; // error mixed ~> number and (negation) number ~> empty
     }
   }
 }

tests/type_guards/consistency.js

@@ -7,7 +7,7 @@ class M {}
 function no_return(x: mixed): x is number {} // error no return
 
 function return_true(x: mixed): x is number {
-    return true; // error x: mixed ~> number
+    return true; // error x: mixed ~> number and (negation) number ~> empty
 }
 
 function return_true_in_branch(x: mixed): x is number {
@@ -23,7 +23,7 @@ function negation_on_union(x: number | string | boolean): x is boolean {
 }
 
 function always_false_error(x: mixed): x is A {
-  return false; // error (technically this should hold but that's not what we do in other refinements)
+  return false; // error (negation) A ~> empty, TODO: positive side should not error
 }
 
 function return_false_under_condition(x: number | string | boolean): x is boolean {
@@ -32,7 +32,7 @@ function return_false_under_condition(x: number | string | boolean): x is boolea
   } else if (typeof x ==='string') {
     return false; // error (for the same reason as above)
   } else {
-    return true; // okay
+    return true; // TODO okay (no negation error)
   }
 }
 
@@ -47,7 +47,7 @@ const arrow_error = (x: mixed): x is number => (
 
 class C {
   m(x: mixed): x is number {
-    return typeof x === 'string'; // error x: string ~> number
+    return typeof x === 'string'; // error x: string ~> number and (negation) number ~> empty
   }
 }
 
@@ -91,11 +91,11 @@ function contextual() {
 }
 
 
-function instanceof_ok(x: mixed): x is A {
-  return x instanceof B; // okay
+function instanceof_error_1(x: mixed): x is A {
+  return x instanceof B; // error (negation) A ~> empty
 }
 
-function instanceof_error(x: mixed): x is B {
+function instanceof_error_2(x: mixed): x is B {
   return x instanceof A; // error A ~> B
 }
 
@@ -113,7 +113,7 @@ function non_maybe_poly_1<X>(x: X): x is $NonMaybeType<X> {
   return x != null;
 }
 
-function non_maybe_poly_2<X>(x: ?X): x is X { // okay
+function non_maybe_poly_2<X: {...}>(x: ?X): x is X { // okay
   return x != null;
 }
 
@@ -135,7 +135,7 @@ function pipe_result() {
   }
 
   function error(x: mixed): x is string {
-    return isNumberOrString(x) && isBoolean(x); // okay. empty ~> string
+    return isNumberOrString(x) && isBoolean(x); // error (negation) string ~> empty
   }
 }
 
@@ -168,7 +168,7 @@ function multi_return_ok(x: mixed): x is A {
   if (0 < 1) {
     return x instanceof A; // okay
   }
-  return x instanceof B; // okay
+  return x instanceof B; // error (negation) A ~> empty
 }
 
 function multi_return_one_branch_error(x: mixed): x is B {