fix: record update should type-check like record creation

src/mo_frontend/typing.ml

@@ -729,6 +729,10 @@ let infer_class_cap env obj_sort (tbs : T.bind list) cs =
   | _ ->
     C.NullCap, tbs, cs
 
+let find_field (ef : exp_field) (fts : T.field list) = 
+  let id = ef.it.id.it in
+  List.find_opt T.(fun ft -> ft.lab = id && not (is_typ ft.typ)) fts
+
 (* Types *)
 
 let rec check_typ env (typ : typ) : T.typ =
@@ -2235,14 +2239,13 @@ and infer_check_bases_fields env (check_fields : T.field list) exp_at exp_bases
   check_ids env "object" "field"
     (map (fun (ef : exp_field) -> ef.it.id) exp_fields);
 
-  let infer_or_check rf =
-    let { mut; id; exp } = rf.it in
-    match List.find_opt (fun ft -> ft.T.lab = id.it) check_fields with
-    | Some exp_field ->
-      check_exp_field env rf [exp_field];
-      exp_field
-    | _ -> infer_exp_field env rf in
-
+  let infer_or_check exp_field =
+    match find_field exp_field check_fields with
+    | Some ft ->
+      check_exp_field env exp_field [ft];
+      ft
+    | _ -> infer_exp_field env exp_field
+  in
   let fts = map infer_or_check exp_fields in
   let bases = map (fun b -> infer_exp_promote env b, b) exp_bases in
   let homonymous_fields ft1 ft2 = T.compare_field ft1 ft2 = 0 in
@@ -2411,22 +2414,24 @@ and check_exp' env0 t exp : T.typ =
   | TupE exps, T.Tup ts when List.length exps = List.length ts ->
     List.iter2 (check_exp env) ts exps;
     t
