[nullsafe][annotation graph] Issue a provisional violation in assignments between two provisionally nullables

Summary:
This change is what makes the annotation graph a _graph_.
Now we can detect places when adding one annotation causes an issue that can be
fixed by adding another annotation.

Reviewed By: artempyanykh

Differential Revision: D24650979

fbshipit-source-id: b8452b822

infer/src/nullsafe/AssignmentRule.ml

@@ -266,9 +266,19 @@ module ReportableViolation = struct
 end
 
 let check ~lhs ~rhs =
-  let is_subtype =
-    Nullability.is_subtype
-      ~supertype:(AnnotatedNullability.get_nullability lhs)
-      ~subtype:(InferredNullability.get_nullability rhs)
-  in
-  Result.ok_if_true is_subtype ~error:{lhs; rhs}
+  match (lhs, InferredNullability.get_nullability rhs) with
+  | AnnotatedNullability.ProvisionallyNullable _, Nullability.ProvisionallyNullable ->
+      (* This is a special case. Assignment of something that comes from provisionally nullable annotation to something that
+         is annotated as provisionally nullable is a (provisional) violation.
+         (With an exception when it is an assignment to the same annotation e.g. in recursion calls;
+          but such exceptions are non-essential for the purposes of calculation of the annotation graph.
+         )
+      *)
+      Error {lhs; rhs}
+  | _ ->
+      let is_subtype =
+        Nullability.is_subtype
+          ~supertype:(AnnotatedNullability.get_nullability lhs)
+          ~subtype:(InferredNullability.get_nullability rhs)
+      in
+      Result.ok_if_true is_subtype ~error:{lhs; rhs}