diff --git a/infer/src/nullsafe/AssignmentRule.ml b/infer/src/nullsafe/AssignmentRule.ml
new file mode 100644
index 000000000..21e9b5dcc
--- /dev/null
+++ b/infer/src/nullsafe/AssignmentRule.ml
@@ -0,0 +1,40 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+
+type violation = {lhs: Nullability.t; rhs: Nullability.t} [@@deriving compare]
+
+type assignment_type =
+  | PassingParamToFunction of
+      { param_description: string
+      ; param_position: int
+      ; function_procname: Typ.Procname.t }
+  | AssigningToField of Typ.Fieldname.t
+  | ReturningFromFunction of Typ.Procname.t
+[@@deriving compare]
+
+let check ~lhs ~rhs =
+  Result.ok_if_true (Nullability.is_subtype ~subtype:rhs ~supertype:lhs) ~error:{lhs; rhs}
+
+
+let violation_description _ assignment_type ~rhs_origin_descr =
+  let module MF = MarkupFormatter in
+  match assignment_type with
+  | PassingParamToFunction {param_description; param_position; function_procname} ->
+      Format.asprintf "%a needs a non-null value in parameter %d but argument %a can be null. %s"
+        MF.pp_monospaced
+        (Typ.Procname.to_simplified_string ~withclass:true function_procname)
+        param_position MF.pp_monospaced param_description rhs_origin_descr
+  | AssigningToField field_name ->
+      Format.asprintf "Field %a can be null but is not declared %a. %s" MF.pp_monospaced
+        (Typ.Fieldname.to_simplified_string field_name)
+        MF.pp_monospaced "@Nullable" rhs_origin_descr
+  | ReturningFromFunction function_proc_name ->
+      Format.asprintf "Method %a may return null but it is not annotated with %a. %s"
+        MF.pp_monospaced
+        (Typ.Procname.to_simplified_string function_proc_name)
+        MF.pp_monospaced "@Nullable" rhs_origin_descr
diff --git a/infer/src/nullsafe/AssignmentRule.mli b/infer/src/nullsafe/AssignmentRule.mli
new file mode 100644
index 000000000..6a77f2b3a
--- /dev/null
+++ b/infer/src/nullsafe/AssignmentRule.mli
@@ -0,0 +1,27 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+
+(** Assignment rule should be checked when a value is assigned to a location.
+    Assignment can be explicit (lhs = rhs) or implicit (e.g. returning from a function).
+    This rule checks if null can be passed to a place that does not expect null.
+ *)
+
+type violation [@@deriving compare]
+
+val check : lhs:Nullability.t -> rhs:Nullability.t -> (unit, violation) result
+
+type assignment_type =
+  | PassingParamToFunction of
+      { param_description: string
+      ; param_position: int
+      ; function_procname: Typ.Procname.t }
+  | AssigningToField of Typ.Fieldname.t
+  | ReturningFromFunction of Typ.Procname.t
+[@@deriving compare]
+
+val violation_description : violation -> assignment_type -> rhs_origin_descr:string -> string
diff --git a/infer/src/nullsafe/DereferenceRule.ml b/infer/src/nullsafe/DereferenceRule.ml
new file mode 100644
index 000000000..6ce188b0f
--- /dev/null
+++ b/infer/src/nullsafe/DereferenceRule.ml
@@ -0,0 +1,58 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+
+type violation = Nullability.t [@@deriving compare]
+
+type dereference_type =
+  | MethodCall of Typ.Procname.t
+  | AccessToField of Typ.Fieldname.t
+  | AccessByIndex of {index_desc: string}
+  | ArrayLengthAccess
+[@@deriving compare]
+
+let check = function
+  | Nullability.Nullable as nullability ->
+      Error nullability
+  | Nullability.Nonnull ->
+      Ok ()
+
+
+let violation_description _ dereference_type ~nullable_object_descr ~origin_descr =
+  let module MF = MarkupFormatter in
+  let nullable_object_descr =
+    match dereference_type with
+    | MethodCall _ | AccessToField _ -> (
+      match nullable_object_descr with
+      | None ->
+          "Object"
+      (* Just describe an object itself *)
+      | Some descr ->
+          MF.monospaced_to_string descr )
+    | ArrayLengthAccess | AccessByIndex _ -> (
+      (* In Java, those operations can be applied only to arrays *)
+      match nullable_object_descr with
+      | None ->
+          "Array"
+      | Some descr ->
+          Format.sprintf "Array %s" (MF.monospaced_to_string descr) )
+  in
+  let action_descr =
+    match dereference_type with
+    | MethodCall method_name ->
+        Format.sprintf "calling %s"
+          (MF.monospaced_to_string (Typ.Procname.to_simplified_string method_name))
+    | AccessToField field_name ->
+        Format.sprintf "accessing field %s"
+          (MF.monospaced_to_string (Typ.Fieldname.to_simplified_string field_name))
+    | AccessByIndex {index_desc} ->
+        Format.sprintf "accessing at index %s" (MF.monospaced_to_string index_desc)
+    | ArrayLengthAccess ->
+        "accessing its length"
+  in
+  Format.sprintf "%s is nullable and is not locally checked for null when %s. %s"
+    nullable_object_descr action_descr origin_descr
diff --git a/infer/src/nullsafe/DereferenceRule.mli b/infer/src/nullsafe/DereferenceRule.mli
new file mode 100644
index 000000000..8eda8a339
--- /dev/null
+++ b/infer/src/nullsafe/DereferenceRule.mli
@@ -0,0 +1,29 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+
+(** Dereference rule should be checked every type an object is dereferenced.
+    The rule checks if the reference is nullable.
+ *)
+
+type violation [@@deriving compare]
+
+val check : Nullability.t -> (unit, violation) result
+
+type dereference_type =
+  | MethodCall of Typ.Procname.t
+  | AccessToField of Typ.Fieldname.t
+  | AccessByIndex of {index_desc: string}
+  | ArrayLengthAccess
+[@@deriving compare]
+
+val violation_description :
+     violation
+  -> dereference_type
+  -> nullable_object_descr:string option
+  -> origin_descr:string
+  -> string
diff --git a/infer/src/nullsafe/InheritanceRule.ml b/infer/src/nullsafe/InheritanceRule.ml
new file mode 100644
index 000000000..13ebfbcc3
--- /dev/null
+++ b/infer/src/nullsafe/InheritanceRule.ml
@@ -0,0 +1,59 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+
+type violation = {base: Nullability.t; overridden: Nullability.t} [@@deriving compare]
+
+type type_role = Param | Ret
+
+let check type_role ~base ~overridden =
+  let subtype, supertype =
+    match type_role with
+    | Ret ->
+        (* covariance for ret *)
+        (overridden, base)
+    | Param ->
+        (* contravariance for param *)
+        (base, overridden)
+  in
+  Result.ok_if_true (Nullability.is_subtype ~subtype ~supertype) ~error:{base; overridden}
+
+
+type violation_type =
+  | InconsistentParam of {param_description: string; param_position: int}
+  | InconsistentReturn
+[@@deriving compare]
+
+let violation_description _ violation_type ~base_proc_name ~overridden_proc_name =
+  let module MF = MarkupFormatter in
+  let nullable_annotation = "@Nullable" in
+  let base_method_descr = Typ.Procname.to_simplified_string ~withclass:true base_proc_name in
+  let overridden_method_descr =
+    Typ.Procname.to_simplified_string ~withclass:true overridden_proc_name
+  in
+  match violation_type with
+  | InconsistentReturn ->
+      Format.asprintf "Method %a is annotated with %a but overrides unannotated method %a."
+        MF.pp_monospaced overridden_method_descr MF.pp_monospaced nullable_annotation
+        MF.pp_monospaced base_method_descr
+  | InconsistentParam {param_description; param_position} ->
+      let translate_position = function
+        | 1 ->
+            "First"
+        | 2 ->
+            "Second"
+        | 3 ->
+            "Third"
+        | n ->
+            string_of_int n ^ "th"
+      in
+      Format.asprintf
+        "%s parameter %a of method %a is not %a but is declared %ain the parent class method %a."
+        (translate_position param_position)
+        MF.pp_monospaced param_description MF.pp_monospaced overridden_method_descr
+        MF.pp_monospaced nullable_annotation MF.pp_monospaced nullable_annotation MF.pp_monospaced
+        base_method_descr
diff --git a/infer/src/nullsafe/InheritanceRule.mli b/infer/src/nullsafe/InheritanceRule.mli
new file mode 100644
index 000000000..3b66b1f50
--- /dev/null
+++ b/infer/src/nullsafe/InheritanceRule.mli
@@ -0,0 +1,35 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+
+(** Inheritance rule:
+  a) Return type for an overridden method is covariant:
+       overridden method is allowed to narrow down the return value to a subtype of the one from the
+       base method; this means it is OK to make the return value non-null when it was nullable in the base)
+  b) Parameter type for an overridden method is contravariant.
+       It is OK for a derived method to accept nullable in the params even if the base does not accept nullable.
+  NOTE: Rule a) is based on Java covariance rule for the return type.
+        In contrast, rule b) is nullsafe specific as Java does not support type contravariance for method params.
+ *)
+
+type violation [@@deriving compare]
+
+type violation_type =
+  | InconsistentParam of {param_description: string; param_position: int}
+  | InconsistentReturn
+[@@deriving compare]
+
+type type_role = Param | Ret
+
+val check : type_role -> base:Nullability.t -> overridden:Nullability.t -> (unit, violation) result
+
+val violation_description :
+     violation
+  -> violation_type
+  -> base_proc_name:Typ.Procname.t
+  -> overridden_proc_name:Typ.Procname.t
+  -> string
diff --git a/infer/src/nullsafe/NullsafeRules.ml b/infer/src/nullsafe/NullsafeRules.ml
deleted file mode 100644
index 38a8e5855..000000000
--- a/infer/src/nullsafe/NullsafeRules.ml
+++ /dev/null
@@ -1,35 +0,0 @@
-(*
- * Copyright (c) Facebook, Inc. and its affiliates.
- *
- * This source code is licensed under the MIT license found in the
- * LICENSE file in the root directory of this source tree.
- *)
-
-open! IStd
-
-let passes_assignment_rule ~lhs ~rhs = Nullability.is_subtype ~subtype:rhs ~supertype:lhs
-
-let passes_dereference_rule = function
-  | Nullability.Nullable ->
-      false
-  | Nullability.Nonnull ->
-      true
-
-
-type type_role = Param | Ret
-
-let passes_inheritance_rule type_role ~base ~overridden =
-  let subtype, supertype =
-    match type_role with
-    | Ret ->
-        (* covariance for ret *)
-        (overridden, base)
-    | Param ->
-        (* contravariance for param *)
-        (base, overridden)
-  in
-  Nullability.is_subtype ~subtype ~supertype
-
-
-let is_overannotated ~lhs ~rhs_upper_bound =
-  Nullability.is_strict_subtype ~subtype:rhs_upper_bound ~supertype:lhs
diff --git a/infer/src/nullsafe/NullsafeRules.mli b/infer/src/nullsafe/NullsafeRules.mli
deleted file mode 100644
index 8b5c5cd2b..000000000
--- a/infer/src/nullsafe/NullsafeRules.mli
+++ /dev/null
@@ -1,57 +0,0 @@
-(*
- * Copyright (c) Facebook, Inc. and its affiliates.
- *
- * This source code is licensed under the MIT license found in the
- * LICENSE file in the root directory of this source tree.
- *)
-
-open! IStd
-
-(** This is a single place consolidating core rules driving Nullsafe type checking.
-  Nullsafe enforces similar rules in different places (e.g. places dealing with fields,
-  function calls, assignments, local variables etc.).
-  Those places might have additional specifics, but core checks should be done through this class.
-  If you are writing a new or modifying an existing check, ask yourself if you can directly
-  use already existng rules from this module.
-  If you feel you need a rule of a completely new nature, add it to this module.
-  As a rule of thumb, every different "check" that is responsible for detecting issues, should query
-  this module instead of doing things on their own.
-  *)
-
-val passes_assignment_rule : lhs:Nullability.t -> rhs:Nullability.t -> bool
-(** Assignment rule: No expression of nullable type is ever assigned to a location
-    of non-nullable type.
- *)
-
-val passes_dereference_rule : Nullability.t -> bool
-(** Dereference rule: an object can be dereferenced only when it is not nullable (or believed to be so).
- *)
-
-type type_role = Param | Ret
-
-val passes_inheritance_rule : type_role -> base:Nullability.t -> overridden:Nullability.t -> bool
-(** Inheritance rule:
-  a) Return type for an overridden method is covariant:
-       overridden method is allowed to narrow down the return value to a subtype of the one from the
-       base method; this means it is OK to make the return value non-null when it was nullable in the base)
-  b) Parameter type for an overridden method is contravariant.
-       It is OK for a derived method to accept nullable in the params even if the base does not accept nullable.
-  NOTE: Rule a) is based on Java covariance rule for the return type.
-        In contrast, rule b) is nullsafe specific as Java does not support type contravariance for method params.
- *)
-
-val is_overannotated : lhs:Nullability.t -> rhs_upper_bound:Nullability.t -> bool
-(** Check if a type in signature (e.g. return value) can be made more specific.
-   If an upper bound of `rhs_i` over ALL assignents `lhs = rhs_i` that exist in the program
-   is a _strict_ subtype of lhs, `lhs`'s type can be narrowed to be that upper bound.
-   NOTE: This rule is complementatary to assignment rule.
-         While assignment rule checks a single assignment `lhs = rhs`, this rule
-         checks checks ALL assignments to `lhs` in the program.
-   NOTE: Violation of this rule is not a type violation, hence it should never be surfaced as error:
-         `lhs`'s type can be intentionally made broad by code author
-         (e.g. to anticipate future changes in the implementation).
-         Additional heuristits are required to correctly surface overannotated rule to the user.
-         This rule is useful for some scenarios, especially for nullability code conversions
-         when it is expected that some signatures were annotated with @Nullable defensively, so
-         surfacing such cases can improve API and make migration smooth.
- *)
diff --git a/infer/src/nullsafe/OverAnnotatedRule.ml b/infer/src/nullsafe/OverAnnotatedRule.ml
new file mode 100644
index 000000000..0c1b7feaa
--- /dev/null
+++ b/infer/src/nullsafe/OverAnnotatedRule.ml
@@ -0,0 +1,34 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+
+type violation = {lhs: Nullability.t; rhs_upper_bound: Nullability.t} [@@deriving compare]
+
+let check ~lhs ~rhs_upper_bound =
+  if Nullability.is_strict_subtype ~subtype:rhs_upper_bound ~supertype:lhs then
+    Error {lhs; rhs_upper_bound}
+  else Ok ()
+
+
+type violation_type =
+  | FieldOverAnnoted of Typ.Fieldname.t
+  | ReturnOverAnnotated of Typ.Procname.t  (** Return value of a method can be made non-nullable *)
+[@@deriving compare]
+
+let violation_description _ violation_type =
+  let module MF = MarkupFormatter in
+  let nullable_annotation = "@Nullable" in
+  match violation_type with
+  | FieldOverAnnoted field_name ->
+      Format.asprintf "Field %a is always initialized in the constructor but is declared %a"
+        MF.pp_monospaced
+        (Typ.Fieldname.to_simplified_string field_name)
+        MF.pp_monospaced nullable_annotation
+  | ReturnOverAnnotated proc_name ->
+      Format.asprintf "Method %a is annotated with %a but never returns null." MF.pp_monospaced
+        (Typ.Procname.to_simplified_string proc_name)
+        MF.pp_monospaced nullable_annotation
diff --git a/infer/src/nullsafe/OverAnnotatedRule.mli b/infer/src/nullsafe/OverAnnotatedRule.mli
new file mode 100644
index 000000000..a11f8f558
--- /dev/null
+++ b/infer/src/nullsafe/OverAnnotatedRule.mli
@@ -0,0 +1,34 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+
+(** Checks if a type in signature (e.g. return value) can be made more specific.
+   NOTE: This rule is complementatary to assignment rule.
+         While assignment rule checks a single assignment `lhs = rhs`, this rule
+         checks checks ALL assignments to `lhs` in the program.
+   NOTE: Violation of this rule is not a type violation, hence it should never be surfaced as error:
+         `lhs`'s type can be intentionally made broad by code author
+         (e.g. to anticipate future changes in the implementation).
+         Heuristits are required to correctly surface overannotated rule to the user.
+         This rule is useful for some scenarios, especially for nullability code conversions
+         when it is expected that some signatures were annotated with @Nullable defensively, so
+         surfacing such cases can improve API and make migration smooth.
+ *)
+
+type violation [@@deriving compare]
+
+val check : lhs:Nullability.t -> rhs_upper_bound:Nullability.t -> (unit, violation) result
+(** If an upper bound of `rhs_i` over ALL assignents `lhs = rhs_i` that exist in the program
+   is a _strict_ subtype of lhs, `lhs`'s type can be narrowed to be that upper bound.
+*)
+
+type violation_type =
+  | FieldOverAnnoted of Typ.Fieldname.t
+  | ReturnOverAnnotated of Typ.Procname.t  (** Return value of a method can be made non-nullable *)
+[@@deriving compare]
+
+val violation_description : violation -> violation_type -> string
diff --git a/infer/src/nullsafe/eradicateChecks.ml b/infer/src/nullsafe/eradicateChecks.ml
index a7c318e62..8f2bd488c 100644
--- a/infer/src/nullsafe/eradicateChecks.ml
+++ b/infer/src/nullsafe/eradicateChecks.ml
@@ -28,17 +28,16 @@ let is_virtual = function
 
 let check_object_dereference tenv find_canonical_duplicate curr_pname node instr_ref object_exp
     dereference_type inferred_nullability loc =