-  | ObjE ([], exp_fields) as e, T.Obj(T.Object, fts) -> (* TODO: infer bases? Default does a decent job. *)
-    check_ids env "object" "field"
-      (List.map (fun (ef : exp_field) -> ef.it.id) exp_fields);
-    List.iter (fun ef -> check_exp_field env ef fts) exp_fields;
-    if List.for_all (fun ft ->
-      if not (List.exists (fun (ef : exp_field) -> ft.T.lab = ef.it.id.it) exp_fields)
-      then begin
-      local_error env exp.at "M0151"
-        "object literal is missing field %s from expected type%a"
-        ft.T.lab
-        display_typ_expand t;
-        false
-      end else true
-    ) fts
-    then detect_lost_fields env t e;
-    t
+  | ObjE (exp_bases, exp_fields), T.Obj(T.Object, fts) ->
+    let t' = infer_check_bases_fields env fts exp.at exp_bases exp_fields in
+    let fts' = match T.promote t' with
+      | T.Obj(T.Object, fts') -> fts'
+      | _ -> []
+    in
+    let missing_field_labs =
+      List.filter (fun ft -> not (List.exists (fun ft' -> ft.T.lab = ft'.T.lab) fts')) fts
+      |> List.map (fun ft -> Printf.sprintf "'%s'" ft.T.lab)
+    in
+    begin match missing_field_labs with
+    | [] -> check_inferred env0 env t t' exp
+    | fts ->
+      (* Future work: Replace this error with a general subtyping error once better explanations are available. *)
+      let s = if List.length fts = 1 then "" else "s" in
+      local_error env exp.at "M0151" "missing field%s %s from expected type%a" s (String.concat ", " fts) display_typ_expand t;
+      t'
+    end
   | OptE exp1, _ when T.is_opt t ->
     check_exp env (T.as_opt t) exp1;
     t
@@ -2529,18 +2534,21 @@ and check_exp' env0 t exp : T.typ =
     t
   | (ImportE _ | ImplicitLibE _), t ->
     t
-  | e, _ ->
+  | _, _ ->
     let t' = infer_exp env0 exp in
-    if not (sub env exp.at t' t) then
-    begin
-      local_error env0 exp.at "M0096"
-        "expression of type%a\ncannot produce expected type%a%s"
-        display_typ_expand t'
-        display_typ_expand t
-        (Suggest.suggest_conversion env.libs env.vals t' t)
-    end
-    else detect_lost_fields env t e;
-    t'
+    check_inferred env0 env t t' exp
+
+and check_inferred env0 env t t' exp = 
+  if not (sub env exp.at t' t) then
+  begin
+    local_error env0 exp.at "M0096"
+      "expression of type%a\ncannot produce expected type%a%s"
+      display_typ_expand t'
+      display_typ_expand t
+      (Suggest.suggest_conversion env.libs env.vals t' t)
+  end
+  else detect_lost_fields env t exp.it;
+  t'
 
 and check_exp_field env (ef : exp_field) fts =
   let { mut; id; exp } = ef.it in

test/fail/issue2331.mo

@@ -1 +1,2 @@
 ignore ({foo = 0} : { bar : Nat });
+ignore ({foo = 0} : { bar : Nat; qux : Float });

test/fail/ok/check-record.tc.ok

@@ -7,12 +7,10 @@ but found mutable 'var' field (delete 'var'?)
 check-record.mo:12.11-12.16: type error [M0149], expected mutable 'var' field a of type
   Int
 but found immutable field (insert 'var'?)
-check-record.mo:14.9-14.11: type error [M0151], object literal is missing field a from expected type
+check-record.mo:14.9-14.11: type error [M0151], missing field 'a' from expected type
   {a : Nat}
 check-record.mo:16.18-16.23: warning [M0215], field `b` is provided but not expected in record of type
   {a : Nat}
 check-record.mo:21.30-21.31: type error [M0057], unbound variable c
-check-record.mo:24.9-24.27: type error [M0096], expression of type
-  {a : Nat}
-cannot produce expected type
+check-record.mo:24.9-24.27: type error [M0151], missing field 'b' from expected type
   {b : Nat}

test/fail/ok/issue2331.tc.ok

@@ -1,2 +1,4 @@
-issue2331.mo:1.9-1.18: type error [M0151], object literal is missing field bar from expected type
+issue2331.mo:1.9-1.18: type error [M0151], missing field 'bar' from expected type
   {bar : Nat}
+issue2331.mo:2.9-2.18: type error [M0151], missing fields 'bar', 'qux' from expected type
+  {bar : Nat; qux : Float}

test/run/record-update-inference.mo

@@ -0,0 +1,62 @@
+// Issue #418: type inference on record update should be as strong as on record creation
+
+// Stub for Map
+module Map {
+  public type Node<K, V> = {
+    #leaf : Leaf<K, V>;
+    #internal : Internal<K, V>;
+  };
+
+  public type Data<K, V> = {
+    kvs : [var ?(K, V)];
+    var count : Nat;
+  };
+
+  public type Internal<K, V> = {
+    data : Data<K, V>;
+    children : [var ?Node<K, V>];
+  };
+
+  public type Leaf<K, V> = {
+    data : Data<K, V>;
+  };
+
+  public type Map<K, V> = {
+    var root : Node<K, V>;
+    var size : Nat;
+  };
+  public func empty<K, V>() : Map<K, V> = {
+    var root = #leaf { data = { kvs = [var]; var count = 0 } };
+    var size = 0;
+  };
+};
+
+type Exercise = {
+  name : Text;
+  sets : Nat;
+};
+
+type Workout = {
+  exercises : Map.Map<Nat, Exercise>;
+  duration : Nat;
+  timestamp : Int;
+};
+
+func createWorkout(duration : Nat) : Workout {
+  {
+    exercises = Map.empty();
+    duration;
+    timestamp = 0;
+  }
+};
+
+func updateWorkout(workout : Workout, duration : Nat) : Workout {
+  {
+    workout with
+    exercises = Map.empty(); // should typecheck without instantiation
+    duration;
+  }
+};
+
+let workout1 = createWorkout(30);
+ignore updateWorkout(workout1, 45);