New inference: remove redundant upper bounds when solving with a lower bound that...
commitf8abf47d6d15bf11e9f8caa8a6bbcb2cde225ad4
authorAndrew Kennedy <akenn@fb.com>
Mon, 21 Jan 2019 14:43:44 +0000 (21 06:43 -0800)
committerHhvm Bot <hhvm-bot@users.noreply.github.com>
Mon, 21 Jan 2019 14:47:36 +0000 (21 06:47 -0800)
tree9f066a62ab452f78f41293398e8b307f4a4f2e29
parent741a552a1814355748ca5fca78c580ff12fffca0
New inference: remove redundant upper bounds when solving with a lower 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
hphp/hack/src/typing/typing_env.ml
hphp/hack/src/typing/typing_env.mli
hphp/hack/src/typing/typing_subtype.ml
hphp/hack/test/typecheck/new_inference/extra_union.php [new file with mode: 0644]
hphp/hack/test/typecheck/new_inference/extra_union.php.exp [new file with mode: 0644]