-  if
-    not
-      (NullsafeRules.passes_dereference_rule
-         (InferredNullability.get_nullability inferred_nullability))
-  then
-    let origin_descr = InferredNullability.descr_origin inferred_nullability in
-    let nullable_object_descr = explain_expr tenv node object_exp in
-    let type_error =
-      TypeErr.Nullable_dereference {nullable_object_descr; dereference_type; origin_descr}
-    in
-    report_error tenv find_canonical_duplicate type_error (Some instr_ref) loc curr_pname
+  Result.iter_error
+    (DereferenceRule.check (InferredNullability.get_nullability inferred_nullability))
+    ~f:(fun dereference_violation ->
+      let origin_descr = InferredNullability.descr_origin inferred_nullability in
+      let nullable_object_descr = explain_expr tenv node object_exp in
+      let type_error =
+        TypeErr.Nullable_dereference
+          {dereference_violation; nullable_object_descr; dereference_type; origin_descr}
+      in
+      report_error tenv find_canonical_duplicate type_error (Some instr_ref) loc curr_pname )
 
 
 (** Where the condition is coming from *)
@@ -144,22 +143,27 @@ let check_field_assignment tenv find_canonical_duplicate curr_pdesc node instr_r
     in
     Annotations.ia_is_cleanup ret_annotation_deprecated
   in
