Fix soundness and analysis gaps found in review

Four review findings on #8597, all confirmed by probe or inspection:

Variance ignored field mutability. The old phantom "x#=" setter member
was an arrow whose contravariant occurrence incidentally made settable
fields invariant; removing the phantom left compute_variance treating
every field payload with the ambient variance, so an explicitly covariant
parameter could annotate a settable field and leak write capability
through an abstract type. The Tfield arm now sends a Mutable field's
payload through Variance.full, like a mutable record label; Immutable
fields keep the ambient variance, preserving read-only covariance.
Pinned by object_settable_field_covariant_param (Bad_variance).

Writes instantiated polymorphic field schemes. Assigning to
{@set "id": 'a. 'a => 'a} typed the value at one instance, so a
monomorphic function satisfied the field while reads kept instantiating
the unchanged scheme. A field's type is a scheme: reading eliminates it,
writing must establish it. The write path now uses the checker's
scheme-introduction discipline - fixed instantiation, typing at that
instance, check_univars - extracted as type_object_field_value next to
its record twin type_label_exp, returning the value at an ordinary
instance as both siblings do. type_label_exp's PR#4862 retry is a
label-specific completeness recovery and is deliberately not replicated;
the helper's comment records that. Pinned by
object_write_poly_field_less_general (Less_general) and a positive
settable-poly case in object_poly_field.

Along the way, instance_poly's positional boolean becomes ~fixed with a
contract comment in ctype.mli: the flag controls fixed copying of
polymorphic-variant rows; scheme introduction is identified by the whole
operation, not by this flag.

reanalyze missed Texp_object_literal. Side-effect analysis fell through
to the permissive default, so a dead binding whose object literal called
effectful code was classified as removable; it now checks every field
expression (ObjectLiteralSideEffects deadcode case). Termination
analysis crashed on the wildcard; it now compiles the literal as an
ordered sequence of its fields - ordered, not unordered, because fields
evaluate in source order and crediting a later field's progress past a
non-returning earlier field would be unsound (the
testObjectLiteralRecursionFirst case is now reported as a possible
infinite loop while testObjectLiteralProgressFirst passes).
Texp_object_get/Texp_object_set traverse their receiver and value
instead of asserting (testObjectAccess).

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

analysis/reanalyze/src/arnold.ml

@@ -1003,12 +1003,16 @@ module Compile = struct
     | Texp_for_await_of (_id, _pat, e1, e2) ->
       let open Command in
       expression ~ctx e1 +++ expression ~ctx e2
-    | Texp_object_get _ ->
-      not_implemented "Texp_object_get";
-      assert false
-    | Texp_object_set _ ->
-      not_implemented "Texp_object_set";
-      assert false
+    | Texp_object_literal fields ->
+      (* Fields are emitted and evaluated in source order *)
+      fields
+      |> List.map (fun (_name, e) -> e |> expression ~ctx)
+      |> Command.sequence
+    | Texp_object_get (e, _) -> e |> expression ~ctx
+    | Texp_object_set (e1, _, e2) ->
+      (* Receiver first, then the assigned value *)
+      let open Command in
+      expression ~ctx e1 +++ expression ~ctx e2
     | Texp_letmodule _ ->
       not_implemented "Texp_letmodule";
       assert false

analysis/reanalyze/src/side_effects.ml

@@ -65,6 +65,8 @@ let rec expr_no_side_effects (expr : Typedtree.expression) =
     e1 |> expr_no_side_effects && e2 |> expr_no_side_effects
     && e3 |> expr_no_side_effects
   | Texp_for_of _ | Texp_for_await_of _ -> false
+  | Texp_object_literal fields ->
+    fields |> List.for_all (fun (_name, e) -> e |> expr_no_side_effects)
   | Texp_object_get _ -> false
   | Texp_object_set _ -> false
   | Texp_letexception (_ec, e) -> e |> expr_no_side_effects

compiler/ml/ctype.ml

@@ -1014,7 +1014,7 @@ let rec copy_sep fixed free bound visited ty =
         | _ -> copy_type_desc copy_rec ty.desc);
       t
 
