(*
 * Copyright (c) Meta Platforms, Inc. and affiliates.
 *
 * This source code is licensed under the MIT license found in the
 * LICENSE file in the root directory of this source tree.
 *)

open Reason
open Type_subst
open Type
open Type.AConstraint
open TypeUtil

let object_like_op = function
  | Annot_SpecializeT _
  | Annot_ThisSpecializeT _
  | Annot_UseT_TypeT _
  | Annot_ConcretizeForImportsExports _
  | Annot_CJSRequireT _
  | Annot_ImportTypeofT _
  | Annot_ImportNamedT _
  | Annot_ImportDefaultT _
  | Annot_ImportModuleNsT _
  | Annot_CJSExtractNamedExportsT _
  | Annot_ExportNamedT _
  | Annot_ExportTypeT _
  | Annot_AssertExportIsTypeT _
  | Annot_CopyNamedExportsT _
  | Annot_CopyTypeExportsT _
  | Annot_ElemT _
  | Annot_GetStaticsT _
  | Annot_MakeExactT _
  | Annot_MixinT _
  | Annot_ObjKitT _
  | Annot_ObjTestProtoT _
  | Annot_ArithT _
  | Annot_UnaryArithT _
  | Annot_NotT _
  | Annot_ObjKeyMirror _
  | Annot_ObjMapConst _
  | Annot_GetKeysT _
  | Annot_DeepReadOnlyT _
  | Annot_ToStringT _
  | Annot__Future_added_value__ _ ->
    false
  | Annot_GetPropT _
  | Annot_GetElemT _
  | Annot_LookupT _
  | Annot_ObjRestT _
  | Annot_GetValuesT _ ->
    true

let primitive_promoting_op = function
  | Annot_GetPropT _
  | Annot_GetElemT _
  | Annot_LookupT _ ->
    true
  (* TODO: enumerate all use types *)
  | _ -> false

let function_like_op op = object_like_op op

let get_fully_resolved_type cx id =
  let (_, constraints) = Context.find_constraints cx id in
  match constraints with
  | Constraint.FullyResolved (lazy t) -> t
  | Constraint.Resolved _
  | Constraint.Unresolved _ ->
    failwith "unexpected unresolved constraint in annotation inference"

let get_builtin_typeapp cx reason x targs =
  let t = Flow_js_utils.lookup_builtin_strict cx x reason in
  TypeUtil.typeapp ~use_desc:false reason t targs

module type S = sig
  val mk_typeof_annotation : Context.t -> ?trace:Type.trace -> Reason.t -> Type.t -> Type.t

  val mk_type_reference : Context.t -> Reason.t -> Type.t -> Type.t

  val mk_instance : Context.t -> ?trace:Type.trace -> reason -> ?use_desc:bool -> Type.t -> Type.t

  val reposition : Context.t -> ALoc.t -> ?annot_loc:ALoc.t -> Type.t -> Type.t

  val get_prop :
    Context.t -> Type.use_op -> Reason.t -> ?op_reason:Reason.t -> Reason.name -> Type.t -> Type.t

  val get_elem : Context.t -> Type.use_op -> Reason.t -> key:Type.t -> Type.t -> Type.t

  val get_builtin : Context.t -> ?trace:Type.trace -> name -> reason -> Type.t

  val qualify_type :
    Context.t -> Type.use_op -> Reason.t -> Reason.t * Reason.name -> Type.t -> Type.t

  val assert_export_is_type : Context.t -> Reason.t -> string -> Type.t -> Type.t

  val mk_sig_tvar : Context.t -> Reason.t -> Type.t Lazy.t -> Type.t

  val cjs_require : Context.t -> Type.t -> Reason.t -> bool -> bool -> Type.t

  val export_named :
    Context.t ->
    Reason.reason ->
    Type.export_kind ->
    Type.named_symbol NameUtils.Map.t ->
    Type.t ->
    Type.t

  val cjs_extract_named_exports :
    Context.t -> Reason.reason -> Reason.reason * Type.exporttypes * bool -> Type.t -> Type.t

  val import_default :
    Context.t -> Reason.t -> Type.import_kind -> string -> string -> bool -> Type.t -> Type.t

  val import_named :
    Context.t -> Reason.t -> Type.import_kind -> string -> string -> bool -> Type.t -> Type.t

  val import_ns : Context.t -> Reason.t -> bool -> Type.t -> Type.t

  val import_typeof : Context.t -> Reason.t -> string -> Type.t -> Type.t

  val specialize :
    Context.t ->
    Type.t ->
    Type.use_op ->
    Reason.t ->
    Reason.t ->
    Type.t list Base.Option.t ->
    Type.t

  val copy_named_exports : Context.t -> from_ns:Type.t -> Reason.t -> module_t:Type.t -> Type.t

  val copy_type_exports : Context.t -> from_ns:Type.t -> Reason.t -> module_t:Type.t -> Type.t

  val arith : Context.t -> Reason.t -> Type.t -> Type.t -> Type.ArithKind.t -> Type.t

  val unary_arith : Context.t -> Reason.t -> Type.t -> Type.UnaryArithKind.t -> Type.t

  val unary_not : Context.t -> Reason.t -> Type.t -> Type.t

  val mixin : Context.t -> Reason.t -> Type.t -> Type.t

  val object_spread :
    Context.t ->
    Type.use_op ->
    Reason.reason ->
    Type.Object.Spread.target ->
    Type.Object.Spread.state ->
    Type.t ->
    Type.t

  val widen_obj_type :
    Context.t -> ?trace:Type.trace -> use_op:Type.use_op -> Reason.reason -> Type.t -> Type.t

  val obj_test_proto : Context.t -> Reason.t -> Type.t -> Type.t

  val obj_rest : Context.t -> Reason.t -> string list -> Type.t -> Type.t

  val arr_rest : Context.t -> Type.use_op -> Reason.t -> int -> Type.t -> Type.t

  val set_dst_cx : Context.t -> unit

  val elab_t : Context.t -> ?seen:ISet.t -> Type.t -> Type.AConstraint.op -> Type.t
end