-  let should_report_nullable =
-    (not
-       (NullsafeRules.passes_assignment_rule
-          ~lhs:(InferredNullability.get_nullability inferred_nullability_lhs)
-          ~rhs:(InferredNullability.get_nullability inferred_nullability_rhs)))
-    && (not (AndroidFramework.is_destroy_method curr_pname))
-    && PatternMatch.type_is_class t_lhs
-    && (not (Typ.Fieldname.Java.is_outer_instance fname))
-    && (not (field_is_injector_readwrite ()))
-    && not (field_is_in_cleanup_context ())
+  let assignment_check_result =
+    AssignmentRule.check
+      ~lhs:(InferredNullability.get_nullability inferred_nullability_lhs)
+      ~rhs:(InferredNullability.get_nullability inferred_nullability_rhs)
   in
-  if should_report_nullable then
-    let rhs_origin_descr = InferredNullability.descr_origin inferred_nullability_rhs in
-    report_error tenv find_canonical_duplicate
-      (TypeErr.Bad_assignment {rhs_origin_descr; assignment_type= TypeErr.AssigningToAField fname})
-      (Some instr_ref) loc curr_pdesc
+  Result.iter_error assignment_check_result ~f:(fun assignment_violation ->
+      let should_report =
+        (not (AndroidFramework.is_destroy_method curr_pname))
+        && PatternMatch.type_is_class t_lhs
+        && (not (Typ.Fieldname.Java.is_outer_instance fname))
+        && (not (field_is_injector_readwrite ()))
+        && not (field_is_in_cleanup_context ())
+      in
+      if should_report then
+        let rhs_origin_descr = InferredNullability.descr_origin inferred_nullability_rhs in
+        report_error tenv find_canonical_duplicate
+          (TypeErr.Bad_assignment
+             { assignment_violation
+             ; rhs_origin_descr
+             ; assignment_type= AssignmentRule.AssigningToField fname })
+          (Some instr_ref) loc curr_pdesc )
 
 
 let is_nonnull AnnotatedField.{annotated_type} =
