[flow] typing of one-sided type guards

Summary:
**Refinement** (flow_js.ml) Given a function
```
function isT(x: S): implies x is T {
  return e;
}
```
we want `isT(x)` to refine just the then-branch of a conditional:
```
declare var x: T | R;
if (isT(x)) {
  x as T; // okay, x is T
} else {
  x as R; // error T ~> R, x is unrefined (T | R)
}
```
**Consistency checking:** the check we perform for "implies" type guards is the same as the one for default type guards. This will change later when we fix the default case to also account for the negation/else branch. (statement.ml)

**Subtyping** (subtyping_kit.ml): "implies" is a weakening qualifier
```
(x: S): x is T <: (x: S): implies x is T
```

Changelog: [internal]

Reviewed By: SamChou19815

Differential Revision: D56506763

fbshipit-source-id: c1ddb7c66a174910e6acdc5e9a9784e4d610e539

src/common/reason.ml

@@ -244,6 +244,7 @@ type 'loc virtual_reason_desc =
   | RUninitialized
   | RPossiblyUninitialized
   | RUnannotatedNext
+  | RTypeGuard
   | RTypeGuardParam of string
   | RComponent of name
   | RComponentType
@@ -279,8 +280,8 @@ let rec map_desc_locs f = function
     | RTupleOutOfBoundsAccess _ | RFunction _ | RFunctionType | RFunctionBody | RFunctionCallType
     | RFunctionUnusedArgument | RJSXChild | RJSXFunctionCall _ | RJSXIdentifier _
     | RJSXElementProps _ | RJSXElement _ | RJSXText | RFbt | RUninitialized | RPossiblyUninitialized
-    | RUnannotatedNext | REmptyArrayElement | RMappedType | RTypeGuardParam _ | RComponent _
-    | RComponentType | RInferredUnionElemArray _ ) as r ->
+    | RUnannotatedNext | REmptyArrayElement | RMappedType | RTypeGuard | RTypeGuardParam _
+    | RComponent _ | RComponentType | RInferredUnionElemArray _ ) as r ->
     r
   | RFunctionCall desc -> RFunctionCall (map_desc_locs f desc)
   | RUnknownUnspecifiedProperty desc -> RUnknownUnspecifiedProperty (map_desc_locs f desc)
@@ -764,6 +765,7 @@ let rec string_of_desc = function
   | RUninitialized -> "uninitialized variable"
   | RPossiblyUninitialized -> "possibly uninitialized variable"
   | RUnannotatedNext -> "undefined (default `next` of unannotated generator function)"
+  | RTypeGuard -> "type guard"
   | RTypeGuardParam s -> spf "type guard parameter `%s`" s
   | RComponent name -> spf "component %s" (display_string_of_name name)
   | RComponentType -> "component"
@@ -1560,6 +1562,7 @@ let classification_of_reason_desc desc =
   | RUnionBranching _
   | REnum _
   | RUnannotatedNext
