diff --git a/.depend b/.depend
index df9b02bd5c9..1cbf1481012 100644
--- a/.depend
+++ b/.depend
@@ -972,6 +972,7 @@ typing/includeclass.cmi : \
     typing/env.cmi \
     typing/ctype.cmi
 typing/includecore.cmo : \
+    utils/zero_alloc_utils.cmi \
     typing/types.cmi \
     typing/typedtree.cmi \
     typing/printtyp.cmi \
@@ -990,6 +991,7 @@ typing/includecore.cmo : \
     parsing/asttypes.cmi \
     typing/includecore.cmi
 typing/includecore.cmx : \
+    utils/zero_alloc_utils.cmx \
     typing/types.cmx \
     typing/typedtree.cmx \
     typing/printtyp.cmx \
@@ -1948,6 +1950,7 @@ typing/typedecl.cmi : \
     typing/ident.cmi \
     typing/errortrace.cmi \
     typing/env.cmi \
+    parsing/builtin_attributes.cmi \
     parsing/asttypes.cmi
 typing/typedecl_properties.cmo : \
     typing/types.cmi \
@@ -2254,6 +2257,7 @@ typing/types.cmo : \
     typing/jkind.cmi \
     typing/ident.cmi \
     utils/config.cmi \
+    parsing/builtin_attributes.cmi \
     parsing/asttypes.cmi \
     typing/types.cmi
 typing/types.cmx : \
@@ -2269,6 +2273,7 @@ typing/types.cmx : \
     typing/jkind.cmx \
     typing/ident.cmx \
     utils/config.cmx \
+    parsing/builtin_attributes.cmx \
     parsing/asttypes.cmi \
     typing/types.cmi
 typing/types.cmi : \
@@ -2281,6 +2286,7 @@ typing/types.cmi : \
     parsing/location.cmi \
     typing/jkind.cmi \
     typing/ident.cmi \
+    parsing/builtin_attributes.cmi \
     parsing/asttypes.cmi
 typing/typetexp.cmo : \
     typing/types.cmi \
diff --git a/boot/ocamlc b/boot/ocamlc
index 5d8eab1c5df..cb379c41dde 100755
Binary files a/boot/ocamlc and b/boot/ocamlc differ
diff --git a/lambda/lambda.ml b/lambda/lambda.ml
index 1f7a5bbc5f4..10b6d52612c 100644
--- a/lambda/lambda.ml
+++ b/lambda/lambda.ml
@@ -641,12 +641,14 @@ type check_attribute = Builtin_attributes.check_attribute =
   | Check of { property: property;
                strict: bool;
                opt: bool;
+               arity: int;
                loc: Location.t;
              }
   | Assume of { property: property;
                 strict: bool;
-                loc: Location.t;
                 never_returns_normally: bool;
+                arity: int;
+                loc: Location.t;
               }
 
 type loop_attribute =
diff --git a/lambda/lambda.mli b/lambda/lambda.mli
index 19877718bf5..2fbdc50b8d8 100644
--- a/lambda/lambda.mli
+++ b/lambda/lambda.mli
@@ -515,12 +515,14 @@ type check_attribute = Builtin_attributes.check_attribute =
                   exceptional returns or divering loops are ignored).
                   This definition may not be applicable to new properties. *)
                opt: bool;
+               arity: int;
                loc: Location.t;
              }
   | Assume of { property: property;
                 strict: bool;
-                loc: Location.t;
                 never_returns_normally: bool;
+                arity: int;
+                loc: Location.t;
               }
 
 type loop_attribute =
diff --git a/parsing/builtin_attributes.ml b/parsing/builtin_attributes.ml
index 50de8c5b181..621974eb590 100644
--- a/parsing/builtin_attributes.ml
+++ b/parsing/builtin_attributes.ml
@@ -685,12 +685,14 @@ type check_attribute =
   | Check of { property: property;
                strict: bool;
                opt: bool;
+               arity: int;
                loc: Location.t;
              }
   | Assume of { property: property;
                 strict: bool;
-                loc: Location.t;
                 never_returns_normally: bool;
+                arity: int;
+                loc: Location.t;
               }
 
 let is_check_enabled ~opt property =
@@ -751,16 +753,23 @@ let get_id_from_exp =
   | { pexp_desc = Pexp_ident { txt = Longident.Lident id } } -> Result.Ok id
   | _ -> Result.Error ()
 
-let get_ids_from_exp exp =
+let get_id_or_constant_from_exp =
+  let open Parsetree in
+  function
+  | { pexp_desc = Pexp_ident { txt = Longident.Lident id } } -> Result.Ok id
+  | { pexp_desc = Pexp_constant (Pconst_integer (s,None)) } -> Result.Ok s
+  | _ -> Result.Error ()
+
+let get_ids_and_constants_from_exp exp =
   let open Parsetree in
   (match exp with
    | { pexp_desc = Pexp_apply (exp, args) } ->
-     get_id_from_exp exp ::
+     get_id_or_constant_from_exp exp ::
      List.map (function
-       | (Asttypes.Nolabel, arg) -> get_id_from_exp arg
+       | (Asttypes.Nolabel, arg) -> get_id_or_constant_from_exp arg
        | (_, _) -> Result.Error ())
        args
-   | _ -> [get_id_from_exp exp])
+   | _ -> [get_id_or_constant_from_exp exp])
   |> List.fold_left (fun acc r ->
     match acc, r with
     | Result.Ok ids, Ok id -> Result.Ok (id::ids)
@@ -788,52 +797,113 @@ let parse_optional_id_payload txt loc ~empty cases payload =
       | Some r -> Ok r
       | None -> warn ()
 
-let parse_ids_payload txt loc ~default ~empty cases payload =
-  let[@local] warn () =
-    let ( %> ) f g x = g (f x) in
-    let msg =
-      cases
-      |> List.map (fst %> String.concat " " %> Printf.sprintf "'%s'")
-      |> String.concat ", "
-      |> Printf.sprintf "It must be either %s or empty"
-    in
-    Location.prerr_warning loc (Warnings.Attribute_payload (txt, msg));
-    default
+(* Looks for `arity n` in payload. If present, this returns `n` and an updated
+   payload with `arity n` removed. Note it may change the order of the payload,
+   which is fine because we sort it later. *)
+let filter_arity payload =
+  let is_arity s1 s2 =
+    match s1 with
+    | "arity" -> int_of_string_opt s2
+    | _ -> None
   in
-  match get_optional_payload get_ids_from_exp payload with
-  | Error () -> warn ()
-  | Ok None -> empty
-  | Ok (Some ids) ->
-      match List.assoc_opt (List.sort String.compare ids) cases with
-      | Some r -> r
-      | None -> warn ()
+  let rec find_arity acc payload =
+    match payload with
+    | [] | [_] -> None
+    | s1 :: ((s2 :: payload) as payload') ->
+      begin match is_arity s1 s2 with
+      | Some n -> Some (n, acc @ payload)
+      | None -> find_arity (s1 :: acc) payload'
+      end
+  in
+  find_arity [] payload
+
+let zero_alloc_lookup_table =
+  (* These are the possible payloads (sans arity) paired with a function that
+     returns the corresponding check_attribute, given the arity and the loc. *)
+  let property = Zero_alloc in
+  [
+    (["assume"],
+     fun arity loc ->
+       Assume { property; strict = false; never_returns_normally = false;
+                arity; loc; });
+    (["strict"],
+     fun arity loc ->
+       Check { property; strict = true; opt = false; arity; loc; });
+    (["opt"],
+     fun arity loc ->
+       Check { property; strict = false; opt = true; arity; loc; });
+    (["opt"; "strict"; ],
+     fun arity loc ->
+       Check { property; strict = true; opt = true; arity; loc; });
+    (["assume"; "strict"],
+     fun arity loc ->
+       Assume { property; strict = true; never_returns_normally = false;
+                arity; loc; });
+    (["assume"; "never_returns_normally"],
+     fun arity loc ->
+       Assume { property; strict = false; never_returns_normally = true;
+                arity; loc; });
+    (["assume"; "never_returns_normally"; "strict"],
+     fun arity loc ->
+       Assume { property; strict = true; never_returns_normally = true;
+                arity; loc; });
+    (["ignore"], fun _ _ -> Ignore_assert_all property)
+  ]
 
-let parse_property_attribute attr property =
+let parse_zero_alloc_payload ~loc ~arity ~warn ~empty payload =
+  (* This parses the remainder of the payload after arity has been parsed
+     out. *)
+  match payload with
+  | [] -> empty
+  | _ :: _ ->
+    let payload = List.sort String.compare payload in
+    match List.assoc_opt payload zero_alloc_lookup_table with
+    | None -> warn (); Default_check
+    | Some ca -> ca arity loc
+
+let parse_zero_alloc_attribute ~is_arity_allowed ~default_arity attr =
   match attr with
   | None -> Default_check
-  | Some {Parsetree.attr_name = {txt; loc}; attr_payload = payload}->
-      parse_ids_payload txt loc
-        ~default:Default_check
-        ~empty:(Check { property; strict = false; opt = false; loc; } )
-        [
-          ["assume"],
-          Assume { property; strict = false; never_returns_normally = false; loc; };
-          ["strict"], Check { property; strict = true; opt = false; loc; };
-          ["opt"], Check { property; strict = false; opt = true; loc; };
-          ["opt"; "strict"; ], Check { property; strict = true; opt = true; loc; };
-          ["assume"; "strict"],
-          Assume { property; strict = true; never_returns_normally = false; loc; };
-          ["assume"; "never_returns_normally"],
-          Assume { property; strict = false; never_returns_normally = true; loc; };
-          ["assume"; "never_returns_normally"; "strict"],
-          Assume { property; strict = true; never_returns_normally = true; loc; };
-          ["ignore"], Ignore_assert_all property
-        ]
-        payload
-
-let get_property_attribute l p =
+  | Some {Parsetree.attr_name = {txt; loc}; attr_payload = payload} ->
+    let warn () =
+      let ( %> ) f g x = g (f x) in
+      let msg =
+        zero_alloc_lookup_table
+        |> List.map (fst %> String.concat " " %> Printf.sprintf "'%s'")
+        |> String.concat ", "
+        |> Printf.sprintf "It must be either %s or empty"
+      in
+      Location.prerr_warning loc (Warnings.Attribute_payload (txt, msg))
+    in
+    let empty arity =
+      Check {property = Zero_alloc; strict = false; opt = false; arity; loc; }
+    in
+    match get_optional_payload get_ids_and_constants_from_exp payload with
+    | Error () -> warn (); Default_check
+    | Ok None -> empty default_arity
+    | Ok (Some payload) ->
+      let arity, payload =
+        match filter_arity payload with
+        | None -> default_arity, payload
+        | Some (user_arity, payload) ->
+          if is_arity_allowed then
+            user_arity, payload
+          else
+            (warn_payload loc txt
+               "The \"arity\" field is only supported on \"zero_alloc\" in \
+                signatures";
+             default_arity, payload)
+      in
+      parse_zero_alloc_payload ~loc ~arity ~warn ~empty:(empty arity) payload
+
+let get_property_attribute ~in_signature ~default_arity l p =
   let attr = find_attribute (is_property_attribute p) l in
-  let res = parse_property_attribute attr p in
+  let res =
+    match p with
+    | Zero_alloc ->
+      parse_zero_alloc_attribute ~is_arity_allowed:in_signature ~default_arity
+        attr
+  in
   (match attr, res with
    | None, Default_check -> ()
    | _, Default_check -> ()
@@ -841,10 +911,10 @@ let get_property_attribute l p =
    | Some _, Ignore_assert_all _ -> ()
    | Some _, Assume _ -> ()
    | Some attr, Check { opt; _ } ->
-     if is_check_enabled ~opt p && !Clflags.native_code then
-       (* The warning for unchecked functions will not trigger if the check is requested
-          through the [@@@zero_alloc all] top-level annotation rather than through the
-          function annotation [@zero_alloc]. *)
+     if not in_signature && is_check_enabled ~opt p && !Clflags.native_code then
+       (* The warning for unchecked functions will not trigger if the check is
+          requested through the [@@@zero_alloc all] top-level annotation rather
+          than through the function annotation [@zero_alloc]. *)
        register_property attr.attr_name);
    res
 
diff --git a/parsing/builtin_attributes.mli b/parsing/builtin_attributes.mli
index aa70ccd7ced..c766d3d5440 100644
--- a/parsing/builtin_attributes.mli
+++ b/parsing/builtin_attributes.mli
@@ -251,17 +251,24 @@ type check_attribute =
                   exceptional returns or diverging loops are ignored).
                   This definition may not be applicable to new properties. *)
                opt: bool;
