Require mutability backing in private-row signature inclusion

The private/open-object manifest path in includecore compared paired
fields by type only, so a signature could declare
type t = private {..@set "x": int} over an implementation whose field was
not settable - and since access follows the published row, clients could
write straight through the abstraction. In the phantom-setter encoding
this could not happen structurally: granting required an interface
"x#=" member with no implementation partner (rejected by the missing-
field check), while forgetting was the interface simply omitting the
member (absorbed by the ignored implementation-side misses). Stage D
turned the capability into a flag on the field, and nothing had taken
over the width mechanism's job.

The pairing now requires a settable implementation field wherever the
interface field is settable; an implementation's settable field may
still be abstracted to a read-only one. Probe-verified equivalent to the
released (phantom-encoding) compiler in all directions, including that
paired field types remain compared by equality - private rows allow
width and capability forgetting, never depth subtyping.

The @set inclusion matrix is now pinned per comparison arm, since the
flag participates in several independently-changeable relations:
object_private_row_grants_set (the new includecore rule),
object_manifest_set_mismatch (transparent manifests are equations -
eqtype), object_value_signature_set_mismatch (value signatures claim
instances - moregeneral), and the legal forgetting direction compiles in
object_mutability_pin.res.

Signed-Off-By: Cristiano Calcagno <ccrisccris@gmail.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PCtQiaDijUqA2fujQXvKUw

Author: cristianoc

compiler/ml/includecore.ml

@@ -137,6 +137,15 @@ let type_manifest env ty1 params1 ty2 params2 priv2 =
     &&
     let pairs, _miss1, miss2 = Ctype.associate_fields fields1 fields2 in
     miss2 = []
+    (* The signature must not grant write capability the implementation
+          lacks; an implementation's settable field may be abstracted to a
+          read-only one. *)
+    && List.for_all
+         (fun ((f1 : Ctype.field_info), (f2 : Ctype.field_info)) ->
+           match Btype.mutability_repr f2.f_mut with
+           | Mutable -> Btype.mutability_repr f1.f_mut = Asttypes.Mutable
+           | Immutable -> true)
+         pairs
     &&
     let tl1, tl2 =
       List.split

tests/ERROR_VARIANTS.md

