From ab841600a2027c6fa434da30ba874ed0e7f64f37 Mon Sep 17 00:00:00 2001 From: Andrew Kennedy Date: Mon, 11 Feb 2019 02:24:25 -0800 Subject: [PATCH] New inference: flatten unions when solving for lower bounds Summary: Currently it is possible for a solution to a type variable to contain nested unions. e.g. if we have ``` int, (string | int) <: v ``` then we will solve with `v := int | (string | int)`. Also, we might end up with spurious "circular type" errors if `v` occurs somewhere in the flattened union, even though `v | t <: v` iff `t <: v`. So before creating the union, we normalize the set of types, flattening unions, locating `null` and nullable types, and removing `v` from the set. Reviewed By: manzyuk Differential Revision: D13986135 fbshipit-source-id: 847ff1083ba6501792d06e1aeb7686b066db5212 --- hphp/hack/src/typing/typing_subtype.ml | 36 ++++++++++++++++++---- .../new_inference/eager_solve/circular_bug_2.php | 34 ++++++++++++++++++++ .../eager_solve/circular_bug_2.php.exp | 3 ++ .../new_inference/transitive_simplify_2.php.exp | 2 +- 4 files changed, 68 insertions(+), 7 deletions(-) create mode 100644 hphp/hack/test/typecheck/new_inference/eager_solve/circular_bug_2.php create mode 100644 hphp/hack/test/typecheck/new_inference/eager_solve/circular_bug_2.php.exp diff --git a/hphp/hack/src/typing/typing_subtype.ml b/hphp/hack/src/typing/typing_subtype.ml index b36fa819413..2812eb4698b 100644 --- a/hphp/hack/src/typing/typing_subtype.ml +++ b/hphp/hack/src/typing/typing_subtype.ml @@ -2477,25 +2477,49 @@ let expand_types env tys = tys (env, Typing_set.empty) +(* Given a set of types, expand solved type variables, and eliminate + * top-level unions by folding types back into the set. Remove any use of + * `null` or `?t`, instead returning a boolean if + * a null type exists in the set. Finally, remove any type variable match `var` + *) +let expand_and_flatten_type_set env var tys = + + let rec expand_and_flatten_type_list env tys has_null res = + match tys with + | [] -> env, has_null, Typing_set.elements res + | ty::tys -> + let env, ety = Env.expand_type env ty in + match ety with + | _, Tunresolved tys' -> expand_and_flatten_type_list env (tys' @ tys) has_null res + | _, Toption ty -> expand_and_flatten_type_list env (ty::tys) true res + | _, Tprim Nast.Tnull -> expand_and_flatten_type_list env tys true res + | _, Tvar var' when var=var' -> expand_and_flatten_type_list env tys has_null res + | _ -> expand_and_flatten_type_list env tys has_null (Typing_set.add ety res) + in + expand_and_flatten_type_list env (TySet.elements tys) false TySet.empty + (* Solve type variable var by assigning it to the union of its lower bounds. * If freshen=true, first freshen the covariant and contravariant components of * the bounds. *) let bind_to_lower_bound ~freshen env r var lower_bounds = - let env, lower_bounds = expand_types env lower_bounds in (* Construct the union of the lower bounds, normalizing null|t to ?t because * some code is still sensitive to this representation. * Note that if there are no lower bounds then we will construct the empty - * type, i.e. Tunresolved []. *) - let (nulls, nonnulls) = - List.partition_tf (Typing_set.elements lower_bounds) - (fun ty -> match ty with (_, Tprim Nast.Tnull) -> true | _ -> false) in + * type, i.e. Tunresolved []. + * Also note that `var` is eliminated from the bounds, as + * var | t1 | ... | tn <: var + * iff t1 | ... | tn <: var + * This prevents it getting picked up later during the "occurs check" and + * reported as a circular type error. + *) + let env, has_null, nonnulls = expand_and_flatten_type_set env var lower_bounds in let ty = match nonnulls with | [ty] -> ty | tys -> (r, Tunresolved tys) in let ty = - if List.is_empty nulls + if not has_null then ty else (fst ty, Toption ty) in (* Freshen components of the types in the union wrt their variance. diff --git a/hphp/hack/test/typecheck/new_inference/eager_solve/circular_bug_2.php b/hphp/hack/test/typecheck/new_inference/eager_solve/circular_bug_2.php new file mode 100644 index 00000000000..b55dc9d8553 --- /dev/null +++ b/hphp/hack/test/typecheck/new_inference/eager_solve/circular_bug_2.php @@ -0,0 +1,34 @@ +>; +} + +async function genEnforce( + arraykey $key, +): Awaitable { +//UNSAFE +} + +async function genmk( + (function (Tk): Awaitable) $gen, + Traversable $keys, +): Awaitable> { + return Map{}; +} +function keys( + KeyedTraversable $traversable, +): vec { + return vec[]; +} +async function stuff(varray $group_ids): Awaitable { + $groups = await genmk( + async $id ==> await genEnforce($id), + $group_ids, + ); + $members = await genmk( + async $id ==> await $groups[$id]->query(), + keys($groups), + ); +} diff --git a/hphp/hack/test/typecheck/new_inference/eager_solve/circular_bug_2.php.exp b/hphp/hack/test/typecheck/new_inference/eager_solve/circular_bug_2.php.exp new file mode 100644 index 00000000000..c8e168d9b27 --- /dev/null +++ b/hphp/hack/test/typecheck/new_inference/eager_solve/circular_bug_2.php.exp @@ -0,0 +1,3 @@ +File "circular_bug_2.php", line 25, characters 16-20: + There are remaining unsolved constraints!: int <: int +No errors diff --git a/hphp/hack/test/typecheck/new_inference/transitive_simplify_2.php.exp b/hphp/hack/test/typecheck/new_inference/transitive_simplify_2.php.exp index 4324619e6af..0d04daeebbf 100644 --- a/hphp/hack/test/typecheck/new_inference/transitive_simplify_2.php.exp +++ b/hphp/hack/test/typecheck/new_inference/transitive_simplify_2.php.exp @@ -1,3 +1,3 @@ File "transitive_simplify_2.php", line 19, characters 10-13: - There are remaining unsolved constraints!: (nothing <: nothing && nothing <: nothing && nothing <: nothing) + There are remaining unsolved constraints!: (nothing <: nothing && nothing <: nothing && nothing <: nothing && nothing <: nothing) No errors -- 2.11.4.GIT