Fix ty_compare for Tdestructure

Summary: This diff moves the destructuring subtyping rules to be above the catch-all `Tvar _, _` rule and fixes the `ty_compare` function in the case of Tdestructure. Previously, it was saying that `list(#1, #2)` is equivalent to `list(#3, #4)`, so the lower bounds on the inner type variables were not being computed.

Reviewed By: kmeht

Differential Revision: D16846102

fbshipit-source-id: 051685e9991a63bc5dc09a3eba568a8027816ce7

hphp/hack/src/typing/typing_defs.ml

@@ -716,6 +716,8 @@ let abstract_kind_con_ordinal ak =
  * aliases.
  * But if ty_compare ty1 ty2 = 0, then the types must not be distinguishable
  * by any typing rules.
+ *
+ * TODO(T52611361): Make this comparison exhaustive on ty1 to remove the _ catchall
  *)
 let rec ty_compare ?(normalize_lists = false) ty1 ty2 =
   let rec ty_compare ty1 ty2 =
@@ -727,6 +729,7 @@ let rec ty_compare ?(normalize_lists = false) ty1 ty2 =
         ty_compare ty ty2
       | Tfun fty, Tfun fty2 ->
         tfun_compare fty fty2
+      | Tdestructure tyl1, Tdestructure tyl2
       | Tunion tyl1, Tunion tyl2
       | Tintersection tyl1, Tintersection tyl2 ->
         tyl_compare ~sort:normalize_lists ~normalize_lists tyl1 tyl2

hphp/hack/src/typing/typing_subtype.ml

@@ -998,6 +998,35 @@ and simplify_subtype
       invalid ()
     end
 