+               arity: int;
                loc: Location.t;
              }
   | Assume of { property: property;
                 strict: bool;
-                loc: Location.t;
                 never_returns_normally: bool;
+                arity: int;
+                loc: Location.t;
               }
 
 val is_check_enabled : opt:bool -> property -> bool
 
-val get_property_attribute : Parsetree.attributes -> property -> check_attribute
+(* Gets a zero_alloc attribute.  [~in_signature] controls both whether the
+   "arity n" field is allowed, and whether we track this attribute for
+   warning 199. *)
+val get_property_attribute :
+  in_signature:bool -> default_arity:int -> Parsetree.attributes ->
+  property -> check_attribute
 
 val assume_zero_alloc :
   is_check_allowed:bool -> check_attribute -> Zero_alloc_utils.Assume_info.t
diff --git a/testsuite/tests/typing-zero-alloc/signatures.ml b/testsuite/tests/typing-zero-alloc/signatures.ml
new file mode 100644
index 00000000000..a469c7dbf67
--- /dev/null
+++ b/testsuite/tests/typing-zero-alloc/signatures.ml
@@ -0,0 +1,1005 @@
+(* TEST
+   expect;
+*)
+
+(* This tests the typing behavior of `[@zero_alloc]` annotation in signatures.
+
+   These tests are just about what is allowed and not allowed by the
+   typechecker.  The implementation of the actual `[@zero_alloc]` backend checks
+   (including how the annotations in signatures affect those checks) are tested
+   in the `tests/backend/checkmach` directory at the root of the project.
+*)
+
+(*******************************************)
+(* Test 1: Allowed and disallowed payloads *)
+module type S_payloads_base = sig
+  val[@zero_alloc] f : int -> int
+end
+
+module type S_payloads_strict = sig
+  val[@zero_alloc strict] f : int -> int
+end
+
+[%%expect{|
+module type S_payloads_base = sig val f : int -> int [@@zero_alloc] end
+module type S_payloads_strict =
+  sig val f : int -> int [@@zero_alloc strict] end
+|}]
+
+module type S_payloads_opt = sig
+  val[@zero_alloc opt] f : int -> int
+end
+[%%expect{|
+Line 2, characters 2-37:
+2 |   val[@zero_alloc opt] f : int -> int
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: "zero_alloc opt" is not supported in signatures.
+|}]
+
+module type S_payloads_strict_opt = sig
+  val[@zero_alloc strict opt] f : int -> int
+end
+[%%expect{|
+Line 2, characters 2-44:
+2 |   val[@zero_alloc strict opt] f : int -> int
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: "zero_alloc opt" is not supported in signatures.
+|}]
+
+module type S_payloads_assume = sig
+  val[@zero_alloc assume] f : int -> int
+end
+[%%expect{|
+Line 2, characters 2-40:
+2 |   val[@zero_alloc assume] f : int -> int
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: zero_alloc "assume" attributes are not supported in signatures
+|}]
+
+module type S_payloads_ignore = sig
+  val[@zero_alloc ignore] f : int -> int
+end
+[%%expect{|
+Line 2, characters 2-40:
+2 |   val[@zero_alloc ignore] f : int -> int
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: zero_alloc "ignore" attributes are not supported in signatures
+|}]
+
+(******************************)
+(* Test 2: allowed inclusions *)
+module type S_good_inc_base = sig
+  val[@zero_alloc] f : 'a -> 'a
+end
+
+module M_base : S_good_inc_base = struct
+  let[@zero_alloc] f x = x
+end
+
+module M_assume : S_good_inc_base = struct
+  let[@zero_alloc assume] f x = x
+end
+
+module M_assume_nrn : S_good_inc_base = struct
+  let[@zero_alloc assume never_returns_normally] f x = x
+end
+
+module M_stict : S_good_inc_base = struct
+  let[@zero_alloc strict] f x = x
+end
+
+module M_assume_strict : S_good_inc_base = struct
+  let[@zero_alloc assume strict] f x = x
+end
+
+module M_assume_strict_nrn : S_good_inc_base = struct
+  let[@zero_alloc assume strict never_returns_normally] f x = x
+end
+
+[%%expect{|
+module type S_good_inc_base = sig val f : 'a -> 'a [@@zero_alloc] end
+module M_base : S_good_inc_base
+module M_assume : S_good_inc_base
+module M_assume_nrn : S_good_inc_base
+module M_stict : S_good_inc_base
+module M_assume_strict : S_good_inc_base
+module M_assume_strict_nrn : S_good_inc_base
+|}]
+
+(* CR ccasinghino: The below should work once we allow opt in signatures. *)
+(* module type S_good_inc_opt = sig
+ *   val[@zero_alloc opt] f : 'a -> 'a
+ * end
+ *
+ * module M_base : S_good_inc_opt = struct
+ *   let[@zero_alloc] f x = x
+ * end
+ *
+ * module M_opt : S_good_inc_opt = struct
+ *   let[@zero_alloc opt] f x = x
+ * end
+ *
+ * module M_assume : S_good_inc_opt = struct
+ *   let[@zero_alloc assume] f x = x
+ * end
+ *
+ * module M_assume_nrn : S_good_inc_opt = struct
+ *   let[@zero_alloc assume never_returns_normally] f x = x
+ * end
+ *
+ * module M_strict : S_good_inc_opt = struct
+ *   let[@zero_alloc strict] f x = x
+ * end
+ *
+ * module M_strict_opt : S_good_inc_opt = struct
+ *   let[@zero_alloc strict opt] f x = x
+ * end
+ *
+ * module M_assume_strict : S_good_inc_opt = struct
+ *   let[@zero_alloc assume strict] f x = x
+ * end
+ *
+ * module M_assume_strict_nrn : S_good_inc_opt = struct
+ *   let[@zero_alloc assume strict never_returns_normally] f x = x
+ * end
+ *
+ * [%%expect{|
+ * module type S_good_inc_opt = sig val f : 'a -> 'a [@@zero_alloc opt] end
+ * module M_base : S_good_inc_opt
+ * module M_opt : S_good_inc_opt
+ * module M_assume : S_good_inc_opt
+ * module M_assume_nrn : S_good_inc_opt
+ * module M_strict : S_good_inc_opt
+ * module M_strict_opt : S_good_inc_opt
+ * module M_assume_strict : S_good_inc_opt
+ * module M_assume_strict_nrn : S_good_inc_opt
+ * |}] *)
+
+module type S_good_inc_strict = sig
+  val[@zero_alloc strict] f : 'a -> 'a
+end
+
+module M_strict : S_good_inc_strict = struct
+  let[@zero_alloc strict] f x = x
+end
+
+module M_assume_strict : S_good_inc_strict = struct
+  let[@zero_alloc assume strict] f x = x
+end
+
+module M_assume_strict_nrn : S_good_inc_strict = struct
+  let[@zero_alloc assume strict never_returns_normally] f x = x
+end
+
+[%%expect{|
+module type S_good_inc_strict =
+  sig val f : 'a -> 'a [@@zero_alloc strict] end
+module M_strict : S_good_inc_strict
+module M_assume_strict : S_good_inc_strict
+module M_assume_strict_nrn : S_good_inc_strict
+|}]
+
+(* CR ccasinghino: The below should work once we allow opt in signatures. *)
+(* module type S_good_inc_strict_opt = sig
+ *   val[@zero_alloc strict opt] f : 'a -> 'a
+ * end
+ *
+ * module M_strict : S_good_inc_strict_opt = struct
+ *   let[@zero_alloc strict] f x = x
+ * end
+ *
+ * module M_strict_opt : S_good_inc_strict_opt = struct
+ *   let[@zero_alloc strict opt] f x = x
+ * end
+ *
+ * module M_assume_strict : S_good_inc_strict_opt = struct
+ *   let[@zero_alloc assume strict] f x = x
+ * end
+ *
+ * module M_assume_strict_nrn : S_good_inc_strict_opt = struct
+ *   let[@zero_alloc assume strict never_returns_normally] f x = x
+ * end
+ *
+ * [%%expect{|
+ * module type S_good_inc_strict_opt =
+ *   sig val f : 'a -> 'a [@@zero_alloc strict opt] end
+ * module M_strict : S_good_inc_strict_opt
+ * module M_strict_opt : S_good_inc_strict_opt
+ * module M_assume_strict : S_good_inc_strict_opt
+ * module M_assume_strict_nrn : S_good_inc_strict_opt
+ * |}] *)
+
+
+(*********************************)
+(* Test 3: disallowed inclusions *)
+
+module type S_bad_inc_base = sig
+  val[@zero_alloc] f : 'a -> 'a
+end
+
+module M_absent : S_bad_inc_base = struct
+  let f x = x
+end
+
+[%%expect{|
+module type S_bad_inc_base = sig val f : 'a -> 'a [@@zero_alloc] end
+Lines 5-7, characters 35-3:
+5 | ...................................struct
+6 |   let f x = x
+7 | end
+Error: Signature mismatch:
+       Modules do not match:
+         sig val f : 'a -> 'a end
+       is not included in
+         S_bad_inc_base
+       Values do not match:
+         val f : 'a -> 'a
+       is not included in
+         val f : 'a -> 'a [@@zero_alloc]
+       The former provides a weaker "zero_alloc" guarantee than the latter.
+       Hint: Add a "zero_alloc" attribute (without opt) to the implementation.
+|}]
+
+module M_opt : S_bad_inc_base = struct
+  let[@zero_alloc opt] f x = x
+end
+
+[%%expect{|
+Lines 1-3, characters 32-3:
+1 | ................................struct
+2 |   let[@zero_alloc opt] f x = x
+3 | end
+Error: Signature mismatch:
+       Modules do not match:
+         sig val f : 'a -> 'a end
+       is not included in
+         S_bad_inc_base
+       Values do not match:
+         val f : 'a -> 'a
+       is not included in
+         val f : 'a -> 'a [@@zero_alloc]
+       The former provides a weaker "zero_alloc" guarantee than the latter.
+       Hint: Add a "zero_alloc" attribute (without opt) to the implementation.
+|}]
+
+(* CR ccasinghino: The below should work once we allow opt in signatures. *)
+(* module type S_bad_inc_opt = sig
+ *   val[@zero_alloc opt] f : 'a -> 'a
+ * end
+ *
+ * module M_absent : S_bad_inc_opt = struct
+ *   let f x = x
+ * end
+ *
+ * [%%expect{|
+ * module type S_bad_inc_opt = sig val f : 'a -> 'a [@@zero_alloc opt] end
+ * Lines 5-7, characters 34-3:
+ * 5 | ..................................struct
+ * 6 |   let f x = x
+ * 7 | end
+ * Error: Signature mismatch:
+ *        Modules do not match:
+ *          sig val f : 'a -> 'a end
+ *        is not included in
+ *          S_bad_inc_opt
+ *        Values do not match:
+ *          val f : 'a -> 'a
+ *        is not included in
+ *          val f : 'a -> 'a [@@zero_alloc opt]
+ *        The former provides a weaker "zero_alloc" guarantee than the latter.
+ *        Hint: Add a "zero_alloc" attribute to the implementation.
+ * |}] *)
+
+module type S_bad_inc_strict = sig
+  val[@zero_alloc strict] f : 'a -> 'a
+end
+
+module M_absent : S_bad_inc_strict = struct
+  let f x = x
+end
+
+[%%expect{|
+module type S_bad_inc_strict = sig val f : 'a -> 'a [@@zero_alloc strict] end
+Lines 5-7, characters 37-3:
+5 | .....................................struct
+6 |   let f x = x
+7 | end
+Error: Signature mismatch:
+       Modules do not match:
+         sig val f : 'a -> 'a end
+       is not included in
+         S_bad_inc_strict
+       Values do not match:
+         val f : 'a -> 'a
+       is not included in
+         val f : 'a -> 'a [@@zero_alloc strict]
+       The former provides a weaker "zero_alloc" guarantee than the latter.
+       Hint: Add a "zero_alloc" attribute (without opt) to the implementation.
+|}]
+
+module M_base : S_bad_inc_strict = struct
+  let[@zero_alloc] f x = x
+end
+[%%expect{|
+Lines 1-3, characters 35-3:
+1 | ...................................struct
+2 |   let[@zero_alloc] f x = x
+3 | end
+Error: Signature mismatch:
+       Modules do not match:
+         sig val f : 'a -> 'a [@@zero_alloc] end
+       is not included in
+         S_bad_inc_strict
+       Values do not match:
+         val f : 'a -> 'a [@@zero_alloc]
+       is not included in
+         val f : 'a -> 'a [@@zero_alloc strict]
+       The former provides a weaker "zero_alloc" guarantee than the latter.
+|}]
+
+module M_assume : S_bad_inc_strict = struct
+  let[@zero_alloc assume] f x = x
+end
+
+[%%expect{|
+Lines 1-3, characters 37-3:
+1 | .....................................struct
+2 |   let[@zero_alloc assume] f x = x
+3 | end
+Error: Signature mismatch:
+       Modules do not match:
+         sig val f : 'a -> 'a [@@zero_alloc] end
+       is not included in
+         S_bad_inc_strict
+       Values do not match:
+         val f : 'a -> 'a [@@zero_alloc]
+       is not included in
+         val f : 'a -> 'a [@@zero_alloc strict]
+       The former provides a weaker "zero_alloc" guarantee than the latter.
+|}]
+
+module M_opt : S_bad_inc_strict = struct
+  let[@zero_alloc opt] f x = x
+end
+
+[%%expect{|
+Lines 1-3, characters 34-3:
+1 | ..................................struct
+2 |   let[@zero_alloc opt] f x = x
+3 | end
+Error: Signature mismatch:
+       Modules do not match:
+         sig val f : 'a -> 'a end
+       is not included in
+         S_bad_inc_strict
+       Values do not match:
+         val f : 'a -> 'a
+       is not included in
+         val f : 'a -> 'a [@@zero_alloc strict]
+       The former provides a weaker "zero_alloc" guarantee than the latter.
+       Hint: Add a "zero_alloc" attribute (without opt) to the implementation.
+|}]
+
+module M_strict_opt : S_bad_inc_strict = struct
+  let[@zero_alloc strict opt] f x = x
+end
+
+[%%expect{|
+Lines 1-3, characters 41-3:
+1 | .........................................struct
+2 |   let[@zero_alloc strict opt] f x = x
+3 | end
+Error: Signature mismatch:
+       Modules do not match:
+         sig val f : 'a -> 'a end
+       is not included in
+         S_bad_inc_strict
+       Values do not match:
+         val f : 'a -> 'a
+       is not included in
+         val f : 'a -> 'a [@@zero_alloc strict]
+       The former provides a weaker "zero_alloc" guarantee than the latter.
+       Hint: Add a "zero_alloc" attribute (without opt) to the implementation.
+|}]
+
+module M_assume_nrn : S_bad_inc_strict = struct
+  let[@zero_alloc assume never_returns_normally] f x = x
+end
+
+[%%expect{|
+Lines 1-3, characters 41-3:
+1 | .........................................struct
+2 |   let[@zero_alloc assume never_returns_normally] f x = x
+3 | end
+Error: Signature mismatch:
+       Modules do not match:
+         sig val f : 'a -> 'a [@@zero_alloc] end
+       is not included in
+         S_bad_inc_strict
+       Values do not match:
+         val f : 'a -> 'a [@@zero_alloc]
+       is not included in
+         val f : 'a -> 'a [@@zero_alloc strict]
+       The former provides a weaker "zero_alloc" guarantee than the latter.
+|}]
+
+(* CR ccasinghino: The below should work once we allow opt in signatures. *)
+(* module type S_strict_opt = sig
+ *   val[@zero_alloc strict opt] f : 'a -> 'a
+ * end
+ *
+ * module M_absent : S_strict_opt = struct
+ *   let f x = x
+ * end
+ *
+ * [%%expect{|
+ * module type S_strict_opt = sig val f : 'a -> 'a [@@zero_alloc strict opt] end
+ * Lines 5-7, characters 33-3:
+ * 5 | .................................struct
+ * 6 |   let f x = x
+ * 7 | end
+ * Error: Signature mismatch:
+ *        Modules do not match:
+ *          sig val f : 'a -> 'a end
+ *        is not included in
+ *          S_strict_opt
+ *        Values do not match:
+ *          val f : 'a -> 'a
+ *        is not included in
+ *          val f : 'a -> 'a [@@zero_alloc strict opt]
+ *        The former provides a weaker "zero_alloc" guarantee than the latter.
+ *        Hint: Add a "zero_alloc" attribute to the implementation.
+ * |}]
+ *
+ * module M_assume : S_strict_opt = struct
+ *   let[@zero_alloc assume] f x = x
+ * end
+ *
+ * [%%expect{|
+ * Lines 1-3, characters 33-3:
+ * 1 | .................................struct
+ * 2 |   let[@zero_alloc assume] f x = x
+ * 3 | end
+ * Error: Signature mismatch:
+ *        Modules do not match:
+ *          sig val f : 'a -> 'a [@@zero_alloc] end
+ *        is not included in
+ *          S_strict_opt
+ *        Values do not match:
+ *          val f : 'a -> 'a [@@zero_alloc]
+ *        is not included in
+ *          val f : 'a -> 'a [@@zero_alloc strict opt]
+ *        The former provides a weaker "zero_alloc" guarantee than the latter.
+ * |}]
+ *
+ * module M_opt : S_strict_opt = struct
+ *   let[@zero_alloc opt] f x = x
+ * end
+ *
+ * [%%expect{|
+ * Lines 1-3, characters 30-3:
+ * 1 | ..............................struct
+ * 2 |   let[@zero_alloc opt] f x = x
+ * 3 | end
+ * Error: Signature mismatch:
+ *        Modules do not match:
+ *          sig val f : 'a -> 'a [@@zero_alloc opt] end
+ *        is not included in
+ *          S_strict_opt
+ *        Values do not match:
+ *          val f : 'a -> 'a [@@zero_alloc opt]
+ *        is not included in
+ *          val f : 'a -> 'a [@@zero_alloc strict opt]
+ *        The former provides a weaker "zero_alloc" guarantee than the latter.
+ * |}]
+ *
+ * module M_assume_nrn : S_strict_opt = struct
+ *   let[@zero_alloc assume never_returns_normally] f x = x
+ * end
+ *
+ * [%%expect{|
+ * Lines 1-3, characters 37-3:
+ * 1 | .....................................struct
+ * 2 |   let[@zero_alloc assume never_returns_normally] f x = x
+ * 3 | end
+ * Error: Signature mismatch:
+ *        Modules do not match:
+ *          sig val f : 'a -> 'a [@@zero_alloc] end
+ *        is not included in
+ *          S_strict_opt
+ *        Values do not match:
+ *          val f : 'a -> 'a [@@zero_alloc]
+ *        is not included in
+ *          val f : 'a -> 'a [@@zero_alloc strict opt]
+ *        The former provides a weaker "zero_alloc" guarantee than the latter.
+ * |}] *)
+
+(*************************************************************************)
+(* Test 4: Requires valid arity, inferred or provided, without expansion *)
+
+module type S_non_func_int = sig
+  val[@zero_alloc] x : int
+end
+[%%expect{|
+Line 2, characters 2-26:
+2 |   val[@zero_alloc] x : int
+      ^^^^^^^^^^^^^^^^^^^^^^^^
+Error: In signatures, zero_alloc is only supported on function declarations.
+       Found no arrows in this declaration's type.
+       Hint: You can write "[@zero_alloc arity n]" to specify the arity
+       of an alias (for n > 0).
+|}]
+
+module type S_non_func_alias = sig
+  type t = string
+  val[@zero_alloc] x : t
+end
+[%%expect{|
+Line 3, characters 2-24:
+3 |   val[@zero_alloc] x : t
+      ^^^^^^^^^^^^^^^^^^^^^^
+Error: In signatures, zero_alloc is only supported on function declarations.
+       Found no arrows in this declaration's type.
+       Hint: You can write "[@zero_alloc arity n]" to specify the arity
+       of an alias (for n > 0).
+|}]
+
+module type S_func_alias = sig
+  type t = int -> int
+  type s = t
+  val[@zero_alloc] x : s
+end
+[%%expect{|
+Line 4, characters 2-24:
+4 |   val[@zero_alloc] x : s
+      ^^^^^^^^^^^^^^^^^^^^^^
+Error: In signatures, zero_alloc is only supported on function declarations.
+       Found no arrows in this declaration's type.
+       Hint: You can write "[@zero_alloc arity n]" to specify the arity
+       of an alias (for n > 0).
+|}]
+
+module type S_func_alias = sig
+  type t = int -> int
+  val[@zero_alloc arity 0] x : t
+end
+[%%expect{|
+Line 3, characters 2-32:
+3 |   val[@zero_alloc arity 0] x : t
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: In signatures, zero_alloc is only supported on function declarations.
+       Found no arrows in this declaration's type.
+       Hint: You can write "[@zero_alloc arity n]" to specify the arity
+       of an alias (for n > 0).
+|}]
+
+module type S_arity_0 = sig
+  val[@zero_alloc arity 0] f : int -> int
+end
+[%%expect{|
+Line 2, characters 2-41:
+2 |   val[@zero_alloc arity 0] f : int -> int
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: Invalid zero_alloc attribute: arity must be greater than 0.
+|}]
+
+module type S_arity_negative = sig
+  val[@zero_alloc arity (-1)] f : int -> int
+end
+[%%expect{|
+Line 2, characters 2-44:
+2 |   val[@zero_alloc arity (-1)] f : int -> int
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: Invalid zero_alloc attribute: arity must be greater than 0.
+|}]
+
+(********************************************)
+(* Test 5: impl arity must match intf arity *)
+
+type t_two_args = int -> int -> int
+
+module type S_arity_int_int = sig
+  val[@zero_alloc] f : int -> int -> int
+end
+
+module M_int_int_params : S_arity_int_int = struct
+  let[@zero_alloc] f x y = x + y
+end
+
+module M_int_param_int_case : S_arity_int_int = struct
+  let[@zero_alloc] f x =
+    function 0 -> x + x
+           | n -> x + n
+end
+
+module M_nested_functions : S_arity_int_int = struct
+  let[@zero_alloc] f x = fun y -> x + y
+end
+[%%expect{|
+type t_two_args = int -> int -> int
+module type S_arity_int_int =
+  sig val f : int -> int -> int [@@zero_alloc] end
+module M_int_int_params : S_arity_int_int
+module M_int_param_int_case : S_arity_int_int
+Lines 17-19, characters 46-3:
+17 | ..............................................struct
+18 |   let[@zero_alloc] f x = fun y -> x + y
+19 | end
+Error: Signature mismatch:
+       Modules do not match:
+         sig val f : int -> int -> int [@@zero_alloc arity 1] end
+       is not included in
+         S_arity_int_int
+       Values do not match:
+         val f : int -> int -> int [@@zero_alloc arity 1]
+       is not included in
+         val f : int -> int -> int [@@zero_alloc]
+       zero_alloc arity mismatch:
+       When using "zero_alloc" in a signature, the syntactic arity of
+       the implementation must match the function type in the interface.
+       Here the former is 1 and the latter is 2.
+|}]
+
+module type S_alias_no_arity = sig
+  val[@zero_alloc] f : t_two_args
+end
+[%%expect{|
+Line 2, characters 2-33:
+2 |   val[@zero_alloc] f : t_two_args
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: In signatures, zero_alloc is only supported on function declarations.
+       Found no arrows in this declaration's type.
+       Hint: You can write "[@zero_alloc arity n]" to specify the arity
+       of an alias (for n > 0).
+|}]
+
+module type S_alias_explicit_arity_2 = sig
+  val[@zero_alloc arity 2] f : t_two_args
+end
+
+module M_good_explicit_arity_2 : S_alias_explicit_arity_2 = struct
+  let[@zero_alloc] f x y = x + y
+end
+[%%expect{|
+module type S_alias_explicit_arity_2 =
+  sig val f : t_two_args [@@zero_alloc arity 2] end
+module M_good_explicit_arity_2 : S_alias_explicit_arity_2
+|}]
+
+module M_bad_explicit_arity_2 : S_alias_explicit_arity_2 = struct
+  let[@zero_alloc] f x = fun y -> x + y
+end
+[%%expect{|
+Lines 1-3, characters 59-3:
+1 | ...........................................................struct
+2 |   let[@zero_alloc] f x = fun y -> x + y
+3 | end
+Error: Signature mismatch:
+       Modules do not match:
+         sig val f : int -> int -> int [@@zero_alloc arity 1] end
+       is not included in
+         S_alias_explicit_arity_2
+       Values do not match:
+         val f : int -> int -> int [@@zero_alloc arity 1]
+       is not included in
+         val f : t_two_args [@@zero_alloc arity 2]
+       zero_alloc arity mismatch:
+       When using "zero_alloc" in a signature, the syntactic arity of
+       the implementation must match the function type in the interface.
+       Here the former is 1 and the latter is 2.
+|}]
+
+module type S_alias_explicit_arity_1 = sig
+  val[@zero_alloc arity 1] f : t_two_args
+end
+
+module M_bad_explicit_arity_1 : S_alias_explicit_arity_1 = struct
+  let[@zero_alloc] f x y = x + y
+end
+[%%expect{|
+module type S_alias_explicit_arity_1 =
+  sig val f : t_two_args [@@zero_alloc arity 1] end
+Lines 5-7, characters 59-3:
+5 | ...........................................................struct
+6 |   let[@zero_alloc] f x y = x + y
+7 | end
+Error: Signature mismatch:
+       Modules do not match:
+         sig val f : int -> int -> int [@@zero_alloc] end
+       is not included in
+         S_alias_explicit_arity_1
+       Values do not match:
+         val f : int -> int -> int [@@zero_alloc]
+       is not included in
+         val f : t_two_args [@@zero_alloc arity 1]
+       zero_alloc arity mismatch:
+       When using "zero_alloc" in a signature, the syntactic arity of
+       the implementation must match the function type in the interface.
+       Here the former is 2 and the latter is 1.
+|}]
+
+module M_good_explicit_arity_1 : S_alias_explicit_arity_1 = struct
+  let[@zero_alloc] f x = fun y -> x + y
+end
+[%%expect{|
+module M_good_explicit_arity_1 : S_alias_explicit_arity_1
+|}]
+
+(******************************************************************)
+(* Test 6: we don't update the arity as a result of substitutions *)
+
+module type S_abstract = sig
+  type t
+  val[@zero_alloc] f : int -> t
+end
+
+module M_abstract : S_abstract = struct
+  type t = int
+  let[@zero_alloc] f x = x
+end
+
+module type S_subst = S_abstract with type t = int -> int
+
+module M_subst_good : S_subst  = struct
+  type t = int -> int
+  let[@zero_alloc] f x = fun y -> x + y
+end
+
+module M_subst_bad : S_subst  = struct
+  type t = int -> int
+  let[@zero_alloc] f x y = x + y
+end
+[%%expect{|
+module type S_abstract = sig type t val f : int -> t [@@zero_alloc] end
+module M_abstract : S_abstract
+module type S_subst =
+  sig type t = int -> int val f : int -> t [@@zero_alloc] end
+module M_subst_good : S_subst
+Lines 18-21, characters 32-3:
+18 | ................................struct
+19 |   type t = int -> int
+20 |   let[@zero_alloc] f x y = x + y
+21 | end
+Error: Signature mismatch:
+       Modules do not match:
+         sig type t = int -> int val f : int -> int -> int [@@zero_alloc] end
+       is not included in
+         S_subst
+       Values do not match:
+         val f : int -> int -> int [@@zero_alloc]
+       is not included in
+         val f : int -> t [@@zero_alloc]
+       zero_alloc arity mismatch:
+       When using "zero_alloc" in a signature, the syntactic arity of
+       the implementation must match the function type in the interface.
+       Here the former is 2 and the latter is 1.
+|}]
+
+(********************************************************************)
+(* Test 7: A practicalish example of a non-obvious zero_alloc arity *)
+
+module type S_fun_in_fun = sig
+  val[@zero_alloc arity 2] f : int -> int -> int -> int*int
+end
+
+(* The expected behavior from the backend analysis for the two funtions below
+   is checked in [tests/backend/checkmach/test_arity.ml] *)
+
+module M_fun_in_fun_good : S_fun_in_fun = struct
+  let[@zero_alloc] f x y =
+    if x = y+1 then fun z -> (z,z) else fun z -> (z,0)
+end
+
+module M_fun_in_fun_bad : S_fun_in_fun = struct
+  let[@zero_alloc] f x y z =
+    if x = y+1 then (z,z) else (z,0)
+end
+
+[%%expect{|
+module type S_fun_in_fun =
+  sig val f : int -> int -> int -> int * int [@@zero_alloc arity 2] end
+module M_fun_in_fun_good : S_fun_in_fun
+Lines 13-16, characters 41-3:
+13 | .........................................struct
+14 |   let[@zero_alloc] f x y z =
+15 |     if x = y+1 then (z,z) else (z,0)
+16 | end
+Error: Signature mismatch:
+       Modules do not match:
+         sig val f : int -> int -> int -> int * int [@@zero_alloc] end
+       is not included in
+         S_fun_in_fun
+       Values do not match:
+         val f : int -> int -> int -> int * int [@@zero_alloc]
+       is not included in
+         val f : int -> int -> int -> int * int [@@zero_alloc arity 2]
+       zero_alloc arity mismatch:
+       When using "zero_alloc" in a signature, the syntactic arity of
+       the implementation must match the function type in the interface.
+       Here the former is 3 and the latter is 2.
+|}]
+
+(*************************************)
+(* Test 8: Parsing "arity n" works *)
+
+(* CR ccasinghino: when we have support for opt, add tests for all the
+   combinations here. *)
+module type S_arity_42 = sig
+  val[@zero_alloc arity 42] f : int -> int
+end
+
+module type S_arity_42_strict = sig
+  val[@zero_alloc arity 42 strict] f : int -> int
+end
+
+module type S_strict_arity_42 = sig
+  val[@zero_alloc strict arity 42] f : int -> int
+end
+
+[%%expect{|
+module type S_arity_42 = sig val f : int -> int [@@zero_alloc arity 42] end
+module type S_arity_42_strict =
+  sig val f : int -> int [@@zero_alloc strict arity 42] end
+module type S_strict_arity_42 =
+  sig val f : int -> int [@@zero_alloc strict arity 42] end
+|}]
+
+(**************************************************)
+(* Test 9: arity n in structures gives warning 47 *)
+
+module M_struct_arity_let_1 = struct
+  let[@zero_alloc arity 2] f x y = x + y
+end
+
+[%%expect{|
+Line 2, characters 7-17:
+2 |   let[@zero_alloc arity 2] f x y = x + y
+           ^^^^^^^^^^
+Warning 47 [attribute-payload]: illegal payload for attribute 'zero_alloc'.
+The "arity" field is only supported on "zero_alloc" in signatures
+
+module M_struct_arity_let_1 :
+  sig val f : int -> int -> int [@@zero_alloc] end
+|}]
+
+module M_struct_arity_let_2 = struct
+  let[@zero_alloc arity 2] f = fun x y -> x + y
+end
+[%%expect{|
+Line 2, characters 7-17:
+2 |   let[@zero_alloc arity 2] f = fun x y -> x + y
+           ^^^^^^^^^^
+Warning 47 [attribute-payload]: illegal payload for attribute 'zero_alloc'.
+The "arity" field is only supported on "zero_alloc" in signatures
+
+module M_struct_arity_let_2 :
+  sig val f : int -> int -> int [@@zero_alloc] end
+|}]
+
+module M_struct_arity_let_fun_1 = struct
+  let f = fun[@zero_alloc arity 2]  x y -> x + y
+end
+[%%expect{|
+Line 2, characters 15-25:
+2 |   let f = fun[@zero_alloc arity 2]  x y -> x + y
+                   ^^^^^^^^^^
+Warning 47 [attribute-payload]: illegal payload for attribute 'zero_alloc'.
+The "arity" field is only supported on "zero_alloc" in signatures
+
+module M_struct_arity_let_fun_1 :
+  sig val f : int -> int -> int [@@zero_alloc] end
+|}]
+
+module M_struct_arity_let_fun_2 = struct
+  let f x =
+    if x = 42 then
+      fun[@zero_alloc arity 1] y -> y
+    else
+      fun y -> y + 1
+end
+[%%expect{|
+Line 4, characters 11-21:
+4 |       fun[@zero_alloc arity 1] y -> y
+               ^^^^^^^^^^
+Warning 47 [attribute-payload]: illegal payload for attribute 'zero_alloc'.
+The "arity" field is only supported on "zero_alloc" in signatures
+
+module M_struct_arity_let_fun_2 : sig val f : int -> int -> int end
+|}]
+
+(*********************************)
+(* Test 10: module type of works *)
+
+module M_base_for_mto = struct
+  let[@zero_alloc] f x = x+1
+end
+
+module type S_base_mto = module type of M_base_for_mto
+
+module M_mto_base_good : S_base_mto = struct
+  let[@zero_alloc] f x = x + 2
+end
+
+module M_mto_base_bad : S_base_mto = struct
+  let f x = x + 3
+end
+
+[%%expect{|
+module M_base_for_mto : sig val f : int -> int [@@zero_alloc] end
+module type S_base_mto = sig val f : int -> int [@@zero_alloc] end
+module M_mto_base_good : S_base_mto
+Lines 11-13, characters 37-3:
+11 | .....................................struct
+12 |   let f x = x + 3
+13 | end
+Error: Signature mismatch:
+       Modules do not match:
+         sig val f : int -> int end
+       is not included in
+         S_base_mto
+       Values do not match:
+         val f : int -> int
+       is not included in
+         val f : int -> int [@@zero_alloc]
+       The former provides a weaker "zero_alloc" guarantee than the latter.
+       Hint: Add a "zero_alloc" attribute (without opt) to the implementation.
+|}]
+
+module M_strict_for_mto = struct
+  let[@zero_alloc strict] f x = x+1
+end
+
+module type S_strict_mto = module type of M_strict_for_mto
+
+module M_mto_strict_good : S_strict_mto = struct
+  let[@zero_alloc strict] f x = x + 2
+end
+
+module M_mto_strict_bad : S_strict_mto = struct
+  let[@zero_alloc] f x = x + 3
+end
+
+[%%expect{|
+module M_strict_for_mto : sig val f : int -> int [@@zero_alloc strict] end
+module type S_strict_mto = sig val f : int -> int [@@zero_alloc strict] end
+module M_mto_strict_good : S_strict_mto
+Lines 11-13, characters 41-3:
+11 | .........................................struct
+12 |   let[@zero_alloc] f x = x + 3
+13 | end
+Error: Signature mismatch:
+       Modules do not match:
+         sig val f : int -> int [@@zero_alloc] end
+       is not included in
+         S_strict_mto
+       Values do not match:
+         val f : int -> int [@@zero_alloc]
+       is not included in
+         val f : int -> int [@@zero_alloc strict]
+       The former provides a weaker "zero_alloc" guarantee than the latter.
+|}]
+
+(* You can't sneakily get never_returns_normally or assume in a signature with
+   module type of, but nice try.  These tests rely on the fact that the
+   printer would show that information, but indeed it would (see printtyp).
+
+   (At the moment the backend doesn't allow for checking never_return_normally,
+   but it wouldn't be hard to add, and then we could revisit this). *)
+module M_assume_for_mto = struct
+  let[@zero_alloc assume] f x = (x+1,x+2)
+end
+
+module type S_no_assume = module type of M_assume_for_mto
+
+module M_nrn_for_mto = struct
+  let[@zero_alloc assume never_returns_normally] f x = (x+1,x+2)
+end
+
+module type S_no_nrn = module type of M_nrn_for_mto
+
+[%%expect{|
+module M_assume_for_mto : sig val f : int -> int * int [@@zero_alloc] end
+module type S_no_assume = sig val f : int -> int * int [@@zero_alloc] end
+module M_nrn_for_mto : sig val f : int -> int * int [@@zero_alloc] end
+module type S_no_nrn = sig val f : int -> int * int [@@zero_alloc] end
+|}]
diff --git a/testsuite/tests/typing-zero-alloc/signatures_native.ml b/testsuite/tests/typing-zero-alloc/signatures_native.ml
new file mode 100644
index 00000000000..e9c76c22033
--- /dev/null
+++ b/testsuite/tests/typing-zero-alloc/signatures_native.ml
@@ -0,0 +1,15 @@
+(* TEST
+   native;
+*)
+
+(* This test is just checking that zero_alloc attributes in signatures don't
+   result in warning 199 when compiling to native code (which was a bug in the
+   initial implementation. *)
+
+module type S = sig
+  type t
+
+  val[@zero_alloc] f : int -> int
+
+  val[@zero_alloc arity 3] g : t
+end
diff --git a/testsuite/tests/warnings/w53.compilers.reference b/testsuite/tests/warnings/w53.compilers.reference
index 2fe8139d56e..79e8628b67d 100644
--- a/testsuite/tests/warnings/w53.compilers.reference
+++ b/testsuite/tests/warnings/w53.compilers.reference
@@ -1083,132 +1083,122 @@ File "w53.ml", line 479, characters 19-29:
                          ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53.ml", line 480, characters 17-27:
-480 |   val x : int [@@zero_alloc] (* rejected *)
-                       ^^^^^^^^^^
-Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
-
-File "w53.ml", line 481, characters 24-34:
-481 |   val f : int -> int [@@zero_alloc] (* rejected *)
-                              ^^^^^^^^^^
-Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
-
-File "w53.ml", line 483, characters 22-32:
-483 |   external y : (int [@zero_alloc]) -> (int [@zero_alloc]) = "x" (* rejected *)
+File "w53.ml", line 482, characters 22-32:
+482 |   external y : (int [@zero_alloc]) -> (int [@zero_alloc]) = "x" (* rejected *)
                             ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53.ml", line 483, characters 45-55:
-483 |   external y : (int [@zero_alloc]) -> (int [@zero_alloc]) = "x" (* rejected *)
+File "w53.ml", line 482, characters 45-55:
+482 |   external y : (int [@zero_alloc]) -> (int [@zero_alloc]) = "x" (* rejected *)
                                                    ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53.ml", line 484, characters 39-49:
-484 |   external z : int -> int = "x" "y" [@@zero_alloc] (* rejected *)
+File "w53.ml", line 483, characters 39-49:
+483 |   external z : int -> int = "x" "y" [@@zero_alloc] (* rejected *)
                                              ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53.ml", line 485, characters 12-22:
-485 |   external[@zero_alloc] q : int -> int = "x" "y" (* rejected *)
+File "w53.ml", line 484, characters 12-22:
+484 |   external[@zero_alloc] q : int -> int = "x" "y" (* rejected *)
                   ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53.ml", line 487, characters 9-19:
-487 |   class[@zero_alloc] c : (* rejected *)
+File "w53.ml", line 486, characters 9-19:
+486 |   class[@zero_alloc] c : (* rejected *)
                ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53.ml", line 489, characters 11-21:
-489 |       val[@zero_alloc] foo : int * int (* rejected *)
+File "w53.ml", line 488, characters 11-21:
+488 |       val[@zero_alloc] foo : int * int (* rejected *)
                  ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53.ml", line 490, characters 11-21:
-490 |       val[@zero_alloc] bar : int -> int (* rejected *)
+File "w53.ml", line 489, characters 11-21:
+489 |       val[@zero_alloc] bar : int -> int (* rejected *)
                  ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53.ml", line 491, characters 14-24:
-491 |       method[@zero_alloc] baz : int * int (* rejected *)
+File "w53.ml", line 490, characters 14-24:
+490 |       method[@zero_alloc] baz : int * int (* rejected *)
                     ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53.ml", line 492, characters 14-24:
-492 |       method[@zero_alloc] boz : int -> int (* rejected *)
+File "w53.ml", line 491, characters 14-24:
+491 |       method[@zero_alloc] boz : int -> int (* rejected *)
                     ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53.ml", line 497, characters 21-31:
-497 |   type 'a t1 = 'a [@@zero_alloc] (* rejected *)
+File "w53.ml", line 496, characters 21-31:
+496 |   type 'a t1 = 'a [@@zero_alloc] (* rejected *)
                            ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53.ml", line 498, characters 19-29:
-498 |   type s1 = Foo1 [@zero_alloc] (* rejected *)
+File "w53.ml", line 497, characters 19-29:
+497 |   type s1 = Foo1 [@zero_alloc] (* rejected *)
                          ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53.ml", line 499, characters 22-32:
-499 |   let x : int = 42 [@@zero_alloc] (* rejected *)
+File "w53.ml", line 498, characters 22-32:
+498 |   let x : int = 42 [@@zero_alloc] (* rejected *)
                             ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53.ml", line 501, characters 7-17:
-501 |   let[@zero_alloc] w = 42 (* rejected *)
+File "w53.ml", line 500, characters 7-17:
+500 |   let[@zero_alloc] w = 42 (* rejected *)
              ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53.ml", line 505, characters 22-32:
-505 |   external y : (int [@zero_alloc]) -> (int [@zero_alloc]) = "x" (* rejected *)
+File "w53.ml", line 504, characters 22-32:
+504 |   external y : (int [@zero_alloc]) -> (int [@zero_alloc]) = "x" (* rejected *)
                             ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53.ml", line 505, characters 45-55:
-505 |   external y : (int [@zero_alloc]) -> (int [@zero_alloc]) = "x" (* rejected *)
+File "w53.ml", line 504, characters 45-55:
+504 |   external y : (int [@zero_alloc]) -> (int [@zero_alloc]) = "x" (* rejected *)
                                                    ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53.ml", line 506, characters 39-49:
-506 |   external z : int -> int = "x" "y" [@@zero_alloc] (* rejected *)
+File "w53.ml", line 505, characters 39-49:
+505 |   external z : int -> int = "x" "y" [@@zero_alloc] (* rejected *)
                                              ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53.ml", line 507, characters 12-22:
-507 |   external[@zero_alloc] q : int -> int = "x" "y" (* rejected *)
+File "w53.ml", line 506, characters 12-22:
+506 |   external[@zero_alloc] q : int -> int = "x" "y" (* rejected *)
                   ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53.ml", line 509, characters 9-19:
-509 |   class[@zero_alloc] foo _y = (* rejected *)
+File "w53.ml", line 508, characters 9-19:
+508 |   class[@zero_alloc] foo _y = (* rejected *)
                ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53.ml", line 511, characters 10-20:
-511 |     (fun[@zero_alloc] z -> (* rejected *)
+File "w53.ml", line 510, characters 10-20:
+510 |     (fun[@zero_alloc] z -> (* rejected *)
                 ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53.ml", line 513, characters 11-21:
-513 |       val[@zero_alloc] bar = (4, 5) (* rejected *)
+File "w53.ml", line 512, characters 11-21:
+512 |       val[@zero_alloc] bar = (4, 5) (* rejected *)
                  ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53.ml", line 515, characters 14-24:
-515 |       method[@zero_alloc] baz x = (f (z+10), x+1) (* rejected *)
+File "w53.ml", line 514, characters 14-24:
+514 |       method[@zero_alloc] baz x = (f (z+10), x+1) (* rejected *)
                     ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53.ml", line 527, characters 14-24:
-527 |     ((boz x)[@zero_alloc assume]) (* rejected *)
+File "w53.ml", line 526, characters 14-24:
+526 |     ((boz x)[@zero_alloc assume]) (* rejected *)
                     ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53.ml", line 532, characters 7-17:
-532 |   let[@zero_alloc assume] foo = (* rejected *)
+File "w53.ml", line 531, characters 7-17:
+531 |   let[@zero_alloc assume] foo = (* rejected *)
              ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53.ml", line 536, characters 7-17:
-536 |   let[@zero_alloc] bar = (* rejected *)
+File "w53.ml", line 535, characters 7-17:
+535 |   let[@zero_alloc] bar = (* rejected *)
              ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
diff --git a/testsuite/tests/warnings/w53.ml b/testsuite/tests/warnings/w53.ml
index f4299588f59..8c9cbadcdff 100644
--- a/testsuite/tests/warnings/w53.ml
+++ b/testsuite/tests/warnings/w53.ml
@@ -477,8 +477,7 @@ end
 module type TestZeroAllocSig = sig
   type 'a t1 = 'a [@@zero_alloc] (* rejected *)
   type s1 = Foo1 [@zero_alloc] (* rejected *)
-  val x : int [@@zero_alloc] (* rejected *)
-  val f : int -> int [@@zero_alloc] (* rejected *)
+  val f : int -> int [@@zero_alloc] (* accepted *)
 
   external y : (int [@zero_alloc]) -> (int [@zero_alloc]) = "x" (* rejected *)
   external z : int -> int = "x" "y" [@@zero_alloc] (* rejected *)
diff --git a/testsuite/tests/warnings/w53_zero_alloc_all.compilers.reference b/testsuite/tests/warnings/w53_zero_alloc_all.compilers.reference
index 58e0ac12e19..237da00852f 100644
--- a/testsuite/tests/warnings/w53_zero_alloc_all.compilers.reference
+++ b/testsuite/tests/warnings/w53_zero_alloc_all.compilers.reference
@@ -8,132 +8,122 @@ File "w53_zero_alloc_all.ml", line 20, characters 19-29:
                         ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53_zero_alloc_all.ml", line 21, characters 17-27:
-21 |   val x : int [@@zero_alloc] (* rejected *)
-                      ^^^^^^^^^^
-Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
-
-File "w53_zero_alloc_all.ml", line 22, characters 24-34:
-22 |   val f : int -> int [@@zero_alloc] (* rejected *)
-                             ^^^^^^^^^^
-Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
-
-File "w53_zero_alloc_all.ml", line 24, characters 22-32:
-24 |   external y : (int [@zero_alloc]) -> (int [@zero_alloc]) = "x" (* rejected *)
+File "w53_zero_alloc_all.ml", line 23, characters 22-32:
+23 |   external y : (int [@zero_alloc]) -> (int [@zero_alloc]) = "x" (* rejected *)
                            ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53_zero_alloc_all.ml", line 24, characters 45-55:
-24 |   external y : (int [@zero_alloc]) -> (int [@zero_alloc]) = "x" (* rejected *)
+File "w53_zero_alloc_all.ml", line 23, characters 45-55:
+23 |   external y : (int [@zero_alloc]) -> (int [@zero_alloc]) = "x" (* rejected *)
                                                   ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53_zero_alloc_all.ml", line 25, characters 39-49:
-25 |   external z : int -> int = "x" "y" [@@zero_alloc] (* rejected *)
+File "w53_zero_alloc_all.ml", line 24, characters 39-49:
+24 |   external z : int -> int = "x" "y" [@@zero_alloc] (* rejected *)
                                             ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53_zero_alloc_all.ml", line 26, characters 12-22:
-26 |   external[@zero_alloc] q : int -> int = "x" "y" (* rejected *)
+File "w53_zero_alloc_all.ml", line 25, characters 12-22:
+25 |   external[@zero_alloc] q : int -> int = "x" "y" (* rejected *)
                  ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53_zero_alloc_all.ml", line 28, characters 9-19:
-28 |   class[@zero_alloc] c : (* rejected *)
+File "w53_zero_alloc_all.ml", line 27, characters 9-19:
+27 |   class[@zero_alloc] c : (* rejected *)
               ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53_zero_alloc_all.ml", line 30, characters 11-21:
-30 |       val[@zero_alloc] foo : int * int (* rejected *)
+File "w53_zero_alloc_all.ml", line 29, characters 11-21:
+29 |       val[@zero_alloc] foo : int * int (* rejected *)
                 ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53_zero_alloc_all.ml", line 31, characters 11-21:
-31 |       val[@zero_alloc] bar : int -> int (* rejected *)
+File "w53_zero_alloc_all.ml", line 30, characters 11-21:
+30 |       val[@zero_alloc] bar : int -> int (* rejected *)
                 ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53_zero_alloc_all.ml", line 32, characters 14-24:
-32 |       method[@zero_alloc] baz : int * int (* rejected *)
+File "w53_zero_alloc_all.ml", line 31, characters 14-24:
+31 |       method[@zero_alloc] baz : int * int (* rejected *)
                    ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53_zero_alloc_all.ml", line 33, characters 14-24:
-33 |       method[@zero_alloc] boz : int -> int (* rejected *)
+File "w53_zero_alloc_all.ml", line 32, characters 14-24:
+32 |       method[@zero_alloc] boz : int -> int (* rejected *)
                    ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53_zero_alloc_all.ml", line 38, characters 21-31:
-38 |   type 'a t1 = 'a [@@zero_alloc] (* rejected *)
+File "w53_zero_alloc_all.ml", line 37, characters 21-31:
+37 |   type 'a t1 = 'a [@@zero_alloc] (* rejected *)
                           ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53_zero_alloc_all.ml", line 39, characters 19-29:
-39 |   type s1 = Foo1 [@zero_alloc] (* rejected *)
+File "w53_zero_alloc_all.ml", line 38, characters 19-29:
+38 |   type s1 = Foo1 [@zero_alloc] (* rejected *)
                         ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53_zero_alloc_all.ml", line 40, characters 22-32:
-40 |   let x : int = 42 [@@zero_alloc] (* rejected *)
+File "w53_zero_alloc_all.ml", line 39, characters 22-32:
+39 |   let x : int = 42 [@@zero_alloc] (* rejected *)
                            ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53_zero_alloc_all.ml", line 42, characters 7-17:
-42 |   let[@zero_alloc] w = 42 (* rejected *)
+File "w53_zero_alloc_all.ml", line 41, characters 7-17:
+41 |   let[@zero_alloc] w = 42 (* rejected *)
             ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53_zero_alloc_all.ml", line 46, characters 22-32:
-46 |   external y : (int [@zero_alloc]) -> (int [@zero_alloc]) = "x" (* rejected *)
+File "w53_zero_alloc_all.ml", line 45, characters 22-32:
+45 |   external y : (int [@zero_alloc]) -> (int [@zero_alloc]) = "x" (* rejected *)
                            ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53_zero_alloc_all.ml", line 46, characters 45-55:
-46 |   external y : (int [@zero_alloc]) -> (int [@zero_alloc]) = "x" (* rejected *)
+File "w53_zero_alloc_all.ml", line 45, characters 45-55:
+45 |   external y : (int [@zero_alloc]) -> (int [@zero_alloc]) = "x" (* rejected *)
                                                   ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53_zero_alloc_all.ml", line 47, characters 39-49:
-47 |   external z : int -> int = "x" "y" [@@zero_alloc] (* rejected *)
+File "w53_zero_alloc_all.ml", line 46, characters 39-49:
+46 |   external z : int -> int = "x" "y" [@@zero_alloc] (* rejected *)
                                             ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53_zero_alloc_all.ml", line 48, characters 12-22:
-48 |   external[@zero_alloc] q : int -> int = "x" "y" (* rejected *)
+File "w53_zero_alloc_all.ml", line 47, characters 12-22:
+47 |   external[@zero_alloc] q : int -> int = "x" "y" (* rejected *)
                  ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53_zero_alloc_all.ml", line 50, characters 9-19:
-50 |   class[@zero_alloc] foo _y = (* rejected *)
+File "w53_zero_alloc_all.ml", line 49, characters 9-19:
+49 |   class[@zero_alloc] foo _y = (* rejected *)
               ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53_zero_alloc_all.ml", line 52, characters 10-20:
-52 |     (fun[@zero_alloc] z -> (* rejected *)
+File "w53_zero_alloc_all.ml", line 51, characters 10-20:
+51 |     (fun[@zero_alloc] z -> (* rejected *)
                ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53_zero_alloc_all.ml", line 54, characters 11-21:
-54 |       val[@zero_alloc] bar = (4, 5) (* rejected *)
+File "w53_zero_alloc_all.ml", line 53, characters 11-21:
+53 |       val[@zero_alloc] bar = (4, 5) (* rejected *)
                 ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53_zero_alloc_all.ml", line 56, characters 14-24:
-56 |       method[@zero_alloc] baz x = (f (z+10), x+1) (* rejected *)
+File "w53_zero_alloc_all.ml", line 55, characters 14-24:
+55 |       method[@zero_alloc] baz x = (f (z+10), x+1) (* rejected *)
                    ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53_zero_alloc_all.ml", line 68, characters 14-24:
-68 |     ((boz x)[@zero_alloc assume]) (* rejected *)
+File "w53_zero_alloc_all.ml", line 67, characters 14-24:
+67 |     ((boz x)[@zero_alloc assume]) (* rejected *)
                    ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53_zero_alloc_all.ml", line 73, characters 7-17:
-73 |   let[@zero_alloc assume] foo = (* rejected *)
+File "w53_zero_alloc_all.ml", line 72, characters 7-17:
+72 |   let[@zero_alloc assume] foo = (* rejected *)
             ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
 
-File "w53_zero_alloc_all.ml", line 77, characters 7-17:
-77 |   let[@zero_alloc] bar = (* rejected *)
+File "w53_zero_alloc_all.ml", line 76, characters 7-17:
+76 |   let[@zero_alloc] bar = (* rejected *)
             ^^^^^^^^^^
 Warning 53 [misplaced-attribute]: the "zero_alloc" attribute cannot appear in this context
diff --git a/testsuite/tests/warnings/w53_zero_alloc_all.ml b/testsuite/tests/warnings/w53_zero_alloc_all.ml
index 16a5c737395..84e49a4a6e3 100644
--- a/testsuite/tests/warnings/w53_zero_alloc_all.ml
+++ b/testsuite/tests/warnings/w53_zero_alloc_all.ml
@@ -18,8 +18,7 @@
 module type TestZeroAllocSig = sig
   type 'a t1 = 'a [@@zero_alloc] (* rejected *)
   type s1 = Foo1 [@zero_alloc] (* rejected *)
-  val x : int [@@zero_alloc] (* rejected *)
-  val f : int -> int [@@zero_alloc] (* rejected *)
+  val f : int -> int [@@zero_alloc] (* accepted *)
 
   external y : (int [@zero_alloc]) -> (int [@zero_alloc]) = "x" (* rejected *)
   external z : int -> int = "x" "y" [@@zero_alloc] (* rejected *)
diff --git a/toplevel/native/topeval.ml b/toplevel/native/topeval.ml
index c4ef03b4351..26afa34abba 100644
--- a/toplevel/native/topeval.ml
+++ b/toplevel/native/topeval.ml
@@ -132,7 +132,8 @@ let name_expression ~loc ~attrs sort exp =
       val_kind = Val_reg;
       val_loc = loc;
       val_attributes = attrs;
-      val_uid = Uid.internal_not_actually_unique; }
+      val_uid = Uid.internal_not_actually_unique;
+      val_zero_alloc = Default_check }
    in
    let sg = [Sig_value(id, vd, Exported)] in
    let pat =
diff --git a/typing/includecore.ml b/typing/includecore.ml
index 4c1236d05f5..55a90ed81d9 100644
--- a/typing/includecore.ml
+++ b/typing/includecore.ml
@@ -22,6 +22,8 @@ open Typedtree
 
 type position = Errortrace.position = First | Second
 
+module ZA = Zero_alloc_utils
+
 (* Inclusion between value descriptions *)
 
 type primitive_mismatch =
@@ -40,6 +42,8 @@ type value_mismatch =
   | Primitive_mismatch of primitive_mismatch
   | Not_a_primitive
   | Type of Errortrace.moregen_error
+  | Zero_alloc of { missing_entirely : bool }
+  | Zero_alloc_arity of int * int
 
 exception Dont_match of value_mismatch
 
@@ -86,6 +90,70 @@ let primitive_descriptions pd1 pd2 =
   else
     native_repr_args pd1.prim_native_repr_args pd2.prim_native_repr_args
 
+let zero_alloc za1 za2 =
+  (* The core of the check here is that we translate both attributes into the
+     abstract domain and use the existing inclusion check from there, ensuring
+     what we do in the typechecker matches the backend.
+
+     There are a few additional details:
+
+     - [opt] is not captured by the abstract domain, so we need a special check
+       for it.  But it doesn't interact at all with the abstract domain - it's
+       just about whether or not the check happens - so this special check can
+       be fully separate.
+     - [arity] is also not captured by the abstract domain - it exists only for
+       use here, in typechecking.  If the arities do not match, we issue an
+       error. It's essential for the soundness of the way we (will, in the next
+       PR) use zero_alloc in signatures that the apparent arity of the type in
+       the signature matches the syntactic arity of the function.
+     - [ignore] can not appear in zero_alloc attributes in signatures, and is
+       erased from structure items when computing their signature, so we don't
+       need to consider it here.
+     *)
+  let open Builtin_attributes in
+  (* abstract domain check *)
+  let abstract_value za =
+    match za with
+    | Default_check | Ignore_assert_all _ -> ZA.Assume_info.Value.top ()
+    | Check { strict; _ } ->
+      ZA.Assume_info.Value.of_annotation ~strict ~never_returns_normally:false
+    | Assume { strict; never_returns_normally } ->
+      ZA.Assume_info.Value.of_annotation ~strict ~never_returns_normally
+  in
+  let v1 = abstract_value za1 in
+  let v2 = abstract_value za2 in
+  if not (ZA.Assume_info.Value.lessequal v1 v2) then
+    begin let missing_entirely =
+        match za1 with
+        | Default_check -> true
+        | Ignore_assert_all _ | Check _ | Assume _ -> false
+      in
+      raise (Dont_match (Zero_alloc {missing_entirely}))
+    end;
+  (* opt check *)
+  begin match za1, za2 with
+  | Check { opt = opt1; _ }, Check { opt = opt2; _ } ->
+    if opt1 && not opt2 then
+      raise (Dont_match (Zero_alloc {missing_entirely = false}))
+  | (Check _ | Default_check | Assume _ | Ignore_assert_all _), _ -> ()
+  end;
+  (* arity check *)
+  let get_arity = function
+    | Check { arity; _ } | Assume { arity; _ } -> Some arity
+    | Default_check | Ignore_assert_all _ -> None
+  in
+  match get_arity za1, get_arity za2 with
+  | Some arity1, Some arity2 ->
+    (* Check *)
+    if not (arity1 = arity2) then
+      raise (Dont_match (Zero_alloc_arity (arity1, arity2)))
+  | Some _, None -> ()
+    (* Forgetting zero_alloc info is fine *)
+  | None, Some _ ->
+    (* Fabricating it is not, but earlier cases should have ruled this out *)
+    Misc.fatal_error "Includecore.check_attributes"
+  | None, None -> ()
+
 let value_descriptions ~loc env name
     (vd1 : Types.value_description)
     (vd2 : Types.value_description) =
@@ -95,6 +163,7 @@ let value_descriptions ~loc env name
     loc
     vd1.val_attributes vd2.val_attributes
     name;
+  zero_alloc vd1.val_zero_alloc vd2.val_zero_alloc;
   match vd1.val_kind with
   | Val_prim p1 -> begin
      match vd2.val_kind with
@@ -303,6 +372,17 @@ let report_value_mismatch first second env ppf err =
       Printtyp.report_moregen_error ppf Type_scheme env trace
         (fun ppf -> Format.fprintf ppf "The type")
         (fun ppf -> Format.fprintf ppf "is not compatible with the type")
+  | Zero_alloc { missing_entirely } ->
+    pr "The former provides a weaker \"zero_alloc\" guarantee than the latter.";
+    if missing_entirely then
+      pr "@ Hint: Add a \"zero_alloc\" attribute (without opt) to the \
+          implementation."
+  | Zero_alloc_arity (n1, n2) ->
+    pr "zero_alloc arity mismatch:@ \
+        When using \"zero_alloc\" in a signature, the syntactic arity of@ \
+        the implementation must match the function type in the interface.@ \
+        Here the former is %d and the latter is %d."
+      n1 n2
 
 let report_type_inequality env ppf err =
   Printtyp.report_equality_error ppf Type_scheme env err
diff --git a/typing/includecore.mli b/typing/includecore.mli
index 055c8467967..aac298595de 100644
--- a/typing/includecore.mli
+++ b/typing/includecore.mli
@@ -36,6 +36,8 @@ type value_mismatch =
   | Primitive_mismatch of primitive_mismatch
   | Not_a_primitive
   | Type of Errortrace.moregen_error
+  | Zero_alloc of { missing_entirely : bool }
+  | Zero_alloc_arity of int * int
 
 exception Dont_match of value_mismatch
 
diff --git a/typing/printtyp.ml b/typing/printtyp.ml
index c3b42d99bde..d1c3b1f529f 100644
--- a/typing/printtyp.ml
+++ b/typing/printtyp.ml
@@ -1980,11 +1980,43 @@ let tree_of_value_description id decl =
   (* Important: process the fvs *after* the type; tree_of_type_scheme
      resets the naming context *)
   let qtvs = extract_qtvs [decl.val_type] in
+  let apparent_arity =
+    let rec count n typ =
+      match get_desc typ with
+      | Tarrow (_,_,typ,_) -> count (n+1) typ
+      | _ -> n
+    in
+    count 0 decl.val_type
+  in
+  let attrs =
+    match decl.val_zero_alloc with
+    | Default_check | Ignore_assert_all _ -> []
+    | Check { strict; opt; arity; _ } ->
+      [{ oattr_name =
+           String.concat ""
+             ["zero_alloc";
+              if strict then " strict" else "";
+              if opt then " opt" else "";
+              if arity = apparent_arity then "" else
+                Printf.sprintf " arity %d" arity;
+             ] }]
+    | Assume { strict; never_returns_normally; arity; _ } ->
+      [{ oattr_name =
+           String.concat ""
+             ["zero_alloc assume";
+              if strict then " strict" else "";
+              if never_returns_normally then " never_returns_normally" else "";
+              if arity = apparent_arity then "" else
+                Printf.sprintf " arity %d" arity;
+             ]
+       }]
+  in
   let vd =
     { oval_name = id;
       oval_type = Otyp_poly(qtvs, ty);
       oval_prims = [];
-      oval_attributes = [] }
+      oval_attributes = attrs
+    }
   in
   let vd =
     match decl.val_kind with
diff --git a/typing/subst.ml b/typing/subst.ml
index bbb5ec8b175..05ebf646f1e 100644
--- a/typing/subst.ml
+++ b/typing/subst.ml
@@ -740,6 +740,7 @@ let rec subst_lazy_value_description s descr =
   { val_type = Wrap.substitute ~compose Keep s descr.val_type;
     val_kind = descr.val_kind;
     val_loc = loc s descr.val_loc;
+    val_zero_alloc = descr.val_zero_alloc;
     val_attributes = attrs s descr.val_attributes;
     val_uid = descr.val_uid;
   }
diff --git a/typing/typeclass.ml b/typing/typeclass.ml
index 69bb192f6ce..ac538a346b7 100644
--- a/typing/typeclass.ml
+++ b/typing/typeclass.ml
@@ -446,7 +446,7 @@ and class_type_aux env virt self_scope scty =
         match l with
         | Position _ -> ctyp Ttyp_call_pos (Ctype.newconstr Predef.path_lexing_position [])
         | Optional _ | Labelled _ | Nolabel ->
-          transl_simple_type ~new_var_jkind:Any env ~closed:false Alloc.Const.legacy sty 
+          transl_simple_type ~new_var_jkind:Any env ~closed:false Alloc.Const.legacy sty
       in
       let ty = cty.ctyp_type in
       let ty =
@@ -489,6 +489,7 @@ let enter_ancestor_met ~loc name ~sign ~meths ~cl_num ~ty ~attrs met_env =
   let desc =
     { val_type = ty; val_kind = kind;
       val_attributes = attrs;
+      val_zero_alloc = Builtin_attributes.Default_check;
       Types.val_loc = loc;
       val_uid = Uid.mk ~current_unit:(Env.get_unit_name ()) }
   in
@@ -504,6 +505,7 @@ let add_self_met loc id sign self_var_kind vars cl_num
   let desc =
     { val_type = ty; val_kind = kind;
       val_attributes = attrs;
+      val_zero_alloc = Builtin_attributes.Default_check;
       Types.val_loc = loc;
       val_uid = Uid.mk ~current_unit:(Env.get_unit_name ()) }
   in
@@ -520,6 +522,7 @@ let add_instance_var_met loc label id sign cl_num attrs met_env =
     { val_type = ty; val_kind = kind;
       val_attributes = attrs;
       Types.val_loc = loc;
+      val_zero_alloc = Builtin_attributes.Default_check;
       val_uid = Uid.mk ~current_unit:(Env.get_unit_name ()) }
   in
   Env.add_value id desc met_env
@@ -1266,10 +1269,10 @@ and class_expr_aux cl_num val_env met_env virt self_scope scl =
       if not_nolabel_function cl.cl_type then begin
         match l with
         | Nolabel | Labelled _ -> ()
-        | Optional _ -> 
+        | Optional _ ->
           Location.prerr_warning pat.pat_loc
             Warnings.Unerasable_optional_argument;
-        | Position _ -> 
+        | Position _ ->
           Location.prerr_warning pat.pat_loc
             Warnings.Unerasable_position_argument;
       end;
@@ -1350,7 +1353,7 @@ and class_expr_aux cl_num val_env met_env virt self_scope scl =
                        (not optional && l' = Nolabel)
                     then
                       (remaining_sargs, use_arg sarg l')
-                    else if optional && label_is_absent_in_remaining_args () 
+                    else if optional && label_is_absent_in_remaining_args ()
                     then (sargs, eliminate_optional_arg ())
                     else if Btype.is_position l && label_is_absent_in_remaining_args ()
                     then (sargs, eliminate_position_arg ())
@@ -1414,7 +1417,7 @@ and class_expr_aux cl_num val_env met_env virt self_scope scl =
         Typecore.type_let In_class_def val_env rec_flag sdefs in
       let (vals, met_env) =
         List.fold_right
-          (fun (id, modes_and_sorts) (vals, met_env) ->
+          (fun (id, modes_and_sorts, _) (vals, met_env) ->
              List.iter
                (fun (loc, mode, sort) ->
                   Typecore.escape ~loc ~env:val_env ~reason:Other mode;
@@ -1447,6 +1450,7 @@ and class_expr_aux cl_num val_env met_env virt self_scope scl =
                {val_type = expr.exp_type;
                 val_kind = Val_ivar (Immutable, cl_num);
                 val_attributes = [];
+                val_zero_alloc = Builtin_attributes.Default_check;
                 Types.val_loc = vd.val_loc;
                 val_uid = vd.val_uid;
                }
@@ -1455,7 +1459,7 @@ and class_expr_aux cl_num val_env met_env virt self_scope scl =
              ((id', expr)
               :: vals,
               Env.add_value id' desc met_env))
-          (let_bound_idents_with_modes_and_sorts defs)
+          (let_bound_idents_with_modes_sorts_and_checks defs)
           ([], met_env)
       in
       let cl = class_expr cl_num val_env met_env virt self_scope scl' in
diff --git a/typing/typecore.ml b/typing/typecore.ml
index 969210c2114..6eb492a77b5 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -1091,11 +1091,13 @@ let iter_pattern_variables_type f : pattern_variable list -> unit =
 
 let add_pattern_variables ?check ?check_as env pv =
   List.fold_right
-    (fun {pv_id; pv_uid; pv_mode; pv_type; pv_loc; pv_as_var; pv_attributes} env ->
+    (fun {pv_id; pv_uid; pv_mode; pv_type; pv_loc; pv_as_var; pv_attributes}
+      env ->
        let check = if pv_as_var then check_as else check in
        Env.add_value ?check ~mode:pv_mode pv_id
          {val_type = pv_type; val_kind = Val_reg; Types.val_loc = pv_loc;
           val_attributes = pv_attributes;
+          val_zero_alloc = Builtin_attributes.Default_check;
           val_uid = pv_uid
          } env
     )
@@ -2879,6 +2881,7 @@ let type_class_arg_pattern cl_num val_env met_env l spat =
             { val_type = pv_type
             ; val_kind = Val_reg
             ; val_attributes = pv_attributes
+            ; val_zero_alloc = Builtin_attributes.Default_check
             ; val_loc = pv_loc
             ; val_uid = pv_uid
             }
@@ -2889,6 +2892,7 @@ let type_class_arg_pattern cl_num val_env met_env l spat =
             { val_type = pv_type
             ; val_kind = Val_ivar (Immutable, cl_num)
             ; val_attributes = pv_attributes
+            ; val_zero_alloc = Builtin_attributes.Default_check
             ; val_loc = pv_loc
             ; val_uid = pv_uid
             }
@@ -5035,7 +5039,12 @@ let add_check_attribute expr attributes =
   in
   match expr.exp_desc with
   | Texp_function fn ->
-    begin match get_property_attribute attributes Zero_alloc with
+    let default_arity = function_arity fn.params fn.body in
+    let za =
+      get_property_attribute ~in_signature:false ~default_arity attributes
+        Zero_alloc
+    in
+    begin match za with
     | Default_check -> expr
     | (Ignore_assert_all _ | Check _ | Assume _) as check ->
       begin match fn.zero_alloc with
@@ -5377,9 +5386,10 @@ and type_expect_
         type_application env loc expected_mode pm funct funct_mode sargs rt
       in
       let assume_zero_alloc =
+        let default_arity = List.length args in
         let zero_alloc =
-          Builtin_attributes.get_property_attribute sfunct.pexp_attributes
-            Zero_alloc
+          Builtin_attributes.get_property_attribute ~in_signature:false
+            ~default_arity sfunct.pexp_attributes Zero_alloc
         in
         Builtin_attributes.assume_zero_alloc ~is_check_allowed:false zero_alloc
       in
@@ -7391,6 +7401,7 @@ and type_argument ?explanation ?recarg env (mode : expected_mode) sarg
         let desc =
           { val_type = ty; val_kind = Val_reg;
             val_attributes = [];
+            val_zero_alloc = Builtin_attributes.Default_check;
             val_loc = Location.none;
             val_uid = Uid.mk ~current_unit:(Env.get_unit_name ());
           }
@@ -8764,7 +8775,7 @@ and type_n_ary_function
         region_locked;
       }
     in
-    let { function_ = exp_type, params, body;
+    let { function_ = exp_type, result_params, body;
           newtypes; params_contain_gadt = contains_gadt;
           ret_info; fun_alloc_mode;
         } =
@@ -8783,6 +8794,8 @@ and type_n_ary_function
             "[ret_info] can't be None -- that indicates a function with \
              no parameters."
     in
+    let params = List.map (fun { param } -> param) result_params in
+    let syntactic_arity = function_arity params body in
     (* Require that the n-ary function is known to have at least n arrows
         in the type. This prevents GADT equations introduced by the parameters
         from hiding arrows from the resulting type.
@@ -8829,12 +8842,6 @@ and type_n_ary_function
                       "Jkind_error not expected as this point; this should \
                        have been caught when the function was typechecked."
               in
-              let syntactic_arity =
-                List.length params +
-                (match body with
-                | Tfunction_body _ -> 0
-                | Tfunction_cases _ -> 1)
-              in
               let err =
                 Function_arity_type_clash
                   { syntactic_arity;
@@ -8849,7 +8856,7 @@ and type_n_ary_function
               filter_ty_ret_exn ret_ty param.fp_arg_label
                 ~force_tpoly:(not has_poly))
             exp_type
-            params
+            result_params
         in
         match body with
         | Tfunction_body _ -> ()
@@ -8857,9 +8864,9 @@ and type_n_ary_function
             ignore
               (filter_ty_ret_exn ret_ty Nolabel ~force_tpoly:true : type_expr)
     end;
-    let params = List.map (fun { param } -> param) params in
     let zero_alloc =
-      Builtin_attributes.get_property_attribute attributes Zero_alloc
+      Builtin_attributes.get_property_attribute ~in_signature:false
+        ~default_arity:syntactic_arity attributes Zero_alloc
     in
     re
       { exp_desc =
diff --git a/typing/typedecl.ml b/typing/typedecl.ml
index fa1c30736e4..a62dcf8c395 100644
--- a/typing/typedecl.ml
+++ b/typing/typedecl.ml
@@ -117,6 +117,10 @@ type error =
   | Modalities_on_value_description
   | Missing_unboxed_attribute_on_non_value_sort of Jkind.Sort.const
   | Non_value_sort_not_upstream_compatible of Jkind.Sort.const
+  | Zero_alloc_attr_unsupported of Builtin_attributes.check_attribute
+  | Zero_alloc_attr_non_function
+  | Zero_alloc_attr_bad_user_arity
+  | Zero_alloc_attr_opt
 
 open Typedtree
 
@@ -2668,8 +2672,35 @@ let transl_value_decl env loc valdecl =
   let v =
   match valdecl.pval_prim with
     [] when Env.is_in_signature env ->
+      let default_arity =
+        let rec count_arrows n ty =
+          match get_desc ty with
+          | Tarrow (_, _, t2, _) -> count_arrows (n+1) t2
+          | _ -> n
+        in
+        count_arrows 0 ty
+      in
+      let zero_alloc =
+        Builtin_attributes.get_property_attribute ~in_signature:true
+          ~default_arity valdecl.pval_attributes Zero_alloc
+      in
+      begin match zero_alloc with
+      | Default_check -> ()
+      | Check za ->
+        if default_arity = 0 && za.arity <= 0 then
+          raise (Error(valdecl.pval_loc, Zero_alloc_attr_non_function));
+        if za.arity <= 0 then
+          raise (Error(valdecl.pval_loc, Zero_alloc_attr_bad_user_arity));
+        if za.opt then
+          (* CR ccasinghino: It would be nice to support opt, but it's not
+             obvious what its meaning should be. *)
+          raise (Error(valdecl.pval_loc, Zero_alloc_attr_opt));
+      | Assume _ | Ignore_assert_all _ ->
+        raise (Error(valdecl.pval_loc, Zero_alloc_attr_unsupported zero_alloc))
+      end;
       { val_type = ty; val_kind = Val_reg; Types.val_loc = loc;
         val_attributes = valdecl.pval_attributes;
+        val_zero_alloc = zero_alloc;
         val_uid = Uid.mk ~current_unit:(Env.get_unit_name ());
       }
   | [] ->
@@ -2709,6 +2740,7 @@ let transl_value_decl env loc valdecl =
       check_unboxable env loc ty;
       { val_type = ty; val_kind = Val_prim prim; Types.val_loc = loc;
         val_attributes = valdecl.pval_attributes;
+        val_zero_alloc = Builtin_attributes.Default_check;
         val_uid = Uid.mk ~current_unit:(Env.get_unit_name ());
       }
   in
@@ -3461,6 +3493,26 @@ let report_error ppf = function
          the use of -extension-universe (no_extensions|\
          upstream_compatible).@]"
       Jkind.Sort.format_const sort
+  | Zero_alloc_attr_unsupported ca ->
+      let variety = match ca with
+        | Default_check | Check _ -> assert false
+        | Assume _ -> "assume"
+        | Ignore_assert_all _ -> "ignore"
+      in
+      fprintf ppf
+        "@[zero_alloc \"%s\" attributes are not supported in signatures@]"
+        variety
+  | Zero_alloc_attr_non_function ->
+    fprintf ppf
+      "@[In signatures, zero_alloc is only supported on function declarations.\
+         @ Found no arrows in this declaration's type.\
+         @ Hint: You can write \"[@zero_alloc arity n]\" to specify the arity\
+         @ of an alias (for n > 0).@]"
+  | Zero_alloc_attr_bad_user_arity ->
+    fprintf ppf
+      "@[Invalid zero_alloc attribute: arity must be greater than 0.@]"
+  | Zero_alloc_attr_opt ->
+    fprintf ppf "@[\"zero_alloc opt\" is not supported in signatures.@]"
 
 let () =
   Location.register_error_of_exn
diff --git a/typing/typedecl.mli b/typing/typedecl.mli
index 4b0c86183ce..89ec6e3d183 100644
--- a/typing/typedecl.mli
+++ b/typing/typedecl.mli
@@ -161,6 +161,10 @@ type error =
   | Modalities_on_value_description
   | Missing_unboxed_attribute_on_non_value_sort of Jkind.Sort.const
   | Non_value_sort_not_upstream_compatible of Jkind.Sort.const
+  | Zero_alloc_attr_unsupported of Builtin_attributes.check_attribute
+  | Zero_alloc_attr_non_function
+  | Zero_alloc_attr_bad_user_arity
+  | Zero_alloc_attr_opt
 
 exception Error of Location.t * error
 
diff --git a/typing/typedtree.ml b/typing/typedtree.ml
index b00766a267b..0d3463283a2 100644
--- a/typing/typedtree.ml
+++ b/typing/typedtree.ml
@@ -1037,16 +1037,27 @@ let rev_let_bound_idents_full bindings =
   List.iter (fun vb -> iter_bound_idents add vb.vb_pat) bindings;
   !idents_full
 
-let let_bound_idents_with_modes_and_sorts bindings =
+let let_bound_idents_with_modes_sorts_and_checks bindings =
   let modes_and_sorts = Ident.Tbl.create 3 in
   let f id sloc _ _uid mode sort =
     Ident.Tbl.add modes_and_sorts id (sloc.loc, mode, sort)
   in
-  List.iter (fun vb ->
-    iter_pattern_full ~both_sides_of_or:true f vb.vb_sort vb.vb_pat)
-    bindings;
+  let checks =
+    List.fold_left (fun checks vb ->
+      iter_pattern_full ~both_sides_of_or:true f vb.vb_sort vb.vb_pat;
+       match vb.vb_pat.pat_desc, vb.vb_expr.exp_desc with
+       | Tpat_var (id, _, _, _), Texp_function fn ->
+         Ident.Map.add id fn.zero_alloc checks
+       | _ -> checks
+    ) Ident.Map.empty bindings
+  in
   List.rev_map
-    (fun (id, _, _, _) -> id, List.rev (Ident.Tbl.find_all modes_and_sorts id))
+    (fun (id, _, _, _) ->
+       let zero_alloc =
+         Option.value (Ident.Map.find_opt id checks)
+           ~default:Builtin_attributes.Default_check
+       in
+       id, List.rev (Ident.Tbl.find_all modes_and_sorts id), zero_alloc)
     (rev_let_bound_idents_full bindings)
 
 let let_bound_idents_full bindings =
@@ -1124,3 +1135,9 @@ let rec exp_is_nominal exp =
   | Texp_field (parent, _, _, _) | Texp_send (parent, _, _) ->
       exp_is_nominal parent
   | _ -> false
+
+let function_arity params body =
+  List.length params +
+  match body with
+  | Tfunction_body _ -> 0
+  | Tfunction_cases _ -> 1
diff --git a/typing/typedtree.mli b/typing/typedtree.mli
index c290b11f442..47fa558ac99 100644
--- a/typing/typedtree.mli
+++ b/typing/typedtree.mli
@@ -1107,9 +1107,23 @@ val exists_pattern: (pattern -> bool) -> pattern -> bool
 val let_bound_idents: value_binding list -> Ident.t list
 val let_bound_idents_full:
     value_binding list -> (Ident.t * string loc * Types.type_expr * Uid.t) list
-val let_bound_idents_with_modes_and_sorts:
+
+(* [let_bound_idents_with_modes_sorts_and_checks] finds all the idents in the
+   let bindings and computes their modes, sorts, and whether they have any check
+   attributes (zero_alloc).
+
+   Note that:
+   * The list associated with each ident can only have more than one element in
+     the case of or pattern, where the ident is bound on both sides.
+   * We return just one check_attribute per identifier, because this attribute
+     can only be something other than [Default_check] in the case of a simple
+     variable pattern bound to a function (in which case the list will also
+     have just one element).
+*)
+val let_bound_idents_with_modes_sorts_and_checks:
   value_binding list
-  -> (Ident.t * (Location.t * Mode.Value.l * Jkind.sort) list) list
+  -> (Ident.t * (Location.t * Mode.Value.l * Jkind.sort) list
+              * Builtin_attributes.check_attribute) list
 
 (** Alpha conversion of patterns *)
 val alpha_pat:
@@ -1132,3 +1146,6 @@ val split_pattern:
 (** Whether an expression looks nice as the subject of a sentence in a error
     message. *)
 val exp_is_nominal : expression -> bool
+
+(** Calculates the syntactic arity of a function based on its parameters and body. *)
+val function_arity : function_param list -> function_body -> int
diff --git a/typing/typemod.ml b/typing/typemod.ml
index 3700eedcd8d..89f9a330f9c 100644
--- a/typing/typemod.ml
+++ b/typing/typemod.ml
@@ -2795,7 +2795,7 @@ and type_structure ?(toplevel = None) funct_body anchor env sstr =
            will be marked as being used during the signature inclusion test. *)
         let items, shape_map =
           List.fold_left
-            (fun (acc, shape_map) (id, modes) ->
+            (fun (acc, shape_map) (id, id_info, zero_alloc) ->
               List.iter
                 (fun (loc, mode, sort) ->
                    Typecore.escape ~loc ~env:newenv ~reason:Other mode;
@@ -2806,16 +2806,35 @@ and type_structure ?(toplevel = None) funct_body anchor env sstr =
                    then raise (Error (loc, env,
                                    Toplevel_nonvalue (Ident.name id,sort)))
                 )
-                modes;
-              let (first_loc, _, _) = List.hd modes in
+                id_info;
+              let zero_alloc =
+                (* We only allow "Check" attributes in signatures.  Here we
+                   convert "Assume"s in structures to the equivalent "Check" for
+                   the signature. *)
+                let open Builtin_attributes in
+                match[@warning "+9"] zero_alloc with
+                | Default_check | Ignore_assert_all _ -> Default_check
+                | Check c when not c.opt -> zero_alloc
+                | Check _ ->
+                  (* CR ccasinghino: We'd like to allow opt in signatures, but
+                     for now we don't, and must make sure you can't get it in a
+                     signature by writing it in a structure and using module
+                     type of. *)
+                  Default_check
+                | Assume { property; strict; arity; loc;
+                           never_returns_normally = _ } ->
+                  Check { strict; property; arity; loc; opt = false }
+              in
+              let (first_loc, _, _) = List.hd id_info in
               Signature_names.check_value names first_loc id;
               let vd =  Env.find_value (Pident id) newenv in
               let vd = Subst.Lazy.force_value_description vd in
+              let vd = { vd with val_zero_alloc = zero_alloc } in
               Sig_value(id, vd, Exported) :: acc,
               Shape.Map.add_value shape_map id vd.val_uid
             )
             ([], shape_map)
-            (let_bound_idents_with_modes_and_sorts defs)
+            (let_bound_idents_with_modes_sorts_and_checks defs)
         in
         Tstr_value(rec_flag, defs),
         List.rev items,
diff --git a/typing/types.ml b/typing/types.ml
index 6e89ced5eeb..759d18ee67b 100644
--- a/typing/types.ml
+++ b/typing/types.ml
@@ -412,6 +412,7 @@ module type Wrapped = sig
     { val_type: type_expr wrapped;                (* Type of the value *)
       val_kind: value_kind;
       val_loc: Location.t;
+      val_zero_alloc: Builtin_attributes.check_attribute;
       val_attributes: Parsetree.attributes;
       val_uid: Uid.t;
     }
@@ -486,10 +487,12 @@ module Map_wrapped(From : Wrapped)(To : Wrapped) = struct
       | Unit -> To.Unit
       | Named (id,mty) -> To.Named (id, module_type m mty)
 
-  let value_description m {val_type; val_kind; val_attributes; val_loc; val_uid} =
+  let value_description m {val_type; val_kind; val_zero_alloc;
+                           val_attributes; val_loc; val_uid} =
     To.{
       val_type = m.map_type_expr m val_type;
       val_kind;
+      val_zero_alloc;
       val_attributes;
       val_loc;
       val_uid
diff --git a/typing/types.mli b/typing/types.mli
index 909bed2f1a8..3a3c9838fec 100644
--- a/typing/types.mli
+++ b/typing/types.mli
@@ -709,6 +709,7 @@ module type Wrapped = sig
     { val_type: type_expr wrapped;                (* Type of the value *)
       val_kind: value_kind;
       val_loc: Location.t;
+      val_zero_alloc: Builtin_attributes.check_attribute;
       val_attributes: Parsetree.attributes;
       val_uid: Uid.t;
     }
diff --git a/utils/zero_alloc_utils.ml b/utils/zero_alloc_utils.ml
index 4f79ddeac41..80160608252 100644
--- a/utils/zero_alloc_utils.ml
+++ b/utils/zero_alloc_utils.ml
@@ -30,6 +30,8 @@
 module type WS = sig
   type t
 
+  val empty : t
+
   val join : t -> t -> t
 
   val meet : t -> t -> t
@@ -135,6 +137,10 @@ module Make (Witnesses : WS) = struct
 
     let relaxed w = { nor = V.Safe; exn = V.Top w; div = V.Top w }
 
+    let of_annotation ~strict ~never_returns_normally =
+      let res = if strict then safe else relaxed Witnesses.empty in
+      if never_returns_normally then { res with nor = V.Bot } else res
+
     let print ~witnesses ppf { nor; exn; div } =
       let pp = V.print ~witnesses in
       Format.fprintf ppf "{ nor=%a; exn=%a; div=%a }" pp nor pp exn pp div
@@ -206,11 +212,7 @@ module Assume_info = struct
   let none = No_assume
 
   let create ~strict ~never_returns_normally =
-    let res = if strict then Value.safe else Value.relaxed Witnesses.empty in
-    let res =
-      if never_returns_normally then { res with nor = V.Bot } else res
-    in
-    Assume res
+    Assume (Value.of_annotation ~strict ~never_returns_normally)
 
   let get_value t = match t with No_assume -> None | Assume v -> Some v
 
diff --git a/utils/zero_alloc_utils.mli b/utils/zero_alloc_utils.mli
index b0e4d85ad17..cd021faa7c2 100644
--- a/utils/zero_alloc_utils.mli
+++ b/utils/zero_alloc_utils.mli
@@ -6,6 +6,8 @@
 module type WS = sig
   type t
 
+  val empty : t
+
   val join : t -> t -> t
 
   val meet : t -> t -> t
@@ -80,6 +82,9 @@ module Make (Witnesses : WS) : sig
         (i.e., [nor] component is Safe, others are Top.  *)
     val relaxed : Witnesses.t -> t
 
+    (** Constructs a value from a user annotation. The witness will be empty. *)
+    val of_annotation : strict:bool -> never_returns_normally:bool -> t
+
     val print : witnesses:bool -> Format.formatter -> t -> unit
 
     (** Use [compare] for structural comparison of terms, for example
@@ -127,6 +132,8 @@ module Assume_info : sig
   module Witnesses : sig
     type t = unit
 
+    val empty : t
+
     val join : t -> t -> t
 
     val lessequal : t -> t -> bool