@@ -289,17 +293,19 @@ let check_constructor_initialization tenv find_canonical_duplicate curr_construc
               | None ->
                   ()
               | Some annotated_field ->
-                  if
-                    Config.eradicate_field_over_annotated
-                    && NullsafeRules.is_overannotated
-                         ~lhs:
-                           (AnnotatedNullability.get_nullability
-                              annotated_field.annotated_type.nullability)
-                         ~rhs_upper_bound:(field_nullability_upper_bound_over_all_typestates ())
-                  then
-                    report_error tenv find_canonical_duplicate
-                      (TypeErr.Over_annotation (TypeErr.FieldOverAnnotedAsNullable field_name))
-                      None loc curr_constructor_pdesc )
+                  if Config.eradicate_field_over_annotated then
+                    let lhs =
+                      AnnotatedNullability.get_nullability
+                        annotated_field.annotated_type.nullability
+                    in
+                    let rhs_upper_bound = field_nullability_upper_bound_over_all_typestates () in
+                    Result.iter_error (OverAnnotatedRule.check ~lhs ~rhs_upper_bound)
+                      ~f:(fun over_annotated_violation ->
+                        report_error tenv find_canonical_duplicate
+                          (TypeErr.Over_annotation
+                             { over_annotated_violation
+                             ; violation_type= OverAnnotatedRule.FieldOverAnnoted field_name })
+                          None loc curr_constructor_pdesc ) )
           in
           List.iter ~f:do_field fields
       | None ->
