Overwriting typing (ocaml-flambda#3157)

* First draft of type checking

* Check in uniqueness analysis that tags stay the same during overwriting

* Report a syntax error on overwriting anything except an allocation

* Full type-checking for tuples and records

* Type checking fully implemented

* Clean up type-checking and add ability to overwrite arbitrary expressions

* Fix checking of tags

* Test (labeled) tuples

* Final tests and allow overwrite of inlined records

* Review suggestion

Co-authored-by: Richard Eisenberg <[email protected]>

* Review suggestion

Co-authored-by: Richard Eisenberg <[email protected]>

* Review feedback: add more tests

* Uniqueness analysis: Change grammar of error message to indicate parallel evaluation

* Review feedback: Fix typo

Co-authored-by: Richard Eisenberg <[email protected]>

* Review feedback: add comments and tests

* Prevent nested allocations in overwrite

* Review feedback: Fix comment and improve readability

* Review feedback: add comments, tests and nicer error messages

* Fix nested record bug

* Improve code quality

* Disallow overwriting of unboxed records

* Review feedback

* Clarify the overwriting state for type_label_exp

* Add debugging printers for uniqueness

Sadly this doesn't actually work in the debugger.

* Temporarily allow unique mutable fields for better tests of overwriting tags (to be reverted)

* New scheme for checking that overwrite does not change tags

* Refactor: split up Learned_tags and Overwrites and use match_with_learned_tags instead of seq

* Add comment about fold_left1 and zero of semiring

* Fix submode error attribution in records

* Tune errors in tag checker

* Don't record tags that have been overwritten and matched with a learned tag

* Review feedback: comments and small improvements

* Review feedback: tune comments

---------

Co-authored-by: Richard Eisenberg <[email protected]>
Co-authored-by: Richard Eisenberg <[email protected]>

file_formats/cmt_format.ml

@@ -227,7 +227,7 @@ let iter_on_occurrences
       | Texp_object _ | Texp_pack _ | Texp_letop _ | Texp_unreachable
       | Texp_list_comprehension _ | Texp_array_comprehension _ | Texp_probe _
       | Texp_probe_is_enabled _ | Texp_exclave _
-      | Texp_open _ | Texp_src_pos -> ());
+      | Texp_open _ | Texp_src_pos | Texp_overwrite _ | Texp_hole _ -> ());
       default_iterator.expr sub e);
 
   (* Remark: some types get iterated over twice due to how constraints are

lambda/translcore.ml

@@ -1207,6 +1207,10 @@ and transl_exp0 ~in_new_scope ~scopes sort e =
         ]
       in
       Lconst(Const_block(0, cl))
+  | Texp_overwrite (_, _) ->
+      Location.todo_overwrite_not_implemented ~kind:"Translcore" e.exp_loc
+  | Texp_hole _ ->
+      Location.todo_overwrite_not_implemented ~kind:"Translcore" e.exp_loc
 
 and pure_module m =
   match m.mod_desc with

parsing/ast_helper.ml

@@ -245,7 +245,7 @@ module Exp = struct
   let unreachable ?loc ?attrs () = mk ?loc ?attrs Pexp_unreachable
   let stack ?loc ?attrs e = mk ?loc ?attrs (Pexp_stack e)
   let comprehension ?loc ?attrs e = mk ?loc ?attrs (Pexp_comprehension e)
-  let overwrite ?loc ?attrs x e = mk ?loc ?attrs (Pexp_overwrite (x, e))
+  let overwrite ?loc ?attrs a b = mk ?loc ?attrs (Pexp_overwrite (a, b))
   let hole ?loc ?attrs () = mk ?loc ?attrs Pexp_hole
 
   let case lhs ?guard rhs =

parsing/ast_helper.mli

@@ -210,7 +210,7 @@ module Exp:
     val stack : ?loc:loc -> ?attrs:attrs -> expression -> expression
     val comprehension :
       ?loc:loc -> ?attrs:attrs -> comprehension_expression -> expression
-    val overwrite : ?loc:loc -> ?attrs:attrs -> lid -> expression -> expression
+    val overwrite : ?loc:loc -> ?attrs:attrs -> expression -> expression -> expression
     val hole : ?loc:loc -> ?attrs:attrs -> unit -> expression
 
     val case: pattern -> ?guard:expression -> expression -> case

parsing/ast_iterator.ml

@@ -532,7 +532,7 @@ module E = struct
     | Pexp_unreachable -> ()
     | Pexp_stack e -> sub.expr sub e
     | Pexp_comprehension e -> iter_comp_exp sub e
-    | Pexp_overwrite (x, e) -> iter_loc sub x; sub.expr sub e
+    | Pexp_overwrite (e1, e2) -> sub.expr sub e1; sub.expr sub e2
     | Pexp_hole -> ()
 
   let iter_binding_op sub {pbop_op; pbop_pat; pbop_exp; pbop_loc} =

