diff --git a/ocaml/testsuite/tests/typing-layouts-float64/unboxed_floats.ml b/ocaml/testsuite/tests/typing-layouts-float64/unboxed_floats.ml index 60c9e6ad699..68613007b9e 100644 --- a/ocaml/testsuite/tests/typing-layouts-float64/unboxed_floats.ml +++ b/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 diff --git a/ocaml/testsuite/tests/typing-layouts-float64/unboxed_floats_disabled.compilers.reference b/ocaml/testsuite/tests/typing-layouts-float64/unboxed_floats_disabled.compilers.reference index 84ee261f67e..3bc97d7449d 100644 --- a/ocaml/testsuite/tests/typing-layouts-float64/unboxed_floats_disabled.compilers.reference +++ b/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 diff --git a/ocaml/testsuite/tests/typing-layouts/erasable_annot.ml b/ocaml/testsuite/tests/typing-layouts/erasable_annot.ml new file mode 100644 index 00000000000..a621fa534f1 --- /dev/null +++ b/ocaml/testsuite/tests/typing-layouts/erasable_annot.ml @@ -0,0 +1,265 @@ +(* TEST + * expect + flags = "-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. +|}];; + +(* Annotations here do nothing and should be accepted *) +module type S = sig + val f : (int as (_ : immediate)) -> (int as (_ : immediate64)) +end + +[%%expect {| +module type S = sig val f : int -> int end +|}];; + + +(* Annotation would affect ['a] and should be rejected *) +module type S = sig + type 'b id = 'b + val f : ('a id as (_ : immediate)) -> 'a +end + +[%%expect {| +Line 3, characters 2-42: +3 | val f : ('a id as (_ : immediate)) -> 'a + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: Usage of layout immediate/immediate64 in f can't be erased. + This error is produced due to the use of -only-erasable-extensions. +|}];; + +(* 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 +|}];; diff --git a/ocaml/typing/ctype.ml b/ocaml/typing/ctype.ml index a7f17c490ee..89ff65b8241 100644 --- a/ocaml/typing/ctype.ml +++ b/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; diff --git a/ocaml/typing/ctype.mli b/ocaml/typing/ctype.mli index bc296f2fae6..458c10a014e 100644 --- a/ocaml/typing/ctype.mli +++ b/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 things: + + 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. *) diff --git a/ocaml/typing/jkind.ml b/ocaml/typing/jkind.ml index fe80cac3889..4ff7864d57c 100644 --- a/ocaml/typing/jkind.ml +++ b/ocaml/typing/jkind.ml @@ -704,6 +704,7 @@ type immediate64_creation_reason = | Local_mode_cross_check | Gc_ignorable_check | Separability_check + | Erasability_check type void_creation_reason = | @@ -1149,6 +1150,8 @@ end = struct fprintf ppf "the check to see whether a value can be ignored by GC" | Separability_check -> fprintf ppf "the check that a type is definitely not `float`" + | Erasability_check -> + fprintf ppf "the check that a type is compatible with upstream" let format_value_creation_reason ppf : value_creation_reason -> _ = function | Class_let_binding -> @@ -1546,6 +1549,7 @@ module Debug_printers = struct | Local_mode_cross_check -> fprintf ppf "Local_mode_cross_check" | Gc_ignorable_check -> fprintf ppf "Gc_ignorable_check" | Separability_check -> fprintf ppf "Separability_check" + | Erasability_check -> fprintf ppf "Erasability_check" let value_creation_reason ppf : value_creation_reason -> _ = function | Class_let_binding -> fprintf ppf "Class_let_binding" diff --git a/ocaml/typing/jkind.mli b/ocaml/typing/jkind.mli index 5cb196f58b3..8ecd21332dd 100644 --- a/ocaml/typing/jkind.mli +++ b/ocaml/typing/jkind.mli @@ -266,6 +266,8 @@ type immediate64_creation_reason = | Gc_ignorable_check (* CR layouts v2.8: Remove Gc_ignorable_check after the check uses modal kinds *) | Separability_check + | Erasability_check +(* CR layouts v2.8: Remove after the check uses modal kinds *) (* CR layouts v5: make new void_creation_reasons *) type void_creation_reason = | diff --git a/ocaml/typing/typecore.ml b/ocaml/typing/typecore.ml index 70a2c0b2f89..19c6132738a 100644 --- a/ocaml/typing/typecore.ml +++ b/ocaml/typing/typecore.ml @@ -8401,8 +8401,8 @@ and type_let ?check ?check_strict ?(force_toplevel = false) (* update pattern variable jkind reasons *) List.iter (fun pv -> - let reason = Jkind.Generalized (Some pv.pv_id, pv.pv_loc) in - Ctype.update_generalized_ty_jkind_reason pv.pv_type reason) + Ctype.check_and_update_generalized_ty_jkind + ~name:pv.pv_id ~loc:pv.pv_loc pv.pv_type) pvs; List.iter2 (fun (_, _, expected_ty) (exp, vars) -> @@ -8430,8 +8430,8 @@ and type_let ?check ?check_strict ?(force_toplevel = false) Tpat_var (id, _, _, _) -> Some id | Tpat_alias(_, id, _, _, _) -> Some id | _ -> None in - let reason = Jkind.Generalized (pat_name, exp.exp_loc) in - Ctype.update_generalized_ty_jkind_reason exp.exp_type reason + Ctype.check_and_update_generalized_ty_jkind + ?name:pat_name ~loc:exp.exp_loc exp.exp_type in List.iter2 update_exp_jkind mode_pat_typ_list exp_list; end diff --git a/ocaml/typing/typedecl.ml b/ocaml/typing/typedecl.ml index 752e1d91f4e..31f0f175ec0 100644 --- a/ocaml/typing/typedecl.ml +++ b/ocaml/typing/typedecl.ml @@ -1231,11 +1231,14 @@ let update_decl_jkind env dpath decl = let update_decls_jkind_reason decls = List.map (fun (id, decl) -> - let reason = Jkind.(Generalized (Some id, decl.type_loc)) in - let update_generalized ty = Ctype.update_generalized_ty_jkind_reason ty reason in + let update_generalized = + Ctype.check_and_update_generalized_ty_jkind + ~name:id ~loc:decl.type_loc + in List.iter update_generalized decl.type_params; Btype.iter_type_expr_kind update_generalized decl.type_kind; Option.iter update_generalized decl.type_manifest; + let reason = Jkind.(Generalized (Some id, decl.type_loc)) in let new_decl = {decl with type_jkind = Jkind.(update_reason decl.type_jkind reason)} in (id, new_decl) @@ -2361,8 +2364,7 @@ let transl_value_decl env loc valdecl = Env.enter_value valdecl.pval_name.txt v env ~check:(fun s -> Warnings.Unused_value_declaration s) in - let reason = Jkind.Generalized (Some id, loc) in - Ctype.update_generalized_ty_jkind_reason ty reason; + Ctype.check_and_update_generalized_ty_jkind ~name:id ~loc ty; let desc = { val_id = id; diff --git a/ocaml/utils/language_extension.ml b/ocaml/utils/language_extension.ml index 1fcaad74fa0..521a36ba671 100644 --- a/ocaml/utils/language_extension.ml +++ b/ocaml/utils/language_extension.ml @@ -123,6 +123,8 @@ module Universe : sig | Any val set : t -> bool + + val is : t -> bool end = struct (** Which extensions can be enabled? *) type t = @@ -180,6 +182,8 @@ end = struct (); universe := new_universe; cmp <> 0 + + let is u = compare u !universe = 0 end (*****************************************) @@ -279,6 +283,8 @@ let restrict_to_erasable_extensions () = (fun (Pair (extn, _)) -> Universe.is_allowed extn) !extensions +let erasable_extensions_only () = Universe.is Only_erasable + let disallow_extensions () = ignore (Universe.set No_extensions : bool); disable_all () diff --git a/ocaml/utils/language_extension.mli b/ocaml/utils/language_extension.mli index 25de5575587..249c68e47a0 100644 --- a/ocaml/utils/language_extension.mli +++ b/ocaml/utils/language_extension.mli @@ -128,6 +128,10 @@ val restrict_to_erasable_extensions : unit -> unit [false].*) val disallow_extensions : unit -> unit +(** Check if the allowable extensions are restricted to only those that are + "erasable". This is true when [restrict_to_erasable_extensions] was called. *) +val erasable_extensions_only : unit -> bool + (**/**) (** Special functionality that can only be used in "pprintast.ml" *) diff --git a/ocaml/utils/language_extension_kernel.ml b/ocaml/utils/language_extension_kernel.ml index f1882df80cd..666a4250bb6 100644 --- a/ocaml/utils/language_extension_kernel.ml +++ b/ocaml/utils/language_extension_kernel.ml @@ -93,10 +93,9 @@ let of_string extn_name : Exist.t option = *) let is_erasable : type a. a t -> bool = function | Local - | Unique -> + | Unique + | Layouts -> true - (* CR layouts v2.6: Layouts should be erasable *) - | Layouts | Comprehensions | Include_functor | Polymorphic_parameters