@@ -313,12 +319,14 @@ let check_return_not_nullable tenv find_canonical_duplicate loc curr_pname curr_
   (* Returning from a function is essentially an assignment the actual return value to the formal `return` *)
   let lhs = AnnotatedNullability.get_nullability ret_signature.ret_annotated_type.nullability in
   let rhs = InferredNullability.get_nullability ret_inferred_nullability in
-  if not (NullsafeRules.passes_assignment_rule ~lhs ~rhs) then
-    let rhs_origin_descr = InferredNullability.descr_origin ret_inferred_nullability in
-    report_error tenv find_canonical_duplicate
-      (TypeErr.Bad_assignment
-         {rhs_origin_descr; assignment_type= TypeErr.ReturningFromAFunction curr_pname})
-      None loc curr_pdesc
+  Result.iter_error (AssignmentRule.check ~lhs ~rhs) ~f:(fun assignment_violation ->
+      let rhs_origin_descr = InferredNullability.descr_origin ret_inferred_nullability in
+      report_error tenv find_canonical_duplicate
+        (TypeErr.Bad_assignment
+           { assignment_violation
+           ; rhs_origin_descr
+           ; assignment_type= AssignmentRule.ReturningFromFunction curr_pname })
+        None loc curr_pdesc )
 
 
 let check_return_overrannotated tenv find_canonical_duplicate loc curr_pname curr_pdesc
@@ -330,10 +338,13 @@ let check_return_overrannotated tenv find_canonical_duplicate loc curr_pname cur
      correct upper bound.
     *)
   let rhs_upper_bound = InferredNullability.get_nullability ret_inferred_nullability in
-  if NullsafeRules.is_overannotated ~lhs ~rhs_upper_bound then
-    report_error tenv find_canonical_duplicate
-      (TypeErr.Over_annotation (TypeErr.ReturnOverAnnotatedAsNullable curr_pname)) None loc
-      curr_pdesc
+  Result.iter_error (OverAnnotatedRule.check ~lhs ~rhs_upper_bound)
+    ~f:(fun over_annotated_violation ->
+      report_error tenv find_canonical_duplicate
+        (TypeErr.Over_annotation
+           { over_annotated_violation
+           ; violation_type= OverAnnotatedRule.ReturnOverAnnotated curr_pname })
+        None loc curr_pdesc )
 
 
 (** Check the annotations when returning from a method. *)
@@ -373,7 +384,7 @@ let check_call_receiver tenv find_canonical_duplicate curr_pdesc node typestate
           loc
       in
       check_object_dereference tenv find_canonical_duplicate curr_pdesc node instr_ref
-        original_this_e (TypeErr.MethodCall callee_pname) this_inferred_nullability loc
+        original_this_e (DereferenceRule.MethodCall callee_pname) this_inferred_nullability loc
   | [] ->
       ()
 
@@ -389,7 +400,7 @@ let check_call_parameters tenv find_canonical_duplicate curr_pdesc node callee_a
     resolved_params loc instr_ref : unit =
   let callee_pname = callee_attributes.ProcAttributes.proc_name in
   let check {num= param_position; formal; actual= orig_e2, nullability_actual} =
-    let report () =
+    let report assignment_violation =
       let param_description =
         match explain_expr tenv node orig_e2 with
         | Some descr ->
@@ -400,9 +411,10 @@ let check_call_parameters tenv find_canonical_duplicate curr_pdesc node callee_a
       let rhs_origin_descr = InferredNullability.descr_origin nullability_actual in
       report_error tenv find_canonical_duplicate
         (TypeErr.Bad_assignment
-           { rhs_origin_descr
+           { assignment_violation
+           ; rhs_origin_descr
            ; assignment_type=
-               TypeErr.PassingParamToAFunction
+               AssignmentRule.PassingParamToFunction
                  {param_description; param_position; function_procname= callee_pname} })
         (Some instr_ref) loc curr_pdesc
     in
@@ -411,7 +423,7 @@ let check_call_parameters tenv find_canonical_duplicate curr_pdesc node callee_a
       to the formal param *)
       let lhs = AnnotatedNullability.get_nullability formal.param_annotated_type.nullability in
       let rhs = InferredNullability.get_nullability nullability_actual in
-      if not (NullsafeRules.passes_assignment_rule ~lhs ~rhs) then report ()
+      Result.iter_error (AssignmentRule.check ~lhs ~rhs) ~f:report
   in
   let should_check_parameters =
     match callee_pname with
@@ -430,35 +442,33 @@ let check_call_parameters tenv find_canonical_duplicate curr_pdesc node callee_a
 
 let check_inheritance_rule_for_return find_canonical_duplicate tenv loc ~base_proc_name
     ~overridden_proc_name ~overridden_proc_desc ~base_nullability ~overridden_nullability =
-  if
-    not
-      (NullsafeRules.passes_inheritance_rule NullsafeRules.Ret ~base:base_nullability
-         ~overridden:overridden_nullability)
-  then
-    report_error tenv find_canonical_duplicate
-      (TypeErr.Inconsistent_subclass
-         { overridden_proc_name
-         ; base_proc_name
-         ; inconsistent_subclass_type= TypeErr.InconsistentReturn })
-      None loc overridden_proc_desc
+  Result.iter_error
+    (InheritanceRule.check InheritanceRule.Ret ~base:base_nullability
+       ~overridden:overridden_nullability) ~f:(fun inheritance_violation ->
+      report_error tenv find_canonical_duplicate
+        (TypeErr.Inconsistent_subclass
+           { inheritance_violation
+           ; violation_type= InheritanceRule.InconsistentReturn
+           ; overridden_proc_name
+           ; base_proc_name })
+        None loc overridden_proc_desc )
 
 
 let check_inheritance_rule_for_param find_canonical_duplicate tenv loc ~overridden_param_name
     ~base_proc_name ~overridden_proc_name ~overridden_proc_desc ~param_position ~base_nullability
     ~overridden_nullability =