-let instance_poly ?(keep_names = false) fixed univars sch =
+let instance_poly ?(keep_names = false) ~fixed univars sch =
   with_copy_session (fun () ->
       let univars = List.map repr univars in
       let copy_var ty =
@@ -1035,7 +1035,7 @@ let instance_label fixed lbl =
       let ty_res = copy lbl.lbl_res in
       let vars, ty_arg =
         match repr lbl.lbl_arg with
-        | {desc = Tpoly (ty, tl)} -> instance_poly fixed tl ty
+        | {desc = Tpoly (ty, tl)} -> instance_poly ~fixed tl ty
         | _ -> ([], copy lbl.lbl_arg)
       in
       (vars, ty_arg, ty_res))
@@ -3785,7 +3785,7 @@ let rec subtype_rec env trace t1 t2 cstrs =
       | Tvariant v, _ when !variant_is_subtype env (row_repr v) t2 -> cstrs
       | Tpoly (u1, []), Tpoly (u2, []) -> subtype_rec env trace u1 u2 cstrs
       | Tpoly (u1, tl1), Tpoly (u2, []) ->
-        let _, u1' = instance_poly false tl1 u1 in
+        let _, u1' = instance_poly ~fixed:false tl1 u1 in
         subtype_rec env trace u1' u2 cstrs
       | Tpoly (u1, tl1), Tpoly (u2, tl2) -> (
         try

compiler/ml/ctype.mli

@@ -166,10 +166,18 @@ val instance_parameterized_type :
 val instance_declaration : type_declaration -> type_declaration
 val instance_poly :
   ?keep_names:bool ->
-  bool ->
+  fixed:bool ->
   type_expr list ->
   type_expr ->
   type_expr list * type_expr
+(* Instantiate a scheme [Tpoly(sch, univars)]: replace the universal
+   variables with fresh ones and return them with the instance. [~fixed]
+   controls the copy of polymorphic-variant rows: a fixed copy keeps their
+   rows closed to further extension. Scheme *use* sites instantiate with
+   [~fixed:false]; scheme *introduction* sites (checking a value against
+   the scheme) instantiate with [~fixed:true] and then verify the value
+   generalizes over the returned variables ([Typecore.check_univars]) -
+   the introduction discipline is that whole operation, not this flag. *)
 (* Take an instance of a type scheme containing free univars *)
 
 val instance_label :

compiler/ml/typecore.ml

@@ -1280,7 +1280,7 @@ and type_pat_aux ~constrs ~labels ~no_existentials ~mode ~explode ~env sp
     match ty.desc with
     | Tpoly (body, tyl) ->
       begin_def ();
-      let _, ty' = instance_poly ~keep_names:true false tyl body in
+      let _, ty' = instance_poly ~keep_names:true ~fixed:false tyl body in
       end_def ();
       generalize ty';
       let id = enter_variable lloc name ty' in
@@ -2339,7 +2339,7 @@ type targs = (Asttypes.arg_label * Typedtree.expression option) list
 let object_field_use_type env typ =
   match Ctype.repr typ with
   | {desc = Tpoly (ty, [])} -> instance env ty
-  | {desc = Tpoly (ty, tl)} -> snd (instance_poly false tl ty)
+  | {desc = Tpoly (ty, tl)} -> snd (instance_poly ~fixed:false tl ty)
   | {desc = Tvar _} as ty ->
     let ty' = newvar () in
     unify env (instance_def ty) (newty (Tpoly (ty', [])));
@@ -3403,8 +3403,7 @@ and type_expect_ ?deprecated_context ~context ?(recarg = Rejected) env sexp
     | Error Owrite_not_mutable ->
       raise (Error (loc, env, Object_field_not_mutable (obj.exp_type, name)))
     | Ok typ ->
-      let typ = object_field_use_type env typ in
-      let value = type_expect ~context:None env svalue typ in
+      let value = type_object_field_value env svalue typ in
       rue
         {
           exp_desc = Texp_object_set (obj, name_loc, value);
@@ -3981,6 +3980,31 @@ and type_label_access env srecord lid =
   in
   (record, label, opath)
 
+(* Typing the right-hand side of an object-field assignment: the
+   introduction dual of [object_field_use_type]. A field's type is a scheme:
+   reading instantiates it, while writing must establish it, so a
+   polymorphic field only accepts a value at least as polymorphic — checked
+   by typing the value at a fixed instance and verifying it generalizes
+   ([instance_poly true] + [check_univars]), the same discipline as
+   [type_label_exp] for record labels and [type_let] for polymorphic
+   annotations. With no quantified variables, establishing and instantiating
+   the scheme coincide. [type_label_exp] additionally retries an expansive
+   value without type propagation (PR#4862); that is a label-specific
+   completeness recovery, not part of the scheme-introduction contract, and
+   is deliberately not replicated here. *)
+and type_object_field_value env svalue typ =
+  match (Ctype.repr typ).desc with
+  | Tpoly (ty, (_ :: _ as tl)) ->
+    begin_def ();
+    let vars, ty' = instance_poly ~fixed:true tl ty in
+    let value = type_expect ~context:None env svalue ty' in
+    end_def ();
+    check_univars env true "field value" value typ vars;
+    {value with exp_type = instance env value.exp_type}
+  | _ ->
+    let typ = object_field_use_type env typ in
+    type_expect ~context:None env svalue typ
+
 (* Typing format strings for printing or reading.
    These formats are used by functions in modules Printf, Format, and Scanf.
    (Handling of * modifiers contributed by Thorsten Ohl.) *)
@@ -4675,7 +4699,7 @@ and type_let ~context ?(check = fun s -> Warnings.Unused_var s)
           | Tpoly (ty, tl) ->
             {
               pat with
-              pat_type = snd (instance_poly ~keep_names:true false tl ty);
+              pat_type = snd (instance_poly ~keep_names:true ~fixed:false tl ty);
             }
           | _ -> pat
         in
@@ -4783,7 +4807,7 @@ and type_let ~context ?(check = fun s -> Warnings.Unused_var s)
         match pat.pat_type.desc with
         | Tpoly (ty, tl) ->
           begin_def ();
-          let vars, ty' = instance_poly ~keep_names:true true tl ty in
+          let vars, ty' = instance_poly ~keep_names:true ~fixed:true tl ty in
           let exp = type_expression ty' in
           end_def ();
           check_univars env true "definition" exp pat.pat_type vars;

compiler/ml/typedecl.ml

@@ -770,7 +770,7 @@ let rec check_constraints_rec env loc visited ty =
         raise (Error (loc, Constraint_failed (ty, ty')));
       List.iter (check_constraints_rec env loc visited) args
     | Tpoly (ty, tl) ->
-      let _, ty = Ctype.instance_poly false tl ty in
+      let _, ty = Ctype.instance_poly ~fixed:false tl ty in
       check_constraints_rec env loc visited ty
     | _ -> Btype.iter_type_expr (check_constraints_rec env loc visited) ty)
 
@@ -1003,7 +1003,7 @@ let check_recursion env loc path decl to_check =
              with Not_found -> ());
           List.iter (check_regular cpath args prev_exp) args'
         | Tpoly (ty, tl) ->
-          let _, ty = Ctype.instance_poly ~keep_names:true false tl ty in
+          let _, ty = Ctype.instance_poly ~keep_names:true ~fixed:false tl ty in
           check_regular cpath args prev_exp ty
         | _ -> Btype.iter_type_expr (check_regular cpath args prev_exp) ty)
     in
@@ -1078,8 +1078,12 @@ let compute_variance env visited vari ty =
               tl decl.type_variance
           with Not_found -> List.iter (compute_variance_rec may_inv) tl)
       | Tobject ty -> compute_same ty
-      | Tfield {typ = ty1; rest = ty2} ->
-        compute_same ty1;
+      | Tfield {mutability; typ = ty1; rest = ty2} ->
+        (* A settable field can be both read and written, so its payload is
+           an invariant occurrence, like a mutable record label. *)
+        (match Btype.mutability_repr mutability with
+        | Mutable -> compute_variance_rec Variance.full ty1
+        | Immutable -> compute_same ty1);
         compute_same ty2
       | Tsubst ty -> compute_same ty
       | Tvariant row ->

tests/ERROR_VARIANTS.md

@@ -223,7 +223,7 @@ Source: [typecore.ml:27](../compiler/ml/typecore.ml).
 | `Abstract_wrong_label` | ✓ | `abstract_wrong_label.res` | Multi-arg function literal where an inner argument label doesn't match the expected arrow's label (e.g. `let f: (~a, ~b) => int = (~a, ~c) => …`). |
 | `Scoping_let_module` | ✓ | `scoping_let_module.res` | |
 | `Not_a_variant_type` | ✓ | `variant_spread_pattern_not_a_variant.res` | Pattern-level variant spread of a non-variant type. |
-| `Less_general` | ✓ | `less_general_universal.res` | |
+| `Less_general` | ✓ | `less_general_universal.res`, `object_write_poly_field_less_general.res` | The latter pins that assigning to a polymorphic object field checks the value against the field's scheme. |
 | `Modules_not_allowed` | ✓ | `super_errors_multi/Modules_not_allowed_toplevel` | Toplevel `let module(M) = …` pattern with `allow_modules=false`. |
 | `Cannot_infer_signature` | ✓ | `cannot_infer_signature.res` | |
 | `Not_a_packed_module` | ✓ | `not_a_packed_module.res` | |
@@ -278,7 +278,7 @@ Type-declaration errors. Source: [typedecl.ml:27](../compiler/ml/typedecl.ml).
 | `Rebind_wrong_type` | ✓ | `extension_rebind_mismatch.res` | Rebinding constructor into a different extensible type fails while unifying the source constructor result with the extension target. |
 | `Rebind_mismatch` | ? | — | The later declaration-shape check after `Rebind_wrong_type`; no source fixture was confirmed in this pass. |
 | `Rebind_private` | ✓ | `extension_rebind_private.res` | Rebinding a private extension constructor as public. |
-| `Bad_variance` | ✓ | `bad_variance.res`, `bad_variance_contra.res` | |
+| `Bad_variance` | ✓ | `bad_variance.res`, `bad_variance_contra.res`, `object_settable_field_covariant_param.res` | The latter pins that a settable object field is an invariant occurrence, like a mutable record label. |
 | `Unavailable_type_constructor` | ☐ (needs build harness) | — | typedecl.ml:778. Requires a type path findable at parse time but missing during constraint enforcement; only cross-unit scenarios where a `.cmi` was found but later removed. |
 | `Bad_fixed_type` | ✓ | `fixed_type_no_row_variable.res` | Fully-bounded closed private polymorphic variant (`type t = private [< #A | #B > #A #B]`) satisfies `is_fixed_type` but has a static (non-`Tvar`) row. |
 | `Unbound_type_var_ext` | ✓ | `unbound_type_var_extension.res` | |

tests/analysis_tests/tests-reanalyze/deadcode/expected/deadcode.txt

@@ -1161,6 +1161,9 @@
   addValueReference Newton.res:31:13 --> Newton.res:29:4
   addValueReference Newton.res:31:23 --> Newton.res:29:4
   addValueReference Newton.res:31:21 --> Newton.res:25:4
+  Scanning ObjectLiteralSideEffects.cmt Source:ObjectLiteralSideEffects.res
+  addValueDeclaration +deadWithEffect ObjectLiteralSideEffects.res:3:4 path:+ObjectLiteralSideEffects
+  addValueDeclaration +deadNoEffect ObjectLiteralSideEffects.res:4:4 path:+ObjectLiteralSideEffects
   Scanning OcamlWarningSuppressToplevel.cmt Source:OcamlWarningSuppressToplevel.res
   addValueDeclaration +suppressed1 OcamlWarningSuppressToplevel.res:3:4 path:+OcamlWarningSuppressToplevel
   addValueDeclaration +suppressed2 OcamlWarningSuppressToplevel.res:4:4 path:+OcamlWarningSuppressToplevel
@@ -2103,7 +2106,7 @@
 
 Forward Liveness Analysis
 
-    decls: 744
+    decls: 746
     roots(external targets): 161
     decl-deps: decls_with_out=451 edges_to_decls=323
 
@@ -3635,6 +3638,8 @@ Forward Liveness Analysis
         -> +Newton.+newton
         -> +Newton.+f
         -> +Newton.+fPrimed
+  Dead Value +ObjectLiteralSideEffects.+deadWithEffect
+  Dead Value +ObjectLiteralSideEffects.+deadNoEffect
   Live (annotated) Value +OcamlWarningSuppressToplevel.+suppressed1
   Live (annotated) Value +OcamlWarningSuppressToplevel.+suppressed2
   Live (annotated) Value +OcamlWarningSuppressToplevel.M.+suppressed3
@@ -5251,6 +5256,18 @@ Forward Liveness Analysis
   Newsyntax.res:12:24-29
   record2.yy is a record label never used to read a value
 
+  Warning Dead Module
+  ObjectLiteralSideEffects.res:0:1
+  ObjectLiteralSideEffects is a dead module as all its items are dead.
+
+  Warning Dead Value With Side Effects
+  ObjectLiteralSideEffects.res:3:1-49
+  deadWithEffect is never used and could have side effects
+
+  Warning Dead Value
+  ObjectLiteralSideEffects.res:4:1-27
+  deadNoEffect is never used
+
   Warning Dead Type
   Opaque.res:2:26-41
   opaqueFromRecords.A is a variant case which is never constructed
@@ -5643,4 +5660,4 @@ Forward Liveness Analysis
   OptArg.res:14:1-42
   optional argument b of function twoArgs is never used
 
-  Analysis reported 327 issues (Incorrect Dead Annotation:1, Warning Dead Exception:2, Warning Dead Module:22, Warning Dead Type:94, Warning Dead Value:178, Warning Dead Value With Side Effects:5, Warning Redundant Optional Argument:7, Warning Unused Argument:18)
+  Analysis reported 330 issues (Incorrect Dead Annotation:1, Warning Dead Exception:2, Warning Dead Module:23, Warning Dead Type:94, Warning Dead Value:179, Warning Dead Value With Side Effects:6, Warning Redundant Optional Argument:7, Warning Unused Argument:18)

tests/analysis_tests/tests-reanalyze/deadcode/src/ObjectLiteralSideEffects.res

@@ -0,0 +1,4 @@
+// An object literal's field expressions determine its side effects: the
+// first binding must be classified with side effects, the second without.
+let deadWithEffect = {"x": Console.log("effect")}
+let deadNoEffect = {"x": 1}

tests/analysis_tests/tests-reanalyze/termination/expected/termination.txt

@@ -150,11 +150,31 @@
 
   Termination Analysis for testTry
 
+  Function Table
+  1 testObjectLiteral: +progress; testObjectLiteral
+
+  Termination Analysis for testObjectLiteral
+
+  Function Table
+  1 testObjectLiteralProgressFirst: +progress; testObjectLiteralProgressFirst; _
+
+  Termination Analysis for testObjectLiteralProgressFirst
+
+  Function Table
+  1 testObjectLiteralRecursionFirst: testObjectLiteralRecursionFirst; +progress; _
+
+  Termination Analysis for testObjectLiteralRecursionFirst
+
+  Function Table
+  1 testObjectAccess: +progress; testObjectAccess
+
+  Termination Analysis for testObjectAccess
+
   Termination Analysis Stats
   Files:1
-  Recursive Blocks:21
-  Functions:49
-  Infinite Loops:10
+  Recursive Blocks:25
+  Functions:53
+  Infinite Loops:11
   Hygiene Errors:2
   Cache Hits:7/30
 
@@ -230,5 +250,11 @@
   Possible infinite loop when calling countRendersCompiled
   CallStack:
     1 countRendersCompiled (TestCyberTruck.res 283)
+
+  Error Termination
+  TestCyberTruck.res:468:20-52
+  Possible infinite loop when calling testObjectLiteralRecursionFirst
+  CallStack:
+    1 testObjectLiteralRecursionFirst (TestCyberTruck.res 467)
 
-  Analysis reported 12 issues (Error Hygiene:2, Error Termination:10)
+  Analysis reported 13 issues (Error Hygiene:2, Error Termination:11)