Handle tyvar rank

Summary:
We allow monomorphic function types to be subtypes of polymorphic function types e.g.

```
function(mixed): void <: function<T>(T): void
```

However, since we do not disallow type variables in monomorphic function types this rule allows higher-rank type parameters to be present in the bounds of type variables in an outer scope.

This diff introduces ranks for type parameters and type variables to avoid this escape.

When we reach a subtype proposition involving a higher-rank type (currently this is only polymorphic function types) we increment the rank. This means that when we introduce fresh type parameters (for supertypes) or fresh type variables (for subtypes) and substitute them into a polymorphic function type, those type parameters & type variables will have higher rank than those occuring in the outer scope.

When we reach a subtype proposition involving a type variable (i.e. C-Var-L `facebook#1 <: T` or C-Var-R `T <: facebook#1`) we check to ensure that there is no type parameter contained in `T` with a greater rank than the rank of `facebook#1`.

This check involves traversing a type, potentially deeply, so we would like to avoid it whenever possible. To do so we add two optimizations:

1) We record when we are in a subtype proposition involving higher rank generics; if we are not then a type _cannot_ contain a higher rank generic and we can avoid the check

2) If we have to perform the check, we avoid fully traversing the type whenever possible by finding the first type parameter with a higher rank. The downside of this will be that when there are multiple higher-rank generics, on the first will be reported and the developer will only see the subsequent errors after the first is fixed.

Reviewed By: andrewjkennedy

Differential Revision: D72312308

fbshipit-source-id: 02ffef9eeb3c1c176a3ce9b8d47ab74da3abafc7

Author: Michael Thomas

hphp/hack/src/oxidized/gen/typing_inference_env.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<<42c0d811e27b0e64fa2c78c8d3ebe66a>>
+// @generated SignedSource<<c1f6f3358eeb2c5c6299c8a5e28c5e7f>>
 //
 // To regenerate this file, run:
 //   hphp/hack/src/oxidized_regen.sh
@@ -96,6 +96,7 @@ pub struct TyvarInfo {
     pub eager_solve_failed: bool,
     pub solving_info: SolvingInfo,
     pub is_error: bool,
+    pub rank: isize,
 }
 
 pub type Tvenv = tvid::map::Map<TyvarInfo>;

hphp/hack/src/oxidized/gen/typing_kinding_defs.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<<6d74a42dbae601505afb7771e7ba9d09>>
+// @generated SignedSource<<8be733e9b0946dd30f0ee749ba761a48>>
 //
 // To regenerate this file, run:
 //   hphp/hack/src/oxidized_regen.sh
@@ -45,6 +45,7 @@ pub struct Kind {
     pub newable: bool,
     pub require_dynamic: bool,
     pub parameters: Vec<NamedKind>,
+    pub rank: isize,
 }
 
 #[derive(

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<<fd303fd24eb18fc63536e0b7e2ce03db>>
+// @generated SignedSource<<84d5e5620eb9e3567cf1f5a85b9433df>>
 //
 // To regenerate this file, run:
 //   hphp/hack/src/oxidized_regen.sh
@@ -355,6 +355,8 @@ pub enum PrjAsymm {
     PrjAsymmArraykey,
     #[rust_to_ocaml(name = "Prj_asymm_num")]
     PrjAsymmNum,
+    #[rust_to_ocaml(name = "Prj_asymm_contains")]
+    PrjAsymmContains,
 }
 impl TrivialDrop for PrjAsymm {}
 arena_deserializer::impl_deserialize_in_arena!(PrjAsymm);
@@ -595,7 +597,7 @@ pub enum WitnessDecl {
     #[rust_to_ocaml(name = "Support_dynamic_type_assume")]
     SupportDynamicTypeAssume(pos_or_decl::PosOrDecl),
     #[rust_to_ocaml(name = "Polymorphic_type_param")]
-    PolymorphicTypeParam(pos_or_decl::PosOrDecl, String),
+    PolymorphicTypeParam(pos_or_decl::PosOrDecl, String, String, isize),
 }
 
 /// Axioms are information about types provided by the user in class or type

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