-  if
-    not
-      (NullsafeRules.passes_inheritance_rule NullsafeRules.Param ~base:base_nullability
-         ~overridden:overridden_nullability)
-  then
-    report_error tenv find_canonical_duplicate
-      (TypeErr.Inconsistent_subclass
-         { base_proc_name
-         ; overridden_proc_name
-         ; inconsistent_subclass_type=
-             TypeErr.InconsistentParam
-               {param_position; param_description= Mangled.to_string overridden_param_name} })
-      None loc overridden_proc_desc
+  Result.iter_error
+    (InheritanceRule.check InheritanceRule.Param ~base:base_nullability
+       ~overridden:overridden_nullability) ~f:(fun inheritance_violation ->
+      report_error tenv find_canonical_duplicate
+        (TypeErr.Inconsistent_subclass
+           { inheritance_violation
+           ; violation_type=
+               InheritanceRule.InconsistentParam
+                 {param_position; param_description= Mangled.to_string overridden_param_name}
+           ; base_proc_name
+           ; overridden_proc_name })
+        None loc overridden_proc_desc )
 
 
 let check_inheritance_rule_for_params find_canonical_duplicate tenv loc ~base_proc_name
diff --git a/infer/src/nullsafe/typeCheck.ml b/infer/src/nullsafe/typeCheck.ml
index 48ff44044..9609c3fc1 100644
--- a/infer/src/nullsafe/typeCheck.ml
+++ b/infer/src/nullsafe/typeCheck.ml
@@ -148,7 +148,7 @@ let rec typecheck_expr find_canonical_duplicate visited checks tenv node instr_r
       in
       if checks.eradicate then
         EradicateChecks.check_object_dereference tenv find_canonical_duplicate curr_pdesc node
-          instr_ref exp (TypeErr.AccessToField field_name) inferred_nullability loc ;
+          instr_ref exp (DereferenceRule.AccessToField field_name) inferred_nullability loc ;
       tr_new
   | Exp.Lindex (array_exp, index_exp) ->
       let _, inferred_nullability =
@@ -161,7 +161,7 @@ let rec typecheck_expr find_canonical_duplicate visited checks tenv node instr_r
       if checks.eradicate then
         EradicateChecks.check_object_dereference tenv find_canonical_duplicate curr_pdesc node
           instr_ref array_exp
-          (TypeErr.AccessByIndex {index_desc})
+          (DereferenceRule.AccessByIndex {index_desc})
           inferred_nullability loc ;
       tr_default
   | _ ->
@@ -472,7 +472,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
       in
       if checks.eradicate then
         EradicateChecks.check_object_dereference tenv find_canonical_duplicate curr_pdesc node
-          instr_ref array_exp TypeErr.ArrayLengthAccess ta loc ;
+          instr_ref array_exp DereferenceRule.ArrayLengthAccess ta loc ;
       TypeState.add_id id
         (Typ.mk (Tint Typ.IInt), InferredNullability.create_nonnull TypeOrigin.New)
         typestate
diff --git a/infer/src/nullsafe/typeErr.ml b/infer/src/nullsafe/typeErr.ml
index 841c6fb7c..57d9906f2 100644
--- a/infer/src/nullsafe/typeErr.ml
+++ b/infer/src/nullsafe/typeErr.ml
@@ -66,41 +66,25 @@ let compare_origin_descr _ _ = 0
 type err_instance =
   | Condition_redundant of (bool * string option)
   | Inconsistent_subclass of
-      { base_proc_name: Typ.Procname.t
-      ; overridden_proc_name: Typ.Procname.t
-      ; inconsistent_subclass_type: inconsistent_subclass_type }
+      { inheritance_violation: InheritanceRule.violation
+      ; violation_type: InheritanceRule.violation_type
+      ; base_proc_name: Typ.Procname.t
+      ; overridden_proc_name: Typ.Procname.t }
   | Field_not_initialized of Typ.Fieldname.t * Typ.Procname.t
-  | Over_annotation of over_annotation_type
+  | Over_annotation of
+      { over_annotated_violation: OverAnnotatedRule.violation
+      ; violation_type: OverAnnotatedRule.violation_type }
   | Nullable_dereference of
