Force supportdyn on element type when widening for array get

Summary:
For array access (e.g. `$x['a']`) through a value whose type is a type variable (e.g. `$x : #0`), we use lower bounds on the type variable (e.g. `Map<string,int> <: #0`) to "narrow" the possible solutions in order to type-check the access. Here, for example, we would use the lower bound to generate a type `KeyedContainer<#1,#2>` that, roughly speaking, is the widest type that supports the operation that is compatible with the lower bound constraint.

We generate a subtype assertion between the lower bound and the "widened" type i.e. `Map<string,int> <: KeyedContainer<#1, #2>`. Note the type variables. Here, `#2` has no constraints, and so solves to `mixed`. In the case that the original type variable has an *upper bound* that supports dynamic (e.g. `supportdyn<mixed>`), this produces code that fails our "pessimisation" conjecture (see new test). Instead, we can employ a heuristic: if the lower bound does support dynamic, then assert that the widened type also supports dynamic. We also generalize the treatment of open shapes, generating a type variable for the "unknown fields" (which typically will solve to `supportdyn<mixed>`) rather than fixing it to be `mixed`.

Differential Revision: D46872355

fbshipit-source-id: 5ad70f81aa92ab4278c6e68f6ea5b87c2f2b60fa

hphp/hack/src/typing/typing_array_access.ml

@@ -151,13 +151,14 @@ let widen_for_array_get ~lhs_of_null_coalesce ~expr_pos index_expr env ty =
         ((env, None), None)
       | _ ->
         let (env, element_ty) = Env.fresh_type_invariant env expr_pos in
+        let (env, rest_ty) = Env.fresh_type_invariant env expr_pos in
         let upper_fdm =
           TShapeMap.add
             field
             { sft_optional = lhs_of_null_coalesce; sft_ty = element_ty }
             TShapeMap.empty
         in
-        let upper_shape_ty = MakeType.open_shape r upper_fdm in
+        let upper_shape_ty = MakeType.shape r rest_ty upper_fdm in
         ((env, None), Some upper_shape_ty))
   end
   | _ -> ((env, None), None)

hphp/hack/src/typing/typing_solver.ml

@@ -880,7 +880,19 @@ let expand_type_and_narrow
             @@ Some (Typing_error.Reasons_callback.unify_error_at p)
           in
           (match res with
-          | (env, None) -> ((env, None), widened_ty)
+          | (env, None) ->
+            let supportdyn = Typing_utils.is_supportdyn env ty in
+            let res2 =
+              if supportdyn then begin
+                TUtils.sub_type
+                  env
+                  widened_ty
+                  (MakeType.supportdyn_mixed (Reason.Rwitness p))
+                @@ Some (Typing_error.Reasons_callback.unify_error_at p)
+              end else
+                (env, None)
+            in
+            (res2, widened_ty)
           | _ ->
             if force_solve then
               expand_type_and_solve env ~description_of_expected p ty