Improve type solving heuristic
commit3b3cd6817bc5412edfb3ae9410571108cd520e05
authorScott Owens <sowens@fb.com>
Wed, 21 Apr 2021 10:57:14 +0000 (21 03:57 -0700)
committerFacebook GitHub Bot <facebook-github-bot@users.noreply.github.com>
Wed, 21 Apr 2021 10:58:24 +0000 (21 03:58 -0700)
treec64f0c9184ec11351464ef3c77d7a5aa6feb6efa
parent30d628e8e813007a4a23b00eb0a2058dd64d9cac
Improve type solving heuristic

Summary:
Update the heuristic for reporting errors when solving a type leads to type `nothing`. Previously, if there were any unsolved type variables, and the type solved to `nothing` an error was generated suggesting a type to  add to the program. The assumption was that the resulting `nothing` was as a result of the type variable itself solving to `nothing`. However, the type could have solved to `nothing` for other reasons that have nothing to do with the variable (e.g., it contained a variable that solved to `null` intersected with one that solved to `nonnull`). This makes the heuristic more precise, in that it will only produce the error when a type variable is actually solved to `nothing` in the process of the whole type solving to `nothing`. This extra precision makes the type checker more complete.

The updated heuristic can change which suggestion gets made. Consider the situation where the type is a variable #1, and we also had #2<:#1. Previously, #1 would get solved to #2 which would get solved to `nothing`, and the error would be based on #1 from the original type. Now, since it's #2 that gets solved to `nothing` the error is based on it instead.

Reviewed By: CatherineGasnier

Differential Revision: D27879773

fbshipit-source-id: 4e86851efb7b54611e9dfa1c444bde13750982f6
hphp/hack/src/typing/typing_solver.ml
hphp/hack/test/typecheck/inter_instanceof_nothing.php [new file with mode: 0644]
hphp/hack/test/typecheck/inter_instanceof_nothing.php.exp [new file with mode: 0644]
hphp/hack/test/typecheck/new_inference/typehole/lambda_with_invoke.php.exp