parsing/ast_mapper.ml

@@ -605,7 +605,7 @@ module E = struct
     | Pexp_unreachable -> unreachable ~loc ~attrs ()
     | Pexp_stack e -> stack ~loc ~attrs (sub.expr sub e)
     | Pexp_comprehension c -> comprehension ~loc ~attrs (map_cexp sub c)
-    | Pexp_overwrite (x, e) -> overwrite ~loc ~attrs (map_loc sub x) (sub.expr sub e)
+    | Pexp_overwrite (e1, e2) -> overwrite ~loc ~attrs (sub.expr sub e1) (sub.expr sub e2)
     | Pexp_hole -> hole ~loc ~attrs ()
 
   let map_binding_op sub {pbop_op; pbop_pat; pbop_exp; pbop_loc} =

parsing/depend.ml

@@ -313,7 +313,7 @@ let rec add_expr bv exp =
       end
   | Pexp_extension e -> handle_extension e
   | Pexp_stack e -> add_expr bv e
-  | Pexp_overwrite (x, e) -> add bv x; add_expr bv e
+  | Pexp_overwrite (e1, e2) -> add_expr bv e1; add_expr bv e2
   | Pexp_hole -> ()
   | Pexp_unreachable -> ()
   | Pexp_comprehension x -> add_comprehension_expr bv x

parsing/location.ml

@@ -1102,6 +1102,6 @@ let () =
 let raise_errorf ?(loc = none) ?(sub = []) =
   Format.kdprintf (fun txt -> raise (Error (mkerror loc sub txt)))
 
-let todo_overwrite_not_implemented t =
-  alert ~kind:"" t "Overwrite not implemented.";
+let todo_overwrite_not_implemented ?(kind = "") t =
+  alert ~kind t "Overwrite not implemented.";
   assert false

parsing/location.mli

@@ -398,4 +398,4 @@ val report_exception: formatter -> exn -> unit
 (** Reraise the exception if it is unknown. *)
 
 (** CR uniqueness: remove this *)
-val todo_overwrite_not_implemented : t -> 'a
+val todo_overwrite_not_implemented : ?kind:string -> t -> 'a

parsing/parser.mly

@@ -2845,7 +2845,7 @@ fun_expr:
       { Pexp_try($3, $5), $2 }
   | TRY ext_attributes seq_expr WITH error
       { syntax_error() }
-  | OVERWRITE ext_attributes mkrhs(val_longident) WITH expr
+  | OVERWRITE ext_attributes seq_expr WITH expr
       { Pexp_overwrite($3, $5), $2 }
   | IF ext_attributes seq_expr THEN expr ELSE expr
       { Pexp_ifthenelse($3, $5, Some $7), $2 }

parsing/parsetree.mli

@@ -491,7 +491,7 @@ and expression_desc =
           - [CLAUSES] is a series of [comprehension_clause].
     *)
   (* CR uniqueness: allow arbitrary expressions instead of identifiers here *)
-  | Pexp_overwrite of Longident.t loc * expression (** overwrite_ x with exp *)
+  | Pexp_overwrite of expression * expression (** overwrite_ exp with exp *)
   | Pexp_hole (** _ *)
 
 and case =

parsing/pprintast.ml

@@ -1090,11 +1090,11 @@ and expression ctxt f x =
           (expression ctxt) body
     | Pexp_extension e -> extension ctxt f e
     | Pexp_unreachable -> pp f "."
-    | Pexp_overwrite (x, e) ->
+    | Pexp_overwrite (e1, e2) ->
         (* Similar to the case of [Pexp_stack] *)
         pp f "@[<hov2>overwrite_@ %a@ with@ %a@]"
-          longident_loc x
-          (expression2 reset_ctxt) e
+          (expression2 reset_ctxt) e1
+          (expression2 reset_ctxt) e2
     | Pexp_hole -> pp f "_"
     | _ -> expression1 ctxt f x
 

parsing/printast.ml

@@ -437,9 +437,10 @@ and expression i ppf x =
   | Pexp_comprehension c ->
       line i ppf "Pexp_comprehension\n";
       comprehension_expression i ppf c
-  | Pexp_overwrite (x, e) ->
-    line i ppf "Pexp_overwrite %a\n" fmt_longident_loc x;
-    expression i ppf e
+  | Pexp_overwrite (e1, e2) ->
+      line i ppf "Pexp_overwrite\n";
+      expression i ppf e1;
+      expression i ppf e2;
   | Pexp_hole ->
     line i ppf "Pexp_hole"
 

printer/printast_with_mappings.ml

@@ -461,9 +461,10 @@ and expression i ppf x =
   | Pexp_comprehension c ->
       line i ppf "Pexp_comprehension\n";
       comprehension_expression i ppf c
