From b3b4cfa7f592f84876f142a8c847b2ec2bd3e7d3 Mon Sep 17 00:00:00 2001 From: Kamil Listopad Date: Mon, 3 Nov 2025 13:48:05 +0100 Subject: [PATCH 1/8] fix: record update should type-check like record creation --- src/mo_frontend/typing.ml | 36 +++++++++------- test/run/record-update-inference.mo | 64 +++++++++++++++++++++++++++++ 2 files changed, 85 insertions(+), 15 deletions(-) create mode 100644 test/run/record-update-inference.mo diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index 96124a18b46..6a70fdae35f 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -2411,11 +2411,13 @@ 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" + | ObjE (exp_bases, exp_fields), T.Obj(T.Object, fts) -> (* TODO: infer bases? Default does a decent job. *) + let t' = infer_check_bases_fields env fts exp.at exp_bases exp_fields in + check_inferred env0 env t t' exp + (* 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 -> + 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" @@ -2427,6 +2429,7 @@ and check_exp' env0 t exp : T.typ = ) fts then detect_lost_fields env t e; t + *) | OptE exp1, _ when T.is_opt t -> check_exp env (T.as_opt t) exp1; t @@ -2529,18 +2532,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 diff --git a/test/run/record-update-inference.mo b/test/run/record-update-inference.mo new file mode 100644 index 00000000000..9ef7ea980e5 --- /dev/null +++ b/test/run/record-update-inference.mo @@ -0,0 +1,64 @@ +// Issue #418: type inference on record update should be as strong as on record creation + +// Stub for Map +module Map { + public type Node = { + #leaf : Leaf; + #internal : Internal; + }; + + public type Data = { + kvs : [var ?(K, V)]; + var count : Nat; + }; + + public type Internal = { + data : Data; + children : [var ?Node]; + }; + + public type Leaf = { + data : Data; + }; + + public type Map = { + var root : Node; + var size : Nat; + }; + public func empty() : Map = { + var root = #leaf { data = { kvs = [var]; var count = 0 } }; + var size = 0; + }; +}; + +type Exercise = { + name : Text; + sets : Nat; +}; + +type Workout = { + exercises : Map.Map; + duration : Nat; + timestamp : Int; +}; + +// Test 1: Record creation - type inference works without explicit +func createWorkout(duration : Nat) : Workout { + { + exercises = Map.empty(); + duration; + timestamp = 0; + } +}; + +// Test 2: Record update - type inference should now work (the fix) +func updateWorkout(workout : Workout, duration : Nat) : Workout { + { + workout with + exercises = Map.empty(); + duration; + } +}; + +let workout1 = createWorkout(30); +ignore updateWorkout(workout1, 45); From 61039d5668ebf6643d2c704ef85e85789fe2e53d Mon Sep 17 00:00:00 2001 From: Kamil Listopad Date: Mon, 3 Nov 2025 15:33:29 +0100 Subject: [PATCH 2/8] fix, rework message, gather more missing fields not just one --- src/mo_frontend/typing.ml | 34 ++++++++++++++++----------------- test/fail/issue2331.mo | 1 + test/fail/ok/check-record.tc.ok | 6 ++---- test/fail/ok/issue2331.tc.ok | 4 +++- 4 files changed, 22 insertions(+), 23 deletions(-) diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index 6a70fdae35f..19c583e29e8 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -2411,25 +2411,23 @@ 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_bases, exp_fields), T.Obj(T.Object, fts) -> (* TODO: infer bases? Default does a decent job. *) + | 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 - check_inferred env0 env t t' exp - (* 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 - *) + let fields = match T.promote t' with + | T.Obj(T.Object, fts) -> fts + | _ -> [] + in + let missing_fields = List.filter (fun ft -> + not (List.exists (fun ft2 -> ft.T.lab = ft2.T.lab) fields)) fts + |> List.map (fun ft -> Printf.sprintf "'%s'" ft.T.lab) + in + begin match missing_fields with + | [] -> check_inferred env0 env t t' exp + | fts -> + 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 diff --git a/test/fail/issue2331.mo b/test/fail/issue2331.mo index a16fbf8933b..3bdcf0afc29 100644 --- a/test/fail/issue2331.mo +++ b/test/fail/issue2331.mo @@ -1 +1,2 @@ ignore ({foo = 0} : { bar : Nat }); +ignore ({foo = 0} : { bar : Nat; qux : Float }); diff --git a/test/fail/ok/check-record.tc.ok b/test/fail/ok/check-record.tc.ok index b9ee96aa06b..0d0faeacbfd 100644 --- a/test/fail/ok/check-record.tc.ok +++ b/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} diff --git a/test/fail/ok/issue2331.tc.ok b/test/fail/ok/issue2331.tc.ok index 841a993ef24..728827bd1e2 100644 --- a/test/fail/ok/issue2331.tc.ok +++ b/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} From e76f35c776e76a53dfeb46854b5a0912b88582e3 Mon Sep 17 00:00:00 2001 From: Kamil Listopad Date: Mon, 3 Nov 2025 15:36:38 +0100 Subject: [PATCH 3/8] test comments --- test/run/record-update-inference.mo | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/test/run/record-update-inference.mo b/test/run/record-update-inference.mo index 9ef7ea980e5..0ab96c03d17 100644 --- a/test/run/record-update-inference.mo +++ b/test/run/record-update-inference.mo @@ -42,7 +42,6 @@ type Workout = { timestamp : Int; }; -// Test 1: Record creation - type inference works without explicit func createWorkout(duration : Nat) : Workout { { exercises = Map.empty(); @@ -51,11 +50,10 @@ func createWorkout(duration : Nat) : Workout { } }; -// Test 2: Record update - type inference should now work (the fix) func updateWorkout(workout : Workout, duration : Nat) : Workout { { workout with - exercises = Map.empty(); + exercises = Map.empty(); // should typecheck without instantiation duration; } }; From 98e84c7d15c9929439c1b0008a61d1fa26c83718 Mon Sep 17 00:00:00 2001 From: Kamil Listopad Date: Tue, 4 Nov 2025 14:59:56 +0100 Subject: [PATCH 4/8] exclude is_typ in lookup --- src/mo_frontend/typing.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index 19c583e29e8..b7a789dd441 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -2237,7 +2237,7 @@ and infer_check_bases_fields env (check_fields : T.field list) exp_at exp_bases 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 + match List.find_opt T.(fun ft -> ft.lab = id.it && not (is_typ ft.typ)) check_fields with | Some exp_field -> check_exp_field env rf [exp_field]; exp_field From 96e6711dbeef0e65719e2bc6f939d913cb816a19 Mon Sep 17 00:00:00 2001 From: Kamil Listopad Date: Tue, 4 Nov 2025 16:01:41 +0100 Subject: [PATCH 5/8] missing_field_labs refactor --- src/mo_frontend/typing.ml | 30 +++++++++++++++++------------- 1 file changed, 17 insertions(+), 13 deletions(-) diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index 2876ade13c5..a32eb575401 100644 --- a/src/mo_frontend/typing.ml +++ b/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 T.(fun ft -> ft.lab = id.it && not (is_typ ft.typ)) 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 @@ -2413,17 +2416,18 @@ and check_exp' env0 t exp : T.typ = 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 fields = match T.promote t' with - | T.Obj(T.Object, fts) -> fts + let fts' = match T.promote t' with + | T.Obj(T.Object, fts') -> fts' | _ -> [] in - let missing_fields = List.filter (fun ft -> - not (List.exists (fun ft2 -> ft.T.lab = ft2.T.lab) fields)) fts + 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_fields with + 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' From 9853c17b4435525d1c2af3a6d4baf0bfbbdf1af9 Mon Sep 17 00:00:00 2001 From: Kamil Listopad Date: Wed, 5 Nov 2025 07:37:45 +0100 Subject: [PATCH 6/8] refactor --- src/mo_frontend/typing.ml | 9 +++------ src/mo_types/type.ml | 8 ++++++-- src/mo_types/type.mli | 1 + 3 files changed, 10 insertions(+), 8 deletions(-) diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index a32eb575401..d1e3c12b40f 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -729,10 +729,6 @@ 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 = @@ -2239,8 +2235,9 @@ 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 exp_field = - match find_field exp_field check_fields with + let infer_or_check (exp_field : exp_field) = + let id = exp_field.it.id.it in + match T.find_val_field_opt id check_fields with | Some ft -> check_exp_field env exp_field [ft]; ft diff --git a/src/mo_types/type.ml b/src/mo_types/type.ml index e0654542b1b..ba91052d0b7 100644 --- a/src/mo_types/type.ml +++ b/src/mo_types/type.ml @@ -705,10 +705,14 @@ let is_immutable_obj obj_type = let _, fields = as_obj_sub [] obj_type in List.for_all (fun f -> not (is_mut f.typ)) fields - -let lookup_val_field_opt l tfs = +let find_val_field_opt l tfs = let is_lab = function {typ = Typ _; _} -> false | {lab; _} -> lab = l in match List.find_opt is_lab tfs with + | Some tf -> Some tf + | None -> None + +let lookup_val_field_opt l tfs = + match find_val_field_opt l tfs with | Some tf -> Some tf.typ | None -> None diff --git a/src/mo_types/type.mli b/src/mo_types/type.mli index 2d7c4f1f747..d9e5614c5bc 100644 --- a/src/mo_types/type.mli +++ b/src/mo_types/type.mli @@ -184,6 +184,7 @@ val arity : typ -> int (* Fields *) +val find_val_field_opt : string -> field list -> field option val lookup_val_field : string -> field list -> typ val lookup_typ_field : string -> field list -> con val lookup_val_field_opt : string -> field list -> typ option From 61aaabd84058d8e98823a8860deea57cf4b20df7 Mon Sep 17 00:00:00 2001 From: Kamil Listopad Date: Wed, 5 Nov 2025 07:53:24 +0100 Subject: [PATCH 7/8] missing_val_field_labs --- src/mo_frontend/typing.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index d1e3c12b40f..70fec2d2886 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -2417,11 +2417,11 @@ and check_exp' env0 t exp : T.typ = | 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 + let missing_val_field_labs = fts + |> List.filter T.(fun ft -> not (is_typ ft.T.typ) && Option.is_none (lookup_val_field_opt ft.lab fts')) |> List.map (fun ft -> Printf.sprintf "'%s'" ft.T.lab) in - begin match missing_field_labs with + begin match missing_val_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. *) From b5f6e98449400df857071cf60354b47be2641e9f Mon Sep 17 00:00:00 2001 From: Kamil Listopad Date: Thu, 6 Nov 2025 13:04:46 +0100 Subject: [PATCH 8/8] review --- Changelog.md | 2 ++ test/run/record-update-inference.mo | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/Changelog.md b/Changelog.md index 814496a0ab2..d4cbc6897ae 100644 --- a/Changelog.md +++ b/Changelog.md @@ -2,6 +2,8 @@ * motoko (`moc`) + * Improved type inference of the record update syntax (#5625). + * Improved solving and error messages for invariant type parameters (#5464). Error messages now include suggested type instantiations when there is no principal solution. diff --git a/test/run/record-update-inference.mo b/test/run/record-update-inference.mo index 0ab96c03d17..5f640a549d2 100644 --- a/test/run/record-update-inference.mo +++ b/test/run/record-update-inference.mo @@ -1,4 +1,4 @@ -// Issue #418: type inference on record update should be as strong as on record creation +// Type inference on record update should be as strong as on record creation // Stub for Map module Map {