+  | RTypeGuard
   | RTypeGuardParam _ ->
     `Unclassified
 

src/common/reason.mli

@@ -202,6 +202,7 @@ type 'loc virtual_reason_desc =
   | RUninitialized
   | RPossiblyUninitialized
   | RUnannotatedNext
+  | RTypeGuard
   | RTypeGuardParam of string
   | RComponent of name
   | RComponentType

src/common/ty/ty.ml

@@ -155,7 +155,7 @@ and fun_t = {
 
 and return_t =
   | ReturnType of t
-  | TypeGuard of string * t
+  | TypeGuard of bool (* implies *) * string * t
 
 and obj_kind =
   | ExactObj

src/common/ty/ty_debug.ml

@@ -196,7 +196,14 @@ struct
   and dump_return_t ~depth t =
     match t with
     | ReturnType t -> dump_t ~depth t
-    | TypeGuard (x, t) -> spf "%s is %s" x (dump_t ~depth t)
+    | TypeGuard (impl, x, t) ->
+      let impl =
+        if impl then
+          "implies "
+        else
+          ""
+      in
+      spf "%s%s is %s" impl x (dump_t ~depth t)
 
   and dump_tuple_element ~depth i name t polarity optional =
     if Base.Option.is_none name && polarity = Neutral && not optional then
@@ -601,11 +608,18 @@ struct
       ]
     and json_of_return_t = function
       | ReturnType t -> Hh_json.(JSON_Object [("type_", json_of_t t)])
-      | TypeGuard (x, t) ->
+      | TypeGuard (impl, x, t) ->
         Hh_json.(
           JSON_Object
             [
-              ("type_guard", JSON_Object [("type_parameter", JSON_String x); ("type_", json_of_t t)]);
+              ( "type_guard",
+                JSON_Object
+                  [
+                    ("implies", JSON_Bool impl);
+                    ("type_parameter", JSON_String x);
+                    ("type_", json_of_t t);
+                  ]
+              );
             ]
         )
     and json_of_obj_t o =

src/common/ty/ty_printer.ml

@@ -309,7 +309,14 @@ let layout_of_elt ~prefer_single_quotes ?(size = 5000) ?(with_comments = true) ~
   and return_t ~depth t =
     match t with
     | ReturnType t -> type_ ~depth t
-    | TypeGuard (x, t) -> fuse_with_space [Atom x; Atom "is"; type_ ~depth t]
+    | TypeGuard (impl, x, t) ->
+      let impl =
+        if impl then
+          [Atom "implies"]
+        else
+          []
+      in
+      fuse_with_space (impl @ [Atom x; Atom "is"; type_ ~depth t])
   and type_object_property =
     let to_key x =
       if property_key_quotes_needed x then

src/common/ty/ty_serializer.ml

@@ -266,16 +266,16 @@ let type_ options =
     | ReturnType t ->
       let%map t = type_ t in
       Ast.Type.Function.TypeAnnotation t
-    | TypeGuard (x, t) ->
+    | TypeGuard (impl, x, t) ->
+      let kind =
+        if impl then
+          T.TypeGuard.Implies
+        else
+          T.TypeGuard.Default
+      in
       let%map t = type_ t in
       T.Function.TypeGuard
-        ( Loc.none,
-          {
-            T.TypeGuard.kind = T.TypeGuard.Default;
-            guard = (id_from_string x, Some t);
-            comments = None;
-          }
-        )
+        (Loc.none, { T.TypeGuard.kind; guard = (id_from_string x, Some t); comments = None })
   and obj_ o =
     let%bind properties = mapM obj_prop o.obj_props in
     let%map (exact, inexact, properties) =

src/parser_utils/type_sig/type_sig.ml

@@ -76,7 +76,12 @@ type ('key, 'loc, 'a) predicate =
 
 type ('loc, 'a) predicate_or_type_guard =
   | Predicate of 'loc * (string, 'loc, 'a) predicate option
-  | TypeGuard of (('loc * string) * 'a)
+  | TypeGuard of {
+      loc: 'loc;
+      param_name: 'loc * string;
+      type_guard: 'a;
+      one_sided: bool;
+    }
 [@@deriving iter, map, show { with_path = false }]
 
 type ('loc, 'a) tparam =

src/parser_utils/type_sig/type_sig_parse.ml

@@ -1577,19 +1577,21 @@ and tuple_element opts scope tbls xs (loc, el) =
     TupleSpread { loc; name; t }
 
 and type_guard_opt opts scope tbls xs guard =
-  let (_, { T.TypeGuard.kind = _; guard = (x, t_opt); _ }) = guard in
+  let (gloc, { T.TypeGuard.kind; guard = (x, t_opt); _ }) = guard in
   match t_opt with
   | Some t ->
+    let gloc = push_loc tbls gloc in
     let (loc, { Ast.Identifier.name; _ }) = x in
     let loc = push_loc tbls loc in
-    Some ((loc, name), annot opts scope tbls xs t)
+    Some (gloc, (loc, name), annot opts scope tbls xs t, kind = T.TypeGuard.Implies)
   | None ->
     (* TODO(pvekris) support assert type guards in type_sig_parse *)
     None
 
 and type_guard_or_predicate_of_type_guard opts scope tbls xs guard =
   match type_guard_opt opts scope tbls xs guard with
-  | Some p -> Some (TypeGuard p)
+  | Some (loc, param_name, type_guard, one_sided) ->
+    Some (TypeGuard { loc; param_name; type_guard; one_sided })
   | None -> None
 
 and return_annot opts scope tbls xs = function
@@ -3555,9 +3557,9 @@ and function_def_helper =
     let predicate =
       let open Option.Let_syntax in
       match type_guard_opt with
-      | Some (loc, p) ->
+      | Some (loc, param_name, type_guard, one_sided) ->
         (* Type-guard and %checks cannot coexist (parse error) *)
-        Some (TypeGuard (loc, p))
+        Some (TypeGuard { loc; param_name; type_guard; one_sided })
       | None ->
         let%map (loc, p) = predicate opts scope tbls ps body p in
         Predicate (loc, p)

src/services/type_info/signature_help.ml

@@ -20,8 +20,15 @@ let string_of_ty = Ty_printer.string_of_t_single_line ~with_comments:false
 
 let string_of_return_t ~exact_by_default = function
   | Ty.ReturnType t -> Ty_printer.string_of_t_single_line ~exact_by_default ~with_comments:false t
-  | Ty.TypeGuard (x, t) ->
-    x ^ " is " ^ Ty_printer.string_of_t_single_line ~exact_by_default ~with_comments:false t
+  | Ty.TypeGuard (impl, x, t) ->
+    let impl =
+      if impl then
+        "implies "
+      else
+        ""
+    in
+    let t = Ty_printer.string_of_t_single_line ~exact_by_default ~with_comments:false t in
+    Utils_js.spf "%s%s is %s" impl x t
 
 let documentation_of_param_infos name : Jsdoc.Param.t -> string =
   let open Jsdoc.Param in

src/typing/debug_js.ml

@@ -192,8 +192,15 @@ let rec dump_t_ (depth, tvars) cx t =
              (kid return_t)
              (match predicate with
              | Some (PredBased _) -> " %checks"
-             | Some (TypeGuardBased { param_name = (_, name); type_guard }) ->
-               spf " %s is %s" name (kid type_guard)
+             | Some (TypeGuardBased { reason = _; one_sided; param_name = (_, name); type_guard })
+               ->
+               let implies =
+                 if one_sided then
+                   "implies "
+                 else
+                   ""
+               in
+               spf " %s%s is %s" implies name (kid type_guard)
              | None -> "")
           )
         t
@@ -1546,6 +1553,8 @@ let dump_error_message =
       spf "EPredicateInvalidParameter (%s)" (dump_reason cx r)
     | ETypeGuardIndexMismatch { use_op; _ } ->
       spf "ETypeGuardIndexMismatch (%s)" (string_of_use_op use_op)
+    | ETypeGuardImpliesMismatch { use_op; _ } ->
+      spf "ETypeGuardImpliesMismatch (%s)" (string_of_use_op use_op)
     | ETypeGuardParamUnbound _ -> "ETypeGuardParamUnbound"
     | ETypeGuardFunctionInvalidWrites _ -> "ETypeGuardFunctionInvalidWrites"
     | ETypeGuardFunctionParamHavoced _ -> "ETypeGuardFunctionParamHavoced"

src/typing/errors/error_message.ml

@@ -233,6 +233,10 @@ and 'loc t' =
       use_op: 'loc virtual_use_op;
       reasons: 'loc virtual_reason * 'loc virtual_reason;
     }
+  | ETypeGuardImpliesMismatch of {
+      use_op: 'loc virtual_use_op;
+      reasons: 'loc virtual_reason * 'loc virtual_reason;
+    }
   | ETypeGuardParamUnbound of 'loc virtual_reason
   | ETypeGuardFunctionInvalidWrites of {
       reason: 'loc virtual_reason;
@@ -965,6 +969,9 @@ let rec map_loc_of_error_message (f : 'a -> 'b) : 'a t' -> 'b t' =
       { pred_reason = map_reason pred_reason; binding_reason = map_reason binding_reason }
   | ETypeGuardIndexMismatch { use_op; reasons = (r1, r2) } ->
     ETypeGuardIndexMismatch { use_op = map_use_op use_op; reasons = (map_reason r1, map_reason r2) }
+  | ETypeGuardImpliesMismatch { use_op; reasons = (r1, r2) } ->
+    ETypeGuardImpliesMismatch
+      { use_op = map_use_op use_op; reasons = (map_reason r1, map_reason r2) }
   | ETypeGuardParamUnbound reason -> ETypeGuardParamUnbound (map_reason reason)
   | ETypeGuardFunctionInvalidWrites { reason; type_guard_reason; write_locs } ->
     ETypeGuardFunctionInvalidWrites
@@ -1440,6 +1447,7 @@ let util_use_op_of_msg nope util = function
   | EPredicateFuncIncompatibility _
   | EPredicateInvalidParameter _
   | ETypeGuardIndexMismatch _
+  | ETypeGuardImpliesMismatch _
   | EInternal (_, _)
   | EUnsupportedSyntax (_, _)
   | EUseArrayLiteral _
@@ -1803,7 +1811,8 @@ let loc_of_msg : 'loc t' -> 'loc option = function
   | EPrimitiveAsInterface _
   | EPredicateFuncArityMismatch _
   | EPredicateFuncIncompatibility _
-  | ETypeGuardIndexMismatch _ ->
+  | ETypeGuardIndexMismatch _
+  | ETypeGuardImpliesMismatch _ ->
     None
 
 let kind_of_msg =
@@ -2274,6 +2283,14 @@ let friendly_message_of_msg = function
         use_op;
         explanation = None;
       }
+  | ETypeGuardImpliesMismatch { use_op; reasons = (lower, upper) } ->
+    UseOp
+      {
+        loc = loc_of_reason lower;
+        message = MessageTypeGuardImpliesMismatch { lower; upper };
+        use_op;
+        explanation = None;
+      }
   | ETypeGuardParamUnbound reason -> Normal (MessageInvalidTypeGuardParamUnbound reason)
   | ETypeGuardFunctionInvalidWrites { reason = _; type_guard_reason; write_locs } ->
     Normal (MessageInvalidTypeGuardFunctionWritten { type_guard_reason; write_locs })
@@ -2873,6 +2890,7 @@ let error_code_of_message err : error_code option =
   | EPredicateFuncIncompatibility _
   | EPredicateInvalidParameter _
   | ETypeGuardIndexMismatch _
+  | ETypeGuardImpliesMismatch _
   | ETypeGuardParamUnbound _
   | ETypeGuardFunctionInvalidWrites _
   | ETypeGuardFunctionParamHavoced _

src/typing/errors/flow_intermediate_error.ml

@@ -3653,6 +3653,8 @@ let to_printable_error :
       ]
     | MessageTypeGuardIndexMismatch { lower; upper } ->
       [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]
     | 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

@@ -873,6 +873,10 @@ type 'loc message =
       lower: 'loc virtual_reason;
       upper: 'loc virtual_reason;
     }
+  | MessageTypeGuardImpliesMismatch of {
+      lower: 'loc virtual_reason;
+      upper: 'loc virtual_reason;
+    }
   | MessageUnclearType
   | MessageUnderconstrainedImplicitInstantiaton of {
       reason_call: 'loc virtual_reason;

src/typing/flow_js.ml

@@ -2620,15 +2620,20 @@ struct
               | Some p -> rec_flow cx trace (tin, PredicateT (p, tout))
               | None -> rec_flow_t ~use_op:unknown_use cx trace (tin, OpenT tout)
             end
-          | (Some (Some name, _), TypeGuardBased { param_name = (_, param_name); type_guard }) ->
+          | ( Some (Some name, _),
+              TypeGuardBased { reason = _; one_sided; param_name = (_, param_name); type_guard }
+            ) ->
             let t =
               if param_name <> name then
                 (* This is not the refined parameter. *)
                 tin
               else if sense then
                 intersect cx tin type_guard
-              else
+              else if not one_sided then
                 type_guard_diff cx tin type_guard
+              else
+                (* Do not refine else branch on one-sided type-guard *)
+                tin
             in
             rec_flow_t ~use_op:unknown_use cx trace (t, OpenT tout)
         end

src/typing/statement.ml

@@ -7531,7 +7531,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 param_loc tg_param tg_reason type_guard =
+    let check_type_guard_consistency cx _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
@@ -7597,21 +7597,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 tg_param type_guard binding_opt =
+      let type_guard_based_checks 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 param_loc tg_param tg_reason type_guard
+          check_type_guard_consistency cx 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 { 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 param_name type_guard matching_binding
+        type_guard_based_checks 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
@@ -7732,17 +7732,11 @@ module Make
             let (t, ast_annot) = Anno.mk_type_available_annotation cx tparams_map annot in
             (Annotated t, Ast.Function.ReturnAnnot.Available ast_annot, None)
           | ( Ast.Function.ReturnAnnot.TypeGuard
-                ( loc,
-                  ( gloc,
-                    {
-                      Ast.Type.TypeGuard.guard = (id_name, Some t);
-                      kind = Ast.Type.TypeGuard.Default as kind;
-                      comments;
-                    }
-                  )
-                ),
+                (loc, (gloc, { Ast.Type.TypeGuard.guard = (id_name, Some t); kind; comments })),
               _
-            ) ->
+            )
+            when kind = Ast.Type.TypeGuard.Default
+                 || (kind = Ast.Type.TypeGuard.Implies && Context.one_sided_type_guards cx) ->
             let (bool_t, guard', predicate) =
               Anno.convert_type_guard
                 cx