-  | Pexp_overwrite (x, e) ->
-      line i ppf "Pexp_overwrite %a\n" fmt_longident_loc x;
-      expression i ppf e
+  | Pexp_overwrite (e1, e2) ->
+      line i ppf "Pexp_overwrite\n";
+      expression i ppf e1;
+      expression i ppf e2
   | Pexp_hole ->
       line i ppf "Pexp_hole"
   )

testsuite/tests/parsetree/source_jane_street.ml

@@ -1203,6 +1203,11 @@ let overwrite_record = function
 let overwrite_record = function
     { a; b } as t -> overwrite_ t with { b = a }
 
+let ret_record () = { a = 1; b = 2 }
+
+let overwrite_record () =
+  overwrite_ (ret_record ()) with { b = a }
+
 type constructor = C of { a : int; b : int }
 
 let overwrite_constructor = function
@@ -1214,7 +1219,7 @@ let overwrite_constructor = function
 Line 2, characters 19-43:
 2 |     (a, b) as t -> overwrite_ t with (b, _)
                        ^^^^^^^^^^^^^^^^^^^^^^^^
-Alert : Overwrite not implemented.
+Alert Translcore: Overwrite not implemented.
 Uncaught exception: File "parsing/location.ml", line 1107, characters 2-8: Assertion failed
 
 |}]

testsuite/tests/typing-modes/modes.ml

@@ -297,7 +297,7 @@ type r = {
   mutable x : string @@ global aliased many
 }
 [%%expect{|
-type r = { mutable x : string; }
+type r = { mutable x : string @@ aliased; }
 |}]
 
 

testsuite/tests/typing-modes/mutable.ml

@@ -75,10 +75,7 @@ Error: This value escapes its region.
    portable record (ignoring mode-crossing). *)
 let foo (s @ portable) = ({s} : _ @@ portable)
 [%%expect{|
-Line 1, characters 26-29:
-1 | let foo (s @ portable) = ({s} : _ @@ portable)
-                              ^^^
-Error: This value is "nonportable" but expected to be "portable".
+val foo : 'a @ portable -> 'a r = <fun>
 |}]
 
 (* This attribute doesn't disable implied modalities on monadic axes. For
@@ -92,15 +89,15 @@ val foo : 'a r -> 'a -> unit = <fun>
 
 let foo (s @ aliased) = ({s} : _ @@ unique)
 [%%expect{|
-val foo : 'a -> 'a r = <fun>
+Line 1, characters 26-27:
+1 | let foo (s @ aliased) = ({s} : _ @@ unique)
+                              ^
+Error: This value is "aliased" but expected to be "unique".
 |}]
 
 let foo (r @ unique) = (r.s : _ @@ unique)
 [%%expect{|
-Line 1, characters 24-27:
-1 | let foo (r @ unique) = (r.s : _ @@ unique)
-                            ^^^
-Error: This value is "aliased" but expected to be "unique".
+val foo : 'a r @ unique -> 'a = <fun>
 |}]
 
 module M : sig
@@ -164,10 +161,7 @@ let r @ portable =
 (* CR mode-crossing: The [m0] in mutable should cross modes upon construction. *)
 [%%expect{|
 type r = { f : string -> string; mutable a : int; }
-Lines 5-6, characters 2-12:
-5 | ..{ f = (fun x -> x);
-6 |     a = 42 }
-Error: This value is "nonportable" but expected to be "portable".
+val r : r = {f = <fun>; a = 42}
 |}]
 
 type r =
@@ -180,8 +174,5 @@ let r @ portable =
    in modality; as a result, it enjoys mode crossing enabled by the modality. *)
 [%%expect{|
 type r = { f : string -> string; mutable g : string -> string @@ portable; }
-Lines 5-6, characters 2-20:
-5 | ..{ f = (fun x -> x);
-6 |     g = fun x -> x }
-Error: This value is "nonportable" but expected to be "portable".
+val r : r = {f = <fun>; g = <fun>}
 |}]

testsuite/tests/typing-modes/portable-contend.ml

@@ -166,10 +166,7 @@ let foo () =
    and the above bar is closing over an nonportable record. Once we allow mutable()
    syntax, we can test this. *)
 [%%expect{|
-Line 2, characters 23-61:
-2 |     let r @ portable = {a = best_bytes (); b = best_bytes ()} in
-                           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: This value is "nonportable" but expected to be "portable".
+val foo : unit -> unit = <fun>
 |}]
 
 

testsuite/tests/typing-modes/val_modalities.ml

@@ -34,7 +34,7 @@ module M = struct
   let foo = {x = "hello"}
 end
 [%%expect{|
-module M : sig val foo : r @@ global many end
+module M : sig val foo : r @@ global many portable end
 |}]
 
 module type S = sig