flambda-backend: Fix check_and_update_generalized_ty_jkind (#2615)

* Add `Warning` to jkind history

* Reword `check_and_update_generalized_ty_jkind`

* Remove duplicate warnings

* Give up on soundness

* Reimplement `has_warned`

---------

Co-authored-by: Diana Kalinichenko <[email protected]>

Author: dkalinichenko-js

testsuite/tests/typing-layouts/erasable_annot.ml

@@ -67,7 +67,6 @@ can't be erased for compatibility with upstream OCaml.
 module type S = sig type _ g = MkG : ('a : immediate). 'a g end
 |}];;
 
-(* CR layouts: only show the warning once; same for tests below *)
 let f (type a : immediate): a -> a = fun x -> x
 [%%expect {|
 Line 1, characters 4-5:
@@ -76,12 +75,6 @@ Line 1, characters 4-5:
 Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
 can't be erased for compatibility with upstream OCaml.
 
-Line 1, characters 6-47:
-1 | let f (type a : immediate): a -> a = fun x -> x
-          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
-can't be erased for compatibility with upstream OCaml.
-
 val f : ('a : immediate). 'a -> 'a = <fun>
 |}];;
 
@@ -93,12 +86,6 @@ Line 1, characters 4-5:
 Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
 can't be erased for compatibility with upstream OCaml.
 
-Line 1, characters 6-31:
-1 | let f x = (x : (_ : immediate))
-          ^^^^^^^^^^^^^^^^^^^^^^^^^
-Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
-can't be erased for compatibility with upstream OCaml.
-
 val f : ('a : immediate). 'a -> 'a = <fun>
 |}];;
 
@@ -110,12 +97,6 @@ Line 1, characters 4-5:
 Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
 can't be erased for compatibility with upstream OCaml.
 
-Line 1, characters 6-63:
-1 | let f v: ((_ : immediate)[@error_message "Custom message"]) = v
-          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
-can't be erased for compatibility with upstream OCaml.
-
 val f : ('a : immediate). 'a -> 'a = <fun>
 |}];;
 
@@ -182,12 +163,6 @@ Line 1, characters 4-5:
 Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
 can't be erased for compatibility with upstream OCaml.
 
-Line 1, characters 6-49:
-1 | let f (type a : immediate64): a -> a = fun x -> x
-          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
-can't be erased for compatibility with upstream OCaml.
-
 val f : ('a : immediate64). 'a -> 'a = <fun>
 |}];;
 
@@ -199,12 +174,6 @@ Line 1, characters 4-5:
 Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
 can't be erased for compatibility with upstream OCaml.
 
-Line 1, characters 6-33:
-1 | let f x = (x : (_ : immediate64))
-          ^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
-can't be erased for compatibility with upstream OCaml.
-
 val f : ('a : immediate64). 'a -> 'a = <fun>
 |}];;
 
@@ -216,12 +185,6 @@ Line 1, characters 4-5:
 Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
 can't be erased for compatibility with upstream OCaml.
 
-Line 1, characters 6-65:
-1 | let f v: ((_ : immediate64)[@error_message "Custom message"]) = v
-          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
-can't be erased for compatibility with upstream OCaml.
-
 val f : ('a : immediate64). 'a -> 'a = <fun>
 |}];;
 
@@ -289,15 +252,13 @@ Line 5, characters 4-5:
 Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
 can't be erased for compatibility with upstream OCaml.
 
-Line 5, characters 6-50:
-5 | let f (module _ : S with type t = 'a) (x : 'a) = x
-          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in f
-can't be erased for compatibility with upstream OCaml.
-
 val f : ('a : immediate). (module S with type t = 'a) -> 'a -> 'a = <fun>
 |}]
 
+(* CR layouts: this example should raise a warning, but it does not.
+   It's quite complicated, and missing it only means that this error
+   will be caught by the upstream compiler later. We have decided that
+   fixing this is not worth the effort. *)
 module type S = sig
   type t [@@immediate]
 end
