Consistently record provenance on lower bound

Summary:
Extended reasons usually accumulates provenance on the subtype except for one case: when adding an upper bound to a type variable. This oversight was causing reasons to be dropped when we have an return type containing an invariant type variable.

This diff modifies provenance generation so that we always accumulate on the lower bound during the transitivity step and makes the necessary change to the derivation generator to recognise nested lower bounds as a transitivity step.

Reviewed By: patriciamckenzie

Differential Revision: D63749923

fbshipit-source-id: af0f87c65e345721e824a33c52d0b8632a6762b1

Author: Michael Thomas

hphp/hack/src/oxidized/gen/typing_reason.rs

@@ -3,7 +3,7 @@
 // This source code is licensed under the MIT license found in the
 // LICENSE file in the "hack" directory of this source tree.
 //
-// @generated SignedSource<<c6b91a87a00d2d2cbe95c809ceda6b2f>>
+// @generated SignedSource<<918b60cd8c49eefa45db8a2647a0d896>>
 //
 // To regenerate this file, run:
 //   hphp/hack/src/oxidized_regen.sh
@@ -601,13 +601,6 @@ pub enum T_ {
     /// Lift a typing-time witness into a reason
     #[rust_to_ocaml(name = "From_witness_locl")]
     FromWitnessLocl(WitnessLocl),
-    /// Records that a type with reason [bound] acted as an upper bound
-    /// for the type with reason [of_]
-    #[rust_to_ocaml(name = "Upper_bound")]
-    UpperBound {
-        bound: Box<T_>,
-        of__: Box<T_>,
-    },
     /// Records that a type with reason [bound] acted as a lower bound
     /// for the type with reason [of_]
     #[rust_to_ocaml(name = "Lower_bound")]

hphp/hack/src/oxidized/manual/typing_reason_impl.rs

@@ -129,8 +129,7 @@ impl Reason {
             | ExprDepType(t, _, _)
             | Typeconst(t, _, _, _)
             | Instantiate(_, _, t) => t.pos(),
-            UpperBound { .. }
-            | LowerBound { .. }
+            LowerBound { .. }
             | Flow { .. }
             | PrjBoth { .. }
             | PrjOne { .. }

hphp/hack/src/oxidized_by_ref/decl_visitor/node_impl_gen.rs

@@ -3,7 +3,7 @@
 // This source code is licensed under the MIT license found in the
 // LICENSE file in the "hack" directory of this source tree.
 //
-// @generated SignedSource<<e9dc8d84abe0c00b2101757aaf332cfd>>
+// @generated SignedSource<<ee638d4fad5c87cb8e20e2ff970bb9be>>
 //
 // To regenerate this file, run:
 //   hphp/hack/src/oxidized_regen.sh
@@ -1306,15 +1306,6 @@ impl<'a> Node<'a> for T_<'a> {
             T_::Instantiate(ref __binding_0) => __binding_0.accept(v),
             T_::NoReason => {}
             T_::FromWitnessLocl(ref __binding_0) => __binding_0.accept(v),
-            T_::UpperBound {
-                bound: ref __binding_0,
-                of__: ref __binding_1,
-            } => {
-                {
-                    __binding_0.accept(v)
-                }
-                { __binding_1.accept(v) }
-            }
             T_::LowerBound {
                 bound: ref __binding_0,
                 of__: ref __binding_1,

hphp/hack/src/oxidized_by_ref/gen/typing_reason.rs

@@ -3,7 +3,7 @@
 // This source code is licensed under the MIT license found in the
 // LICENSE file in the "hack" directory of this source tree.
 //
-// @generated SignedSource<<fee740c29d05ee32c91722b5cbb04967>>
+// @generated SignedSource<<20534e1077f6a68abb03a54b9f33e45a>>
 //
 // To regenerate this file, run:
 //   hphp/hack/src/oxidized_regen.sh
@@ -555,15 +555,6 @@ pub enum T_<'a> {
     #[serde(deserialize_with = "arena_deserializer::arena", borrow)]
     #[rust_to_ocaml(name = "From_witness_locl")]
     FromWitnessLocl(&'a WitnessLocl<'a>),
-    /// Records that a type with reason [bound] acted as an upper bound
-    /// for the type with reason [of_]
-    #[rust_to_ocaml(name = "Upper_bound")]
-    UpperBound {
-        #[serde(deserialize_with = "arena_deserializer::arena", borrow)]
-        bound: &'a T_<'a>,
-        #[serde(deserialize_with = "arena_deserializer::arena", borrow)]
-        of__: &'a T_<'a>,
-    },
     /// Records that a type with reason [bound] acted as a lower bound
     /// for the type with reason [of_]
     #[rust_to_ocaml(name = "Lower_bound")]

hphp/hack/src/oxidized_by_ref/manual/typing_reason_impl.rs

@@ -193,8 +193,7 @@ impl<'a> std::fmt::Debug for T_<'a> {
                 .finish(),
             DynamicCoercion(p) => f.debug_tuple("RdynamicCoercion").field(p).finish(),
             Invalid => f.debug_tuple("Rinvalid").finish(),
-            UpperBound { .. }
-            | LowerBound { .. }
+            LowerBound { .. }
             | Flow { .. }
             | PrjBoth { .. }
             | PrjOne { .. }

hphp/hack/src/typing/typing_reason.ml

@@ -1402,13 +1402,6 @@ type _ t_ =
   (* -- Core flow constructors -- *)
   | From_witness_locl : witness_locl -> locl_phase t_
       (** Lift a typing-time witness into a reason   *)
-  | Upper_bound : {
-      bound: locl_phase t_;
-      of_: locl_phase t_;
-    }
-      -> locl_phase t_
-      (** Records that a type with reason [bound] acted as an upper bound
-          for the type with reason [of_] *)
   | Lower_bound : {
       bound: locl_phase t_;
       of_: locl_phase t_;
@@ -1527,7 +1520,6 @@ let rec to_raw_pos : type ph. ph t_ -> Pos_or_decl.t =
   (* Recurse into flow-like reasons to find the position of the leftmost witness *)
   | Flow { from = t; _ }
   | Lower_bound { bound = t; _ }
-  | Upper_bound { bound = t; _ }
   | Axiom { next = t; _ }
   | Prj_both { sub_prj = t; _ }
   | Prj_one { part = t; _ }
@@ -1609,12 +1601,6 @@ let rec map_pos :
         bound = map_pos pos pos_or_decl bound;
         of_ = map_pos pos pos_or_decl of_;
       }
-  | Upper_bound { bound; of_ } ->
-    Upper_bound
-      {
-        bound = map_pos pos pos_or_decl bound;
-        of_ = map_pos pos pos_or_decl of_;
-      }
   | Axiom { prev; axiom; next } ->
     Axiom
       {
@@ -1660,7 +1646,6 @@ let to_constructor_string : type ph. ph t_ -> string = function
   | From_witness_locl witness -> constructor_string_of_witness_locl witness
   | From_witness_decl witness -> constructor_string_of_witness_decl witness
   | Axiom _ -> "Raxiom"
-  | Upper_bound _ -> "Rupper_bound"
   | Lower_bound _ -> "Rlower_bound"
   | Flow _ -> "Rflow"
   | Prj_both _ -> "Rprj_both"
@@ -1795,7 +1780,6 @@ let rec pp_t_ : type ph. _ -> ph t_ -> unit =
     | Dynamic_coercion r -> pp_t_ fmt r
     | Flow { from; _ } -> pp_t_ fmt from
     | Axiom { next; _ } -> pp_t_ fmt next
-    | Upper_bound { bound; _ } -> pp_t_ fmt bound
     | Lower_bound { bound; _ } -> pp_t_ fmt bound
     | Prj_both { sub_prj; _ } -> pp_t_ fmt sub_prj
     | Prj_one { part; _ } -> pp_t_ fmt part
@@ -1992,14 +1976,6 @@ let rec to_json_help : type a. a t_ -> Hh_json.json list -> Hh_json.json list =
               ] );
         ])
     :: acc
-  | Upper_bound { bound; of_ } ->
-    Hh_json.(
-      JSON_Object
-        [
-          ( "Upper_bound",
-            JSON_Object [("bound", to_json bound); ("of", to_json of_)] );
-        ])
-    :: acc
   | Lower_bound { bound; of_ } ->
     Hh_json.(
       JSON_Object
@@ -2097,7 +2073,6 @@ let rec to_string_help :
     to_string_help prefix solutions r
   | From_witness_locl witness -> [witness_locl_to_string prefix witness]
   | From_witness_decl witness -> [witness_decl_to_string prefix witness]
-  | Upper_bound { bound = r; _ }
   | Lower_bound { bound = r; _ }
   | Axiom { next = r; _ }
   | Def (_, r)
@@ -2552,8 +2527,6 @@ module Constructors = struct
   let axiom_lower_bound ~bound ~of_ =
     Axiom { axiom = Lower_bound; prev = of_; next = bound }
 
-  let trans_upper_bound ~bound ~of_ = Upper_bound { bound; of_ }
-
   let trans_lower_bound ~bound ~of_ = Lower_bound { bound; of_ }
 
   let definition def of_ = Def (def, of_)
@@ -2707,8 +2680,6 @@ module Visitor = struct
         | Axiom { prev; axiom; next } ->
           Axiom
             { prev = this#on_reason prev; axiom; next = this#on_reason next }
-        | Upper_bound { bound; of_ } ->
-          Upper_bound { bound = this#on_reason bound; of_ = this#on_reason of_ }
         | Lower_bound { bound; of_ } ->
           Lower_bound { bound = this#on_reason bound; of_ = this#on_reason of_ }
         | Solved { solution; of_; in_ } ->
@@ -3237,10 +3208,6 @@ module Derivation = struct
         bound: t;
         in_: t;
       }
-    | Upper of {
-        bound: t;
-        in_: t;
-      }
     | Transitive of {
         lower: t;
         upper: t;
@@ -3252,19 +3219,13 @@ module Derivation = struct
 
   let transitive ~upper ~lower ~on_ ~in_ = Transitive { in_; on_; upper; lower }
 
-  let upper_bound ~bound ~in_ = Upper { bound; in_ }
-
   let lower_bound ~bound ~in_ = Lower { bound; in_ }
 
   let to_json t =
     let rec aux = function
       | Derivation steps ->
         Hh_json.(
           JSON_Object [("Derivation", array_ Subtype_step.to_json steps)])
-      | Upper { bound; in_ } ->
-        Hh_json.(
-          JSON_Object
-            [("Upper", JSON_Object [("bound", aux bound); ("in_", aux in_)])])
       | Lower { bound; in_ } ->
         Hh_json.(
           JSON_Object
@@ -3325,7 +3286,6 @@ module Derivation = struct
     | Axiom { prev; _ } -> extract_last prev
     | Flow { into; _ } -> extract_last into
     | Lower_bound { of_; _ } -> extract_last of_
-    | Upper_bound { of_; _ } -> extract_last of_
     | Solved _
     | No_reason
     | From_witness_decl _
@@ -3358,7 +3318,6 @@ module Derivation = struct
     | Axiom { next; _ } -> extract_first next
     | Flow { from; _ } -> extract_first from
     | Lower_bound { bound; _ } -> extract_first bound
-    | Upper_bound { bound; _ } -> extract_first bound
     | Solved _
     | No_reason
     | From_witness_decl _
@@ -3405,8 +3364,12 @@ module Derivation = struct
         let solutions = Tvid.Map.add of_ (extract_first solution) solutions in
         aux (sub, in_) ~deriv ~solutions
       (* -- Transitive constraints -- *)
-      | ( Lower_bound { bound = lb_sub; of_ = lb_super },
-          Upper_bound { bound = ub_super; of_ = ub_sub } ) ->
+      | ( Lower_bound
+            {
+              bound = Lower_bound { bound = lb_sub; of_ = lb_super };
+              of_ = ub_sub;
+            },
+          ub_super ) ->
         let lower = aux (lb_sub, lb_super) ~deriv:[] ~solutions
         and upper = aux (ub_sub, ub_super) ~deriv:[] ~solutions
         and in_ = aux (lb_sub, ub_super) ~deriv ~solutions
@@ -3420,14 +3383,6 @@ module Derivation = struct
         let bound = aux (bound, of_) ~deriv:[] ~solutions
         and in_ = aux (sub, bound) ~deriv ~solutions in
         lower_bound ~bound ~in_
-      | (sub, Upper_bound { bound; of_ }) ->
-        let bound = aux (of_, bound) ~deriv:[] ~solutions
-        and in_ = aux (sub, bound) ~deriv ~solutions in
-        upper_bound ~bound ~in_
-      | (Upper_bound { bound; of_ }, super) ->
-        let bound = aux (of_, bound) ~deriv:[] ~solutions
-        and in_ = aux (bound, super) ~deriv ~solutions in
-        upper_bound ~bound ~in_
       (* -- One-sided projection on subtype -- *)
       | (Prj_one { part; whole; prj }, _) ->
         let step =
@@ -3785,36 +3740,6 @@ module Derivation = struct
           @ with_prefix expl_lower ~prefix:prefix_lower ~sep:"\n\n"
         in
         (expl, st)
-      | Upper { bound; in_ } ->
-        let (expl_main, st) =
-          explain in_ ~st ~cfg ~ctxt:(Context.enter_main ctxt)
-        in
-        let ctxt = Context.deepen ctxt in
-        let (expl_upper, st) =
-          explain bound ~st ~cfg ~ctxt:(Context.enter_upper ctxt)
-        in
-
-        let main_path =
-          Context.(Option.value_exn @@ explain_path @@ enter_main ctxt)
-        in
-        let prefix_main =
-          Format.sprintf
-            "I checked the subtype constraint in [%s] because it was implied by transitivity."
-            main_path
-        and prefix_upper =
-          let upper_path =
-            Context.(Option.value_exn @@ explain_path @@ enter_upper ctxt)
-          in
-          Format.sprintf
-            "I found the supertype for [%s] is when I checked the subtype constraint in [%s]."
-            main_path
-            upper_path
-        in
-        let expl =
-          with_prefix expl_main ~prefix:prefix_main ~sep:"\n\n"
-          @ with_prefix expl_upper ~prefix:prefix_upper ~sep:"\n\n"
-        in
-        (expl, st)
 
     and explain_steps steps ~st ~cfg ~ctxt =
       let steps =
@@ -3971,9 +3896,7 @@ module Derivation = struct
           since we can have `Prj_one` in both subtype and supertype or
          `Prj_both` as subtype and `Prj_one` in supertype and we will always
          follow `Prj_one` before moving into `Prj_both` *)
-      | Lower_bound { of_; _ }
-      | Upper_bound { of_; _ } ->
-        explain_reason of_ ~st ~cfg ~ctxt
+      | Lower_bound { of_; _ } -> explain_reason of_ ~st ~cfg ~ctxt
       | Prj_both { sub_prj; _ } -> explain_reason sub_prj ~st ~cfg ~ctxt
       | Prj_one { part; _ } -> explain_reason part ~st ~cfg ~ctxt
       | Axiom { next; _ } -> explain_reason next ~st ~cfg ~ctxt

hphp/hack/src/typing/typing_reason.mli

@@ -381,9 +381,6 @@ val axiom_lower_bound :
 val trans_lower_bound :
   bound:locl_phase t_ -> of_:locl_phase t_ -> locl_phase t_
 
-val trans_upper_bound :
-  bound:locl_phase t_ -> of_:locl_phase t_ -> locl_phase t_
-
 val definition : Pos_or_decl.t -> locl_phase t_ -> locl_phase t_
 
 (** Record the decomposition of a covariant type parameter when simplifying a

hphp/hack/src/typing/typing_subtype.ml

@@ -7832,10 +7832,6 @@ end = struct
       (r_sub, var_sub)
       cty_super
       (on_error : Typing_error.Reasons_callback.t option) =
-    let cty_super =
-      Typing_env.update_cty_reason env cty_super ~f:(fun bound ->
-          Typing_reason.trans_upper_bound ~bound ~of_:r_sub)
-    in
     let ty_super = ConstraintType cty_super in
     let upper_bounds_before = Env.get_tyvar_upper_bounds env var_sub in
     let env =
@@ -7885,6 +7881,10 @@ end = struct
           in
           List.fold_left
             ~f:(fun (env, prop1) lower_bound ->
+              let lower_bound =
+                Typing_env.update_reason env lower_bound ~f:(fun bound ->
+                    Typing_reason.trans_lower_bound ~bound ~of_:r_sub)
+              in
               (* Since we can have either the rhs of a subtype constraint or
                    the rhs of any other constraint in the upper bounds we
                    have to inspect the upper bound and dispatch to the
@@ -7917,10 +7917,6 @@ end = struct
       ty_super
       (on_error : Typing_error.Reasons_callback.t option) =
     let ty_super = Sd.transform_dynamic_upper_bound ~coerce env ty_super in
-    let ty_super =
-      Typing_env.update_reason env ty_super ~f:(fun bound ->
-          Typing_reason.trans_upper_bound ~bound ~of_:r_sub)
-    in
     let upper_bounds_before = Env.get_tyvar_upper_bounds env var in
     let env =
       Env.add_tyvar_upper_bound_and_update_variances
@@ -7970,12 +7966,16 @@ end = struct
           in
           List.fold_left
             ~f:(fun (env, prop1) lower_bound ->
+              let ty_sub =
+                Typing_env.update_reason env lower_bound ~f:(fun bound ->
+                    Typing_reason.trans_lower_bound ~bound ~of_:r_sub)
+              in
               let (env, prop2) =
                 Subtype.(
                   simplify
                     ~subtype_env
                     ~this_ty:None
-                    ~lhs:{ sub_supportdyn = None; ty_sub = lower_bound }
+                    ~lhs:{ sub_supportdyn = None; ty_sub }
                     ~rhs:
                       {
                         super_like = false;
@@ -8225,6 +8225,7 @@ end = struct
   and tell_cstr env (coerce, ty_sub, ty_super) on_error =
     let (env, ty_sub) = Env.expand_internal_type env ty_sub in
     let (env, ty_super) = Env.expand_internal_type env ty_super in
+
     match (ty_sub, ty_super) with
     | (LoclType lty_sub, LoclType lty_super) -> begin
       match (get_node lty_sub, get_node lty_super) with