Skip to content
Permalink
Browse files

New inference: remove redundant upper bounds when solving with a lowe…

…r bound that is a type variable

Summary:
We are creating superfluous unions when solving using the lower bounds on type variables. (To see this, uncomment the `hh_show_env` in the new test in this diff.)

Suppose we have
```
v1,...,vn,t1,...,tm <: u
```
as lower bounds on a variable `u`, where `v1,...,vn` are themselves variables, and `t1,...,tm` are non-variables. Now suppose we solve `u` to its lower bounds, i.e. constructing a union
```
u := v1 | ... | vn | t1 | ... | tm
```
Necessarily it must be the case that each `vi` has an *upper bound* `u`, and so we end up with upper bounds
```
v1 <: v1 | ... | vn | t1 | ... | tm
...
vn <: v1 | ... | vn | t1 | ... | tm
```
Clearly these upper bounds are redundant, so can be removed.

FUTURE: The dual optimization makes sense for upper solving to the upper bounds on type variables using intersection types.

Reviewed By: manzyuk

Differential Revision: D13671163

fbshipit-source-id: fd1d5d0b624be815e99bc69991e0f0f0fa1c2d4b
  • Loading branch information...
andrewjkennedy authored and hhvm-bot committed Jan 21, 2019
1 parent 741a552 commit f8abf47d6d15bf11e9f8caa8a6bbcb2cde225ad4
@@ -1357,6 +1357,26 @@ let set_tyvar_variance ~tyvars env ty =
then update_variance_of_tyvars_occurring_in_upper_bound env ty
else env

(* Remove type variable `upper_var` from the upper bounds on `var`, if it exists
*)
let remove_tyvar_upper_bound env var upper_var =
let tvinfo = get_tvar_info env.tvenv var in
let upper_bounds = TySet.filter
(fun ty -> match expand_type env ty with _, (_, Tvar v) -> v <> upper_var | _ -> true)
tvinfo.upper_bounds in
env_with_tvenv env (IMap.add var { tvinfo with upper_bounds } env.tvenv)


(* Remove type variable `lower_var` from the lower bounds on `var`, if it exists
*)
let remove_tyvar_lower_bound env var lower_var =
let tvinfo = get_tvar_info env.tvenv var in
let lower_bounds = TySet.filter
(fun ty -> match expand_type env ty with _, (_, Tvar v) -> v <> lower_var | _ -> true)
tvinfo.lower_bounds in
env_with_tvenv env (IMap.add var { tvinfo with lower_bounds } env.tvenv)


(* Add a single new upper bound [ty] to type variable [var] in [env.tvenv].
* If the optional [union] operation is supplied, then use this to avoid
* adding redundant bounds by merging the type with existing bounds. This makes
@@ -144,6 +144,10 @@ val add_tyvar_upper_bound :
val add_tyvar_lower_bound :
?union:(locl ty -> locl ty list -> locl ty list) ->
env -> int -> locl ty -> env
val remove_tyvar_upper_bound :
env -> int -> int -> env
val remove_tyvar_lower_bound :
env -> int -> int -> env
val set_tyvar_appears_covariantly :
env -> int -> env
val set_tyvar_appears_contravariantly :
@@ -2415,7 +2415,7 @@ and freshen_tparams_wrt_variance env variancel tyl =
let bind env r var ty =
Typing_log.(log_with_level env "prop" 2 (fun () ->
log_types (Reason.to_pos r) env
[Log_head (Printf.sprintf "Typing_subtype.solve_tyvar/Typing_unify_recursive.add #%d" var,
[Log_head (Printf.sprintf "Typing_subtype.bind #%d" var,
[Log_type ("ty", ty)])]));

(* Update the variance *)
@@ -2447,10 +2447,30 @@ let bind_to_lower_bound ~freshen env r var =
if List.is_empty nulls
then ty
else (fst ty, Toption ty) in
(* Freshen components of the types in the union wrt their variance.
* For example, if we have
* Cov<C>, Contra<D> <: v
* then we actually construct the union
* Cov<#1> | Contra<#2> with C <: #1 and #2 <: D
*)
let env, ty =
if freshen
then freshen_inside_ty_wrt_variance env ty
else env, ty in
(* If any of the components of the union are type variables, then remove
* var from their upper bounds. Why? Because if we construct
* v1 , ... , vn , t <: var
* for type variables v1, ..., vn and non-type variable t
* then necessarily we must have var as an upper bound on each of vi
* so after binding var we end up with redundant bounds
* vi <: v1 | ... | vn | t
*)
let env =
List.fold_left ~f:(fun env ty ->
match Env.expand_type env ty with
| env, (_, Tvar v) ->
Env.remove_tyvar_upper_bound env v var
| env, _ -> env) ~init:env nonnulls in
(* Now actually make the assignment var := ty, and remove var from tvenv *)
bind env r var ty

@@ -0,0 +1,42 @@
<?hh //strict
class Inv<T> {
public function __construct(public T $item) { }
}
class Cov<+T> {
public function __construct(private T $item) { }
}
function make<T>(T $x):Cov<T> {
return new Cov($x);
}
function test(): Cov<mixed> {
$i = (new Inv("a"))->item;
// At this point we have
// $i : #1
// string <: #1
// Now we generate another fresh variable, say #2
// #1 <: #2
// And to maintain transitive closure property
// string <: #2
// So we have (marking type variable key by [.])
// #1, string <: [#2]
// string <: [#1] <: #2
// $c : Cov<#2>
// But we immediately solve because #2 appears only covariantly
// So #2 := #1|string
// (Note that necessarily we have [#1] <: #2 because every tyvar lower bound
// has itself an upper bound)
// So we now have
// string <: #1 <: #1|string
// We SHOULD be able to simplify the upper bound away (because #1 <: #1|string is an identity)
// to get
// $i:#1|string
// $c:Cov<#1|string>
// string <: #1
$c = make($i);
// hh_show_env();
return $c;
}

0 comments on commit f8abf47

Please sign in to comment.
You can’t perform that action at this time.