Mark layouts extension as erasable and limit the use of immediate/immediate64

ocaml/testsuite/tests/typing-layouts-float64/unboxed_floats.ml

@@ -11,18 +11,16 @@
      flags = "-extension layouts_beta"
    ** bytecode
      flags = "-extension layouts_beta"
+   ** native
+     flags = "-only-erasable-extensions"
+   ** bytecode
+     flags = "-only-erasable-extensions"
    ** setup-ocamlc.byte-build-env
      ocamlc_byte_exit_status = "2"
    *** ocamlc.byte
      flags = "-disable-all-extensions"
      compiler_reference = "${test_source_directory}/unboxed_floats_disabled.compilers.reference"
    **** check-ocamlc.byte-output
-   ** setup-ocamlc.byte-build-env
-     ocamlc_byte_exit_status = "2"
-   *** ocamlc.byte
-     flags = "-only-erasable-extensions"
-     compiler_reference = "${test_source_directory}/unboxed_floats_disabled.compilers.reference"
-   **** check-ocamlc.byte-output
 *)
 
 (* CR layouts v2.6: Layouts should be erasable and we can remove the

ocaml/testsuite/tests/typing-layouts-float64/unboxed_floats_disabled.compilers.reference

@@ -1,4 +1,4 @@
-File "unboxed_floats.ml", line 65, characters 11-16:
-65 |   let pi = #3.14 in
+File "unboxed_floats.ml", line 63, characters 11-16:
+63 |   let pi = #3.14 in
                 ^^^^^
 Error: This construct requires the stable version of the extension "layouts", which is disabled and cannot be used

ocaml/testsuite/tests/typing-layouts/erasable_annot.ml

@@ -0,0 +1,241 @@
+(* TEST
+   * expect
+   flags = "-extension layouts -only-erasable-extensions"
+*)
+
+(* Upstream compatible usages of immediate/immediate64 are allowed *)
+module type S1 = sig
+  type t_immediate : immediate
+  type t_immediate64 : immediate64
+end;;
+[%%expect {|
+module type S1 =
+  sig type t_immediate : immediate type t_immediate64 : immediate64 end
+|}];;
+
+(* Same is not true when constraining type vars *)
+(* immediate *)
+module type S = sig
+  val f_immediate : ('a : immediate). 'a -> 'a -> 'a
+end;;
+[%%expect {|
+Line 2, characters 2-52:
+2 |   val f_immediate : ('a : immediate). 'a -> 'a -> 'a
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: Usage of layout immediate/immediate64 in f_immediate can't be erased.
+       This error is produced due to the use of -only-erasable-extensions.
+|}];;
+
+module type S = sig
+  val f_immediate : ('a : immediate) -> 'a -> 'a
+end;;
+[%%expect {|
+Line 2, characters 2-48:
+2 |   val f_immediate : ('a : immediate) -> 'a -> 'a
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: Usage of layout immediate/immediate64 in f_immediate can't be erased.
+       This error is produced due to the use of -only-erasable-extensions.
+|}];;
+
+module type S = sig
+  type ('a : immediate) t
+end;;
+[%%expect {|
+Line 2, characters 2-25:
+2 |   type ('a : immediate) t
+      ^^^^^^^^^^^^^^^^^^^^^^^
+Error: Usage of layout immediate/immediate64 in t can't be erased.
+       This error is produced due to the use of -only-erasable-extensions.
+|}];;
+
+module type S = sig
+  type _ g = | MkG : ('a : immediate). 'a g
+end;;
+[%%expect {|
+Line 2, characters 2-43:
+2 |   type _ g = | MkG : ('a : immediate). 'a g
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: Usage of layout immediate/immediate64 in g can't be erased.
+       This error is produced due to the use of -only-erasable-extensions.
+|}];;
+
+let f (type a : immediate): a -> a = fun x -> x
+[%%expect {|
+Line 1, characters 4-5:
+1 | let f (type a : immediate): a -> a = fun x -> x
+        ^
+Error: Usage of layout immediate/immediate64 in f can't be erased.
+       This error is produced due to the use of -only-erasable-extensions.
+|}];;
+
+let f x = (x : (_ : immediate))
+[%%expect {|
+Line 1, characters 4-5:
+1 | let f x = (x : (_ : immediate))
+        ^
+Error: Usage of layout immediate/immediate64 in f can't be erased.
+       This error is produced due to the use of -only-erasable-extensions.
+|}];;
+
+let f v: ((_ : immediate)[@error_message "Custom message"]) = v
+[%%expect {|
+Line 1, characters 4-5:
+1 | let f v: ((_ : immediate)[@error_message "Custom message"]) = v
+        ^
+Error: Usage of layout immediate/immediate64 in f can't be erased.
+       This error is produced due to the use of -only-erasable-extensions.
+|}];;
+
+(* immediate64 *)
+module type S = sig
+  val f_immediate64 : ('a : immediate64). 'a -> 'a -> 'a
+end;;
+[%%expect {|
+Line 2, characters 2-56:
+2 |   val f_immediate64 : ('a : immediate64). 'a -> 'a -> 'a
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: Usage of layout immediate/immediate64 in f_immediate64 can't be erased.
+       This error is produced due to the use of -only-erasable-extensions.
+|}];;
+
+module type S = sig
+  val f_immediate64 : ('a : immediate64) -> 'a -> 'a
+end;;
+[%%expect {|
+Line 2, characters 2-52:
+2 |   val f_immediate64 : ('a : immediate64) -> 'a -> 'a
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: Usage of layout immediate/immediate64 in f_immediate64 can't be erased.
+       This error is produced due to the use of -only-erasable-extensions.
+|}];;
+
+module type S = sig
+  type ('a : immediate64) t
+end;;
+[%%expect {|
+Line 2, characters 2-27:
+2 |   type ('a : immediate64) t
+      ^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: Usage of layout immediate/immediate64 in t can't be erased.
+       This error is produced due to the use of -only-erasable-extensions.
+|}];;
+
+module type S = sig
+  type _ g = | MkG : ('a : immediate64). 'a g
+end;;
+[%%expect {|
+Line 2, characters 2-45:
+2 |   type _ g = | MkG : ('a : immediate64). 'a g
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: Usage of layout immediate/immediate64 in g can't be erased.
+       This error is produced due to the use of -only-erasable-extensions.
+|}];;
+
+let f (type a : immediate64): a -> a = fun x -> x
+[%%expect {|
+Line 1, characters 4-5:
+1 | let f (type a : immediate64): a -> a = fun x -> x
+        ^
+Error: Usage of layout immediate/immediate64 in f can't be erased.
+       This error is produced due to the use of -only-erasable-extensions.
+|}];;
+
+let f x = (x : (_ : immediate64))
+[%%expect {|
+Line 1, characters 4-5:
+1 | let f x = (x : (_ : immediate64))
+        ^
+Error: Usage of layout immediate/immediate64 in f can't be erased.
+       This error is produced due to the use of -only-erasable-extensions.
+|}];;
+
+let f v: ((_ : immediate64)[@error_message "Custom message"]) = v
+[%%expect {|
+Line 1, characters 4-5:
+1 | let f v: ((_ : immediate64)[@error_message "Custom message"]) = v
+        ^
+Error: Usage of layout immediate/immediate64 in f can't be erased.
+       This error is produced due to the use of -only-erasable-extensions.
+|}];;
+
+(* CR layouts: This message should change after we fix the package hack.
+   But it should still be an error under [-only-erasable-extensions]. *)
+module type S = sig
+  type t[@@immediate64]
+end
+
+module type K = sig
+  val f : 'a -> (module S with type t = 'a) -> 'a
+end
+
+[%%expect {|
+module type S = sig type t : immediate64 end
+Line 6, characters 16-43:
+6 |   val f : 'a -> (module S with type t = 'a) -> 'a
+                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: In this `with' constraint, the new definition of t
+       does not match its original definition in the constrained signature:
+       Type declarations do not match:
+         type t
+       is not included in
+         type t : immediate64
+       The layout of the first is value, because
+         it's a type declaration in a first-class module.
+       But the layout of the first must be a sublayout of immediate64, because
+         of the definition of t at line 2, characters 2-23.
+|}];;
+
+(* Other annotations are not effected by this flag *)
+module type S = sig
+  val f_any : ('a : any). ('a : any) -> (('a : any)[@error_message ""])
+  type ('a : any) t_any : any
+  type (_ : any) t_any_ = MkG : ('a : any). 'a t_any_
+  val f_bits64 : ('a : bits64). ('a : bits64) -> (('a : bits64)[@error_message ""])
+  type ('a : bits64) t_bits64 : bits64
+  type (_ : bits64) t_bits64_ = MkG : ('a : bits64). 'a t_bits64_
+  val f_bits32 : ('a : bits32). ('a : bits32) -> (('a : bits32)[@error_message ""])
+  type ('a : bits32) t_bits32 : bits32
+  type (_ : bits32) t_bits32_ = MkG : ('a : bits32). 'a t_bits32_
+  val f_float64 : ('a : float64). ('a : float64) -> (('a : float64)[@error_message ""])
+  type ('a : float64) t_float64 : float64
+  type (_ : float64) t_float64_ = MkG : ('a : float64). 'a t_float64_
+  val f_word : ('a : word). ('a : word) -> (('a : word)[@error_message ""])
+  type ('a : word) t_word : word
+  type (_ : word) t_word_ = MkG : ('a : word). 'a t_word_
+end
+
+module M = struct
+  let f_any (type a : any) = ()
+  let f_bits64 (type a : bits64) = ()
+  let f_bits32 (type a : bits32) = ()
+  let f_float64 (type a : float64) = ()
+  let f_word (type a : word) = ()
+end
+[%%expect {|
+module type S =
+  sig
+    val f_any : ('a : any). 'a -> 'a
+    type ('a : any) t_any : any
+    type (_ : any) t_any_ = MkG : ('a : any). 'a t_any_
+    val f_bits64 : ('a : bits64). 'a -> 'a
+    type ('a : bits64) t_bits64 : bits64
+    type (_ : bits64) t_bits64_ = MkG : ('a : bits64). 'a t_bits64_
+    val f_bits32 : ('a : bits32). 'a -> 'a
+    type ('a : bits32) t_bits32 : bits32
+    type (_ : bits32) t_bits32_ = MkG : ('a : bits32). 'a t_bits32_
+    val f_float64 : ('a : float64). 'a -> 'a
+    type ('a : float64) t_float64 : float64
+    type (_ : float64) t_float64_ = MkG : ('a : float64). 'a t_float64_
+    val f_word : ('a : word). 'a -> 'a
+    type ('a : word) t_word : word
+    type (_ : word) t_word_ = MkG : ('a : word). 'a t_word_
+  end
+module M :
+  sig
+    val f_any : unit
+    val f_bits64 : unit
+    val f_bits32 : unit
+    val f_float64 : unit
+    val f_word : unit
+  end
+|}];;

ocaml/typing/ctype.ml

@@ -2005,7 +2005,7 @@ let rec estimate_type_jkind env ty =
        This notably prevents [constrain_type_jkind] from changing layout
        [any] to a sort or changing the externality once the Tvar gets
        generalized.
-       
+
        This, however, still allows sort variables to get instantiated. *)
     Jkind jkind
   | Tvar { jkind } -> TyVar (jkind, ty)
@@ -2149,16 +2149,56 @@ let unification_jkind_check env ty jkind =
   | Delay_checks r -> r := (ty,jkind) :: !r
   | Skip_checks -> ()
 
-let update_generalized_ty_jkind_reason ty reason =
+exception Incompatible_with_erasability_requirements of
+  Ident.t option * Location.t
+
+let () =
+  Location.register_error_of_exn (function
+  | Incompatible_with_erasability_requirements (id, loc) ->
+    let format_id ppf = function
+      | Some id -> Format.fprintf ppf " in %s" (Ident.name id)
+      | None -> ()
+    in
+    Some (Location.errorf ~loc
+      "@[Usage of layout immediate/immediate64%a can't be erased.@;\
+      This error is produced due to the use of -only-erasable-extensions.@]"
+      format_id id)
+  | _ -> None)
+
+let check_and_update_generalized_ty_jkind ?name ~loc ty =
+  let immediacy_check jkind =
+    let is_immediate jkind =
+      let snap = Btype.snapshot () in
+      let result =
+        Result.is_ok (
+          Jkind.sub
+            jkind
+            (Jkind.immediate64 ~why:Erasability_check))
+      in
+      Btype.backtrack snap;
+      result
+    in
+    if Language_extension.erasable_extensions_only ()
+      && is_immediate jkind
+    then
+      raise (Incompatible_with_erasability_requirements (name, loc))
+    else ()
+  in
   let rec inner ty =
     let level = get_level ty in
     if level = generic_level && try_mark_node ty then begin
       begin match get_desc ty with
       | Tvar ({ jkind; _ } as r) ->
-        let new_jkind = Jkind.(update_reason jkind reason) in
+        immediacy_check jkind;
+        let new_jkind =
+          Jkind.(update_reason jkind (Generalized (name, loc)))
+        in
         set_type_desc ty (Tvar {r with jkind = new_jkind})
       | Tunivar ({ jkind; _ } as r) ->
-        let new_jkind = Jkind.(update_reason jkind reason) in
+        immediacy_check jkind;
+        let new_jkind =
+          Jkind.(update_reason jkind (Generalized (name, loc)))
+        in
         set_type_desc ty (Tunivar {r with jkind = new_jkind})
       | _ -> ()
       end;

ocaml/typing/ctype.mli

@@ -555,7 +555,12 @@ val check_type_jkind :
 val constrain_type_jkind :
   Env.t -> type_expr -> Jkind.t -> (unit, Jkind.Violation.t) result
 
-(* Update the jkind reason of all generalized type vars inside the given [type_expr]
+(* This function should get called after a type is generalized.
+
+   It does two thing:
+
+   1. Update the jkind reason of all generalized type vars inside the
+      given [type_expr]
 
    Consider some code like
 
@@ -575,8 +580,26 @@ val constrain_type_jkind :
    is more well suited for discovering properties of well-typed definitions. Instead,
    once a definition is done being type-checked -- that is, once it is generalized --
    we update the histories of all of its types' jkinds to just refer to the definition
-   itself. *)
-val update_generalized_ty_jkind_reason : type_expr -> Jkind.creation_reason -> unit
+   itself.
+
+   2. Performs an upstream-compatibility check around immediacy if
+      [Language_extension.erasable_extensions_only ()] is [true].
+
+   The check makes sure no generalized type variable can have jkind
+   [immediate] or [immediate64]. An exception would be raised when
+   the check fails.
+
+   This prevents code such as:
+
+   {|
+     let f (x : (_ : immediate)) = x;;
+   |}
+
+   which doesn't have an equivalent representation upstream.
+
+   *)
+val check_and_update_generalized_ty_jkind :
+  ?name:Ident.t -> loc:Location.t -> type_expr -> unit
 
 (* False if running in principal mode and the type is not principal.
    True otherwise. *)