@@ -103,7 +103,7 @@ impl WitnessDecl {
             | Self::IllegalRecursiveType(pos_or_decl, _)
             | Self::SupportDynamicTypeAssume(pos_or_decl)
             | Self::TupleFromSplat(pos_or_decl)
-            | Self::PolymorphicTypeParam(pos_or_decl, _) => pos_or_decl,
+            | Self::PolymorphicTypeParam(pos_or_decl, _, _, _) => pos_or_decl,
         }
     }
 }

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<<d94a313f4caef34268f65daaae9dd4db>>
+// @generated SignedSource<<59328d6da7e3aef2ffffc051b04f3155>>
 //
 // To regenerate this file, run:
 //   hphp/hack/src/oxidized_regen.sh
@@ -1672,6 +1672,7 @@ impl<'a> Node<'a> for PrjAsymm {
             PrjAsymm::PrjAsymmNullable => {}
             PrjAsymm::PrjAsymmArraykey => {}
             PrjAsymm::PrjAsymmNum => {}
+            PrjAsymm::PrjAsymmContains => {}
         }
     }
 }

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<<7ba37c48d05da313aa88c07f68aa8101>>
+// @generated SignedSource<<a10e56f0cfaa28819bd70d9cfa97e5d5>>
 //
 // To regenerate this file, run:
 //   hphp/hack/src/oxidized_regen.sh
@@ -548,7 +548,7 @@ pub enum WitnessDecl<'a> {
     #[serde(deserialize_with = "arena_deserializer::arena", borrow)]
     #[rust_to_ocaml(name = "Polymorphic_type_param")]
     #[rust_to_ocaml(inline_tuple)]
-    PolymorphicTypeParam(&'a (&'a pos_or_decl::PosOrDecl<'a>, &'a str)),
+    PolymorphicTypeParam(&'a (&'a pos_or_decl::PosOrDecl<'a>, &'a str, &'a str, isize)),
 }
 impl<'a> TrivialDrop for WitnessDecl<'a> {}
 arena_deserializer::impl_deserialize_in_arena!(WitnessDecl<'arena>);

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

@@ -105,7 +105,7 @@ impl<'a> WitnessDecl<'a> {
             | WitnessDecl::IllegalRecursiveType((p, _))
             | WitnessDecl::SupportDynamicTypeAssume(p)
             | WitnessDecl::PessimisedThis(p)
-            | WitnessDecl::PolymorphicTypeParam((p, _)) => p,
+            | WitnessDecl::PolymorphicTypeParam((p, _, _, _)) => p,
         }
     }
 }

hphp/hack/src/typing/env/typing_env.ml

@@ -93,6 +93,8 @@ let expand_var env r v =
   let (inference_env, ty_solution) = Inf.expand_var env.inference_env r v in
   ({ env with inference_env }, ty_solution)
 
+let rank_of_tvar { inference_env; _ } tvid = Inf.get_rank inference_env tvid
+
 let fresh_type_reason ?variance env p r =
   log_env_change_ "fresh_type_reason" env
   @@
@@ -109,6 +111,18 @@ let fresh_type env p =
   in
   ({ env with inference_env }, res)
 
+let fresh_type_invariant_with_rank env rank p =
+  log_env_change_ "fresh_type_invariant_with_rank" env
+  @@
+  let (inference_env, res) =
+    Inf.fresh_type_invariant_with_rank
+      env.inference_env
+      env.tvar_id_provider
+      rank
+      p
+  in
+  ({ env with inference_env }, res)
+
 let fresh_type_invariant env p =
   log_env_change_ "fresh_type_invariant" env
   @@
@@ -500,6 +514,7 @@ let add_fresh_generic_parameter env pos prefix ~reified ~enforceable ~newable =
         newable;
         require_dynamic = true;
         parameters = [];
+        rank = 0;
       }
   in
   add_fresh_generic_parameter_by_kind env pos prefix kind
@@ -525,6 +540,7 @@ let get_tpenv_tparams env =
               require_dynamic = _;
               (* FIXME what to do here? it seems dangerous to just traverse *)
               parameters = _;