@@ -312,7 +273,10 @@ module type S = sig type t : immediate end
 val x : int = 15
 |}]
 
-(* CR layouts: this should raise a warning *)
+(* CR layouts: this example should raise a warning, but it does not.
+   It's quite complicated, and missing it only means that this error
+   will be caught by the upstream compiler later. We have decided that
+   fixing this is not worth the effort. *)
 let y =
   ignore (fun (type a : immediate) (x : a) ->
     let module _ : S = struct
@@ -580,12 +544,6 @@ Line 1, characters 21-26:
 Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in fails
 can't be erased for compatibility with upstream OCaml.
 
-Line 1, characters 27-68:
-1 | let[@warning "-187"] fails (type a : immediate): a -> a = fun x -> x
-                               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in fails
-can't be erased for compatibility with upstream OCaml.
-
 val fails : ('a : immediate). 'a -> 'a = <fun>
 |}]
 
@@ -603,9 +561,7 @@ can't be erased for compatibility with upstream OCaml.
 module type S1 = sig type ('a : immediate) fails = int end
 |}]
 
-(* Disabling the warning just in the signature isn't sufficient.
-
-   The check here is also ran twice for some reason. *)
+(* Disabling the warning just in the signature isn't sufficient. *)
 module M6 : sig
   [@@@warning "-187"]
   type ('a : immediate) t = 'a * 'a
@@ -619,12 +575,6 @@ Line 5, characters 2-35:
 Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in t
 can't be erased for compatibility with upstream OCaml.
 
-Line 5, characters 2-35:
-5 |   type ('a : immediate) t = 'a * 'a
-      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Warning 187 [incompatible-with-upstream]: Usage of layout immediate/immediate64 in t
-can't be erased for compatibility with upstream OCaml.
-
 module M6 : sig type ('a : immediate) t = 'a * 'a end
 |}]
 

typing/ctype.ml

@@ -2314,32 +2314,34 @@ let check_and_update_generalized_ty_jkind ?name ~loc ty =
                | _ -> false)
     in
     if Language_extension.erasable_extensions_only ()
-      && is_immediate jkind
+      && is_immediate jkind && not (Jkind.has_warned jkind)
     then
       let id =
         match name with
         | Some id -> Ident.name id
         | None -> "<unknown>"
       in
       Location.prerr_warning loc (Warnings.Incompatible_with_upstream
-        (Warnings.Immediate_erasure id))
-    else ()
+        (Warnings.Immediate_erasure id));
+      Jkind.with_warning jkind
+    else jkind
+  in
+  let generalization_check level jkind =
+    if level = generic_level then
+      Jkind.(update_reason jkind (Generalized (name, loc)))
+    else jkind
   in
   let rec inner ty =
     let level = get_level ty in
-    if level = generic_level && try_mark_node ty then begin
+    if try_mark_node ty then begin
       begin match get_desc ty with
       | Tvar ({ jkind; _ } as r) ->
-        immediacy_check jkind;
-        let new_jkind =
-          Jkind.(update_reason jkind (Generalized (name, loc)))
-        in
+        let new_jkind = immediacy_check jkind in
+        let new_jkind = generalization_check level new_jkind in
         set_type_desc ty (Tvar {r with jkind = new_jkind})
       | Tunivar ({ jkind; _ } as r) ->
-        immediacy_check jkind;
-        let new_jkind =
-          Jkind.(update_reason jkind (Generalized (name, loc)))
-        in
+        let new_jkind = immediacy_check jkind in
+        let new_jkind = generalization_check level new_jkind in
         set_type_desc ty (Tunivar {r with jkind = new_jkind})
       | _ -> ()
       end;

typing/jkind.ml

@@ -526,17 +526,22 @@ include Jkind_intf.History
 
 type t = type_expr Jkind_types.t
 