@@ -363,7 +363,7 @@ Wrapper symptoms attached to inclusion failures. Source: [includemod.ml:23](../c
 | Variant | Status | Fixture | Notes |
 |---|---|---|---|
 | `Missing_field` | ✓ | `super_errors_multi/Iface_missing_value` | |
-| `Value_descriptions` | ✓ | `super_errors_multi/Iface_value_descriptions`, `super_errors_multi/Iface_value_arity_mismatch`, `super_errors_multi/Smoke_interface_mismatch`, `super_errors_multi/Cross_external_spec_mismatch`, `super_errors_multi/Cross_external_payload_name`, `super_errors_multi/Cross_external_import_attrs`, `module_sig_value_arity_mismatch*.res` | Arity mismatches print a dedicated hint (implementation vs interface argument counts), including through aliases and nested function types. |
+| `Value_descriptions` | ✓ | `super_errors_multi/Iface_value_descriptions`, `super_errors_multi/Iface_value_arity_mismatch`, `super_errors_multi/Smoke_interface_mismatch`, `super_errors_multi/Cross_external_spec_mismatch`, `super_errors_multi/Cross_external_payload_name`, `super_errors_multi/Cross_external_import_attrs`, `module_sig_value_arity_mismatch*.res`, `object_value_signature_set_mismatch.res` | Arity mismatches print a dedicated hint (implementation vs interface argument counts), including through aliases and nested function types. The object fixture pins that a value signature cannot drop `@set` from an object type (moregeneral requires equal field mutability). |
 | `Type_declarations` | ✓ | `super_errors_multi/Iface_type_decl_record`, `super_errors_multi/Iface_type_decl_variant`, `RecordInclusion.res`, `type_decl_function_arity_mismatch.res` | |
 | `Extension_constructors` | ✓ | `super_errors_multi/Iface_extension_constructors` | |
 | `Module_types` | ✓ | `super_errors_multi/Iface_module_types` | |
@@ -387,7 +387,7 @@ Source: [includecore.ml:159](../compiler/ml/includecore.ml).
 | `Privacy` | ✓ | `super_errors_multi/Iface_privacy_mismatch` | |
 | `Kind` | ✓ | `super_errors_multi/Iface_kind_mismatch` | Record-in-impl vs variant-in-interface. |
 | `Constraint` | ✓ | `super_errors_multi/Iface_constraint_mismatch` | Implementation adds a `constraint 'a = …`; interface has none. |
-| `Manifest` | ✓ | `super_errors_multi/Iface_manifest_mismatch`, `type_decl_function_arity_mismatch.res` | Manifest types differ, including function types with different arities. |
+| `Manifest` | ✓ | `super_errors_multi/Iface_manifest_mismatch`, `type_decl_function_arity_mismatch.res`, `object_private_row_grants_set.res`, `object_manifest_set_mismatch.res` | Manifest types differ, including function types with different arities. The object fixtures pin the `@set` inclusion matrix: a private row's signature cannot grant `@set` its implementation lacks (but may forget it — pinned compiling in `object_mutability_pin.res`), while a transparent manifest is an equation and cannot forget it either. |
 | `Variance` | ✓ | `super_errors_multi/Iface_variance_mismatch` | Interface annotates `+'a`; implementation's inferred variance differs. |
 | `Field_type` | ✓ | `super_errors_multi/Iface_type_decl_record` | |
 | `Field_mutable` | ✓ | `super_errors_multi/Iface_field_mutable_mismatch` | |

tests/build_tests/super_errors/expected/object_manifest_set_mismatch.res.expected

@@ -0,0 +1,28 @@
+
+  We've found a bug for you!
+  /.../fixtures/object_manifest_set_mismatch.res:6:5-8:1
+
+  4 │ module M: {
+  5 │   type t = {"x": int}
+  6 │ } = {
+  7 │   type t = {@set "x": int}
+  8 │ }
+  9 │ 
+
+  Signature mismatch:
+  Modules do not match:
+    {
+  type t = {@set "x": int}
+}
+  is not included in
+    {
+  type t = {"x": int}
+}
+  Type declarations do not match:
+    type t = {@set "x": int}
+  is not included in
+    type t = {"x": int}
+  /.../fixtures/object_manifest_set_mismatch.res:5:3-21:
+    Expected declaration
+  /.../fixtures/object_manifest_set_mismatch.res:7:3-26:
+    Actual declaration

tests/build_tests/super_errors/expected/object_private_row_grants_set.res.expected

@@ -0,0 +1,28 @@
+
+  We've found a bug for you!
+  /.../fixtures/object_private_row_grants_set.res:7:5-9:1
+
+   5 │ module M: {
+   6 │   type t = private {..@set "x": int}
+   7 │ } = {
+   8 │   type t = private {.."x": int}
+   9 │ }
+  10 │ 
+
+  Signature mismatch:
+  Modules do not match:
+    {
+  type t = {.."x": int}
+}
+  is not included in
+    {
+  type t = {..@set "x": int}
+}
+  Type declarations do not match:
+    type t = {.."x": int}
+  is not included in
+    type t = {..@set "x": int}
+  /.../fixtures/object_private_row_grants_set.res:6:3-36:
+    Expected declaration
+  /.../fixtures/object_private_row_grants_set.res:8:3-31:
+    Actual declaration

tests/build_tests/super_errors/expected/object_value_signature_set_mismatch.res.expected

@@ -0,0 +1,28 @@
+
+  We've found a bug for you!
+  /.../fixtures/object_value_signature_set_mismatch.res:7:5-9:1
+
+   5 │ module M: {
+   6 │   let v: {"x": int}
+   7 │ } = {
+   8 │   let v = impl
+   9 │ }
+  10 │ 
+
+  Signature mismatch:
+  Modules do not match:
+    {
+  let v: {@set "x": int}
+}
+  is not included in
+    {
+  let v: {"x": int}
+}
+  Values do not match:
+    let v: {@set "x": int}
+  is not included in
+    let v: {"x": int}
+  /.../fixtures/object_value_signature_set_mismatch.res:6:3-19:
+    Expected declaration
+  /.../fixtures/object_value_signature_set_mismatch.res:8:7:
+    Actual declaration

tests/build_tests/super_errors/fixtures/object_manifest_set_mismatch.res

@@ -0,0 +1,8 @@
+/* A transparent manifest is an equation: unlike a private row
+   (object_private_row_grants_set.res) or a coercion, it cannot forget a
+   field's @set - the flags must be equal in both directions. */
+module M: {
+  type t = {"x": int}
+} = {
+  type t = {@set "x": int}
+}

tests/build_tests/super_errors/fixtures/object_private_row_grants_set.res

@@ -0,0 +1,9 @@
+/* A signature must not grant write capability its implementation lacks:
+   the interface's @set field requires a settable implementation field. The
+   reverse direction (implementation @set abstracted to read-only) is legal
+   and pinned in tests/tests/src/object_mutability_pin.res. */
+module M: {
+  type t = private {..@set "x": int}
+} = {
+  type t = private {.."x": int}
+}

tests/build_tests/super_errors/fixtures/object_value_signature_set_mismatch.res

@@ -0,0 +1,9 @@
+/* A value signature claims an instance of the implementation's type:
+   moregeneral requires equal field mutability, so an interface cannot
+   silently drop @set from a value's object type. */
+@val external impl: {@set "x": int} = "impl"
+module M: {
+  let v: {"x": int}
+} = {
+  let v = impl
+}

tests/tests/src/object_mutability_pin.mjs

@@ -49,6 +49,8 @@ function closed_immutable_covariant(v) {
   return v;
 }
 
+let PrivateRowForgetsSet = {};
+
 export {
   forget_write_covariant,
   open_source_covariant,
@@ -62,5 +64,6 @@ export {
   set_at_int,
   set_at_string,
   closed_immutable_covariant,
+  PrivateRowForgetsSet,
 }
 /* No side effect */

tests/tests/src/object_mutability_pin.res

@@ -58,3 +58,14 @@ let set_at_string = () => set_x(string_target, "s")
 
 /* Closed immutable-to-immutable coercion is covariant (matrix pin). */
 let closed_immutable_covariant = (v: {"x": wide}): {"x": narrow} => (v :> {"x": narrow})
+
+/* Private-row signature inclusion may forget write capability: the
+   implementation's settable field is abstracted to a read-only one. The
+   reverse (a signature granting @set over a plain implementation field) is
+   pinned as an error in
+   tests/build_tests/super_errors/fixtures/object_private_row_grants_set.res. */
+module PrivateRowForgetsSet: {
+  type t = private {.."x": int}
+} = {
+  type t = private {..@set "x": int}
+}