+  (* List destructuring *)
+  | Ttuple tyl, Tdestructure tyl_dest ->
+    if List.length tyl <> List.length tyl_dest then invalid () else
+    List.fold2_exn tyl tyl_dest ~init:(env, TL.valid) ~f:(fun res ty ty_dest ->
+      res &&& simplify_subtype ~seen_generic_params ~this_ty ty ty_dest)
+  | Tclass ((_, x), _, [elt_type]), Tdestructure tyl_dest
+    when x = SN.Collections.cVector
+      || x = SN.Collections.cImmVector
+      || x = SN.Collections.cVec
+      || x = SN.Collections.cConstVector ->
+    List.fold tyl_dest ~init:(env, TL.valid) ~f:(fun res ty_dest ->
+      res &&& simplify_subtype ~seen_generic_params ~this_ty elt_type ty_dest)
+  | Tclass ((_, x), _, tyl), Tdestructure tyl_dest when x = SN.Collections.cPair ->
+    if List.length tyl <> List.length tyl_dest then invalid () else
+    List.fold2_exn tyl tyl_dest ~init:(env, TL.valid) ~f:(fun res ty ty_dest ->
+      res &&& simplify_subtype ~seen_generic_params ~this_ty ty ty_dest)
+  | Tarraykind (AKvec elt_type), Tdestructure tyl_dest
+  | Tarraykind (AKvarray elt_type), Tdestructure tyl_dest ->
+    List.fold tyl_dest ~init:(env, TL.valid) ~f:(fun res ty_dest ->
+      res &&& simplify_subtype ~seen_generic_params ~this_ty elt_type ty_dest)
+  | Tdynamic, Tdestructure tyl_dest ->
+    List.fold tyl_dest ~init:(env, TL.valid) ~f:(fun res ty_dest ->
+      res &&& simplify_subtype ~seen_generic_params ~this_ty ty_sub ty_dest)
+  (* TODO: should remove these any cases *)
+  | Tarraykind (AKany | AKempty), Tdestructure tyl_dest
+  | Tany, Tdestructure tyl_dest ->
+    let any = (fst ty_super, Tany) in
+    List.fold tyl_dest ~init:(env, TL.valid) ~f:(fun res ty_dest ->
+      res &&& simplify_subtype ~seen_generic_params ~this_ty any ty_dest)
   (* ty_sub <: union{ty_super'} iff ty_sub <: ty_super' *)
   | _, Tunion [ty_super'] ->
     simplify_subtype ~seen_generic_params ~this_ty ty_sub ty_super' env
@@ -1135,35 +1164,6 @@ and simplify_subtype
     List.fold_left tyl ~init:(env, TL.invalid ~fail) ~f:(fun res ty_sub ->
       res ||| simplify_subtype ~seen_generic_params ~this_ty ty_sub ty_super)
 
-  | Ttuple tyl, Tdestructure tyl_dest ->
-    if List.length tyl <> List.length tyl_dest then invalid () else
-    List.fold2_exn tyl tyl_dest ~init:(env, TL.valid) ~f:(fun res ty ty_dest ->
-      res &&& simplify_subtype ~seen_generic_params ~this_ty ty ty_dest)
-  | Tclass ((_, x), _, [elt_type]), Tdestructure tyl_dest
-    when x = SN.Collections.cVector
-      || x = SN.Collections.cImmVector
-      || x = SN.Collections.cVec
-      || x = SN.Collections.cConstVector ->
-    List.fold tyl_dest ~init:(env, TL.valid) ~f:(fun res ty_dest ->
-      res &&& simplify_subtype ~seen_generic_params ~this_ty elt_type ty_dest)
-  | Tclass ((_, x), _, tyl), Tdestructure tyl_dest when x = SN.Collections.cPair ->
-    if List.length tyl <> List.length tyl_dest then invalid () else
-    List.fold2_exn tyl tyl_dest ~init:(env, TL.valid) ~f:(fun res ty ty_dest ->
-      res &&& simplify_subtype ~seen_generic_params ~this_ty ty ty_dest)
-  | Tarraykind (AKvec elt_type), Tdestructure tyl_dest
-  | Tarraykind (AKvarray elt_type), Tdestructure tyl_dest ->
-    List.fold tyl_dest ~init:(env, TL.valid) ~f:(fun res ty_dest ->
-      res &&& simplify_subtype ~seen_generic_params ~this_ty elt_type ty_dest)
-  | Tdynamic, Tdestructure tyl_dest ->
-    List.fold tyl_dest ~init:(env, TL.valid) ~f:(fun res ty_dest ->
-      res &&& simplify_subtype ~seen_generic_params ~this_ty ty_sub ty_dest)
-  (* TODO: should remove these any cases *)
-  | Tarraykind (AKany | AKempty), Tdestructure tyl_dest
-  | Tany, Tdestructure tyl_dest ->
-    let any = (fst ty_super, Tany) in
-    List.fold tyl_dest ~init:(env, TL.valid) ~f:(fun res ty_dest ->
-      res &&& simplify_subtype ~seen_generic_params ~this_ty any ty_dest)
-
   | Tany, Tany ->
     valid ()
 

hphp/hack/test/typecheck/list_destructuring_tvar.php

@@ -0,0 +1,42 @@
+<?hh
+
+class Box<T> {
+  public function put(T $x): void {}
+  public function get(): T { throw new Exception(); }
+}
+
+function pull<Tk, Tv1, Tv2>(
+  Tv1 $input,
+  (function(Tv1): Tv2) $value_func,
+  (function(Tv1): Tk) $key_func,
+): void {
+  throw new Exception();
+}
+
+interface A1 {}
+interface A2 {}
+interface B1 {}
+interface B2 {}
+
+function test((A1, A2) $t1, (B1, B2) $t2): void {
+  $x = new Box(); // Box<#1>
+  $x->put($t1);
+  $x->put($t2);
+  $input = $x->get(); // {(A1, A2), (B1, B2)} <: #1
+
+  pull(
+    $input,
+    $in ==> {
+      list(
+        $v1, // A1 <: #3 /\ B1 <: #3
+        $v2  // A2 <: #4 /\ B2 <: #4
+      ) = $in; // (A1, A2) <: list(#3, #4) /\ (B1, B2) <: list(#3, #4);
+    },
+    $in ==> {
+      list($v1, $v2) = $in; // same as above
+      hh_force_solve();
+      hh_show($v1);
+      hh_show($v2);
+    },
+  );
+}

hphp/hack/test/typecheck/list_destructuring_tvar.php.exp

@@ -0,0 +1,10 @@
+File "list_destructuring_tvar.php", line 38, characters 7-18:
+  (A1 | B1)
+File "list_destructuring_tvar.php", line 39, characters 7-18:
+  (A2 | B2)
+File "list_destructuring_tvar.php", line 35, characters 5-128:
+Invalid return type (Typing[4110])
+File "list_destructuring_tvar.php", line 27, characters 3-6:
+Expected nothing
+File "list_destructuring_tvar.php", line 35, characters 5-128:
+But got void because this function implicitly returns void

hphp/hack/test/typecheck/list_destructuring_tvar.php.like_types.exp

@@ -0,0 +1,14 @@
+File "list_destructuring_tvar.php", line 38, characters 7-18:
+  ~?(A1 | B1)
+File "list_destructuring_tvar.php", line 39, characters 7-18:
+  ~?(A2 | B2)
+File "list_destructuring_tvar.php", line 29, characters 5-177:
+Invalid return type (Typing[4110])
+File "list_destructuring_tvar.php", line 8, characters 24-26:
+Some type constraint(s) are violated here
+File "list_destructuring_tvar.php", line 8, characters 24-26:
+Tv2 is a constrained type parameter
+File "list_destructuring_tvar.php", line 29, characters 5-177:
+Expected void because this function implicitly returns void
+File "list_destructuring_tvar.php", line 8, characters 24-26:
+But got dynamic