-      { nullable_object_descr: string option
-      ; dereference_type: dereference_type
+      { dereference_violation: DereferenceRule.violation
+      ; dereference_type: DereferenceRule.dereference_type
+      ; nullable_object_descr: string option
       ; origin_descr: origin_descr }
-  | Bad_assignment of {rhs_origin_descr: origin_descr; assignment_type: assignment_type}
+  | Bad_assignment of
+      { assignment_violation: AssignmentRule.violation
+      ; assignment_type: AssignmentRule.assignment_type
+      ; rhs_origin_descr: origin_descr }
 [@@deriving compare]
 
-and inconsistent_subclass_type =
-  | InconsistentParam of {param_description: string; param_position: int}
-  | InconsistentReturn
-
-and over_annotation_type =
-  | FieldOverAnnotedAsNullable of Typ.Fieldname.t
-  | ReturnOverAnnotatedAsNullable of Typ.Procname.t
-      (** Return value of a method can be made non-nullable *)
-
-and assignment_type =
-  | PassingParamToAFunction of
-      { param_description: string
-      ; param_position: int
-      ; function_procname: Typ.Procname.t }
-  | AssigningToAField of Typ.Fieldname.t
-  | ReturningFromAFunction of Typ.Procname.t
-
-and dereference_type =
-  | MethodCall of Typ.Procname.t
-  | AccessToField of Typ.Fieldname.t
-  | AccessByIndex of {index_desc: string}
-  | ArrayLengthAccess
-
 module H = Hashtbl.Make (struct
   type t = err_instance * InstrRef.t option [@@deriving compare]
 
@@ -221,35 +205,35 @@ type st_report_error =
 let get_infer_issue_type = function
   | Condition_redundant _ ->
       IssueType.eradicate_condition_redundant
-  | Over_annotation (FieldOverAnnotedAsNullable _) ->
+  | Over_annotation {violation_type= OverAnnotatedRule.FieldOverAnnoted _} ->
       IssueType.eradicate_field_over_annotated
-  | Over_annotation (ReturnOverAnnotatedAsNullable _) ->
+  | Over_annotation {violation_type= OverAnnotatedRule.ReturnOverAnnotated _} ->
       IssueType.eradicate_return_over_annotated
   | Field_not_initialized _ ->
       IssueType.eradicate_field_not_initialized
-  | Bad_assignment {assignment_type= PassingParamToAFunction _} ->
+  | Bad_assignment {assignment_type= PassingParamToFunction _} ->
       IssueType.eradicate_parameter_not_nullable
-  | Bad_assignment {assignment_type= AssigningToAField _} ->
+  | Bad_assignment {assignment_type= AssigningToField _} ->
       IssueType.eradicate_field_not_nullable
-  | Bad_assignment {assignment_type= ReturningFromAFunction _} ->
+  | Bad_assignment {assignment_type= ReturningFromFunction _} ->
       IssueType.eradicate_return_not_nullable
   | Nullable_dereference _ ->
       IssueType.eradicate_nullable_dereference
-  | Inconsistent_subclass {inconsistent_subclass_type= InconsistentReturn} ->
+  | Inconsistent_subclass {violation_type= InconsistentReturn} ->
       IssueType.eradicate_inconsistent_subclass_return_annotation
-  | Inconsistent_subclass {inconsistent_subclass_type= InconsistentParam _} ->
+  | Inconsistent_subclass {violation_type= InconsistentParam _} ->
       IssueType.eradicate_inconsistent_subclass_parameter_annotation
 
 
 (* If an error is related to a particular field, we support suppressing the
    error via a supress annotation placed near the field declaration *)
 let get_field_name_for_error_suppressing = function
-  | Over_annotation (FieldOverAnnotedAsNullable field_name) ->
+  | Over_annotation {violation_type= OverAnnotatedRule.FieldOverAnnoted field_name} ->
       Some field_name
   | Field_not_initialized (field_name, _) ->
       Some field_name
   | Condition_redundant _
-  | Over_annotation (ReturnOverAnnotatedAsNullable _)
+  | Over_annotation {violation_type= OverAnnotatedRule.ReturnOverAnnotated _}
   (* In case of assignment to a field, it should be fixed case by case for each assignment *)
   | Bad_assignment _
   | Nullable_dereference _
@@ -263,15 +247,8 @@ let get_error_description err_instance =
   | Condition_redundant (is_always_true, s_opt) ->
       P.sprintf "The condition %s is always %b according to the existing annotations."
         (Option.value s_opt ~default:"") is_always_true
-  | Over_annotation (FieldOverAnnotedAsNullable field_name) ->
-      Format.asprintf "Field %a is always initialized in the constructor but is declared %a"
-        MF.pp_monospaced
-        (Typ.Fieldname.to_simplified_string field_name)
-        MF.pp_monospaced nullable_annotation
-  | Over_annotation (ReturnOverAnnotatedAsNullable proc_name) ->
-      Format.asprintf "Method %a is annotated with %a but never returns null." MF.pp_monospaced
-        (Typ.Procname.to_simplified_string proc_name)
-        MF.pp_monospaced nullable_annotation
+  | Over_annotation {over_annotated_violation; violation_type} ->
+      OverAnnotatedRule.violation_description over_annotated_violation violation_type
   | Field_not_initialized (field_name, proc_name) ->
       let constructor_name =
         if Typ.Procname.is_constructor proc_name then "the constructor"
@@ -285,84 +262,20 @@ let get_error_description err_instance =
       Format.asprintf "Field %a is not initialized in %s and is not declared %a" MF.pp_monospaced
         (Typ.Fieldname.to_simplified_string field_name)
         constructor_name MF.pp_monospaced nullable_annotation
-  | Bad_assignment {rhs_origin_descr= origin_descr_string, _, _; assignment_type} -> (
-    match assignment_type with
-    | PassingParamToAFunction {param_description; param_position; function_procname} ->
-        Format.asprintf "%a needs a non-null value in parameter %d but argument %a can be null. %s"
-          MF.pp_monospaced
-          (Typ.Procname.to_simplified_string ~withclass:true function_procname)
-          param_position MF.pp_monospaced param_description origin_descr_string
-    | AssigningToAField field_name ->
-        Format.asprintf "Field %a can be null but is not declared %a. %s" MF.pp_monospaced
-          (Typ.Fieldname.to_simplified_string field_name)
-          MF.pp_monospaced nullable_annotation origin_descr_string
-    | ReturningFromAFunction function_proc_name ->
-        Format.asprintf "Method %a may return null but it is not annotated with %a. %s"
-          MF.pp_monospaced
-          (Typ.Procname.to_simplified_string function_proc_name)
-          MF.pp_monospaced nullable_annotation origin_descr_string )
-  | Nullable_dereference {nullable_object_descr; dereference_type; origin_descr= origin_str, _, _}
+  | Bad_assignment {rhs_origin_descr= rhs_origin_descr, _, _; assignment_type; assignment_violation}
     ->
-      let nullable_object_descr =
-        match dereference_type with
-        | MethodCall _ | AccessToField _ -> (
-          match nullable_object_descr with
-          | None ->
-              "Object"
-          (* Just describe an object itself *)
-          | Some descr ->
-              MF.monospaced_to_string descr )
-        | ArrayLengthAccess | AccessByIndex _ -> (
-          (* In Java, those operations can be applied only to arrays *)
-          match nullable_object_descr with
-          | None ->
-              "Array"
-          | Some descr ->
-              Format.sprintf "Array %s" (MF.monospaced_to_string descr) )
-      in
-      let action_descr =
-        match dereference_type with
-        | MethodCall method_name ->
-            Format.sprintf "calling %s"
-              (MF.monospaced_to_string (Typ.Procname.to_simplified_string method_name))
-        | AccessToField field_name ->
-            Format.sprintf "accessing field %s"
-              (MF.monospaced_to_string (Typ.Fieldname.to_simplified_string field_name))
-        | AccessByIndex {index_desc} ->
-            Format.sprintf "accessing at index %s" (MF.monospaced_to_string index_desc)
-        | ArrayLengthAccess ->
-            "accessing its length"
-      in
-      Format.sprintf "%s is nullable and is not locally checked for null when %s. %s"
-        nullable_object_descr action_descr origin_str
-  | Inconsistent_subclass {base_proc_name; overridden_proc_name; inconsistent_subclass_type} -> (
-      let base_method_descr = Typ.Procname.to_simplified_string ~withclass:true base_proc_name in
-      let overridden_method_descr =
-        Typ.Procname.to_simplified_string ~withclass:true overridden_proc_name
-      in
-      match inconsistent_subclass_type with
-      | InconsistentReturn ->
-          Format.asprintf "Method %a is annotated with %a but overrides unannotated method %a."
-            MF.pp_monospaced overridden_method_descr MF.pp_monospaced nullable_annotation
-            MF.pp_monospaced base_method_descr
-      | InconsistentParam {param_description; param_position} ->
-          let translate_position = function
-            | 1 ->
-                "First"
-            | 2 ->
-                "Second"
-            | 3 ->
-                "Third"
-            | n ->
-                string_of_int n ^ "th"
-          in
-          Format.asprintf
-            "%s parameter %a of method %a is not %a but is declared %ain the parent class method \
-             %a."
-            (translate_position param_position)
-            MF.pp_monospaced param_description MF.pp_monospaced overridden_method_descr
-            MF.pp_monospaced nullable_annotation MF.pp_monospaced nullable_annotation
-            MF.pp_monospaced base_method_descr )
+      AssignmentRule.violation_description assignment_violation assignment_type ~rhs_origin_descr
+  | Nullable_dereference
+      { dereference_violation
+      ; nullable_object_descr
+      ; dereference_type
+      ; origin_descr= origin_descr, _, _ } ->
+      DereferenceRule.violation_description dereference_violation dereference_type
+        ~nullable_object_descr ~origin_descr
+  | Inconsistent_subclass
+      {inheritance_violation; violation_type; base_proc_name; overridden_proc_name} ->
+      InheritanceRule.violation_description inheritance_violation violation_type ~base_proc_name
+        ~overridden_proc_name
 
 
 (** Report an error right now. *)
diff --git a/infer/src/nullsafe/typeErr.mli b/infer/src/nullsafe/typeErr.mli
index eb3a4a93f..74f7dd70c 100644
--- a/infer/src/nullsafe/typeErr.mli
+++ b/infer/src/nullsafe/typeErr.mli
@@ -38,41 +38,25 @@ type origin_descr = string * Location.t option * AnnotatedSignature.t option
 type err_instance =
   | Condition_redundant of (bool * string option)
   | Inconsistent_subclass of
-      { base_proc_name: Typ.Procname.t
-      ; overridden_proc_name: Typ.Procname.t
-      ; inconsistent_subclass_type: inconsistent_subclass_type }
+      { inheritance_violation: InheritanceRule.violation
+      ; violation_type: InheritanceRule.violation_type
+      ; base_proc_name: Typ.Procname.t
+      ; overridden_proc_name: Typ.Procname.t }
   | Field_not_initialized of Typ.Fieldname.t * Typ.Procname.t
-  | Over_annotation of over_annotation_type
+  | Over_annotation of
+      { over_annotated_violation: OverAnnotatedRule.violation
+      ; violation_type: OverAnnotatedRule.violation_type }
   | Nullable_dereference of
-      { nullable_object_descr: string option
-      ; dereference_type: dereference_type
+      { dereference_violation: DereferenceRule.violation
+      ; dereference_type: DereferenceRule.dereference_type
+      ; nullable_object_descr: string option
       ; origin_descr: origin_descr }
-  | Bad_assignment of {rhs_origin_descr: origin_descr; assignment_type: assignment_type}
+  | Bad_assignment of
+      { assignment_violation: AssignmentRule.violation
+      ; assignment_type: AssignmentRule.assignment_type
+      ; rhs_origin_descr: origin_descr }
 [@@deriving compare]
 
-and inconsistent_subclass_type =
-  | InconsistentParam of {param_description: string; param_position: int}
-  | InconsistentReturn
-
-and over_annotation_type =
-  | FieldOverAnnotedAsNullable of Typ.Fieldname.t
-  | ReturnOverAnnotatedAsNullable of Typ.Procname.t
-      (** Return value of a method can be made non-nullable *)
-
-and assignment_type =
-  | PassingParamToAFunction of
-      { param_description: string
-      ; param_position: int
-      ; function_procname: Typ.Procname.t }
-  | AssigningToAField of Typ.Fieldname.t
-  | ReturningFromAFunction of Typ.Procname.t
-
-and dereference_type =
-  | MethodCall of Typ.Procname.t  (** nullable_object.some_method() *)
-  | AccessToField of Typ.Fieldname.t  (** nullable_object.some_field *)
-  | AccessByIndex of {index_desc: string}  (** nullable_array[some_index] *)
-  | ArrayLengthAccess  (** nullable_array.length *)
-
 val node_reset_forall : Procdesc.Node.t -> unit
 
 type st_report_error =