Suggestion: Improve typechecker error for refinement on container keys

[ssandler]

HHVM Version

HipHop VM 4.13.2 (rel)
Compiler: 1573166016_N
Repo schema: 12f66242996fabd00f4fab1e33c4fbc011981c09

Standalone code, or other way to reproduce the problem

function example(dict<string, mixed> $foo): void {
  if ($foo['bar'] is Traversable<_>) {
    foreach ($foo['bar'] as $it) {
      // do something
    }
  }
}

Actual result

Typing[4110] Invalid foreach
   --> test.hack
  1 | function example(dict<string, mixed> $foo): void {
    |                               ^^^^^ But got mixed
  3 | 		foreach ($foo['bar'] as $it) {
    |            ^^^^^^^^^^^
    |            ^^^^^^^^^^^ Expected Traversable<[unresolved]> because this is used in a foreach statement

1 error found.

Expected result

This is something that consistently trips up new Hack developers as they learn about type refinement and is/as. The most ideal state would be that the typechecker could remember the refinement on a sub-key of a container. But I expect that's a significant change. A perhaps much smaller change would be to provide a clearer error message about how to fix this problem, such as recommending the user pull $foo['bar'] into a local variable before refining its type with the type test.

[Wilfred]

This is hard. I believe we could support refinements like this for shapes, although we currently don't:

function example2(shape('bar' => mixed) $foo): void {
  if ($foo['bar'] is Traversable<_>) {
    foreach ($foo['bar'] as $it) {
      // do something
    }
  }
}

This does work for classes:

class MyClass {
  public function __construct(public mixed $m) {}
}

function example3(MyClass $foo): void {
  if ($foo->m is Traversable<_>) {
    foreach ($foo->m as $it) {
      // do something
    }
  }
}

This technique is called "fake members" in the typechecker, because the definition of MyClass shows a different type. This is a somewhat controversial feature, because it's not always obvious when it can help. We have to conservatively assume that any function could modify $foo and then our refinement is no longer valid.

function totally_unrelated(): void {}

class MyClass {
  public function __construct(public mixed $m) {}
}

function example3(MyClass $foo): void {
  if ($foo->m is Traversable<_>) {
    totally_unrelated(); // Maybe this modified $foo somehow?
    foreach ($foo->m as $it) {
      // do something
    }
  }
}

For your example, we don't want to refine a dict<string, mixed> to a dict<string, mixed or traversable if key is 'foo'>. That's not a type that we want to represent. This is why the shape case could work: it would be refining shape('bar' => mixed) to shape('bar' => Traversable<mixed>), which is a type we can represent.

We could potentially look at making the error message better though. Something like "Consider assigning to a local and then using as".

[Wilfred]

Are you only interested in this error on bad usage of foreach, or more general cases of expecting refinement?

function takes_traversable(Traversable<mixed> $_): void {}

function example(dict<string, mixed> $foo): void {
  if ($foo['bar'] is Traversable<_>) {
    takes_traversable($foo['bar']);
  }
}

[ssandler]

I'm interested in the more general case of expecting refinement. I can see how refining dict keys would not make sense in the type system. An error message that guides people to using a local variable would be quite welcome!

[Wilfred]

I poked at this a little bit today (proof-of-concept internally D18872824, should be exported as a pull request in the next few minutes).

This does roughly what you want for foreach, and it could work for function arguments too.

$ hh_single_type_check ~/scratch/refine_arr.php

Typing[4110] Invalid foreach, consider assigning this value to a variable and using is/as
   --> /home/wilfred/scratch/refine_arr.php
  5 | function example(dict<string, mixed> $foo): void {
    |                               ^^^^^ But got mixed
  8 |     foreach ($foo['bar'] as $it) {
    |              ^^^^^^^^^^^
    |              ^^^^^^^^^^^ Expected Traversable<[unresolved]> because this is used in a foreach statement

1 error found.

I'm not sure if the error message is always a usability win though. It's currently firing for any array or object access, so the code like this would fire:

function example(vec<int> $foo): void {
  foreach ($foo[0] as $it) {
  }
}

In this case, saying "consider assigning to a variable" is actively misleading -- the user has presumably used entirely the wrong variable or type. There's nothing they can do with $foo[0].

Do you have any ideas for good heuristics for when this should fire? I don't want logic that looks for a $foo['bar'] is ... anywhere in the current program, and it would be really awkward to work out whether an earlier if was relevant. It'd need checks for any modifications to $foo.

[Wilfred]

Urgh, PR export failed. Here's the change:

diff --git a/hphp/hack/src/typing/typing.ml b/hphp/hack/src/typing/typing.ml
--- a/hphp/hack/src/typing/typing.ml
+++ b/hphp/hack/src/typing/typing.ml
@@ -444,6 +444,12 @@
   Typing_reactivity.disallow_atmost_rx_as_rxfunc_on_non_functions env param ty;
   (env, ty)
 
+let expr_could_be_refined (e : ('a, 'b, 'c, 'd) Aast.expr) =
+  match snd e with
+  | Aast.Array_get (_, _) -> true
+  | Aast.Class_get (_, _) -> true
+  | _ -> false
+
 (* Return a map describing all the fields in this record, including
    inherited fields, and whether they have a default value. *)
 let all_record_fields (rd : Decl_provider.record_def_decl) :
@@ -1246,7 +1252,7 @@
     let (env, (te1, te2, tb)) =
       LEnv.stash_and_do env [C.Continue; C.Break] (fun env ->
           let env = LEnv.save_and_merge_next_in_cont env C.Continue in
-          let (env, tk, tv) = as_expr env ty1 (fst e1) e2 in
+          let (env, tk, tv) = as_expr env ty1 e1 e2 in
           let alias_depth =
             if env.in_loop then
               1
@@ -1497,7 +1503,7 @@
   let (env, tb) = block env b in
   (env, (env.lenv, (sid, exn, tb)))
 
-and as_expr env ty1 pe e =
+and as_expr env ty1 ((pe, _) as e_iter) e =
   let env = Env.open_tyvars env pe in
   (fun (env, expected_ty, tk, tv) ->
     let rec distribute_union env ty =
@@ -1511,7 +1517,7 @@
           let env = SubType.sub_type env ty tv Errors.unify_error in
           env
         else
-          let ur = Reason.URforeach in
+          let ur = Reason.URforeach (expr_could_be_refined e_iter) in
           Type.sub_type pe ur env ty expected_ty Errors.unify_error
     in
     let env = distribute_union env ty1 in
diff --git a/hphp/hack/src/typing/typing_reason.ml b/hphp/hack/src/typing/typing_reason.ml
--- a/hphp/hack/src/typing/typing_reason.ml
+++ b/hphp/hack/src/typing/typing_reason.ml
@@ -717,7 +717,7 @@
   | URassign_inout
   | URhint
   | URreturn
-  | URforeach
+  | URforeach of bool
   | URthrow
   | URvector
   | URkey
@@ -764,7 +764,13 @@
   | URassign -> "Invalid assignment"
   | URassign_branch -> "Invalid assignment in this branch"
   | URassign_inout -> "Invalid assignment to an inout parameter"
-  | URforeach -> "Invalid foreach"
+  | URforeach b ->
+    "Invalid foreach"
+    ^
+    if b then
+      ", consider assigning this value to a variable and using is/as"
+    else
+      ""
   | URthrow -> "Invalid exception"
   | URvector -> "Some elements in this Vector are incompatible"
   | URkey -> "The keys of this Map are incompatible"
--