From deb75cde183fb14831ac4f10548a1a645bbc7342 Mon Sep 17 00:00:00 2001 From: Scott Owens Date: Fri, 18 Dec 2020 08:36:09 -0800 Subject: [PATCH] Update as and foreach typing for sound dynamic Summary: Update the `as` construct to allow `e as dynamic`. This is a type error if the type `t` of `e` is not coerceable to dynamic; otherwise, it just intersects `t` with `dynamic` following the usual refinement strategy. The update to `foreach` was just a refactoring. Reviewed By: francesco-zappa-nardelli Differential Revision: D24995112 fbshipit-source-id: a81aeb8d8d4adf2fb8c676f0be0fccf9923b4fc1 --- hphp/hack/src/typing/typing.ml | 105 ++++++++++++--------- hphp/hack/test/sound_dynamic/typing/as.good.php | 18 ++++ .../hack/test/sound_dynamic/typing/as.good.php.exp | 1 + hphp/hack/test/sound_dynamic/typing/as2.bad.php | 18 ++++ .../hack/test/sound_dynamic/typing/as2.bad.php.exp | 4 + .../test/sound_dynamic/typing/foreach.good.php | 18 ++++ .../test/sound_dynamic/typing/foreach.good.php.exp | 1 + 7 files changed, 120 insertions(+), 45 deletions(-) create mode 100644 hphp/hack/test/sound_dynamic/typing/as.good.php create mode 100644 hphp/hack/test/sound_dynamic/typing/as.good.php.exp create mode 100644 hphp/hack/test/sound_dynamic/typing/as2.bad.php create mode 100644 hphp/hack/test/sound_dynamic/typing/as2.bad.php.exp create mode 100644 hphp/hack/test/sound_dynamic/typing/foreach.good.php create mode 100644 hphp/hack/test/sound_dynamic/typing/foreach.good.php.exp diff --git a/hphp/hack/src/typing/typing.ml b/hphp/hack/src/typing/typing.ml index 2dc74235042..daf06d9493f 100644 --- a/hphp/hack/src/typing/typing.ml +++ b/hphp/hack/src/typing/typing.ml @@ -1108,39 +1108,42 @@ and catch catchctx env (sid, exn_lvar, b) = and as_expr env ty1 pe e = let env = Env.open_tyvars env pe in - (fun (env, expected_ty, tk, tv) -> - let rec distribute_union env ty = - let (env, ty) = Env.expand_type env ty in - match get_node ty with - | Tunion tyl -> List.fold tyl ~init:env ~f:distribute_union - | _ -> - if SubType.is_sub_type_for_union env ty (MakeType.dynamic Reason.Rnone) - then - let env = SubType.sub_type env ty tk Errors.unify_error in - let env = SubType.sub_type env ty tv Errors.unify_error in - env - else - let ur = Reason.URforeach in - Type.sub_type pe ur env ty expected_ty Errors.unify_error - in - let env = distribute_union env ty1 in - let env = Env.set_tyvar_variance env expected_ty in - (Typing_solver.close_tyvars_and_solve env Errors.unify_error, tk, tv)) - @@ let (env, tv) = Env.fresh_type env pe in - match e with - | As_v _ -> - let tk = MakeType.mixed Reason.Rnone in - (env, MakeType.traversable (Reason.Rforeach pe) tv, tk, tv) - | As_kv _ -> - let (env, tk) = Env.fresh_type env pe in - (env, MakeType.keyed_traversable (Reason.Rforeach pe) tk tv, tk, tv) - | Await_as_v _ -> - let tk = MakeType.mixed Reason.Rnone in - (env, MakeType.async_iterator (Reason.Rasyncforeach pe) tv, tk, tv) - | Await_as_kv _ -> - let (env, tk) = Env.fresh_type env pe in - (env, MakeType.async_keyed_iterator (Reason.Rasyncforeach pe) tk tv, tk, tv) + let (env, expected_ty, tk, tv) = + match e with + | As_v _ -> + let tk = MakeType.mixed Reason.Rnone in + (env, MakeType.traversable (Reason.Rforeach pe) tv, tk, tv) + | As_kv _ -> + let (env, tk) = Env.fresh_type env pe in + (env, MakeType.keyed_traversable (Reason.Rforeach pe) tk tv, tk, tv) + | Await_as_v _ -> + let tk = MakeType.mixed Reason.Rnone in + (env, MakeType.async_iterator (Reason.Rasyncforeach pe) tv, tk, tv) + | Await_as_kv _ -> + let (env, tk) = Env.fresh_type env pe in + ( env, + MakeType.async_keyed_iterator (Reason.Rasyncforeach pe) tk tv, + tk, + tv ) + in + let rec distribute_union env ty = + let (env, ty) = Env.expand_type env ty in + match get_node ty with + | Tunion tyl -> List.fold tyl ~init:env ~f:distribute_union + | _ -> + if SubType.is_sub_type_for_union env ty (MakeType.dynamic Reason.Rnone) + then + let env = SubType.sub_type env ty tk Errors.unify_error in + let env = SubType.sub_type env ty tv Errors.unify_error in + env + else + let ur = Reason.URforeach in + Type.sub_type pe ur env ty expected_ty Errors.unify_error + in + let env = distribute_union env ty1 in + let env = Env.set_tyvar_variance env expected_ty in + (Typing_solver.close_tyvars_and_solve env Errors.unify_error, tk, tv) and bind_as_expr env p ty1 ty2 aexpr = let check_reassigned_mutable env te = @@ -2546,20 +2549,32 @@ and expr_ { (Phase.env_with_self env) with from_class = Some CIstatic } in let (env, hint_ty) = Phase.localize_hint ~ety_env env hint in + let enable_sound_dynamic = + TypecheckerOptions.enable_sound_dynamic env.genv.tcopt + in + let is_dyn = Typing_utils.is_dynamic env hint_ty in + ( if enable_sound_dynamic && is_dyn then + let (_ : env * locl_ty) = + ( SubType.sub_type + ~allow_subtype_of_dynamic:true + env + expr_ty + hint_ty + Errors.unify_error, + hint_ty ) + in + () ); let (env, hint_ty) = - if Typing_utils.is_dynamic env hint_ty then - if TypecheckerOptions.enable_sound_dynamic env.genv.tcopt then - (SubType.sub_type env expr_ty hint_ty Errors.unify_error, hint_ty) - else - let env = - if is_instance_var e then - let (env, ivar) = get_instance_var env e in - set_local env ivar hint_ty - else - env - in - (env, hint_ty) - else if is_nullable then + if is_dyn && not enable_sound_dynamic then + let env = + if is_instance_var e then + let (env, ivar) = get_instance_var env e in + set_local env ivar hint_ty + else + env + in + (env, hint_ty) + else if is_nullable && not is_dyn then let (env, hint_ty) = refine_type env (fst e) expr_ty hint_ty in (env, MakeType.nullable_locl (Reason.Rwitness p) hint_ty) else if is_instance_var e then diff --git a/hphp/hack/test/sound_dynamic/typing/as.good.php b/hphp/hack/test/sound_dynamic/typing/as.good.php new file mode 100644 index 00000000000..1a85cae2668 --- /dev/null +++ b/hphp/hack/test/sound_dynamic/typing/as.good.php @@ -0,0 +1,18 @@ + implements dynamic { +} + +function f(B $i, B $j) : void { +} + +class C { + public function f(B $i) : void { + $x = $i as dynamic; + $x->m(); + $i->m(); + /* Since B isn't enforceable, these work because of the B + * part of the union and not the dynamic part */ + f($i, $x); + } +} diff --git a/hphp/hack/test/sound_dynamic/typing/as.good.php.exp b/hphp/hack/test/sound_dynamic/typing/as.good.php.exp new file mode 100644 index 00000000000..4269126fceb --- /dev/null +++ b/hphp/hack/test/sound_dynamic/typing/as.good.php.exp @@ -0,0 +1 @@ +No errors diff --git a/hphp/hack/test/sound_dynamic/typing/as2.bad.php b/hphp/hack/test/sound_dynamic/typing/as2.bad.php new file mode 100644 index 00000000000..8bd76c3d96f --- /dev/null +++ b/hphp/hack/test/sound_dynamic/typing/as2.bad.php @@ -0,0 +1,18 @@ + { + public T $p; + public function __construct(T $x) { + $this->p = $x; + } + public function get() : T { + return $this->p; + } + public function set(T $x) : void { + $this->p = $x; + } +} + +function f(Box $x) : void { + $y = $x as dynamic; +} diff --git a/hphp/hack/test/sound_dynamic/typing/as2.bad.php.exp b/hphp/hack/test/sound_dynamic/typing/as2.bad.php.exp new file mode 100644 index 00000000000..34eae424ac1 --- /dev/null +++ b/hphp/hack/test/sound_dynamic/typing/as2.bad.php.exp @@ -0,0 +1,4 @@ +File "as2.bad.php", line 17, characters 14-20: +Expected `dynamic` (Typing[4110]) + File "as2.bad.php", line 16, characters 12-19: + But got `Box` diff --git a/hphp/hack/test/sound_dynamic/typing/foreach.good.php b/hphp/hack/test/sound_dynamic/typing/foreach.good.php new file mode 100644 index 00000000000..0a155a64e5e --- /dev/null +++ b/hphp/hack/test/sound_dynamic/typing/foreach.good.php @@ -0,0 +1,18 @@ + $v) { + if ($d) { + return $v->m(); + } + else { + return $k->m(); + } + } + foreach ($d as $v) { + return $v->m(); + } + return $d; + } +} diff --git a/hphp/hack/test/sound_dynamic/typing/foreach.good.php.exp b/hphp/hack/test/sound_dynamic/typing/foreach.good.php.exp new file mode 100644 index 00000000000..4269126fceb --- /dev/null +++ b/hphp/hack/test/sound_dynamic/typing/foreach.good.php.exp @@ -0,0 +1 @@ +No errors -- 2.11.4.GIT