-let fresh_jkind jkind ~why = { jkind; history = Creation why }
+let fresh_jkind jkind ~why =
+  { jkind; history = Creation why; has_warned = false }
 
 (******************************)
 (* constants *)
 
 let any_dummy_jkind =
-  { jkind = Jkind_desc.max; history = Creation (Any_creation Dummy_jkind) }
+  { jkind = Jkind_desc.max;
+    history = Creation (Any_creation Dummy_jkind);
+    has_warned = false
+  }
 
 let value_v1_safety_check =
   { jkind = Jkind_desc.value;
-    history = Creation (Value_creation V1_safety_check)
+    history = Creation (Value_creation V1_safety_check);
+    has_warned = false
   }
 
 (* CR layouts: Should we be doing more memoization here? *)
@@ -761,6 +766,10 @@ let has_imported_history t =
 
 let update_reason t reason = { t with history = Creation reason }
 
+let with_warning t = { t with has_warned = true }
+
+let has_warned t = t.has_warned
+
 let printtyp_path = ref (fun _ _ -> assert false)
 
 let set_printtyp_path f = printtyp_path := f
@@ -1225,8 +1234,9 @@ end
 (******************************)
 (* relations *)
 
-let equate_or_equal ~allow_mutation { jkind = jkind1; history = _ }
-    { jkind = jkind2; history = _ } =
+let equate_or_equal ~allow_mutation
+    { jkind = jkind1; history = _; has_warned = _ }
+    { jkind = jkind2; history = _; has_warned = _ } =
   Jkind_desc.equate_or_equal ~allow_mutation jkind1 jkind2
 
 (* CR layouts v2.8: Switch this back to ~allow_mutation:false *)
@@ -1272,7 +1282,12 @@ let combine_histories reason lhs rhs =
 let intersection ~reason t1 t2 =
   match Jkind_desc.intersection t1.jkind t2.jkind with
   | None -> Error (Violation.of_ (No_intersection (t1, t2)))
-  | Some jkind -> Ok { jkind; history = combine_histories reason t1 t2 }
+  | Some jkind ->
+    Ok
+      { jkind;
+        history = combine_histories reason t1 t2;
+        has_warned = t1.has_warned || t2.has_warned
+      }
 
 (* this is hammered on; it must be fast! *)
 let check_sub sub super = Jkind_desc.sub sub.jkind super.jkind
@@ -1470,7 +1485,7 @@ module Debug_printers = struct
         lhs_history Jkind_desc.Debug_printers.t rhs_jkind history rhs_history
     | Creation c -> fprintf ppf "Creation (%a)" creation_reason c
 
-  let t ppf ({ jkind; history = h } : t) : unit =
+  let t ppf ({ jkind; history = h; has_warned = _ } : t) : unit =
     fprintf ppf "@[<v 2>{ jkind = %a@,; history = %a }@]"
       Jkind_desc.Debug_printers.t jkind history h
 end

typing/jkind.mli

@@ -304,6 +304,12 @@ val has_imported_history : t -> bool
 
 val update_reason : t -> creation_reason -> t
 
+(* Mark the jkind as having produced a compiler warning. *)
+val with_warning : t -> t
+
+(* Whether this jkind has produced a compiler warning. *)
+val has_warned : t -> bool
+
 (******************************)
 (* relations *)
 

typing/jkind_types.ml

@@ -350,7 +350,8 @@ type 'type_expr history =
 
 type 'type_expr t =
   { jkind : 'type_expr Jkind_desc.t;
-    history : 'type_expr history
+    history : 'type_expr history;
+    has_warned : bool
   }
 
 type const =

typing/jkind_types.mli

@@ -129,7 +129,8 @@ type 'type_expr history =
 
 type 'type_expr t =
   { jkind : 'type_expr Jkind_desc.t;
-    history : 'type_expr history
+    history : 'type_expr history;
+    has_warned : bool
   }
 
 type annotation = const * Jane_syntax.Jkind.annotation