+              rank = _;
             }
           acc ->
         let folder ty acc =
@@ -2110,3 +2126,5 @@ let with_outside_expr_tree env ~macro_variables f =
   (env, r1, r2, new_macro_type_mapping)
 
 let is_in_expr_tree env = Option.is_some env.in_expr_tree
+
+let rank_of_tparam env tparam = Type_parameter_env.get_rank env.tpenv tparam

hphp/hack/src/typing/env/typing_env.mli

@@ -74,6 +74,10 @@ val fresh_type_reason :
     it won't be solved automatically at the end of the scope *)
 val fresh_type_invariant : env -> Pos.t -> env * locl_ty
 
+(** Generate a fresh type variable type with a specified ranks for use
+    in subtyping of rank-n polymorphic types *)
+val fresh_type_invariant_with_rank : env -> int -> Pos.t -> env * locl_ty
+
 (** Generate a fresh type variable to stand for an unknown type in the
     case of type errors. *)
 val fresh_type_error : env -> Pos.t -> env * locl_ty
@@ -642,3 +646,7 @@ val update_ity_reason :
   internal_type ->
   f:(locl_phase Typing_reason.t_ -> locl_phase Typing_reason.t_) ->
   internal_type
+
+val rank_of_tvar : env -> Tvid.t -> int
+
+val rank_of_tparam : env -> string -> int

hphp/hack/src/typing/type_parameter_env.ml

@@ -41,6 +41,9 @@ type t = {
 }
 [@@deriving hash, show { with_path = false }]
 
+let bindings { tparams; _ } =
+  List.map ~f:(fun (k, (_, v)) -> (k, v)) (SMap.bindings tparams)
+
 let empty = { tparams = SMap.empty; consistent = true }
 
 let mem name tpenv = SMap.mem name tpenv.tparams
@@ -136,6 +139,11 @@ let get_pos tpenv name =
   | None -> Pos_or_decl.none
   | Some (pos, _) -> pos
 
+let get_rank tpenv name =
+  match get name tpenv with
+  | None -> 0
+  | Some { rank; _ } -> rank
+
 let get_tparam_names tpenv = SMap.keys tpenv.tparams
 
 let is_consistent tpenv = tpenv.consistent
@@ -167,6 +175,7 @@ let add_upper_bound_ tpenv name ty =
             newable = false;
             require_dynamic = false;
             parameters = [];
+            rank = 0;
           } )
       | Some (pos, tp) ->
         (pos, { tp with upper_bounds = TySet.add ty tp.upper_bounds })
@@ -191,6 +200,7 @@ let add_lower_bound_ tpenv name ty =
             newable = false;
             require_dynamic = false;
             parameters = [];
+            rank = 0;
           } )
       | Some (pos, tp) ->
         (pos, { tp with lower_bounds = TySet.add ty tp.lower_bounds })
@@ -236,6 +246,7 @@ let add_upper_bound ?intersect env_tpenv name ty =
     let newable = get_newable env_tpenv name in
     let require_dynamic = get_require_dynamic env_tpenv name in
     let parameters = [] in
+    let rank = get_rank env_tpenv name in
     add
       ~def_pos
       name
@@ -247,6 +258,7 @@ let add_upper_bound ?intersect env_tpenv name ty =
         newable;
         require_dynamic;
         parameters;
+        rank;
       }
       tpenv
 
@@ -280,6 +292,7 @@ let add_lower_bound ?union env_tpenv name ty =
     let newable = get_newable env_tpenv name in
     let require_dynamic = get_require_dynamic env_tpenv name in
     let parameters = [] in
+    let rank = get_rank env_tpenv name in
     add
       ~def_pos
       name
@@ -291,6 +304,7 @@ let add_lower_bound ?union env_tpenv name ty =
         newable;
         require_dynamic;
         parameters;
+        rank;
       }
       tpenv
 
@@ -358,6 +372,7 @@ let add_generic_parameters tpenv tparaml =
       newable;
       require_dynamic;
       parameters = nested_params;
+      rank = 0;
     }
   in