module rec ConsGen : S = struct
  (* Annotation inference is performed in the context of the definition module (this
   * is what the input `cx` in elab_t etc. represents). However, in order to be
   * able to raise errors during annotation inference, we need to have access to the
   * destination context. This is what this reference is for. `dst_cx_ref` is set
   * Check_serivce.mk_check_file once per file right after the destination context
   * is created. *)
  let dst_cx_ref = ref None

  let set_dst_cx cx = dst_cx_ref := Some cx

  (* Errors created with [error_unsupported] are actually reported. Compare this to
   * errors created with Flow_js_utils.add_output which are recorded in the context
   * of the source of the annotations, and are therefore ignored. This function checks
   * that dst_cx_ref has been set and uses that as the target context.
   *
   * The only kind of errors that are reported here are "unsupported" cases. These
   * are mostly cases that rely on subtyping, which is not implemented here; most
   * commonly evaluating call-like EvalTs and speculation. *)
  let error_unsupported_reason ?suggestion cx t reason_op =
    let loc = Reason.loc_of_reason reason_op in
    let msg =
      Error_message.EAnnotationInference (loc, reason_op, TypeUtil.reason_of_t t, suggestion)
    in
    (match !dst_cx_ref with
    | None -> assert false
    | Some dst_cx -> Flow_js_utils.add_annot_inference_error ~src_cx:cx ~dst_cx msg);
    AnyT.error reason_op

  let error_unsupported ?suggestion cx t op =
    let reason_op = AConstraint.display_reason_of_op op in
    error_unsupported_reason ?suggestion cx t reason_op

  let error_recursive cx reason =
    let loc = Reason.loc_of_reason reason in
    let msg = Error_message.EAnnotationInferenceRecursive (loc, reason) in
    (match !dst_cx_ref with
    | None -> assert false
    | Some dst_cx -> Flow_js_utils.add_annot_inference_error ~src_cx:cx ~dst_cx msg);
    AnyT.error reason

  let error_internal_reason cx msg reason_op =
    let loc = Reason.loc_of_reason reason_op in
    let msg = Error_message.(EInternal (loc, UnexpectedAnnotationInference msg)) in
    (match !dst_cx_ref with
    | None -> assert false
    | Some dst_cx -> Flow_js_utils.add_annot_inference_error ~src_cx:cx ~dst_cx msg);
    AnyT.error reason_op

  let error_internal cx msg op =
    let reason_op = AConstraint.display_reason_of_op op in
    error_internal_reason cx msg reason_op

  let dummy_trace = Trace.dummy_trace

  (* Repositioning does not seem to have any perceptible impact in annotation
   * inference. Instead of replicating the convoluted implementation of Flow_js
   * here, we just return the same type intact. *)
  let reposition _cx _loc ?annot_loc:_ t = t

  (*****************)
  (* Instantiation *)
  (*****************)
  module Instantiation_helper = struct
    let cache_instantiate _cx _trace ~use_op:_ ?cache:_ _typeparam _reason_op _reason_tapp t = t

    (* We will not be solving implicit instantiation problems here. The only case
     * where we will need to use this function is when a PolyT needs to be used
     * as a monomorphic type. In this case, the only sensible thing to do is to
     * use the bound of each parameter as the argument to the intantiation. *)
    let mk_targ _cx typeparam _reason_op _reason_tapp = typeparam.Type.bound

    let is_subtype _cx _trace ~use_op:_ (_t1, _t2) = ()

    let unify _cx _trace ~use_op:_ (_t1, _t2) = ()

    let reposition cx ?trace:_ loc ?desc:_ ?annot_loc:_ t = reposition cx loc t
  end

  module InstantiationKit = Flow_js_utils.Instantiation_kit (Instantiation_helper)

  let instantiate_poly cx = InstantiationKit.instantiate_poly cx dummy_trace

  let mk_typeapp_of_poly cx = InstantiationKit.mk_typeapp_of_poly cx dummy_trace

  (***********)
  (* Imports *)
  (***********)
  module Import_export_helper : Flow_js_utils.Import_export_helper_sig with type r = Type.t = struct
    type r = Type.t

    let reposition cx ?trace:_ loc ?desc:_ ?annot_loc:_ t = reposition cx loc t

    let return _cx _trace t = t

    let export_named cx _trace (reason, named, kind) t = ConsGen.export_named cx reason kind named t

    let export_named_fresh_var = export_named

    let export_type cx _trace (reason, export_name, target_module_t) export_t =
      ConsGen.elab_t cx export_t (Annot_ExportTypeT (reason, export_name, target_module_t))

    let cjs_extract_named_exports cx _ (reason, local_module) t =
      ConsGen.cjs_extract_named_exports cx reason local_module t
  end

  let assert_import_is_value _cx _trace _reason _name _export_t = ()

  let with_concretized_type cx r f t = ConsGen.elab_t cx t (Annot_ConcretizeForImportsExports (r, f))

  module CJSRequireTKit = Flow_js_utils.CJSRequireT_kit (Import_export_helper)
  module ImportModuleNsTKit = Flow_js_utils.ImportModuleNsTKit
  module ImportDefaultTKit = Flow_js_utils.ImportDefaultTKit
  module ImportNamedTKit = Flow_js_utils.ImportNamedTKit
  module ImportTypeofTKit = Flow_js_utils.ImportTypeofTKit
  module ExportNamedTKit = Flow_js_utils.ExportNamedT_kit (Import_export_helper)
  module AssertExportIsTypeTKit = Flow_js_utils.AssertExportIsTypeT_kit (Import_export_helper)
  module CopyNamedExportsTKit = Flow_js_utils.CopyNamedExportsT_kit (Import_export_helper)
  module CopyTypeExportsTKit = Flow_js_utils.CopyTypeExportsT_kit (Import_export_helper)
  module ExportTypeTKit = Flow_js_utils.ExportTypeT_kit (Import_export_helper)
  module CJSExtractNamedExportsTKit =
    Flow_js_utils.CJSExtractNamedExportsT_kit (Import_export_helper)

  (***********)
  (* GetProp *)
  (***********)

  module Get_prop_helper = struct
    type r = Type.t

    let cg_lookup_ cx use_op t reason_op propref objt =
      ConsGen.elab_t cx t (Annot_LookupT (reason_op, use_op, propref, objt))

    let error_type _ _ = AnyT.error

    (* We could have just returned `t` here. The OpenT indirection is for compatibility
     * with Flow_js. Specifically, without the OpenT the transformation in
     * https://github.com/facebook/flow/blob/8c3825a1be188e9ade4ad4ed515361bb28c65d8a/src/typing/flow_js.ml#L1744-L1755
     * would fire, causing a divergence in the behavior of this module and Flow_js. *)
    let return cx ~use_op:_ _trace t =
      match t with
      | OpenT _ -> t
      | _ -> Tvar.mk_fully_resolved cx (reason_of_t t) t

    (* We will not be doing subtyping checks in annotation inference. *)
    let dict_read_check _ _ ~use_op:_ _ = ()

    let reposition cx ?trace:_ loc ?desc:_ ?annot_loc:_ t = reposition cx loc t

    let enum_proto cx _trace ~reason (enum_reason, trust, enum) =
      let enum_t = DefT (enum_reason, trust, EnumT enum) in
      let { representation_t; _ } = enum in
      get_builtin_typeapp cx reason (OrdinaryName "$EnumProto") [enum_t; representation_t]

    let cg_lookup cx _trace ~obj_t ~method_accessible:_ t (reason_op, _kind, propref, use_op, _ids)
        =
      cg_lookup_ cx use_op t reason_op propref obj_t

    let cg_get_prop cx _trace t (use_op, access_reason, _, (prop_reason, name)) =
      ConsGen.elab_t
        cx
        t
        (Annot_GetPropT
           (access_reason, use_op, Named { reason = prop_reason; name; from_indexed_access = false })
        )

    let mk_react_dro cx _use_op props_loc t =
      ConsGen.elab_t cx t (Annot_DeepReadOnlyT (reason_of_t t, props_loc))
  end

  module GetPropTKit = Flow_js_utils.GetPropT_kit (Get_prop_helper)

  (** [ensure_annot_resolved cx reason id] ensures that the annotation constraint
   *  associated with [id] has been resolved. If the respective constraint is already
   *  resolved then it returns immediately. Otherwise, it resolves [id] immediately
   *  to the 'any' type. In the case of an [Anno_op (_, _, dep_id)] constraint we also
   *  update the "dependents" set of [dep_id], so that we don't attempt to resolve
   *  [id] once again when [dep_id] gets resolved.
   *)
  let rec ensure_annot_resolved cx reason id =
    let module A = Type.AConstraint in
    match Context.find_avar_opt cx id with
    | None -> get_fully_resolved_type cx id
    | Some (A.Annot_unresolved _) ->
      let t = error_recursive cx reason in
      resolve_id cx reason id t;
      t
    | Some (A.Annot_op { id = dep_id; _ }) ->
      let dep_constraint = Context.find_avar cx dep_id in
      A.update_deps_of_constraint dep_constraint ~f:(fun deps ->
          ISet.filter (fun id2 -> id <> id2) deps
      );
      let t = error_recursive cx reason in
      resolve_id cx reason id t;
      t

  and mk_lazy_tvar cx reason f =
    let id = Reason.mk_id () in
    let tvar = OpenT (reason, id) in
    let t =
      lazy
        ( Avar.unresolved_with_id cx id reason;
          f id;
          (* Before forcing the type constraint of [id] we need to make sure the
           * respective annotation constraint has been processed. If not we infer
           * the empty type. *)
          ensure_annot_resolved cx reason id
        )
    in
    let node = Constraint.create_root (Constraint.FullyResolved t) in
    Context.add_tvar cx id node;
    tvar

  and mk_sig_tvar cx reason (resolved : Type.t Lazy.t) =
    let f id =
      let t = Lazy.force resolved in
      resolve_id cx reason id t
    in
    mk_lazy_tvar cx reason f

  (** [resolve_id cx id1 t] resolves an annotation tvar [id1] to a type [t] *
   *  - If [t] is a concrete type, we mark [id1] as a resolved annotation tvar and
   *    record it as fully resolved in the type graph. *
   *  - If [t] is an OpenT (_, id2), then we unify [id1] and [id2]. (See merge_ids.)
   *)
  and resolve_id cx reason id t =
    match Context.find_avar_opt cx id with
    | None ->
      (* The avar is already resolved. This happens when the avar is recursively
       * reachable and becomes resolved to any. *)
      ()
    | Some constraints1 ->
      let t =
        match t with
        | Type.OpenT (_, id2) -> ensure_annot_resolved cx reason id2
        | _ -> t
      in
      Context.remove_avar cx id;
      Context.add_tvar cx id (Type.Constraint.fully_resolved_node t);
      let dependents1 = deps_of_constraint constraints1 in
      resolve_dependent_set cx reason dependents1 t

  and resolve_dependent_set cx reason dependents t =
    Context.iter_annot_dependent_set
      cx
      (fun id op -> resolve_id cx reason id (elab_t cx t op))
      dependents

  and elab_open cx ~seen reason id op =
    if ISet.mem id seen then
      error_recursive cx reason
    else
      let module A = Type.AConstraint in
      match Context.find_avar_opt cx id with
      | None ->
        (* [id] may refer to a lazily resolved constraint (e.g. created through
         * [mk_lazy_tvar]). To protect against trying to force recursive lazy
         * structures, we introduce a lazy indirection around the resulting
         * constraint. An example that would have cause this unwanted behavior is
         *
         *   declare var x: {
         *     p: number;
         *     q: typeof (x.p);
         *   };
         *
         * This lazy indirection allows the type of `x` to be resolved, before we
         * attempt to force the constraint for `x.p`. *)
        let resolved =
          lazy
            ((* resolved ids definitelly appear in the type graph *)
             let t = get_fully_resolved_type cx id in
             elab_t cx ~seen:(ISet.add id seen) t op
            )
        in
        mk_sig_tvar cx (AConstraint.reason_of_op op) resolved
      | Some (A.Annot_unresolved _)
      | Some (A.Annot_op _) ->
        let fresh_id = Avar.constrained cx op id in
        OpenT (reason, fresh_id)

  and elab_t cx ?(seen = ISet.empty) t op =
    match (t, op) with
    | (EvalT (t, TypeDestructorT (use_op, reason, ReadOnlyType), _), _) ->
      let t = make_readonly cx use_op reason t in
      elab_t cx t op
    | (EvalT (t, TypeDestructorT (_, reason, ReactDRO props_loc), _), _) ->
      let t = elab_t cx t (Annot_DeepReadOnlyT (reason, props_loc)) in
      elab_t cx t op
    | (EvalT (t, TypeDestructorT (use_op, reason, PartialType), _), _) ->
      let t = make_partial cx use_op reason t in
      elab_t cx t op
    | (EvalT (t, TypeDestructorT (use_op, reason, RequiredType), _), _) ->
      let t = make_required cx use_op reason t in
      elab_t cx t op
    | (EvalT (t, TypeDestructorT (use_op, reason, SpreadType (target, todo_rev, head_slice)), _), _)
      ->
      let state =
        {
          Object.Spread.todo_rev;
          acc =
            Base.Option.value_map ~f:(fun x -> [Object.Spread.InlineSlice x]) ~default:[] head_slice;
          spread_id = Reason.mk_id ();
          union_reason = None;
          curr_resolve_idx = 0;
        }
      in

      let t = object_spread cx use_op reason target state t in
      elab_t cx t op
    | (EvalT (t, TypeDestructorT (use_op, reason, RestType (options, r)), _), _) ->
      let state = Object.Rest.One r in
      let t = object_rest cx use_op reason options state t in
      elab_t cx t op
    | (EvalT (t, TypeDestructorT (_, reason, TypeMap ObjectKeyMirror), _), _) ->
      let t = elab_t cx t (Annot_ObjKeyMirror reason) in
      elab_t cx t op
    | (EvalT (t, TypeDestructorT (_, reason, TypeMap (ObjectMapConst t')), _), _) ->
      let t = elab_t cx t (Annot_ObjMapConst (reason, t')) in
      elab_t cx t op
    | (EvalT (t, TypeDestructorT (_, reason, ValuesType), _), _) ->
      let t = elab_t cx t (Annot_GetValuesT reason) in
      elab_t cx t op
    | (EvalT (_, TypeDestructorT (_, _, TypeMap (ObjectMap _)), _), _) ->
      error_unsupported ~suggestion:"$ObjMapConst" cx t op
    | (EvalT (_, TypeDestructorT (_, _, TypeMap (ObjectMapi _)), _), _) ->
      error_unsupported ~suggestion:"$KeyMirror" cx t op
    | (EvalT _, _) -> error_unsupported cx t op
    | (OpenT (reason, id), _) -> elab_open cx ~seen reason id op
    | (TypeDestructorTriggerT _, _)
    | (InternalT _, _) ->
      error_unsupported cx t op
    | (AnnotT (r, t, _), _) ->
      let t = reposition cx (loc_of_reason r) t in
      elab_t cx ~seen t op
    (*********************************************************************)
    (* UseT TypeT (runtime types derive static types through annotation) *)
    (*********************************************************************)
    (* First handle catch-all cases of subtyping_kit.ml *)
    | ((MaybeT _ | OptionalT _), Annot_UseT_TypeT _) -> error_unsupported cx t op
    | (ThisTypeAppT (reason_tapp, c, this, ts), Annot_UseT_TypeT _) ->
      let reason_op = Type.AConstraint.reason_of_op op in
      let tc = specialize_class cx c reason_op reason_tapp ts in
      let t = this_specialize cx reason_tapp this tc in
      elab_t cx t op
    | ( TypeAppT { reason = reason_tapp; use_op = typeapp_use_op; type_; targs; use_desc = _ },
        Annot_UseT_TypeT _
      ) ->
      (* NOTE omitting TypeAppExpansion.push_unless_loop check. *)
      let reason_op = Type.AConstraint.reason_of_op op in
      let t = mk_typeapp_instance cx ~use_op:typeapp_use_op ~reason_op ~reason_tapp type_ targs in
      elab_t cx t op
    | (DefT (reason_tapp, _, PolyT { tparams_loc; tparams = ids; _ }), Annot_UseT_TypeT reason) ->
      Flow_js_utils.add_output
        cx
        (Error_message.EMissingTypeArgs
           {
             reason_op = reason;
             reason_tapp;
             reason_arity = Flow_js_utils.mk_poly_arity_reason tparams_loc;
             min_arity = Flow_js_utils.poly_minimum_arity ids;
             max_arity = Nel.length ids;
           }
        );
      AnyT.error reason
    | (ThisClassT (r, i, is_this, this_name), Annot_UseT_TypeT reason) ->
      let c = Flow_js_utils.fix_this_class cx reason (r, i, is_this, this_name) in
      elab_t cx c op
    | (DefT (_, _, ClassT it), Annot_UseT_TypeT reason) ->
      (* a class value annotation becomes the instance type *)
      reposition cx (loc_of_reason reason) it
    | (DefT (_, _, TypeT (_, l)), Annot_UseT_TypeT _) -> l
    | (DefT (lreason, trust, EnumObjectT enum), Annot_UseT_TypeT _) ->
      (* an enum object value annotation becomes the enum type *)
      mk_enum_type ~trust lreason enum
    | (DefT (enum_reason, _, EnumT _), Annot_UseT_TypeT reason) ->
      Flow_js_utils.add_output cx Error_message.(EEnumMemberUsedAsType { reason; enum_reason });
      AnyT.error reason
    | (l, Annot_UseT_TypeT reason_use) ->
      (match l with
      (* Short-circut as we already error on the unresolved name. *)
      | AnyT (_, AnyError _) -> ()
      | AnyT _ -> Flow_js_utils.add_output cx Error_message.(EAnyValueUsedAsType { reason_use })
      | _ -> Flow_js_utils.add_output cx Error_message.(EValueUsedAsType { reason_use }));
      AnyT.error reason_use
    | (l, Annot_ConcretizeForImportsExports (_, f)) -> f l
    (*******************)
    (* `import typeof` *)
    (*******************)
    | (_, Annot_ImportTypeofT (reason, export_name)) ->
      ImportTypeofTKit.on_concrete_type
        cx
        dummy_trace
        ~mk_typeof_annotation:ConsGen.mk_typeof_annotation
        reason
        export_name
        t
    (******************)
    (* Module exports *)
    (******************)
    | (ModuleT m, Annot_ExportNamedT (reason, tmap, export_kind)) ->
      ExportNamedTKit.on_ModuleT cx dummy_trace (reason, tmap, export_kind) t m
    | (_, Annot_AssertExportIsTypeT (_, name)) ->
      AssertExportIsTypeTKit.on_concrete_type cx dummy_trace name t
    | (ModuleT m, Annot_CopyNamedExportsT (reason, target_module_t)) ->
      CopyNamedExportsTKit.on_ModuleT cx dummy_trace (reason, target_module_t) m
    | (ModuleT m, Annot_CopyTypeExportsT (reason, target_module_t)) ->
      CopyTypeExportsTKit.on_ModuleT cx dummy_trace (reason, target_module_t) m
    | (_, Annot_ExportTypeT (reason, export_name, target_module_t)) ->
      ExportTypeTKit.on_concrete_type cx dummy_trace (reason, export_name, target_module_t) t
    | (AnyT (lreason, _), Annot_CopyNamedExportsT (reason, target_module)) ->
      CopyNamedExportsTKit.on_AnyT cx dummy_trace lreason (reason, target_module)
    | (AnyT (lreason, _), Annot_CopyTypeExportsT (reason, target_module)) ->
      CopyTypeExportsTKit.on_AnyT cx dummy_trace lreason (reason, target_module)
    | (_, Annot_CJSExtractNamedExportsT (reason, local_module)) ->
      CJSExtractNamedExportsTKit.on_concrete_type cx dummy_trace (reason, local_module) t
    (******************)
    (* Module imports *)
    (******************)
    | (ModuleT m, Annot_CJSRequireT { reason; is_strict; legacy_interop }) ->
      CJSRequireTKit.on_ModuleT cx dummy_trace (reason, is_strict, legacy_interop) m
    | (ModuleT m, Annot_ImportModuleNsT (reason, is_strict)) ->
      ImportModuleNsTKit.on_ModuleT cx dummy_trace (reason, is_strict) m
    | (ModuleT m, Annot_ImportDefaultT (reason, import_kind, local, is_strict)) ->
      let (_name_loc_opt, t) =
        ImportDefaultTKit.on_ModuleT
          cx
          dummy_trace
          ~mk_typeof_annotation:ConsGen.mk_typeof_annotation
          ~assert_import_is_value
          ~with_concretized_type
          (reason, import_kind, local, is_strict)
          m
      in
      t
    | (ModuleT m, Annot_ImportNamedT (reason, import_kind, export_name, module_name, is_strict)) ->
      let (_name_loc_opt, t) =
        ImportNamedTKit.on_ModuleT
          cx
          dummy_trace
          ~mk_typeof_annotation:ConsGen.mk_typeof_annotation
          ~assert_import_is_value
          ~with_concretized_type
          (reason, import_kind, export_name, module_name, is_strict)
          m
      in
      t
    | (AnyT (lreason, src), (Annot_CJSRequireT { reason; _ } | Annot_ImportModuleNsT (reason, _)))
      ->
      Flow_js_utils.check_untyped_import cx ImportValue lreason reason;
      AnyT.why src reason
    | (AnyT (lreason, src), Annot_ImportDefaultT (reason, import_kind, _, _)) ->
      Flow_js_utils.check_untyped_import cx import_kind lreason reason;
      AnyT.why src reason
    | (AnyT (lreason, src), Annot_ImportNamedT (reason, import_kind, _, _, _)) ->
      Flow_js_utils.check_untyped_import cx import_kind lreason reason;
      AnyT.why src reason
    (************************************)
    (* Wildcards (idx, maybe, optional) *)
    (************************************)
    | (MaybeT _, _)
    | (OptionalT _, _) ->
      (* These are rare in practice. Will consider adding support if we hit this
       * error case. *)
      error_unsupported cx t op
    (*********************)
    (* Type applications *)
    (*********************)
    | (ThisTypeAppT (reason_tapp, c, this, ts), _) ->
      let reason_op = Type.AConstraint.reason_of_op op in
      let tc = specialize_class cx c reason_op reason_tapp ts in
      let t = this_specialize cx reason_tapp this tc in
      elab_t cx t op
    | (TypeAppT { reason = reason_tapp; use_op = typeapp_use_op; type_; targs; use_desc = _ }, _) ->
      (* NOTE omitting TypeAppExpansion.push_unless_loop check. *)
      let reason_op = Type.AConstraint.reason_of_op op in
      let t = mk_typeapp_instance cx ~use_op:typeapp_use_op ~reason_op ~reason_tapp type_ targs in
      elab_t cx t op
    (****************)
    (* Opaque types *)
    (****************)
    | (OpaqueT (_, { super_t = Some super_t; _ }), Annot_ToStringT { reason; _ }) ->
      elab_t cx super_t (Annot_ToStringT { orig_t = Some t; reason })
    | (OpaqueT (r, { underlying_t = Some t; _ }), _)
      when ALoc.source (loc_of_reason r) = ALoc.source (def_loc_of_reason r) ->
      elab_t cx ~seen t op
    (********)
    (* Keys *)
    (********)
    | (KeysT _, Annot_ToStringT _) -> t
    | (KeysT (reason, t), _) ->
      let t = elab_t cx t (Annot_GetKeysT reason) in
      elab_t cx t op
    | (DefT (_, _, ObjT { flags; props_tmap; _ }), Annot_GetKeysT reason_op) ->
      let dict_t = Obj_type.get_dict_opt flags.obj_kind in
      (* flow the union of keys of l to keys *)
      let keylist = Flow_js_utils.keylist_of_props (Context.find_props cx props_tmap) reason_op in
      let keylist =
        match dict_t with
        | None -> keylist
        | Some { key; _ } ->
          let key = elab_t cx key (Annot_ToStringT { orig_t = None; reason = reason_op }) in
          key :: keylist
      in
      union_of_ts reason_op keylist
    | (DefT (_, _, InstanceT { inst; _ }), Annot_GetKeysT reason_op) ->
      (* methods are not enumerable, so only walk fields *)
      let own_props = Context.find_props cx inst.own_props in
      let keylist = Flow_js_utils.keylist_of_props own_props reason_op in
      union_of_ts reason_op keylist
    | (AnyT _, Annot_GetKeysT reason_op) -> with_trust literal_trust (StrT.why reason_op)
    (***********)
    (* $Values *)
    (***********)
    | (DefT (_, _, ObjT o), Annot_GetValuesT reason) ->
      Flow_js_utils.get_values_type_of_obj_t cx o reason
    | (DefT (_, _, InstanceT { inst = { own_props; inst_dict; _ }; _ }), Annot_GetValuesT reason) ->
      Flow_js_utils.get_values_type_of_instance_t cx own_props inst_dict reason
    (* Any will always be ok *)
    | (AnyT (_, src), Annot_GetValuesT reason) -> AnyT.why src reason
    (********************************)
    (* Union and intersection types *)
    (********************************)
    | (UnionT (reason, rep), Annot_MakeExactT reason_op) ->
      let ts = UnionRep.members rep in
      let f t = ExactT (reason_op, t) in
      let ts' = Base.List.map ts ~f in
      let reason' = repos_reason (loc_of_reason reason_op) reason in
      union_of_ts reason' ts'
    | (UnionT _, Annot_ObjKitT (reason, use_op, resolve_tool, tool)) ->
      object_kit_concrete cx use_op op reason resolve_tool tool t
    | (UnionT (_, rep), _) ->
      let reason = Type.AConstraint.reason_of_op op in
      let ts = UnionRep.members rep in
      let ts = Base.List.map ~f:(fun t -> elab_t cx ~seen t op) ts in
      union_of_ts reason ts
    | (IntersectionT _, Annot_ObjKitT (reason, use_op, resolve_tool, tool)) ->
      object_kit_concrete cx use_op op reason resolve_tool tool t
    | (IntersectionT _, _) ->
      (* Handling intersections as inputs would require use of speculation. Instead,
       * we ask the user to provide a simpler type. *)
      error_unsupported cx t op
    (*************)
    (* Unary not *)
    (*************)
    (* any propagation *)
    | (AnyT _, Annot_NotT _) -> t
    (* !x when x is of unknown truthiness *)
    | (DefT (_, trust, BoolT None), Annot_NotT reason)
    | (DefT (_, trust, StrT AnyLiteral), Annot_NotT reason)
    | (DefT (_, trust, NumT AnyLiteral), Annot_NotT reason) ->
      BoolT.at (loc_of_reason reason) trust
    (* !x when x is falsy *)
    | (DefT (_, trust, BoolT (Some false)), Annot_NotT reason)
    | (DefT (_, trust, SingletonBoolT false), Annot_NotT reason)
    | (DefT (_, trust, StrT (Literal (_, OrdinaryName ""))), Annot_NotT reason)
    | (DefT (_, trust, SingletonStrT (OrdinaryName "")), Annot_NotT reason)
    | (DefT (_, trust, NumT (Literal (_, (0., _)))), Annot_NotT reason)
    | (DefT (_, trust, SingletonNumT (0., _)), Annot_NotT reason)
    | (DefT (_, trust, NullT), Annot_NotT reason)
    | (DefT (_, trust, VoidT), Annot_NotT reason) ->
      let reason = replace_desc_reason (RBooleanLit true) reason in
      DefT (reason, trust, BoolT (Some true))
    (* !x when x is truthy *)
    | (_, Annot_NotT reason) ->
      let reason = replace_desc_reason (RBooleanLit false) reason in
      DefT (reason, bogus_trust (), BoolT (Some false))
    (*****************************)
    (* Singleton primitive types *)
    (*****************************)
    | (DefT (reason, trust, SingletonStrT key), _) ->
      elab_t cx (DefT (reason, trust, StrT (Literal (None, key)))) op
    | (DefT (reason, trust, SingletonNumT lit), _) ->
      elab_t cx (DefT (reason, trust, NumT (Literal (None, lit)))) op
    | (DefT (reason, trust, SingletonBoolT b), _) ->
      elab_t cx (DefT (reason, trust, BoolT (Some b))) op
    | (NullProtoT reason, _) -> elab_t cx (DefT (reason, bogus_trust (), NullT)) op
    (*********)
    (* Exact *)
    (*********)
    | (ExactT (r, t), _) ->
      let t = push_type_alias_reason r t in
      let t = make_exact cx r t in
      elab_t cx t op
    | (DefT (reason_obj, trust, ObjT obj), Annot_MakeExactT reason_op) ->
      TypeUtil.make_exact_object ~reason_obj trust obj ~reason_op
    | (AnyT (_, src), Annot_MakeExactT reason_op) -> AnyT.why src reason_op
    | (DefT (_, trust, VoidT), Annot_MakeExactT reason_op) -> VoidT.why reason_op trust
    | (DefT (_, trust, EmptyT), Annot_MakeExactT reason_op) -> EmptyT.why reason_op trust
    | (_, Annot_MakeExactT reason_op) ->
      Flow_js_utils.add_output cx (Error_message.EUnsupportedExact (reason_op, reason_of_t t));
      AnyT.error reason_op
    (**********)
    (* Mixins *)
    (**********)
    | (ThisClassT (_, DefT (_, trust, InstanceT { inst; _ }), is_this, this_name), Annot_MixinT r)
      ->
      (* A class can be viewed as a mixin by extracting its immediate properties,
       * and "erasing" its static and super *)
      let static = ObjProtoT r in
      let super = ObjProtoT r in
      this_class_type
        (DefT (r, trust, InstanceT { static; super; implements = []; inst }))
        is_this
        this_name
    | ( DefT
          ( _,
            _,
            PolyT
              {
                tparams_loc;
                tparams = xs;
                t_out = ThisClassT (_, DefT (_, trust, InstanceT { inst; _ }), is_this, this_name);
                _;
              }
          ),
        Annot_MixinT r
      ) ->
      let static = ObjProtoT r in
      let super = ObjProtoT r in
      let instance = DefT (r, trust, InstanceT { static; super; implements = []; inst }) in
      poly_type
        (Type.Poly.generate_id ())
        tparams_loc
        xs
        (this_class_type instance is_this this_name)
    | (AnyT (_, src), Annot_MixinT r) -> AnyT.why src r
    (***********************)
    (* Type specialization *)
    (***********************)
    | ( DefT (_, _, PolyT { tparams_loc; tparams = xs; t_out = t; id }),
        Annot_SpecializeT (use_op, reason_op, reason_tapp, ts)
      ) ->
      let ts = Base.Option.value ts ~default:[] in
      mk_typeapp_of_poly cx ~use_op ~reason_op ~reason_tapp id tparams_loc xs t ts
    | ((DefT (_, _, ClassT _) | ThisClassT _), Annot_SpecializeT (_, _, _, None)) -> t
    | (AnyT _, Annot_SpecializeT _) -> t
    | (ThisClassT (_, i, _, this_name), Annot_ThisSpecializeT (reason, this)) ->
      let i = subst cx (Subst_name.Map.singleton this_name this) i in
      reposition cx (loc_of_reason reason) i
    (* this-specialization of non-this-abstracted classes is a no-op *)
    | (DefT (_, _, ClassT i), Annot_ThisSpecializeT (reason, _this)) ->
      reposition cx (loc_of_reason reason) i
    | (AnyT _, Annot_ThisSpecializeT (reason, _)) -> reposition cx (loc_of_reason reason) t
    (**********************)
    (* Type instantiation *)
    (**********************)
    | (DefT (reason_tapp, _, PolyT { tparams_loc; tparams = ids; t_out = t; _ }), _) ->
      let use_op = unknown_use in
      let reason_op = Type.AConstraint.reason_of_op op in
      let (t, _) = instantiate_poly cx ~use_op ~reason_op ~reason_tapp (tparams_loc, ids, t) in
      elab_t cx t op
    | (ThisClassT (r, i, is_this, this_name), _) ->
      let reason = Type.AConstraint.reason_of_op op in
      let t = Flow_js_utils.fix_this_class cx reason (r, i, is_this, this_name) in
      elab_t cx t op
    (*****************************)
    (* React Abstract Components *)
    (*****************************)
    | (DefT (r, _, ReactAbstractComponentT _), (Annot_GetPropT _ | Annot_GetElemT _)) ->
      let statics =
        Flow_js_utils.lookup_builtin_strict cx (OrdinaryName "React$AbstractComponentStatics") r
      in
      elab_t cx statics op
    (****************)
    (* Custom types *)
    (****************)
    | (DefT (reason, trust, CharSetT _), _) -> elab_t cx (StrT.why reason trust) op
    | (CustomFunT (r, _), _) when function_like_op op -> elab_t cx (FunProtoT r) op
    (*****************)
    (* ObjTestProtoT *)
    (*****************)
    | (AnyT (_, src), Annot_ObjTestProtoT reason_op) -> AnyT.why src reason_op
    | (DefT (_, trust, NullT), Annot_ObjTestProtoT reason_op) -> NullProtoT.why reason_op trust
    | (_, Annot_ObjTestProtoT reason_op) ->
      if Flow_js_utils.object_like t then
        reposition cx (loc_of_reason reason_op) t
      else
        let () =
          Flow_js_utils.add_output
            cx
            (Error_message.EInvalidPrototype (loc_of_reason reason_op, reason_of_t t))
        in
        ObjProtoT.why reason_op |> with_trust bogus_trust
    (***************)
    (* Get statics *)
    (***************)
    | (DefT (_, _, InstanceT { static; _ }), Annot_GetStaticsT reason_op) ->
      reposition cx (loc_of_reason reason_op) static
    | (AnyT (_, src), Annot_GetStaticsT reason_op) -> AnyT.why src reason_op
    | (ObjProtoT _, Annot_GetStaticsT reason_op) ->
      (* ObjProtoT not only serves as the instance type of the root class, but
       * also as the statics of the root class. *)
      reposition cx (loc_of_reason reason_op) t
    (***************)
    (* LookupT pt1 *)
    (***************)
    | ( DefT (_lreason, _, InstanceT { super; inst; _ }),
        Annot_LookupT (reason_op, use_op, (Named _ as propref), objt)
      ) ->
      let react_dro =
        match objt with
        | DefT (_, _, ObjT o) -> o.flags.react_dro
        | _ -> None
      in
      (match
         GetPropTKit.get_instance_prop
           cx
           dummy_trace
           ~use_op
           ~ignore_dicts:true
           inst
           propref
           reason_op
       with
      | Some (p, _) ->
        GetPropTKit.perform_read_prop_action
          cx
          dummy_trace
          use_op
          propref
          (Property.type_ p)
          reason_op
          react_dro
      | None -> Get_prop_helper.cg_lookup_ cx use_op super reason_op propref objt)
    | (DefT (_, _, InstanceT _), Annot_LookupT (_, _, Computed _, _)) -> error_unsupported cx t op
    | (DefT (_, _, ObjT o), Annot_LookupT (reason_op, use_op, propref, objt)) ->
      let react_dro =
        match objt with
        | DefT (_, _, ObjT o) -> o.flags.react_dro
        | _ -> None
      in
      (match GetPropTKit.get_obj_prop cx dummy_trace o propref reason_op with
      | Some (p, _) ->
        GetPropTKit.perform_read_prop_action cx dummy_trace use_op propref p reason_op react_dro
      | None -> Get_prop_helper.cg_lookup_ cx use_op o.proto_t reason_op propref objt)
    | (AnyT _, Annot_LookupT (reason_op, _use_op, _propref, _)) -> AnyT.untyped reason_op
    (************)
    (* DRO *)
    (************)
    | (DefT (r, t, ObjT ({ Type.flags; _ } as o)), Annot_DeepReadOnlyT (_, props_loc)) ->
      DefT (r, t, ObjT { o with Type.flags = { flags with react_dro = Some props_loc } })
    | ( DefT (r, trust, ArrT (TupleAT { elem_t; elements; arity; react_dro = _ })),
        Annot_DeepReadOnlyT (_, props_loc)
      ) ->
      DefT (r, trust, ArrT (TupleAT { elem_t; elements; arity; react_dro = Some props_loc }))
    | ( DefT (r, trust, ArrT (ArrayAT { elem_t; tuple_view; react_dro = _ })),
        Annot_DeepReadOnlyT (_, props_loc)
      ) ->
      DefT (r, trust, ArrT (ArrayAT { elem_t; tuple_view; react_dro = Some props_loc }))
    | (DefT (r, trust, ArrT (ROArrayAT (t, _))), Annot_DeepReadOnlyT (_, props_loc)) ->
      DefT (r, trust, ArrT (ROArrayAT (t, Some props_loc)))
    (************)
    (* ObjRestT *)
    (************)
    | ( DefT (reason_obj, _, ObjT { props_tmap; flags = { obj_kind; _ }; _ }),
        Annot_ObjRestT (reason_op, xs)
      ) ->
      Flow_js_utils.objt_to_obj_rest cx props_tmap ~obj_kind ~reason_op ~reason_obj xs
    | (DefT (_, _, InstanceT _), Annot_ObjRestT _) ->
      (* This implementation relies on unsealed objects and set-prop logic that is
       * hard to implement in annotation inference. *)
      error_unsupported cx t op
    | (AnyT (_, src), Annot_ObjRestT (reason, _)) -> AnyT.why src reason
    | (ObjProtoT _, Annot_ObjRestT (reason, _)) ->
      Obj_type.mk_with_proto cx reason ~obj_kind:Exact t
    | (DefT (_, _, (NullT | VoidT)), Annot_ObjRestT (reason, _)) ->
      Obj_type.mk ~obj_kind:Exact cx reason
    (************)
    (* GetPropT *)
    (************)
    | ( DefT (reason_instance, _, InstanceT { super; inst; _ }),
        Annot_GetPropT (reason_op, use_op, (Named _ as propref))
      ) ->
      GetPropTKit.read_instance_prop
        cx
        dummy_trace
        ~use_op
        ~instance_t:t
        ~id:None
        ~method_accessible:false
        ~super
        ~lookup_kind:(Strict reason_instance)
        inst
        propref
        reason_op
    | (DefT (_, _, InstanceT _), Annot_GetPropT (_, _, Computed _)) -> error_unsupported cx t op
    | ( DefT (_, _, ObjT _),
        Annot_GetPropT (reason_op, _, Named { name = OrdinaryName "constructor"; _ })
      ) ->
      Unsoundness.why Constructor reason_op
    | (DefT (reason_obj, _, ObjT o), Annot_GetPropT (reason_op, use_op, propref)) ->
      GetPropTKit.read_obj_prop cx dummy_trace ~use_op o propref reason_obj reason_op None
    | (AnyT _, Annot_GetPropT (reason_op, _, _)) -> AnyT (reason_op, Untyped)
    | ( DefT (reason, _, ClassT instance),
        Annot_GetPropT (_, _, Named { name = OrdinaryName "prototype"; _ })
      ) ->
      reposition cx (loc_of_reason reason) instance
    (**************)
    (* Object Kit *)
    (**************)
    | (_, Annot_ObjKitT (reason, use_op, resolve_tool, tool)) ->
      object_kit_concrete cx use_op op reason resolve_tool tool t
    (********************)
    (* GetElemT / ElemT *)
    (********************)
    | (DefT (_, trust, StrT _), Annot_GetElemT (reason_op, _use_op, _index)) ->
      (* NOTE bypassing check that index is a number *)
      StrT.why reason_op trust
    | ( (DefT (_, _, (ObjT _ | ArrT _ | InstanceT _)) | AnyT _),
        Annot_GetElemT (reason_op, use_op, key)
      ) ->
      elab_t cx key (Annot_ElemT (reason_op, use_op, t))
    | (_, Annot_ElemT (reason_op, use_op, (DefT (_, _, (ObjT _ | InstanceT _)) as obj))) ->
      let propref = Flow_js_utils.propref_for_elem_t t in
      elab_t cx obj (Annot_GetPropT (reason_op, use_op, propref))
    | (_, Annot_ElemT (reason_op, _use_op, (AnyT _ as _obj))) ->
      let value = AnyT.untyped reason_op in
      reposition cx (loc_of_reason reason_op) value
    | (AnyT _, Annot_ElemT (reason_op, _, DefT (_, _, ArrT arrtype))) ->
      let value = elemt_of_arrtype arrtype in
      reposition cx (loc_of_reason reason_op) value
    | (DefT (_, _, NumT _), Annot_ElemT (reason_op, use_op, DefT (reason_tup, _, ArrT arrtype))) ->
      let (value, _, _, _) =
        Flow_js_utils.array_elem_check
          ~write_action:false
          cx
          dummy_trace
          t
          use_op
          reason_op
          reason_tup
          arrtype
      in
      reposition cx (loc_of_reason reason_op) value
    | (DefT (_, trust, ObjT o), Annot_ObjKeyMirror reason_op) ->
      Flow_js_utils.obj_key_mirror cx trust o reason_op
    | (DefT (_, trust, ObjT o), Annot_ObjMapConst (reason_op, target)) ->
      Flow_js_utils.obj_map_const cx trust o reason_op target
    (***********************)
    (* Opaque types (pt 2) *)
    (***********************)
    | (OpaqueT (_, { super_t = Some t; _ }), _) -> elab_t cx t op
    (**************************)
    (* Binary arith operators *)
    (**************************)
    | (lhs_t, Annot_ArithT { reason; flip; rhs_t; kind }) ->
      if Flow_js_utils.needs_resolution rhs_t || Flow_js_utils.is_generic rhs_t then
        elab_t cx rhs_t (Annot_ArithT { reason; flip = not flip; rhs_t = lhs_t; kind })
      else
        let (lhs_t, rhs_t) =
          if flip then
            (rhs_t, lhs_t)
          else
            (lhs_t, rhs_t)
        in
        Flow_js_utils.flow_arith cx reason lhs_t rhs_t kind
    (*************************)
    (* Unary arith operators *)
    (*************************)
    | (l, Annot_UnaryArithT (reason, kind)) -> Flow_js_utils.flow_unary_arith cx l reason kind
    (********************)
    (* Function Statics *)
    (********************)
    | (DefT (reason, _, FunT (static, _)), _) when object_like_op op ->
      let static = reposition cx (loc_of_reason reason) static in
      elab_t cx static op
    (*****************)
    (* Class statics *)
    (*****************)
    | (DefT (reason, _, ClassT instance), _) when object_like_op op ->
      let t = get_statics cx reason instance in
      elab_t cx t op
    (*********)
    (* Enums *)
    (*********)
    | ( DefT (enum_reason, trust, EnumObjectT enum),
        Annot_GetPropT (access_reason, use_op, Named { reason = prop_reason; name; _ })
      ) ->
      let access = (use_op, access_reason, None, (prop_reason, name)) in
      GetPropTKit.on_EnumObjectT cx dummy_trace enum_reason trust enum access
    | (DefT (enum_reason, _, EnumObjectT _), Annot_GetElemT (reason_op, _, elem)) ->
      let reason = reason_of_t elem in
      Flow_js_utils.add_output
        cx
        (Error_message.EEnumInvalidMemberAccess
           { member_name = None; suggestion = None; reason; enum_reason }
        );
      AnyT.error reason_op
    (***************)
    (* LookupT pt2 *)
    (***************)
    | (ObjProtoT _, Annot_LookupT (reason_op, _, Named { name; _ }, _))
      when Flow_js_utils.is_object_prototype_method name ->
      Flow_js_utils.lookup_builtin_strict cx (OrdinaryName "Object") reason_op
    | (FunProtoT _, Annot_LookupT (reason_op, _, Named { name; _ }, _))
      when Flow_js_utils.is_function_prototype name ->
      Flow_js_utils.lookup_builtin_strict cx (OrdinaryName "Function") reason_op
    | ( (DefT (_, _, NullT) | ObjProtoT _ | FunProtoT _),
        Annot_LookupT (reason_op, use_op, Named { reason = reason_prop; name; _ }, _)
      ) ->
      let error_message =
        Error_message.EPropNotFound
          { reason_prop; reason_obj = reason_op; prop_name = Some name; use_op; suggestion = None }
      in
      Flow_js_utils.add_output cx error_message;
      AnyT.error_of_kind UnresolvedName reason_op
    (****************************************)
    (* Object, function, etc. library calls *)
    (****************************************)
    | (ObjProtoT reason, _) ->
      let use_desc = true in
      let obj_proto = get_builtin_type cx reason ~use_desc (OrdinaryName "Object") in
      elab_t cx obj_proto op
    | (FunProtoT reason, _) ->
      let use_desc = true in
      let fun_proto = get_builtin_type cx reason ~use_desc (OrdinaryName "Function") in
      elab_t cx fun_proto op
    (*************)
    (* ToStringT *)
    (*************)
    | (DefT (_, _, StrT _), Annot_ToStringT _) -> t
    | (_, Annot_ToStringT { reason; _ }) -> with_trust bogus_trust (StrT.why reason)
    (************)
    (* GetPropT *)
    (************)
    | (DefT (reason, _, ArrT (ArrayAT { elem_t; _ })), (Annot_GetPropT _ | Annot_LookupT _)) ->
      let arr = get_builtin_typeapp cx reason (OrdinaryName "Array") [elem_t] in
      elab_t cx arr op
    | ( DefT (reason, trust, ArrT (TupleAT { arity; _ })),
        Annot_GetPropT (reason_op, _, Named { name = OrdinaryName "length"; _ })
      ) ->
      GetPropTKit.on_array_length cx dummy_trace reason trust arity reason_op
    | ( DefT (reason, _, ArrT ((TupleAT _ | ROArrayAT _) as arrtype)),
        (Annot_GetPropT _ | Annot_LookupT _)
      ) ->
      let t = elemt_of_arrtype arrtype in
      elab_t cx (get_builtin_typeapp cx reason (OrdinaryName "$ReadOnlyArray") [t]) op
    (************************)
    (* Promoting primitives *)
    (************************)
    | (DefT (reason, _, StrT _), _) when primitive_promoting_op op ->
      let builtin = get_builtin_type cx reason ~use_desc:true (OrdinaryName "String") in
      elab_t cx builtin op
    | (DefT (reason, _, NumT _), _) when primitive_promoting_op op ->
      let builtin = get_builtin_type cx reason ~use_desc:true (OrdinaryName "Number") in
      elab_t cx builtin op
    | (DefT (reason, _, BoolT _), _) when primitive_promoting_op op ->
      let builtin = get_builtin_type cx reason ~use_desc:true (OrdinaryName "Boolean") in
      elab_t cx builtin op
    | (DefT (reason, _, SymbolT), _) when primitive_promoting_op op ->
      let builtin = get_builtin_type cx reason ~use_desc:true (OrdinaryName "Symbol") in
      elab_t cx builtin op
    | (DefT (lreason, _, MixedT Mixed_function), (Annot_GetPropT _ | Annot_LookupT _)) ->
      elab_t cx (FunProtoT lreason) op
    | (_, _) ->
      let open Error_message in
      let reason_op = reason_of_op op in
      let lower = (reason_of_t t, Flow_js_utils.error_message_kind_of_lower t) in
      let upper = (reason_op, IncompatibleUnclassified (string_of_operation op)) in
      let use_op = use_op_of_operation op in
      Flow_js_utils.add_output cx (EIncompatible { lower; upper; use_op; branches = [] });
      AnyT.error reason_op

  and get_builtin_type cx reason ?(use_desc = false) name =
    let t = Flow_js_utils.lookup_builtin_strict cx name reason in
    mk_instance_raw cx reason ~use_desc ~reason_type:(reason_of_t t) t

  and get_builtin cx ?trace:_ x reason =
    let builtin = Flow_js_utils.lookup_builtin_strict cx x reason in
    let f id = resolve_id cx reason id builtin in
    mk_lazy_tvar cx reason f

  and specialize cx t use_op reason_op reason_tapp ts =
    elab_t cx t (Annot_SpecializeT (use_op, reason_op, reason_tapp, ts))

  and this_specialize cx reason this t = elab_t cx t (Annot_ThisSpecializeT (reason, this))

  and specialize_class cx c reason_op reason_tapp ts =
    match ts with
    | None -> c
    | Some ts -> specialize cx c unknown_use reason_op reason_tapp (Some ts)

  and mk_type_reference cx reason c =
    let f id = resolve_id cx reason id (elab_t cx c (Annot_UseT_TypeT reason)) in
    let tvar = mk_lazy_tvar cx reason f in
    AnnotT (reason, tvar, false)

  and mk_instance cx ?trace:_ instance_reason ?use_desc c =
    mk_instance_raw cx instance_reason ?use_desc ~reason_type:instance_reason c

  and mk_instance_raw cx instance_reason ?(use_desc = false) ~reason_type c =
    let source = elab_t cx c (Annot_UseT_TypeT reason_type) in
    AnnotT (instance_reason, source, use_desc)

  and mk_typeapp_instance cx ~use_op ~reason_op ~reason_tapp c ts =
    let t = specialize cx c use_op reason_op reason_tapp (Some ts) in
    mk_instance_raw cx reason_tapp ~reason_type:(reason_of_t c) t

  and get_statics cx reason t = elab_t cx t (Annot_GetStaticsT reason)

  and get_prop cx use_op reason ?(op_reason = reason) name t =
    elab_t
      cx
      t
      (Annot_GetPropT (op_reason, use_op, Named { reason; name; from_indexed_access = false }))

  and get_elem cx use_op reason ~key t = elab_t cx t (Annot_GetElemT (reason, use_op, key))

  and qualify_type cx use_op reason (reason_name, name) t =
    let open Type in
    let f id =
      let t =
        elab_t
          cx
          t
          (Annot_GetPropT
             (reason, use_op, Named { reason = reason_name; name; from_indexed_access = false })
          )
      in
      resolve_id cx reason id t
    in
    mk_lazy_tvar cx reason f

  (* Unlike Flow_js, types in this module are 0->1, so there is no need for a
   * mechanism similar to BecomeT of Flow_js. *)
  and mk_typeof_annotation cx ?trace:_ reason t =
    let annot_loc = loc_of_reason reason in
    let t = reposition cx (loc_of_reason reason) t in
    AnnotT (opt_annot_reason ~annot_loc reason, t, false)

  and assert_export_is_type cx reason name t =
    let f id =
      let t = elab_t cx t (Annot_AssertExportIsTypeT (reason, Reason.OrdinaryName name)) in
      resolve_id cx reason id t
    in
    mk_lazy_tvar cx reason f

  and cjs_require cx t reason is_strict legacy_interop =
    elab_t cx t (Annot_CJSRequireT { reason; is_strict; legacy_interop })

  and export_named cx reason kind named t = elab_t cx t (Annot_ExportNamedT (reason, named, kind))

  and cjs_extract_named_exports cx reason local_module t =
    elab_t cx t (Annot_CJSExtractNamedExportsT (reason, local_module))

  and import_typeof cx reason export_name t = elab_t cx t (Annot_ImportTypeofT (reason, export_name))

  and import_default cx reason import_kind export_name module_name is_strict t =
    elab_t cx t (Annot_ImportDefaultT (reason, import_kind, (export_name, module_name), is_strict))

  and import_named cx reason import_kind export_name module_name is_strict t =
    elab_t cx t (Annot_ImportNamedT (reason, import_kind, export_name, module_name, is_strict))

  and import_ns cx reason is_strict t = elab_t cx t (Annot_ImportModuleNsT (reason, is_strict))

  and copy_named_exports cx ~from_ns reason ~module_t =
    elab_t cx from_ns (Annot_CopyNamedExportsT (reason, module_t))

  and copy_type_exports cx ~from_ns reason ~module_t =
    elab_t cx from_ns (Annot_CopyTypeExportsT (reason, module_t))

  and arith cx reason lhs_t rhs_t kind =
    elab_t cx lhs_t (Annot_ArithT { reason; flip = false; rhs_t; kind })

  and unary_arith cx reason_op t kind = elab_t cx t (Annot_UnaryArithT (reason_op, kind))

  and unary_not cx reason_op t = elab_t cx t (Annot_NotT reason_op)

  and mixin cx reason t = elab_t cx t (Annot_MixinT reason)

  and obj_rest cx reason xs t = elab_t cx t (Annot_ObjRestT (reason, xs))

  and arr_rest cx _use_op reason_op _i t = error_unsupported_reason cx t reason_op

  and widen_obj_type cx ?trace:_ ~use_op reason t =
    match t with
    | OpenT (_, id) ->
      let open Constraint in
      begin
        match Context.find_graph cx id with
        | exception Union_find.Tvar_not_found _ -> error_internal_reason cx "widen_obj_type" reason
        | Unresolved _
        | Resolved _ ->
          failwith "widen_obj_type unexpected non-FullyResolved tvar"
        | FullyResolved (lazy t) -> widen_obj_type cx ~use_op reason t
      end
    | UnionT (r, rep) ->
      UnionT
        ( r,
          UnionRep.ident_map
            (fun t ->
              if is_proper_def t then
                widen_obj_type cx ~use_op reason t
              else
                t)
            rep
        )
    | t -> t

  and object_kit_concrete =
    let add_output cx msg : unit = Flow_js_utils.add_output cx msg in
    let return _cx _use_op t = t in
    let recurse cx use_op reason resolve_tool tool x =
      object_kit cx use_op reason resolve_tool tool x
    in
    let object_spread options state cx =
      let dict_check _cx _use_op _d1 _d2 = () in
      Slice_utils.object_spread
        ~dict_check
        ~widen_obj_type:(widen_obj_type ?trace:None)
        ~add_output
        ~return
        ~recurse
        options
        state
        cx
    in
    let object_rest options state cx =
      let return _ _ _ t = t in
      (* No subtyping checks in annotation inference *)
      let subt_check ~use_op:_ _ _ = () in
      Slice_utils.object_rest ~add_output ~return ~recurse ~subt_check options state cx
    in
    let check_component_config cx pmap =
      let return _ _ t = t in
      Slice_utils.check_component_config ~add_output ~return pmap cx
    in
    let object_read_only cx _use_op = Slice_utils.object_read_only cx in
    let object_partial cx _use_op = Slice_utils.object_update_optionality `Partial cx in
    let object_required cx _use_op = Slice_utils.object_update_optionality `Required cx in
    let next op cx use_op tool reason x =
      Object.(
        match tool with
        | Spread (options, state) -> object_spread options state cx use_op reason x
        | Rest (options, state) -> object_rest options state cx use_op reason x
        | Partial -> object_partial cx use_op reason x
        | Required -> object_required cx use_op reason x
        | ReadOnly -> object_read_only cx use_op reason x
        | ReactConfig _ -> error_internal cx "ReactConfig" op
        | Object.ReactCheckComponentConfig pmap -> check_component_config cx pmap use_op reason x
        | ObjectRep -> error_internal cx "ObjectRep" op
        | ObjectWiden _ -> error_internal cx "ObjectWiden" op
        | Object.ObjectMap _ ->
          (* TODO(jmbrown): Annotation inference for Mapped Types *)
          error_internal cx "ObjectMap" op
      )
    in
    let statics = get_statics in
    fun cx use_op op reason resolve_tool tool t ->
      Slice_utils.run
        ~add_output
        ~return
        ~next:(next op)
        ~recurse
        ~statics
        cx
        use_op
        reason
        resolve_tool
        tool
        t

  and object_kit cx use_op reason resolve_tool tool t =
    elab_t cx t (Annot_ObjKitT (reason, use_op, resolve_tool, tool))

  and object_spread cx use_op reason target state t =
    let resolve_tool = Type.Object.(Resolve Next) in
    let tool = Type.Object.Spread (target, state) in
    object_kit cx use_op reason resolve_tool tool t

  and object_rest cx use_op reason target state t =
    let resolve_tool = Type.Object.(Resolve Next) in
    let tool = Type.Object.Rest (target, state) in
    object_kit cx use_op reason resolve_tool tool t

  and make_readonly cx use_op reason t =
    let resolve_tool = Type.Object.(Resolve Next) in
    object_kit cx use_op reason resolve_tool Type.Object.ReadOnly t

  and make_partial cx use_op reason t =
    let resolve_tool = Type.Object.(Resolve Next) in
    object_kit cx use_op reason resolve_tool Type.Object.Partial t

  and make_required cx use_op reason t =
    let resolve_tool = Type.Object.(Resolve Next) in
    object_kit cx use_op reason resolve_tool Type.Object.Required t

  and make_exact cx reason t = elab_t cx t (Annot_MakeExactT reason)

  and obj_test_proto cx reason_op t = elab_t cx t (Annot_ObjTestProtoT reason_op)
end
