Check field mutability in record coercion (#9086)

* Check field mutability in record coercion

Why:
    `:>` between record types compared field names, optionality and
    runtime names, but not mutability. A record with an immutable field
    could be coerced to one where the field is mutable and written through
    it, although the compiler treats the field as immutable: reads of it
    were constant-folded to the stale value. A field mutable in both
    records was also coerced covariantly, so a wider value could be
    written into a narrower field.

Diagnostic modified (coercion that makes a field writable):
Example:
    type ro = {x: float}
    type rw = {mutable x: float}

    let toRw = (r: ro) => (r :> rw)
Before (js):
    let r = { x: 0 };
    r.x = 1;
    console.log(0);   // r.x, folded to its initial value
After (diagnostic):
    Type ro is not a subtype of rw

    The record ro cannot be coerced to the record rw because:
    - The field x is mutable in record rw, but not in record ro. A coercion can't make a field writable.

Diagnostic modified (mutable field of a wider type):
Example:
    type narrow = {mutable tag: [#A]}
    type wide = {mutable tag: [#A | #B]}

    let widen = (n: narrow) => (n :> wide)
Before (diagnostic): accepted
After (diagnostic):
    Type narrow is not a subtype of wide

    The second polymorphic variant is closed and doesn't include the constructor: #B.

Review: Is coercing a mutable field to an immutable one still allowed?
    Yes. A read-only view is sound: the source is known to be mutable,
    so its reads are not folded.

Breaking: A coercion that makes a field mutable, or that changes the type
    of a field mutable in both records, is now an error. Declare the field
    mutable in the source record, or copy the record instead of coercing.

Fixes: #9063
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Kbf3gLMawVgtmiKy3TMBc3
Signed-off-by: Christoph Knittel <ck@cca.io>

* Test the record coercions that stay allowed

Codex review on #9086: the fixtures only covered rejected coercions. The
new test runs a read-only view of a mutable field, a mutable field kept
mutable with shared writes through both views, and an immutable target
field of a wider type.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Kbf3gLMawVgtmiKy3TMBc3
Signed-off-by: Christoph Knittel <ck@cca.io>

---------

Signed-off-by: Christoph Knittel <ck@cca.io>
Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

Author: cknitt

changes/record-coercion-mutability.fix.md

@@ -0,0 +1 @@
+- Record coercion no longer turns an immutable field into a mutable one, and requires a field that is mutable in both records to have the same type in both.

compiler/ml/printtyp.ml

@@ -1707,6 +1707,13 @@ let print_record_field_subtype_violation ppf
       label
       (Path.name right_record_name)
       (Path.name left_record_name)
+  | Mutable_mismatch {label} ->
+    fprintf ppf
+      "The field @{<info>%s@} is mutable in record @{<info>%s@}, but not in \
+       record @{<info>%s@}. A coercion can't make a field writable."
+      label
+      (Path.name right_record_name)
+      (Path.name left_record_name)
 
 let report_subtyping_error ppf env tr1 txt1 tr2 ctx =
   wrap_printing_env env (fun () ->

compiler/ml/record_coercion.ml

@@ -10,6 +10,7 @@ type record_field_subtype_violation =
       right_as: string option;
     }
   | Field_missing of {label: string}
+  | Mutable_mismatch of {label: string}
 
 let check_record_fields (fields1 : Types.label_declaration list)
     (fields2 : Types.label_declaration list) =
@@ -40,7 +41,16 @@ let check_record_fields (fields1 : Types.label_declaration list)
                left_as = ld1.ld_runtime_name;
                right_as = ld2.ld_runtime_name;
              });
-      (ld1.ld_type :: acc1, ld2.ld_type :: acc2)
+      (match (ld1.ld_mutable, ld2.ld_mutable) with
+      | Immutable, Mutable ->
+        (* writing through the target would change a field that the source
+           treats as immutable *)
+        add_violation (Mutable_mismatch {label = ld1.ld_id.name})
+      | _ -> ());
+      if ld1.ld_mutable = Mutable && ld2.ld_mutable = Mutable then
+        (* a field read and written through both types: subtyping both ways *)
+        (ld1.ld_type :: ld2.ld_type :: acc1, ld2.ld_type :: ld1.ld_type :: acc2)
+      else (ld1.ld_type :: acc1, ld2.ld_type :: acc2)
     | None ->
       (* field must be present *)
       add_violation (Field_missing {label = ld2.ld_id.name});

tests/build_tests/super_errors/expected/record_coercion_immutable_to_mutable.res.expected

@@ -0,0 +1,13 @@
+
+  We've found a bug for you!
+  /.../fixtures/record_coercion_immutable_to_mutable.res:4:24-30
+
+  2 │ type rw = {mutable x: float}
+  3 │ 
+  4 │ let toRw = (r: ro) => (r :> rw)
+  5 │ 
+
+  Type ro is not a subtype of rw 
+
+  The record ro cannot be coerced to the record rw because:
+  - The field x is mutable in record rw, but not in record ro. A coercion can't make a field writable.

tests/build_tests/super_errors/expected/record_coercion_mutable_field_invariant.res.expected

@@ -0,0 +1,16 @@
+
+  We've found a bug for you!
+  /.../fixtures/record_coercion_mutable_field_invariant.res:4:29-37
+
+  2 │ type wide = {mutable tag: [#A | #B]}
+  3 │ 
+  4 │ let widen = (n: narrow) => (n :> wide)
+  5 │ 
+
+  Type narrow is not a subtype of wide 
+  
+  The second polymorphic variant is closed and doesn't include the constructor: #B.
+  
+  Possible solutions:
+  - Either make the second variant open so it can accept additional constructors. To do this, make sure the type starts with [> instead of [
+  - Or add the missing constructor to it.

tests/build_tests/super_errors/fixtures/record_coercion_immutable_to_mutable.res

@@ -0,0 +1,4 @@
+type ro = {x: float}
+type rw = {mutable x: float}
+
+let toRw = (r: ro) => (r :> rw)

tests/build_tests/super_errors/fixtures/record_coercion_mutable_field_invariant.res

@@ -0,0 +1,4 @@
+type narrow = {mutable tag: [#A]}
+type wide = {mutable tag: [#A | #B]}
+
+let widen = (n: narrow) => (n :> wide)

tests/tests/src/record_coercion_mutable_test.mjs

@@ -0,0 +1,25 @@
+// Generated by ReScript, PLEASE EDIT WITH CARE
+
+import * as Mocha from "mocha";
+import * as Test_utils from "./test_utils.mjs";
+
+Mocha.describe("Record_coercion_mutable_test", () => {
+  Mocha.test("read-only view sees later writes", () => {
+    let c_count = 0;
+    c_count = c_count + 1 | 0;
+    Test_utils.eq("File \"record_coercion_mutable_test.res\", line 23, characters 7-14", 1, c_count);
+  });
+  Mocha.test("mutable to mutable shares writes", () => {
+    let b_value = 1;
+    b_value = 2;
+    Test_utils.eq("File \"record_coercion_mutable_test.res\", line 30, characters 7-14", 2, b_value);
+    b_value = 3;
+    Test_utils.eq("File \"record_coercion_mutable_test.res\", line 32, characters 7-14", 3, b_value);
+  });
+  Mocha.test("immutable target field can widen its type", () => {
+    let n = "A";
+    Test_utils.eq("File \"record_coercion_mutable_test.res\", line 38, characters 7-14", "A", n);
+  });
+});
+
+/*  Not a pure module */

tests/tests/src/record_coercion_mutable_test.res

@@ -0,0 +1,40 @@
+open Mocha
+open Test_utils
+
+// A mutable field can be viewed through an immutable one: a read-only view.
+type counter = {mutable count: int, label: string}
+type readOnlyCounter = {count: int}
+
+// A field mutable in both records keeps its type, and both views share the
+// same object, so writes through either are seen through the other.
+type box = {mutable value: int, extra: string}
+type smallBox = {mutable value: int}
+
+// The field type may still be widened when the field is immutable in the
+// target, here from a closed polymorphic variant to a wider one.
+type narrow = {mutable tag: [#A]}
+type wideReadOnly = {tag: [#A | #B]}
+
+describe(__MODULE__, () => {
+  test("read-only view sees later writes", () => {
+    let c = {count: 0, label: "c"}
+    let view = (c :> readOnlyCounter)
+    c.count = c.count + 1
+    eq(__LOC__, 1, view.count)
+  })
+
+  test("mutable to mutable shares writes", () => {
+    let b = {value: 1, extra: "x"}
+    let small = (b :> smallBox)
+    small.value = 2
+    eq(__LOC__, 2, b.value)
+    b.value = 3
+    eq(__LOC__, 3, small.value)
+  })
+
+  test("immutable target field can widen its type", () => {
+    let n: narrow = {tag: #A}
+    let w = (n :> wideReadOnly)
+    eq(__LOC__, #A, w.tag)
+  })
+})