From b3bde75c458e6660c91b55b8fc91a7f72da8fb14 Mon Sep 17 00:00:00 2001 From: Kamil Listopad Date: Fri, 24 Oct 2025 15:54:55 +0200 Subject: [PATCH 01/19] fix: Redundant type instantiation wrong when return expression --- src/mo_frontend/typing.ml | 35 +++++++++++++----------- test/{fail => run}/lambdas-core.mo | 21 ++++++++++++++ test/{fail => run}/ok/lambdas-core.tc.ok | 1 + 3 files changed, 41 insertions(+), 16 deletions(-) rename test/{fail => run}/lambdas-core.mo (98%) rename test/{fail => run}/ok/lambdas-core.tc.ok (85%) diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index a8068889729..b8f7b15b4d9 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -55,6 +55,7 @@ type env = in_prog : bool; context : exp' list; pre : bool; + skip_note_typ : bool; weak : bool; msgs : Diag.msg_store; scopes : Source.region T.ConEnv.t; @@ -81,6 +82,7 @@ let env_of_scope ?(viper_mode=false) msgs scope = in_prog = true; context = []; pre = false; + skip_note_typ = false; weak = false; msgs; scopes = T.ConEnv.empty; @@ -1662,11 +1664,11 @@ and infer_exp_and_promote env exp : T.typ * T.typ = and infer_exp_wrapper inf f env exp : T.typ = - assert (exp.note.note_typ = T.Pre); + assert (env.skip_note_typ || exp.note.note_typ = T.Pre); let t = inf env exp in assert (t <> T.Pre); let t' = f t in - if not env.pre then begin + if not (env.pre || env.skip_note_typ) then begin let t'' = T.normalize t' in assert (t'' <> T.Pre); let note_eff = A.infer_effect_exp exp in @@ -2325,12 +2327,14 @@ and check_exp_weak env t exp = check_exp {env with weak = true} t exp and check_exp env t exp = - assert (not env.pre); - assert (exp.note.note_typ = T.Pre); + assert (env.skip_note_typ || not env.pre); + assert (env.skip_note_typ || exp.note.note_typ = T.Pre); assert (t <> T.Pre); let t' = check_exp' env (T.normalize t) exp in - let e = A.infer_effect_exp exp in - exp.note <- {exp.note with note_typ = t'; note_eff = e} + if not (env.skip_note_typ) then begin + let e = A.infer_effect_exp exp in + exp.note <- {exp.note with note_typ = t'; note_eff = e} + end and check_exp' env0 t exp : T.typ = let env = {env0 with in_prog = false; in_actor = false; context = exp.it :: env0.context } in @@ -2951,18 +2955,17 @@ and infer_call_instantiation env t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt (* Check the function input type and prepare for inferring the body *) let env', body_typ, codom = check_func_step false env (shared_pat, pat, typ_opt, body) (s, c, ts1, ts2) in (* [codom] comes from [ts2] which might contain unsolved type variables. *) - let closed = Bi_match.is_closed remaining codom in - if not env.pre && (closed || body_typ <> codom) then begin - (* Closed [codom] implies closed [body_typ]. - * [body_typ] is closed when it comes from [typ_opt] (which is when it is different from [codom]) - *) + let closed_codom = Bi_match.is_closed remaining codom in + (* Closed [codom] implies closed [body_typ]. [body_typ] is closed when it comes from [typ_opt] *) + let closed_body_typ = closed_codom || Option.is_some typ_opt in + let env' = if closed_body_typ then env' else { env' with rets = None } in + if closed_body_typ && not (env.pre || env.skip_note_typ) then begin assert (Bi_match.is_closed remaining body_typ); - (* Since [body_typ] is closed, no need to infer *) check_exp env' body_typ body; end; (* When [codom] is open, we need to solve it *) - if not closed then + if not closed_codom then if body_typ <> codom then (* [body_typ] is closed, body is already checked above, we just need to solve the subtype problem *) subs := (body_typ, codom) :: !subs @@ -2972,7 +2975,7 @@ and infer_call_instantiation env t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt subs := (actual_t, body_typ) :: !subs; end | HoleE _, typ -> - if not env.pre then begin + if not (env.pre || env.skip_note_typ) then begin (* Check that all type variables in the type are fixed, fail otherwise *) Bi_match.fail_when_types_are_not_closed remaining [typ]; check_exp env typ exp @@ -3062,7 +3065,7 @@ and infer_call_instantiation env t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt and is_redundant_instantiation ts env infer_instantiation = assert env.pre; match Diag.with_message_store (recover_opt (fun msgs -> - let env_without_errors = { env with msgs } in + let env_without_errors = { env with msgs; skip_note_typ = true } in let ts', _, _ = infer_instantiation env_without_errors in List.length ts = List.length ts' && List.for_all2 (T.eq ?src_fields:None) ts ts' )) @@ -4007,7 +4010,7 @@ and infer_block_exps env decs : T.typ = | [] -> T.unit | [dec] -> infer_dec env dec | dec::decs' -> - if not env.pre then recover (check_dec env T.unit) dec; + if not (env.pre || env.skip_note_typ) then recover (check_dec env T.unit) dec; infer_block_exps env decs' and infer_dec env dec : T.typ = diff --git a/test/fail/lambdas-core.mo b/test/run/lambdas-core.mo similarity index 98% rename from test/fail/lambdas-core.mo rename to test/run/lambdas-core.mo index 4982fb74557..c1bf839bcc3 100644 --- a/test/fail/lambdas-core.mo +++ b/test/run/lambdas-core.mo @@ -544,6 +544,27 @@ module Issue5418 { ); }; }; + +module Return { + public func test1() { + let ar = Array.tabulate(3, func i { + if (i == 0) return false; + true; + }); + assert ar == []; + }; + // Future work: improve type inference to handle `return` + // public func test2() { + // let ar = Array.tabulate(3, func i { + // if (i == 0) return false; + // true; + // }); + // assert ar == [false, true, true]; + // }; +}; +Return.test1(); +// Return.test2(); + //SKIP comp //SKIP run-ir //SKIP run-low diff --git a/test/fail/ok/lambdas-core.tc.ok b/test/run/ok/lambdas-core.tc.ok similarity index 85% rename from test/fail/ok/lambdas-core.tc.ok rename to test/run/ok/lambdas-core.tc.ok index 580887ce748..ed7579e47f9 100644 --- a/test/fail/ok/lambdas-core.tc.ok +++ b/test/run/ok/lambdas-core.tc.ok @@ -4,3 +4,4 @@ lambdas-core.mo:480.22-480.33: warning [M0223], redundant type instantiation lambdas-core.mo:483.28-483.39: warning [M0223], redundant type instantiation lambdas-core.mo:500.17-500.34: warning [M0223], redundant type instantiation lambdas-core.mo:513.22-513.39: warning [M0223], redundant type instantiation +lambdas-core.mo:550.28-550.34: warning [M0223], redundant type instantiation From c743a5a441f1327ab6703c435096b590a3c9d731 Mon Sep 17 00:00:00 2001 From: Kamil Listopad Date: Fri, 24 Oct 2025 16:31:47 +0200 Subject: [PATCH 02/19] use skip_note_typ where necessary --- src/mo_frontend/typing.ml | 81 ++++++++++++++++++++-------------- test/run/ok/lambdas-core.tc.ok | 1 - 2 files changed, 49 insertions(+), 33 deletions(-) diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index b8f7b15b4d9..8af1f1ea006 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -1712,29 +1712,31 @@ and infer_exp'' env exp : T.typ = let t1 = infer_exp_promote env exp1 in let t = Operator.type_unop op t1 in if not env.pre then begin - assert (!ot = Type.Pre); + assert (env.skip_note_typ || !ot = T.Pre); if not (Operator.has_unop op t) then error env exp.at "M0059" "operator is not defined for operand type%a" display_typ_expand t; - ot := t; + if not env.skip_note_typ then + ot := t end; t | BinE (ot, exp1, op, exp2) -> let t1, t2 = infer_bin_exp env exp1 exp2 in let t = Operator.type_binop op (T.lub ~src_fields:env.srcs (T.promote t1) (T.promote t2)) in - if not env.pre then begin - assert (!ot = Type.Pre); + if not env.pre && not env.skip_note_typ then begin + assert (env.skip_note_typ || !ot = T.Pre); if not (Operator.has_binop op t) then error_bin_op env exp.at t1 t2 else if op = Operator.SubOp && eq env exp.at t T.nat then warn env exp.at "M0155" "operator may trap for inferred type%a" display_typ_expand t; - ot := t + if not env.skip_note_typ then + ot := t end; t | RelE (ot, exp1, op, exp2) -> - if not env.pre then begin - assert (!ot = Type.Pre); + if not env.pre && not env.skip_note_typ then begin + assert (env.skip_note_typ || !ot = T.Pre); let t1, t2 = infer_bin_exp env exp1 exp2 in let t = Operator.type_relop op (T.lub ~src_fields:env.srcs (T.promote t1) (T.promote t2)) in if not (Operator.has_relop op t) then @@ -1751,7 +1753,8 @@ and infer_exp'' env exp : T.typ = display_typ_expand t1 display_typ_expand t2 display_typ_expand t; - ot := t; + if not env.skip_note_typ then + ot := t end; T.bool | ShowE (ot, exp1) -> @@ -1760,7 +1763,8 @@ and infer_exp'' env exp : T.typ = if not (Show.can_show t) then error env exp.at "M0063" "show is not defined for operand type%a" display_typ_expand t; - ot := t + if not env.skip_note_typ then + ot := t end; T.text | ToCandidE exps -> @@ -1914,7 +1918,8 @@ and infer_exp'' env exp : T.typ = let t1, ve1 = infer_pat_exhaustive (if T.is_shared_sort sort then local_error else warn) env' pat in let ve2 = T.Env.adjoin ve ve1 in let ts2 = List.map (check_typ_item env') ts2 in - typ.note <- T.seq ts2; (* HACK *) + if not env.skip_note_typ then + typ.note <- T.seq ts2; (* HACK *) let codom = T.codom c (fun () -> T.Con(List.hd cs,[])) ts2 in if not env.pre then begin let env'' = @@ -2389,11 +2394,13 @@ and check_exp' env0 t exp : T.typ = | _ -> error env exp.at "M0090" "actor reference must have an actor type" end | UnE (ot, op, exp1), _ when Operator.has_unop op t -> - ot := t; + if not env.skip_note_typ then + ot := t; check_exp env t exp1; t | BinE (ot, exp1, op, exp2), _ when Operator.has_binop op t -> - ot := t; + if not env.skip_note_typ then + ot := t; check_exp env t exp1; check_exp env t exp2; if env.weak && op = Operator.SubOp && eq env exp.at t T.nat then @@ -2803,7 +2810,7 @@ and infer_call env exp1 inst (parenthesized, ref_exp2) at t_expect_opt = then wrong_call_args env tbs exp2.at t_args implicits_arity syntax_args else T.seq t_args in - if not env.pre then ref_exp2 := exp2; (* TODO: is this good enough *) + if not env.pre && not env.skip_note_typ then ref_exp2 := exp2; (* TODO: is this good enough *) let ts, t_arg', t_ret' = match tbs, inst.it with | [], (None | Some (_, [])) (* no inference required *) @@ -2814,16 +2821,19 @@ and infer_call env exp1 inst (parenthesized, ref_exp2) at t_expect_opt = let ts = check_inst_bounds env sort tbs typs t_ret at in let t_arg' = T.open_ ts t_arg in let t_ret' = T.open_ ts t_ret in - if not env.pre then check_exp_strong env t_arg' exp2 - else if typs <> [] && Flags.is_warning_enabled "M0223" && - is_redundant_instantiation ts env (fun env' -> - infer_call_instantiation env' t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt extra_subtype_problems) then - warn env inst.at "M0223" "redundant type instantiation"; + if not env.pre then begin + check_exp_strong env t_arg' exp2; + if typs <> [] && Flags.is_warning_enabled "M0223" && + is_redundant_instantiation ts env (fun env' -> + infer_call_instantiation env' t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt extra_subtype_problems) then + warn env inst.at "M0223" "redundant type instantiation"; + end; ts, t_arg', t_ret' | _::_, None -> (* implicit, infer *) infer_call_instantiation env t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt extra_subtype_problems in - inst.note <- ts; + if not env.skip_note_typ then + inst.note <- ts; if not env.pre then begin if Type.is_shared_sort sort then begin if not (T.concrete t_arg') then @@ -2959,7 +2969,7 @@ and infer_call_instantiation env t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt (* Closed [codom] implies closed [body_typ]. [body_typ] is closed when it comes from [typ_opt] *) let closed_body_typ = closed_codom || Option.is_some typ_opt in let env' = if closed_body_typ then env' else { env' with rets = None } in - if closed_body_typ && not (env.pre || env.skip_note_typ) then begin + if closed_body_typ && not env.pre then begin assert (Bi_match.is_closed remaining body_typ); check_exp env' body_typ body; end; @@ -2975,7 +2985,7 @@ and infer_call_instantiation env t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt subs := (actual_t, body_typ) :: !subs; end | HoleE _, typ -> - if not (env.pre || env.skip_note_typ) then begin + if not env.pre then begin (* Check that all type variables in the type are fixed, fail otherwise *) Bi_match.fail_when_types_are_not_closed remaining [typ]; check_exp env typ exp @@ -3063,7 +3073,7 @@ and infer_call_instantiation env t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt Format.asprintf "\nto produce result of expected type%a" display_typ t) and is_redundant_instantiation ts env infer_instantiation = - assert env.pre; + assert (not env.pre); match Diag.with_message_store (recover_opt (fun msgs -> let env_without_errors = { env with msgs; skip_note_typ = true } in let ts', _, _ = infer_instantiation env_without_errors in @@ -3125,9 +3135,9 @@ and infer_pat_exhaustive warnOrError env pat : T.typ * Scope.val_env = t, ve and infer_pat name_types env pat : T.typ * Scope.val_env = - assert (pat.note = T.Pre); + assert (env.skip_note_typ || pat.note = T.Pre); let t, ve = infer_pat' name_types env pat in - if not env.pre then + if not env.pre && not env.skip_note_typ then pat.note <- T.normalize t; t, ve @@ -3239,11 +3249,11 @@ and check_pat env t pat : Scope.val_env = check_pat_aux env t pat Scope.Declaration and check_pat_aux env t pat val_kind : Scope.val_env = - assert (pat.note = T.Pre); + assert (env.skip_note_typ || pat.note = T.Pre); if t = T.Pre then snd (infer_pat false env pat) else let t' = T.normalize t in let ve = check_pat_aux' env t' pat val_kind in - if not env.pre then pat.note <- t'; + if not env.pre && not env.skip_note_typ then pat.note <- t'; ve and check_pat_aux' env t pat val_kind : Scope.val_env = @@ -4010,7 +4020,7 @@ and infer_block_exps env decs : T.typ = | [] -> T.unit | [dec] -> infer_dec env dec | dec::decs' -> - if not (env.pre || env.skip_note_typ) then recover (check_dec env T.unit) dec; + if not env.pre then recover (check_dec env T.unit) dec; infer_block_exps env decs' and infer_dec env dec : T.typ = @@ -4113,8 +4123,9 @@ and infer_dec env dec : T.typ = | TypD _ -> T.unit in - let eff = A.infer_effect_dec dec in - dec.note <- {empty_typ_note with note_typ = t; note_eff = eff}; + if not env.skip_note_typ then ( + let eff = A.infer_effect_dec dec in + dec.note <- {empty_typ_note with note_typ = t; note_eff = eff}); t @@ -4141,7 +4152,8 @@ and check_dec env t dec = match dec.it with | ExpD exp -> check_exp env t exp; - dec.note <- exp.note + if not env.skip_note_typ then + dec.note <- exp.note | _ -> let t' = infer_dec env dec in if not (eq env dec.at t T.unit || sub env dec.at t' t) then @@ -4236,7 +4248,9 @@ and gather_dec env scope dec : Scope.t = in let pre_k = T.Abs (pre_tbs, T.Pre) in let c = match id.note with - | None -> let c = Cons.fresh id.it pre_k in id.note <- Some c; c + | None -> + assert (not env.skip_note_typ); + let c = Cons.fresh id.it pre_k in id.note <- Some c; c | Some c -> c in let val_env = match dec.it with @@ -4408,7 +4422,9 @@ and infer_dec_typdecs env dec : Scope.t = and infer_id_typdecs env at id c k : Scope.con_env = assert (match k with T.Abs (_, T.Pre) -> false | _ -> true); (match Cons.kind c with - | T.Abs (_, T.Pre) -> T.set_kind c k; id.note <- Some c + | T.Abs (_, T.Pre) -> + assert (not env.skip_note_typ); + T.set_kind c k; id.note <- Some c | k' -> assert (eq_kind env at k' k) (* may diverge on expansive types *) ); T.ConSet.singleton c @@ -4564,6 +4580,7 @@ let check_lib scope pkg_opt lib : Scope.t Diag.result = let { imports; body = cub; _ } = lib.it in let (imp_ds, ds) = CompUnit.decs_of_lib lib in let typ, _ = infer_block env (imp_ds @ ds) lib.at false in + assert (not env.skip_note_typ); List.iter2 (fun import imp_d -> import.note <- imp_d.note.note_typ) imports imp_ds; cub.note <- {empty_typ_note with note_typ = typ}; let imp_scope = match cub.it with diff --git a/test/run/ok/lambdas-core.tc.ok b/test/run/ok/lambdas-core.tc.ok index ed7579e47f9..580887ce748 100644 --- a/test/run/ok/lambdas-core.tc.ok +++ b/test/run/ok/lambdas-core.tc.ok @@ -4,4 +4,3 @@ lambdas-core.mo:480.22-480.33: warning [M0223], redundant type instantiation lambdas-core.mo:483.28-483.39: warning [M0223], redundant type instantiation lambdas-core.mo:500.17-500.34: warning [M0223], redundant type instantiation lambdas-core.mo:513.22-513.39: warning [M0223], redundant type instantiation -lambdas-core.mo:550.28-550.34: warning [M0223], redundant type instantiation From 3ec404a77c856e139ef4fa46ede93f9bd42cfe3e Mon Sep 17 00:00:00 2001 From: Kamil Listopad Date: Fri, 24 Oct 2025 16:56:20 +0200 Subject: [PATCH 03/19] up --- src/mo_frontend/typing.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index 8af1f1ea006..400a4eefaeb 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -1723,7 +1723,7 @@ and infer_exp'' env exp : T.typ = | BinE (ot, exp1, op, exp2) -> let t1, t2 = infer_bin_exp env exp1 exp2 in let t = Operator.type_binop op (T.lub ~src_fields:env.srcs (T.promote t1) (T.promote t2)) in - if not env.pre && not env.skip_note_typ then begin + if not env.pre then begin assert (env.skip_note_typ || !ot = T.Pre); if not (Operator.has_binop op t) then error_bin_op env exp.at t1 t2 @@ -1735,7 +1735,7 @@ and infer_exp'' env exp : T.typ = end; t | RelE (ot, exp1, op, exp2) -> - if not env.pre && not env.skip_note_typ then begin + if not env.pre then begin assert (env.skip_note_typ || !ot = T.Pre); let t1, t2 = infer_bin_exp env exp1 exp2 in let t = Operator.type_relop op (T.lub ~src_fields:env.srcs (T.promote t1) (T.promote t2)) in From dd3114f43c6cca9894047be566f75800806fed2a Mon Sep 17 00:00:00 2001 From: Kamil Listopad Date: Fri, 24 Oct 2025 17:21:11 +0200 Subject: [PATCH 04/19] redundant check first, check after, otherwise we cheat on literals --- src/mo_frontend/typing.ml | 38 +++++++++++++++++++++----------------- 1 file changed, 21 insertions(+), 17 deletions(-) diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index 400a4eefaeb..6aeae8ec9fe 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -1150,6 +1150,10 @@ let check_text env at s = local_error env at "M0049" "string literal \"%s\": is not valid utf8" (String.escaped s); s +let set_lit env lit t = + if not env.skip_note_typ then + lit := t + let infer_lit env lit at : T.prim = match !lit with | NullLit -> T.Null @@ -1170,19 +1174,19 @@ let infer_lit env lit at : T.prim = | BlobLit _ -> T.Blob | PreLit (s, T.Nat) -> if not env.pre then - lit := NatLit (check_nat env at s); (* default *) + set_lit env lit (NatLit (check_nat env at s)); (* default *) T.Nat | PreLit (s, T.Int) -> if not env.pre then - lit := IntLit (check_int env at s); (* default *) + set_lit env lit (IntLit (check_int env at s)); (* default *) T.Int | PreLit (s, T.Float) -> if not env.pre then - lit := FloatLit (check_float env at s); (* default *) + set_lit env lit (FloatLit (check_float env at s)); (* default *) T.Float | PreLit (s, T.Text) -> if not env.pre then - lit := TextLit (check_text env at s); (* default *) + set_lit env lit (TextLit (check_text env at s)); (* default *) T.Text | PreLit _ -> assert false @@ -1190,29 +1194,29 @@ let infer_lit env lit at : T.prim = let check_lit env t lit at suggest = match t, !lit with | T.Prim T.Nat, PreLit (s, T.Nat) -> - lit := NatLit (check_nat env at s) + set_lit env lit (NatLit (check_nat env at s)) | T.Prim T.Nat8, PreLit (s, T.Nat) -> - lit := Nat8Lit (check_nat8 env at s) + set_lit env lit (Nat8Lit (check_nat8 env at s)) | T.Prim T.Nat16, PreLit (s, T.Nat) -> - lit := Nat16Lit (check_nat16 env at s) + set_lit env lit (Nat16Lit (check_nat16 env at s)) | T.Prim T.Nat32, PreLit (s, T.Nat) -> - lit := Nat32Lit (check_nat32 env at s) + set_lit env lit (Nat32Lit (check_nat32 env at s)) | T.Prim T.Nat64, PreLit (s, T.Nat) -> - lit := Nat64Lit (check_nat64 env at s) + set_lit env lit (Nat64Lit (check_nat64 env at s)) | T.Prim T.Int, PreLit (s, (T.Nat | T.Int)) -> - lit := IntLit (check_int env at s) + set_lit env lit (IntLit (check_int env at s)) | T.Prim T.Int8, PreLit (s, (T.Nat | T.Int)) -> - lit := Int8Lit (check_int8 env at s) + set_lit env lit (Int8Lit (check_int8 env at s)) | T.Prim T.Int16, PreLit (s, (T.Nat | T.Int)) -> - lit := Int16Lit (check_int16 env at s) + set_lit env lit (Int16Lit (check_int16 env at s)) | T.Prim T.Int32, PreLit (s, (T.Nat | T.Int)) -> - lit := Int32Lit (check_int32 env at s) + set_lit env lit (Int32Lit (check_int32 env at s)) | T.Prim T.Int64, PreLit (s, (T.Nat | T.Int)) -> - lit := Int64Lit (check_int64 env at s) + set_lit env lit (Int64Lit (check_int64 env at s)) | T.Prim T.Float, PreLit (s, (T.Nat | T.Int | T.Float)) -> - lit := FloatLit (check_float env at s) + set_lit env lit (FloatLit (check_float env at s)) | T.Prim T.Blob, PreLit (s, T.Text) -> - lit := BlobLit s + set_lit env lit (BlobLit s) | t, _ -> let t' = T.Prim (infer_lit env lit at) in if not (sub env at t' t) then @@ -2822,11 +2826,11 @@ and infer_call env exp1 inst (parenthesized, ref_exp2) at t_expect_opt = let t_arg' = T.open_ ts t_arg in let t_ret' = T.open_ ts t_ret in if not env.pre then begin - check_exp_strong env t_arg' exp2; if typs <> [] && Flags.is_warning_enabled "M0223" && is_redundant_instantiation ts env (fun env' -> infer_call_instantiation env' t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt extra_subtype_problems) then warn env inst.at "M0223" "redundant type instantiation"; + check_exp_strong env t_arg' exp2; end; ts, t_arg', t_ret' | _::_, None -> (* implicit, infer *) From dfa090393ebf66e18b053490f1dd5459ab13a351 Mon Sep 17 00:00:00 2001 From: Kamil Listopad Date: Mon, 27 Oct 2025 13:14:13 +0100 Subject: [PATCH 05/19] perf: skip redundancy check when env.skip_note_typ --- src/mo_frontend/typing.ml | 2 ++ test/run/ok/redundant-instantiations.tc.ok | 11 +++++--- test/run/redundant-instantiations.mo | 30 ++++++++++++++++++++++ 3 files changed, 39 insertions(+), 4 deletions(-) diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index 6aeae8ec9fe..8048cd4ec76 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -3078,6 +3078,8 @@ and infer_call_instantiation env t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt and is_redundant_instantiation ts env infer_instantiation = assert (not env.pre); + (* Perf: Skip checking nested instantiations to ensure that every instantiation is checked for redundancy exactly once *) + if env.skip_note_typ then false else match Diag.with_message_store (recover_opt (fun msgs -> let env_without_errors = { env with msgs; skip_note_typ = true } in let ts', _, _ = infer_instantiation env_without_errors in diff --git a/test/run/ok/redundant-instantiations.tc.ok b/test/run/ok/redundant-instantiations.tc.ok index b10c1d15a1d..975294dcdf0 100644 --- a/test/run/ok/redundant-instantiations.tc.ok +++ b/test/run/ok/redundant-instantiations.tc.ok @@ -1,4 +1,7 @@ -redundant-instantiations.mo:20.18-20.23: warning [M0223], redundant type instantiation -redundant-instantiations.mo:29.18-29.23: warning [M0223], redundant type instantiation -redundant-instantiations.mo:36.18-36.25: warning [M0223], redundant type instantiation -redundant-instantiations.mo:43.18-43.24: warning [M0223], redundant type instantiation +redundant-instantiations.mo:22.18-22.23: warning [M0223], redundant type instantiation +redundant-instantiations.mo:31.18-31.23: warning [M0223], redundant type instantiation +redundant-instantiations.mo:38.18-38.25: warning [M0223], redundant type instantiation +redundant-instantiations.mo:45.18-45.24: warning [M0223], redundant type instantiation +redundant-instantiations.mo:52.24-52.30: warning [M0223], redundant type instantiation +redundant-instantiations.mo:54.26-54.32: warning [M0223], redundant type instantiation +redundant-instantiations.mo:56.28-56.34: warning [M0223], redundant type instantiation diff --git a/test/run/redundant-instantiations.mo b/test/run/redundant-instantiations.mo index 8c95d191d20..208f62c8627 100644 --- a/test/run/redundant-instantiations.mo +++ b/test/run/redundant-instantiations.mo @@ -1,4 +1,6 @@ //MOC-FLAG -W M0223 +import Prim "mo:prim"; + // Empty instantiations, no warning func empty<>(x : Int): Int = x; assert empty<>(1) == 1; @@ -44,3 +46,31 @@ let t2 = inferred("abc"); // Redundant vaText[0] := t2; let t3 = inferred("blob"); vaBlob[0] := t3; + +module Nested { + public func test() : Bool { + Prim.Array_tabulate(2, func i { // Redundant + if (i == 0) false else + Prim.Array_tabulate(2, func i { // Redundant + if (i == 0) false else + Prim.Array_tabulate(2, func i { // Redundant + if (i == 0) false else + true; + })[1]; + })[1]; + })[1]; + }; + // Future work: improve type inference to handle `return` and detect these redundant instantiations + public func testWithReturns() : Bool { + Prim.Array_tabulate(2, func i { + if (i == 0) return false; + Prim.Array_tabulate(2, func i { + if (i == 0) return false; + Prim.Array_tabulate(2, func i { + if (i == 0) return false; + true; + })[1]; + })[1]; + })[1]; + }; +}; From 77630a4312e0e340eb1a65d270a3c1e0ce818c74 Mon Sep 17 00:00:00 2001 From: Kamil Listopad Date: Mon, 27 Oct 2025 13:46:45 +0100 Subject: [PATCH 06/19] refactor --- src/mo_frontend/typing.ml | 80 +++++++++++++++++++-------------------- 1 file changed, 38 insertions(+), 42 deletions(-) diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index 8048cd4ec76..444c493dfc0 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -54,7 +54,9 @@ type env = in_actor : bool; in_prog : bool; context : exp' list; + (* [pre] phase skips thorough checks and avoids recording note types (and other internal state modifications) *) pre : bool; + (* [skip_note_typ] avoids recording note types. Used to perform full checking ([not pre]) without modifying the internal state *) skip_note_typ : bool; weak : bool; msgs : Diag.msg_store; @@ -101,6 +103,14 @@ let use_identifier env id = let is_unused_identifier env id = not (S.mem id !(env.used_identifiers)) +let set env lit t = + if not env.skip_note_typ then + lit := t + +let set_note env ap n = + if not env.skip_note_typ then + ap.note <- n + let get_identifiers identifiers = T.Env.fold (fun id _ set -> S.add id set) identifiers S.empty @@ -1150,10 +1160,6 @@ let check_text env at s = local_error env at "M0049" "string literal \"%s\": is not valid utf8" (String.escaped s); s -let set_lit env lit t = - if not env.skip_note_typ then - lit := t - let infer_lit env lit at : T.prim = match !lit with | NullLit -> T.Null @@ -1174,19 +1180,19 @@ let infer_lit env lit at : T.prim = | BlobLit _ -> T.Blob | PreLit (s, T.Nat) -> if not env.pre then - set_lit env lit (NatLit (check_nat env at s)); (* default *) + set env lit (NatLit (check_nat env at s)); (* default *) T.Nat | PreLit (s, T.Int) -> if not env.pre then - set_lit env lit (IntLit (check_int env at s)); (* default *) + set env lit (IntLit (check_int env at s)); (* default *) T.Int | PreLit (s, T.Float) -> if not env.pre then - set_lit env lit (FloatLit (check_float env at s)); (* default *) + set env lit (FloatLit (check_float env at s)); (* default *) T.Float | PreLit (s, T.Text) -> if not env.pre then - set_lit env lit (TextLit (check_text env at s)); (* default *) + set env lit (TextLit (check_text env at s)); (* default *) T.Text | PreLit _ -> assert false @@ -1194,29 +1200,29 @@ let infer_lit env lit at : T.prim = let check_lit env t lit at suggest = match t, !lit with | T.Prim T.Nat, PreLit (s, T.Nat) -> - set_lit env lit (NatLit (check_nat env at s)) + set env lit (NatLit (check_nat env at s)) | T.Prim T.Nat8, PreLit (s, T.Nat) -> - set_lit env lit (Nat8Lit (check_nat8 env at s)) + set env lit (Nat8Lit (check_nat8 env at s)) | T.Prim T.Nat16, PreLit (s, T.Nat) -> - set_lit env lit (Nat16Lit (check_nat16 env at s)) + set env lit (Nat16Lit (check_nat16 env at s)) | T.Prim T.Nat32, PreLit (s, T.Nat) -> - set_lit env lit (Nat32Lit (check_nat32 env at s)) + set env lit (Nat32Lit (check_nat32 env at s)) | T.Prim T.Nat64, PreLit (s, T.Nat) -> - set_lit env lit (Nat64Lit (check_nat64 env at s)) + set env lit (Nat64Lit (check_nat64 env at s)) | T.Prim T.Int, PreLit (s, (T.Nat | T.Int)) -> - set_lit env lit (IntLit (check_int env at s)) + set env lit (IntLit (check_int env at s)) | T.Prim T.Int8, PreLit (s, (T.Nat | T.Int)) -> - set_lit env lit (Int8Lit (check_int8 env at s)) + set env lit (Int8Lit (check_int8 env at s)) | T.Prim T.Int16, PreLit (s, (T.Nat | T.Int)) -> - set_lit env lit (Int16Lit (check_int16 env at s)) + set env lit (Int16Lit (check_int16 env at s)) | T.Prim T.Int32, PreLit (s, (T.Nat | T.Int)) -> - set_lit env lit (Int32Lit (check_int32 env at s)) + set env lit (Int32Lit (check_int32 env at s)) | T.Prim T.Int64, PreLit (s, (T.Nat | T.Int)) -> - set_lit env lit (Int64Lit (check_int64 env at s)) + set env lit (Int64Lit (check_int64 env at s)) | T.Prim T.Float, PreLit (s, (T.Nat | T.Int | T.Float)) -> - set_lit env lit (FloatLit (check_float env at s)) + set env lit (FloatLit (check_float env at s)) | T.Prim T.Blob, PreLit (s, T.Text) -> - set_lit env lit (BlobLit s) + set env lit (BlobLit s) | t, _ -> let t' = T.Prim (infer_lit env lit at) in if not (sub env at t' t) then @@ -1720,8 +1726,7 @@ and infer_exp'' env exp : T.typ = if not (Operator.has_unop op t) then error env exp.at "M0059" "operator is not defined for operand type%a" display_typ_expand t; - if not env.skip_note_typ then - ot := t + set env ot t end; t | BinE (ot, exp1, op, exp2) -> @@ -1734,8 +1739,7 @@ and infer_exp'' env exp : T.typ = else if op = Operator.SubOp && eq env exp.at t T.nat then warn env exp.at "M0155" "operator may trap for inferred type%a" display_typ_expand t; - if not env.skip_note_typ then - ot := t + set env ot t end; t | RelE (ot, exp1, op, exp2) -> @@ -1757,8 +1761,7 @@ and infer_exp'' env exp : T.typ = display_typ_expand t1 display_typ_expand t2 display_typ_expand t; - if not env.skip_note_typ then - ot := t + set env ot t end; T.bool | ShowE (ot, exp1) -> @@ -1767,8 +1770,7 @@ and infer_exp'' env exp : T.typ = if not (Show.can_show t) then error env exp.at "M0063" "show is not defined for operand type%a" display_typ_expand t; - if not env.skip_note_typ then - ot := t + set env ot t end; T.text | ToCandidE exps -> @@ -1922,8 +1924,7 @@ and infer_exp'' env exp : T.typ = let t1, ve1 = infer_pat_exhaustive (if T.is_shared_sort sort then local_error else warn) env' pat in let ve2 = T.Env.adjoin ve ve1 in let ts2 = List.map (check_typ_item env') ts2 in - if not env.skip_note_typ then - typ.note <- T.seq ts2; (* HACK *) + set_note env typ (T.seq ts2); (* HACK *) let codom = T.codom c (fun () -> T.Con(List.hd cs,[])) ts2 in if not env.pre then begin let env'' = @@ -2398,13 +2399,11 @@ and check_exp' env0 t exp : T.typ = | _ -> error env exp.at "M0090" "actor reference must have an actor type" end | UnE (ot, op, exp1), _ when Operator.has_unop op t -> - if not env.skip_note_typ then - ot := t; + set env ot t; check_exp env t exp1; t | BinE (ot, exp1, op, exp2), _ when Operator.has_binop op t -> - if not env.skip_note_typ then - ot := t; + set env ot t; check_exp env t exp1; check_exp env t exp2; if env.weak && op = Operator.SubOp && eq env exp.at t T.nat then @@ -2814,7 +2813,7 @@ and infer_call env exp1 inst (parenthesized, ref_exp2) at t_expect_opt = then wrong_call_args env tbs exp2.at t_args implicits_arity syntax_args else T.seq t_args in - if not env.pre && not env.skip_note_typ then ref_exp2 := exp2; (* TODO: is this good enough *) + if not env.pre then set env ref_exp2 exp2; (* TODO: is this good enough *) let ts, t_arg', t_ret' = match tbs, inst.it with | [], (None | Some (_, [])) (* no inference required *) @@ -2836,8 +2835,7 @@ and infer_call env exp1 inst (parenthesized, ref_exp2) at t_expect_opt = | _::_, None -> (* implicit, infer *) infer_call_instantiation env t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt extra_subtype_problems in - if not env.skip_note_typ then - inst.note <- ts; + set_note env inst ts; if not env.pre then begin if Type.is_shared_sort sort then begin if not (T.concrete t_arg') then @@ -3143,8 +3141,7 @@ and infer_pat_exhaustive warnOrError env pat : T.typ * Scope.val_env = and infer_pat name_types env pat : T.typ * Scope.val_env = assert (env.skip_note_typ || pat.note = T.Pre); let t, ve = infer_pat' name_types env pat in - if not env.pre && not env.skip_note_typ then - pat.note <- T.normalize t; + if not env.pre then set_note env pat (T.normalize t); t, ve and infer_pat' name_types env pat : T.typ * Scope.val_env = @@ -3259,7 +3256,7 @@ and check_pat_aux env t pat val_kind : Scope.val_env = if t = T.Pre then snd (infer_pat false env pat) else let t' = T.normalize t in let ve = check_pat_aux' env t' pat val_kind in - if not env.pre && not env.skip_note_typ then pat.note <- t'; + if not env.pre then set_note env pat t'; ve and check_pat_aux' env t pat val_kind : Scope.val_env = @@ -4158,8 +4155,7 @@ and check_dec env t dec = match dec.it with | ExpD exp -> check_exp env t exp; - if not env.skip_note_typ then - dec.note <- exp.note + set_note env dec exp.note | _ -> let t' = infer_dec env dec in if not (eq env dec.at t T.unit || sub env dec.at t' t) then From 82c5b00c2d2e12b6aa792d7f38328dc013d698c4 Mon Sep 17 00:00:00 2001 From: Kamil Listopad Date: Mon, 27 Oct 2025 13:51:44 +0100 Subject: [PATCH 07/19] is_warning_enabled when not env.errors_only --- src/mo_frontend/typing.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index 444c493dfc0..6037bef3e8f 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -250,6 +250,9 @@ let info env at fmt = Format.kasprintf (fun s -> if not env.errors_only then Diag.add_msg env.msgs (type_info at s)) fmt +let is_warning_enabled env code = + not env.errors_only && Flags.is_warning_enabled code + let check_deprecation env at desc id depr = match depr with | Some ("M0235" as code) -> @@ -1618,7 +1621,7 @@ let contextual_dot env name receiver_ty : (ctx_dot_candidate, 'a context_dot_err let check_can_dot env ctx_dot (exp : Syntax.exp) tys es at = if not env.pre then - if Flags.get_warning_level "M0236" <> Flags.Allow then + if is_warning_enabled env "M0236" then match ctx_dot with | Some _ -> () (* already dotted *) | None -> @@ -2733,7 +2736,7 @@ and insert_holes at ts es = | args -> TupE args and check_explicit_arguments env saturated_arity implicits_arity arg_typs syntax_args = - if Flags.get_warning_level "M0237" <> Flags.Allow then + if is_warning_enabled env "M0237" then if List.length syntax_args = saturated_arity && implicits_arity < saturated_arity then let _, explicit_implicits = List.fold_right2 (fun typ arg (pos, acc) -> @@ -2825,7 +2828,7 @@ and infer_call env exp1 inst (parenthesized, ref_exp2) at t_expect_opt = let t_arg' = T.open_ ts t_arg in let t_ret' = T.open_ ts t_ret in if not env.pre then begin - if typs <> [] && Flags.is_warning_enabled "M0223" && + if typs <> [] && is_warning_enabled env "M0223" && is_redundant_instantiation ts env (fun env' -> infer_call_instantiation env' t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt extra_subtype_problems) then warn env inst.at "M0223" "redundant type instantiation"; From 82c3624077ab9179e462567f6f3376c8ef4215f1 Mon Sep 17 00:00:00 2001 From: Kamil Listopad Date: Mon, 27 Oct 2025 13:53:38 +0100 Subject: [PATCH 08/19] changelog --- Changelog.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Changelog.md b/Changelog.md index 742aaacb166..551132e92fe 100644 --- a/Changelog.md +++ b/Changelog.md @@ -4,6 +4,8 @@ * motoko (`moc`) + * Fix the `M0223` warning check for redundant type instantiations to avoid false positives (#5605). + * Enable parser recovery to gather more syntax errors at once (previously only enabled for `moc.js`) (#5589). * Custom syntax error message when a record is provided where a block is expected (#5589). From 9632e766899f9fef4639f7daa7cd583abcedcfff Mon Sep 17 00:00:00 2001 From: Kamil Listopad Date: Mon, 27 Oct 2025 15:03:49 +0100 Subject: [PATCH 09/19] double redundant, but should be only one --- test/run/ok/redundant-instantiations.tc.ok | 2 ++ test/run/redundant-instantiations.mo | 30 ++++++++++++++++++++++ 2 files changed, 32 insertions(+) diff --git a/test/run/ok/redundant-instantiations.tc.ok b/test/run/ok/redundant-instantiations.tc.ok index 975294dcdf0..b30bf5a3297 100644 --- a/test/run/ok/redundant-instantiations.tc.ok +++ b/test/run/ok/redundant-instantiations.tc.ok @@ -5,3 +5,5 @@ redundant-instantiations.mo:45.18-45.24: warning [M0223], redundant type instant redundant-instantiations.mo:52.24-52.30: warning [M0223], redundant type instantiation redundant-instantiations.mo:54.26-54.32: warning [M0223], redundant type instantiation redundant-instantiations.mo:56.28-56.34: warning [M0223], redundant type instantiation +redundant-instantiations.mo:79.35-79.45: warning [M0223], redundant type instantiation +redundant-instantiations.mo:81.38-81.42: warning [M0223], redundant type instantiation diff --git a/test/run/redundant-instantiations.mo b/test/run/redundant-instantiations.mo index 208f62c8627..7a3d8b7dcef 100644 --- a/test/run/redundant-instantiations.mo +++ b/test/run/redundant-instantiations.mo @@ -73,4 +73,34 @@ module Nested { })[1]; })[1]; }; + + type R = { x : Int; y : Nat }; + public func testVarTab0() { + var grid = Prim.Array_tabulate<[var ?R]>( // Redundant + 3, + func _ = Prim.Array_tabulateVar(5, func _ = null), // TODO: Should not be redundant because the other already is + ); + ignore grid; + }; + public func testVarTab1() { + var grid = Prim.Array_tabulate<[var ?R]>( + 3, + func _ = Prim.Array_tabulateVar(5, func _ = null), + ); + ignore grid; + }; + public func testVarTab2() { + var grid = Prim.Array_tabulate( + 3, + func _ = Prim.Array_tabulateVar(5, func _ = null), + ); + ignore grid; + }; + public func testVarTab3() { + var grid : [[var ?R]] = Prim.Array_tabulate( + 3, + func _ = Prim.Array_tabulateVar(5, func _ = null) // TODO: why this instantiation is not redundant? + ); + ignore grid; + }; }; From 82bc000fcb106b9b7254eed8cc5fe6171623abb1 Mon Sep 17 00:00:00 2001 From: Kamil Listopad Date: Tue, 28 Oct 2025 10:33:30 +0100 Subject: [PATCH 10/19] when redundant avoid check_exp, infer instead --- src/mo_frontend/typing.ml | 26 +++++++++++++++------- test/run/ok/redundant-instantiations.tc.ok | 1 - test/run/redundant-instantiations.mo | 2 +- 3 files changed, 19 insertions(+), 10 deletions(-) diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index 6037bef3e8f..5658eab1ddb 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -2827,14 +2827,24 @@ and infer_call env exp1 inst (parenthesized, ref_exp2) at t_expect_opt = let ts = check_inst_bounds env sort tbs typs t_ret at in let t_arg' = T.open_ ts t_arg in let t_ret' = T.open_ ts t_ret in - if not env.pre then begin - if typs <> [] && is_warning_enabled env "M0223" && - is_redundant_instantiation ts env (fun env' -> - infer_call_instantiation env' t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt extra_subtype_problems) then - warn env inst.at "M0223" "redundant type instantiation"; - check_exp_strong env t_arg' exp2; - end; - ts, t_arg', t_ret' + + if not env.pre && typs <> [] && is_warning_enabled env "M0223" && + is_redundant_instantiation ts env (fun env' -> + infer_call_instantiation env' t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt extra_subtype_problems) + then ( + warn env inst.at "M0223" "redundant type instantiation"; + (* Continue as if there was no instantiation. Needed because: + 1. Correctly influences nested instantiations, avoiding emitting too many warnings, e.g. + When there are 2 nested instantiations, one of them might be necessary, + but in isolation both might be redundant. Emit a warning only for the 1st one) + 2. Infer again, but now without the skip_note_typ to commit the state + *) + let env = { env with weak = false } in + infer_call_instantiation env t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt extra_subtype_problems) + else ( + if not env.pre then + check_exp_strong env t_arg' exp2; + ts, t_arg', t_ret') | _::_, None -> (* implicit, infer *) infer_call_instantiation env t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt extra_subtype_problems in diff --git a/test/run/ok/redundant-instantiations.tc.ok b/test/run/ok/redundant-instantiations.tc.ok index b30bf5a3297..f7e6d50958f 100644 --- a/test/run/ok/redundant-instantiations.tc.ok +++ b/test/run/ok/redundant-instantiations.tc.ok @@ -6,4 +6,3 @@ redundant-instantiations.mo:52.24-52.30: warning [M0223], redundant type instant redundant-instantiations.mo:54.26-54.32: warning [M0223], redundant type instantiation redundant-instantiations.mo:56.28-56.34: warning [M0223], redundant type instantiation redundant-instantiations.mo:79.35-79.45: warning [M0223], redundant type instantiation -redundant-instantiations.mo:81.38-81.42: warning [M0223], redundant type instantiation diff --git a/test/run/redundant-instantiations.mo b/test/run/redundant-instantiations.mo index 7a3d8b7dcef..ed1dbd52115 100644 --- a/test/run/redundant-instantiations.mo +++ b/test/run/redundant-instantiations.mo @@ -78,7 +78,7 @@ module Nested { public func testVarTab0() { var grid = Prim.Array_tabulate<[var ?R]>( // Redundant 3, - func _ = Prim.Array_tabulateVar(5, func _ = null), // TODO: Should not be redundant because the other already is + func _ = Prim.Array_tabulateVar(5, func _ = null), // Should NOT be redundant. Only one of these two is redundant. ); ignore grid; }; From d2e80fc16e19507280150ef1a1fd2b3636b971b2 Mon Sep 17 00:00:00 2001 From: Kamil Listopad Date: Tue, 28 Oct 2025 10:46:43 +0100 Subject: [PATCH 11/19] BimatchRet --- src/mo_frontend/typing.ml | 44 +++++++++++++--------- test/run/lambdas-core.mo | 17 ++++----- test/run/ok/lambdas-core.tc.ok | 1 + test/run/ok/redundant-instantiations.tc.ok | 2 +- test/run/redundant-instantiations.mo | 7 ++-- 5 files changed, 39 insertions(+), 32 deletions(-) diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index 5658eab1ddb..f2181022b23 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -19,7 +19,6 @@ module S = Set.Make(String) type avl = Available | Unavailable type lab_env = T.typ T.Env.t -type ret_env = T.typ option type val_info = T.typ * Source.region * Scope.val_kind * avl type val_env = val_info T.Env.t @@ -69,6 +68,10 @@ type env = errors_only : bool; srcs : Field_sources.t; } +and ret_env = + | NoRet + | Ret of T.typ + | BimatchRet of (env -> exp -> unit) let env_of_scope ?(viper_mode=false) msgs scope = { vals = available scope.Scope.val_env; @@ -78,7 +81,7 @@ let env_of_scope ?(viper_mode=false) msgs scope = cons = scope.Scope.con_env; objs = T.Env.empty; labs = T.Env.empty; - rets = None; + rets = NoRet; async = Async_cap.NullCap; in_actor = false; in_prog = true; @@ -1933,7 +1936,7 @@ and infer_exp'' env exp : T.typ = let env'' = { env' with labs = T.Env.empty; - rets = Some codom; + rets = Ret codom; (* async = None; *) } in let initial_usage = enter_scope env'' in @@ -2023,7 +2026,7 @@ and infer_exp'' env exp : T.typ = check_ErrorCap env "try" exp.at; if cases <> [] then coverage_cases "try handler" env cases T.catch exp.at; - Option.iter (check_exp_strong { env with async = C.NullCap; rets = None; labs = T.Env.empty } T.unit) exp2_opt + Option.iter (check_exp_strong { env with async = C.NullCap; rets = NoRet; labs = T.Env.empty } T.unit) exp2_opt end; T.lub ~src_fields:env.srcs t1 t2 | WhileE (exp1, exp2) -> @@ -2085,11 +2088,13 @@ and infer_exp'' env exp : T.typ = | RetE exp1 -> if not env.pre then begin match env.rets with - | Some T.Pre -> + | Ret T.Pre -> local_error env exp.at "M0084" "cannot infer return type" - | Some t -> + | Ret t -> check_exp_strong env t exp1 - | None -> + | BimatchRet k -> + k env exp1 + | NoRet -> local_error env exp.at "M0085" "misplaced return" end; T.Non @@ -2109,7 +2114,7 @@ and infer_exp'' env exp : T.typ = let env' = {(adjoin_typs env ce_scope cs) with labs = T.Env.empty; - rets = Some T.Pre; + rets = Ret T.Pre; async = next_cap c; scopes = T.ConEnv.add c exp.at env.scopes } in let t = infer_exp env' exp1 in @@ -2497,7 +2502,7 @@ and check_exp' env0 t exp : T.typ = let env' = {(adjoin_typs env ce_scope cs) with labs = T.Env.empty; - rets = Some t'; + rets = Ret t'; async = next_cap c; scopes = T.ConEnv.add c exp.at env.scopes; } in @@ -2524,7 +2529,7 @@ and check_exp' env0 t exp : T.typ = if cases <> [] then coverage_cases "try handler" env cases T.catch exp.at; if not env.pre then - Option.iter (check_exp_strong { env with async = C.NullCap; rets = None; labs = T.Env.empty; } T.unit) exp2_opt; + Option.iter (check_exp_strong { env with async = C.NullCap; rets = NoRet; labs = T.Env.empty } T.unit) exp2_opt; t (* TODO: allow shared with one scope par *) | FuncE (_, shared_pat, [], pat, typ_opt, _sugar, exp), T.Func (s, c, [], ts1, ts2) -> @@ -2610,7 +2615,7 @@ and check_func_step in_actor env (shared_pat, pat, typ_opt, exp) (s, c, ts1, ts2 let env' = { env with labs = T.Env.empty; - rets = Some exp_typ; + rets = Ret exp_typ; async = C.NullCap; } in (adjoin_vals env' ve2), exp_typ, codom @@ -2970,6 +2975,10 @@ and infer_call_instantiation env t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt (* Prepare subtyping constraints for the 2nd round *) let subs = ref [] in + let infer_body body_typ env body = + let actual_t = infer_exp env body in + subs := (actual_t, body_typ) :: !subs + in deferred |> List.iter (fun (exp, typ) -> (* Substitute fixed type variables *) let typ = T.open_ ts typ in @@ -2983,7 +2992,7 @@ and infer_call_instantiation env t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt let closed_codom = Bi_match.is_closed remaining codom in (* Closed [codom] implies closed [body_typ]. [body_typ] is closed when it comes from [typ_opt] *) let closed_body_typ = closed_codom || Option.is_some typ_opt in - let env' = if closed_body_typ then env' else { env' with rets = None } in + let env' = if closed_body_typ then env' else { env' with rets = BimatchRet (infer_body body_typ) } in if closed_body_typ && not env.pre then begin assert (Bi_match.is_closed remaining body_typ); check_exp env' body_typ body; @@ -2996,8 +3005,7 @@ and infer_call_instantiation env t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt subs := (body_typ, codom) :: !subs else begin (* We just have open [codom], we need to infer the body *) - let actual_t = infer_exp env' body in - subs := (actual_t, body_typ) :: !subs; + infer_body body_typ env' body; end | HoleE _, typ -> if not env.pre then begin @@ -3668,7 +3676,7 @@ and infer_obj env obj_sort exp_opt dec_fields at : T.typ = { env with in_actor = true; labs = T.Env.empty; - rets = None; + rets = NoRet; } in let decs = List.map (fun (df : dec_field) -> df.it.dec) dec_fields in @@ -3788,7 +3796,7 @@ and infer_migration env obj_sort exp_opt = if obj_sort.it <> T.Actor then local_error env exp.at "M0209" "misplaced actor migration expression on module or object"; - infer_exp_promote { env with async = C.NullCap; rets = None; labs = T.Env.empty } exp) + infer_exp_promote { env with async = C.NullCap; rets = NoRet; labs = T.Env.empty } exp) exp_opt and check_migration env (stab_tfs : T.field list) exp_opt = @@ -4101,7 +4109,7 @@ and infer_dec env dec : T.typ = let env''' = { (add_val env'' self_id self_typ) with labs = T.Env.empty; - rets = None; + rets = NoRet; async = async_cap; in_actor; } @@ -4422,7 +4430,7 @@ and infer_dec_typdecs env dec : Scope.t = let env'' = { (add_val (adjoin_vals env' ve) self_id self_typ) with labs = T.Env.empty; - rets = None; + rets = NoRet; async = async_cap; in_actor} in diff --git a/test/run/lambdas-core.mo b/test/run/lambdas-core.mo index c1bf839bcc3..dd2058fa810 100644 --- a/test/run/lambdas-core.mo +++ b/test/run/lambdas-core.mo @@ -553,17 +553,16 @@ module Return { }); assert ar == []; }; - // Future work: improve type inference to handle `return` - // public func test2() { - // let ar = Array.tabulate(3, func i { - // if (i == 0) return false; - // true; - // }); - // assert ar == [false, true, true]; - // }; + public func test2() { + let ar = Array.tabulate(3, func i { + if (i == 0) return false; + true; + }); + assert ar == []; + }; }; Return.test1(); -// Return.test2(); +Return.test2(); //SKIP comp //SKIP run-ir diff --git a/test/run/ok/lambdas-core.tc.ok b/test/run/ok/lambdas-core.tc.ok index 580887ce748..ed7579e47f9 100644 --- a/test/run/ok/lambdas-core.tc.ok +++ b/test/run/ok/lambdas-core.tc.ok @@ -4,3 +4,4 @@ lambdas-core.mo:480.22-480.33: warning [M0223], redundant type instantiation lambdas-core.mo:483.28-483.39: warning [M0223], redundant type instantiation lambdas-core.mo:500.17-500.34: warning [M0223], redundant type instantiation lambdas-core.mo:513.22-513.39: warning [M0223], redundant type instantiation +lambdas-core.mo:550.28-550.34: warning [M0223], redundant type instantiation diff --git a/test/run/ok/redundant-instantiations.tc.ok b/test/run/ok/redundant-instantiations.tc.ok index f7e6d50958f..21473acd64e 100644 --- a/test/run/ok/redundant-instantiations.tc.ok +++ b/test/run/ok/redundant-instantiations.tc.ok @@ -5,4 +5,4 @@ redundant-instantiations.mo:45.18-45.24: warning [M0223], redundant type instant redundant-instantiations.mo:52.24-52.30: warning [M0223], redundant type instantiation redundant-instantiations.mo:54.26-54.32: warning [M0223], redundant type instantiation redundant-instantiations.mo:56.28-56.34: warning [M0223], redundant type instantiation -redundant-instantiations.mo:79.35-79.45: warning [M0223], redundant type instantiation +redundant-instantiations.mo:78.35-78.45: warning [M0223], redundant type instantiation diff --git a/test/run/redundant-instantiations.mo b/test/run/redundant-instantiations.mo index ed1dbd52115..ade35652f6b 100644 --- a/test/run/redundant-instantiations.mo +++ b/test/run/redundant-instantiations.mo @@ -60,13 +60,12 @@ module Nested { })[1]; })[1]; }; - // Future work: improve type inference to handle `return` and detect these redundant instantiations public func testWithReturns() : Bool { - Prim.Array_tabulate(2, func i { + Prim.Array_tabulate(2, func i { if (i == 0) return false; - Prim.Array_tabulate(2, func i { + Prim.Array_tabulate(2, func i { if (i == 0) return false; - Prim.Array_tabulate(2, func i { + Prim.Array_tabulate(2, func i { if (i == 0) return false; true; })[1]; From b76dc907622b94e0e11f0707b550df4be0d066b5 Mon Sep 17 00:00:00 2001 From: Kamil Listopad Date: Tue, 28 Oct 2025 13:50:09 +0100 Subject: [PATCH 12/19] revert some from #5615 --- Changelog.md | 3 --- src/mo_frontend/typing.ml | 1 + test/{run => fail}/lambdas-core.mo | 20 -------------------- test/{run => fail}/ok/lambdas-core.tc.ok | 1 - 4 files changed, 1 insertion(+), 24 deletions(-) rename test/{run => fail}/lambdas-core.mo (98%) rename test/{run => fail}/ok/lambdas-core.tc.ok (85%) diff --git a/Changelog.md b/Changelog.md index 72e3bcfe297..97a5d14f3ae 100644 --- a/Changelog.md +++ b/Changelog.md @@ -6,9 +6,6 @@ * Fix the `M0223` warning check for redundant type instantiations to avoid false positives (#5605). - * Fixes type inference of deferred funcs that use `return` in their body (#5605). - Avoids confusing errors like `Bool does not have expected type T` on `return` expressions. Should type check successfully now. - * Use `self` parameter, not `Self` type, to enable contextual dot notation (#5574). * Enable parser recovery to gather more syntax errors at once (previously only enabled for `moc.js`) (#5589). diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index 067bad35bb7..90e154b91c2 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -19,6 +19,7 @@ module S = Set.Make(String) type avl = Available | Unavailable type lab_env = T.typ T.Env.t +type ret_env = T.typ option type val_info = T.typ * Source.region * Scope.val_kind * avl type val_env = val_info T.Env.t diff --git a/test/run/lambdas-core.mo b/test/fail/lambdas-core.mo similarity index 98% rename from test/run/lambdas-core.mo rename to test/fail/lambdas-core.mo index dd2058fa810..4982fb74557 100644 --- a/test/run/lambdas-core.mo +++ b/test/fail/lambdas-core.mo @@ -544,26 +544,6 @@ module Issue5418 { ); }; }; - -module Return { - public func test1() { - let ar = Array.tabulate(3, func i { - if (i == 0) return false; - true; - }); - assert ar == []; - }; - public func test2() { - let ar = Array.tabulate(3, func i { - if (i == 0) return false; - true; - }); - assert ar == []; - }; -}; -Return.test1(); -Return.test2(); - //SKIP comp //SKIP run-ir //SKIP run-low diff --git a/test/run/ok/lambdas-core.tc.ok b/test/fail/ok/lambdas-core.tc.ok similarity index 85% rename from test/run/ok/lambdas-core.tc.ok rename to test/fail/ok/lambdas-core.tc.ok index ed7579e47f9..580887ce748 100644 --- a/test/run/ok/lambdas-core.tc.ok +++ b/test/fail/ok/lambdas-core.tc.ok @@ -4,4 +4,3 @@ lambdas-core.mo:480.22-480.33: warning [M0223], redundant type instantiation lambdas-core.mo:483.28-483.39: warning [M0223], redundant type instantiation lambdas-core.mo:500.17-500.34: warning [M0223], redundant type instantiation lambdas-core.mo:513.22-513.39: warning [M0223], redundant type instantiation -lambdas-core.mo:550.28-550.34: warning [M0223], redundant type instantiation From b77ce37f2039b034f301531ffa32d3458ebac678 Mon Sep 17 00:00:00 2001 From: Kamil Listopad Date: Tue, 28 Oct 2025 13:51:06 +0100 Subject: [PATCH 13/19] revert more --- src/mo_frontend/typing.ml | 34 ++++++++++++++-------------------- 1 file changed, 14 insertions(+), 20 deletions(-) diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index 90e154b91c2..30f8592258f 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -69,10 +69,6 @@ type env = errors_only : bool; srcs : Field_sources.t; } -and ret_env = - | NoRet - | Ret of T.typ - | BimatchRet of (env -> exp -> unit) let env_of_scope ?(viper_mode=false) msgs scope = { vals = available scope.Scope.val_env; @@ -82,7 +78,7 @@ let env_of_scope ?(viper_mode=false) msgs scope = cons = scope.Scope.con_env; objs = T.Env.empty; labs = T.Env.empty; - rets = NoRet; + rets = None; async = Async_cap.NullCap; in_actor = false; in_prog = true; @@ -1927,7 +1923,7 @@ and infer_exp'' env exp : T.typ = let env'' = { env' with labs = T.Env.empty; - rets = Ret codom; + rets = Some codom; (* async = None; *) } in let initial_usage = enter_scope env'' in @@ -2017,7 +2013,7 @@ and infer_exp'' env exp : T.typ = check_ErrorCap env "try" exp.at; if cases <> [] then coverage_cases "try handler" env cases T.catch exp.at; - Option.iter (check_exp_strong { env with async = C.NullCap; rets = NoRet; labs = T.Env.empty } T.unit) exp2_opt + Option.iter (check_exp_strong { env with async = C.NullCap; rets = None; labs = T.Env.empty } T.unit) exp2_opt end; T.lub ~src_fields:env.srcs t1 t2 | WhileE (exp1, exp2) -> @@ -2079,13 +2075,11 @@ and infer_exp'' env exp : T.typ = | RetE exp1 -> if not env.pre then begin match env.rets with - | Ret T.Pre -> + | Some T.Pre -> local_error env exp.at "M0084" "cannot infer return type" - | Ret t -> + | Some t -> check_exp_strong env t exp1 - | BimatchRet k -> - k env exp1 - | NoRet -> + | None -> local_error env exp.at "M0085" "misplaced return" end; T.Non @@ -2105,7 +2099,7 @@ and infer_exp'' env exp : T.typ = let env' = {(adjoin_typs env ce_scope cs) with labs = T.Env.empty; - rets = Ret T.Pre; + rets = Some T.Pre; async = next_cap c; scopes = T.ConEnv.add c exp.at env.scopes } in let t = infer_exp env' exp1 in @@ -2493,7 +2487,7 @@ and check_exp' env0 t exp : T.typ = let env' = {(adjoin_typs env ce_scope cs) with labs = T.Env.empty; - rets = Ret t'; + rets = Some t'; async = next_cap c; scopes = T.ConEnv.add c exp.at env.scopes; } in @@ -2520,7 +2514,7 @@ and check_exp' env0 t exp : T.typ = if cases <> [] then coverage_cases "try handler" env cases T.catch exp.at; if not env.pre then - Option.iter (check_exp_strong { env with async = C.NullCap; rets = NoRet; labs = T.Env.empty } T.unit) exp2_opt; + Option.iter (check_exp_strong { env with async = C.NullCap; rets = None; labs = T.Env.empty } T.unit) exp2_opt; t (* TODO: allow shared with one scope par *) | FuncE (_, shared_pat, [], pat, typ_opt, _sugar, exp), T.Func (s, c, [], ts1, ts2) -> @@ -2606,7 +2600,7 @@ and check_func_step in_actor env (shared_pat, pat, typ_opt, exp) (s, c, ts1, ts2 let env' = { env with labs = T.Env.empty; - rets = Ret exp_typ; + rets = Some exp_typ; async = C.NullCap; } in (adjoin_vals env' ve2), exp_typ, codom @@ -3667,7 +3661,7 @@ and infer_obj env obj_sort exp_opt dec_fields at : T.typ = { env with in_actor = true; labs = T.Env.empty; - rets = NoRet; + rets = None; } in let decs = List.map (fun (df : dec_field) -> df.it.dec) dec_fields in @@ -3787,7 +3781,7 @@ and infer_migration env obj_sort exp_opt = if obj_sort.it <> T.Actor then local_error env exp.at "M0209" "misplaced actor migration expression on module or object"; - infer_exp_promote { env with async = C.NullCap; rets = NoRet; labs = T.Env.empty } exp) + infer_exp_promote { env with async = C.NullCap; rets = None; labs = T.Env.empty } exp) exp_opt and check_migration env (stab_tfs : T.field list) exp_opt = @@ -4100,7 +4094,7 @@ and infer_dec env dec : T.typ = let env''' = { (add_val env'' self_id self_typ) with labs = T.Env.empty; - rets = NoRet; + rets = None; async = async_cap; in_actor; } @@ -4421,7 +4415,7 @@ and infer_dec_typdecs env dec : Scope.t = let env'' = { (add_val (adjoin_vals env' ve) self_id self_typ) with labs = T.Env.empty; - rets = NoRet; + rets = None; async = async_cap; in_actor} in From a5cce2c621227834da6e05588e310cf1501c0693 Mon Sep 17 00:00:00 2001 From: Kamil Listopad Date: Tue, 28 Oct 2025 13:52:59 +0100 Subject: [PATCH 14/19] revert more --- src/mo_frontend/typing.ml | 20 +++++++++----------- 1 file changed, 9 insertions(+), 11 deletions(-) diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index 30f8592258f..8f1262e26b5 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -2960,10 +2960,6 @@ and infer_call_instantiation env t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt (* Prepare subtyping constraints for the 2nd round *) let subs = ref [] in - let infer_body body_typ env body = - let actual_t = infer_exp env body in - subs := (actual_t, body_typ) :: !subs - in deferred |> List.iter (fun (exp, typ) -> (* Substitute fixed type variables *) let typ = T.open_ ts typ in @@ -2974,23 +2970,25 @@ and infer_call_instantiation env t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt (* Check the function input type and prepare for inferring the body *) let env', body_typ, codom = check_func_step false env (shared_pat, pat, typ_opt, body) (s, c, ts1, ts2) in (* [codom] comes from [ts2] which might contain unsolved type variables. *) - let closed_codom = Bi_match.is_closed remaining codom in - (* Closed [codom] implies closed [body_typ]. [body_typ] is closed when it comes from [typ_opt] *) - let closed_body_typ = closed_codom || Option.is_some typ_opt in - let env' = if closed_body_typ then env' else { env' with rets = BimatchRet (infer_body body_typ) } in - if closed_body_typ && not env.pre then begin + let closed = Bi_match.is_closed remaining codom in + if not env.pre && (closed || body_typ <> codom) then begin + (* Closed [codom] implies closed [body_typ]. + * [body_typ] is closed when it comes from [typ_opt] (which is when it is different from [codom]) + *) assert (Bi_match.is_closed remaining body_typ); + (* Since [body_typ] is closed, no need to infer *) check_exp env' body_typ body; end; (* When [codom] is open, we need to solve it *) - if not closed_codom then + if not closed then if body_typ <> codom then (* [body_typ] is closed, body is already checked above, we just need to solve the subtype problem *) subs := (body_typ, codom) :: !subs else begin (* We just have open [codom], we need to infer the body *) - infer_body body_typ env' body; + let actual_t = infer_exp env' body in + subs := (actual_t, body_typ) :: !subs; end | HoleE _, typ -> if not env.pre then begin From fb5890f4199120aa5547e701c77105cf27a9b75c Mon Sep 17 00:00:00 2001 From: Kamil Listopad Date: Tue, 28 Oct 2025 13:54:03 +0100 Subject: [PATCH 15/19] fix test --- test/run/ok/redundant-instantiations.tc.ok | 2 +- test/run/redundant-instantiations.mo | 12 ------------ 2 files changed, 1 insertion(+), 13 deletions(-) diff --git a/test/run/ok/redundant-instantiations.tc.ok b/test/run/ok/redundant-instantiations.tc.ok index 21473acd64e..9212efe47b0 100644 --- a/test/run/ok/redundant-instantiations.tc.ok +++ b/test/run/ok/redundant-instantiations.tc.ok @@ -5,4 +5,4 @@ redundant-instantiations.mo:45.18-45.24: warning [M0223], redundant type instant redundant-instantiations.mo:52.24-52.30: warning [M0223], redundant type instantiation redundant-instantiations.mo:54.26-54.32: warning [M0223], redundant type instantiation redundant-instantiations.mo:56.28-56.34: warning [M0223], redundant type instantiation -redundant-instantiations.mo:78.35-78.45: warning [M0223], redundant type instantiation +redundant-instantiations.mo:66.35-66.45: warning [M0223], redundant type instantiation diff --git a/test/run/redundant-instantiations.mo b/test/run/redundant-instantiations.mo index ade35652f6b..fd56236a327 100644 --- a/test/run/redundant-instantiations.mo +++ b/test/run/redundant-instantiations.mo @@ -60,18 +60,6 @@ module Nested { })[1]; })[1]; }; - public func testWithReturns() : Bool { - Prim.Array_tabulate(2, func i { - if (i == 0) return false; - Prim.Array_tabulate(2, func i { - if (i == 0) return false; - Prim.Array_tabulate(2, func i { - if (i == 0) return false; - true; - })[1]; - })[1]; - })[1]; - }; type R = { x : Int; y : Nat }; public func testVarTab0() { From 21ca3b3f826557a5d4eb6f602de4fe06186ec3bd Mon Sep 17 00:00:00 2001 From: Kamil Listopad Date: Tue, 28 Oct 2025 15:13:10 +0100 Subject: [PATCH 16/19] try revert strategy --- src/lang_utils/diag.ml | 4 + src/lang_utils/diag.mli | 4 + src/mo_frontend/typing.ml | 147 +++++++++++---------- test/run/ok/redundant-instantiations.tc.ok | 4 +- 4 files changed, 84 insertions(+), 75 deletions(-) diff --git a/src/lang_utils/diag.ml b/src/lang_utils/diag.ml index 142dd9d4f51..94e5ec3c7bb 100644 --- a/src/lang_utils/diag.ml +++ b/src/lang_utils/diag.ml @@ -120,3 +120,7 @@ let flush_messages : 'a result -> 'a option = function let run r = match flush_messages r with | None -> exit 1 | Some x -> x + +type save = messages +let save_store s = !s +let load_store s msgs = s := msgs diff --git a/src/lang_utils/diag.mli b/src/lang_utils/diag.mli index 7a350c30648..8c30acfbf74 100644 --- a/src/lang_utils/diag.mli +++ b/src/lang_utils/diag.mli @@ -62,3 +62,7 @@ val is_error_free : msg_store -> bool val add_msg : msg_store -> message -> unit val add_msgs : msg_store -> messages -> unit val with_message_store : ?allow_errors:bool -> (msg_store -> 'a option) -> 'a result + +type save +val save_store : msg_store -> save +val load_store : msg_store -> save -> unit diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index 8f1262e26b5..6310cb86867 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -37,6 +37,8 @@ let initial_scope = type unused_warnings = (string * Source.region * Scope.val_kind) List.t +type reverts = (unit -> unit) list + type env = { vals : val_env; libs : Scope.lib_env; @@ -56,8 +58,9 @@ type env = context : exp' list; (* [pre] phase skips thorough checks and avoids recording note types (and other internal state modifications) *) pre : bool; - (* [skip_note_typ] avoids recording note types. Used to perform full checking ([not pre]) without modifying the internal state *) - skip_note_typ : bool; + reverts : reverts ref option; + (* [redo] ignores and recalculates the state of the expressions *) + redo : bool; weak : bool; msgs : Diag.msg_store; scopes : Source.region T.ConEnv.t; @@ -84,7 +87,8 @@ let env_of_scope ?(viper_mode=false) msgs scope = in_prog = true; context = []; pre = false; - skip_note_typ = false; + reverts = None; + redo = false; weak = false; msgs; scopes = T.ConEnv.empty; @@ -103,12 +107,14 @@ let use_identifier env id = let is_unused_identifier env id = not (S.mem id !(env.used_identifiers)) -let set env lit t = - if not env.skip_note_typ then - lit := t +let commit env ref v = + env.reverts |> Option.iter (fun l -> + let old_v = !ref in + l := (fun () -> ref := old_v) :: !l); + ref := v let set_note env ap n = - if not env.skip_note_typ then + (* if not env.skip_note_typ then *) ap.note <- n let get_identifiers identifiers = @@ -1183,19 +1189,19 @@ let infer_lit env lit at : T.prim = | BlobLit _ -> T.Blob | PreLit (s, T.Nat) -> if not env.pre then - set env lit (NatLit (check_nat env at s)); (* default *) + commit env lit (NatLit (check_nat env at s)); (* default *) T.Nat | PreLit (s, T.Int) -> if not env.pre then - set env lit (IntLit (check_int env at s)); (* default *) + commit env lit (IntLit (check_int env at s)); (* default *) T.Int | PreLit (s, T.Float) -> if not env.pre then - set env lit (FloatLit (check_float env at s)); (* default *) + commit env lit (FloatLit (check_float env at s)); (* default *) T.Float | PreLit (s, T.Text) -> if not env.pre then - set env lit (TextLit (check_text env at s)); (* default *) + commit env lit (TextLit (check_text env at s)); (* default *) T.Text | PreLit _ -> assert false @@ -1203,29 +1209,29 @@ let infer_lit env lit at : T.prim = let check_lit env t lit at suggest = match t, !lit with | T.Prim T.Nat, PreLit (s, T.Nat) -> - set env lit (NatLit (check_nat env at s)) + commit env lit (NatLit (check_nat env at s)) | T.Prim T.Nat8, PreLit (s, T.Nat) -> - set env lit (Nat8Lit (check_nat8 env at s)) + commit env lit (Nat8Lit (check_nat8 env at s)) | T.Prim T.Nat16, PreLit (s, T.Nat) -> - set env lit (Nat16Lit (check_nat16 env at s)) + commit env lit (Nat16Lit (check_nat16 env at s)) | T.Prim T.Nat32, PreLit (s, T.Nat) -> - set env lit (Nat32Lit (check_nat32 env at s)) + commit env lit (Nat32Lit (check_nat32 env at s)) | T.Prim T.Nat64, PreLit (s, T.Nat) -> - set env lit (Nat64Lit (check_nat64 env at s)) + commit env lit (Nat64Lit (check_nat64 env at s)) | T.Prim T.Int, PreLit (s, (T.Nat | T.Int)) -> - set env lit (IntLit (check_int env at s)) + commit env lit (IntLit (check_int env at s)) | T.Prim T.Int8, PreLit (s, (T.Nat | T.Int)) -> - set env lit (Int8Lit (check_int8 env at s)) + commit env lit (Int8Lit (check_int8 env at s)) | T.Prim T.Int16, PreLit (s, (T.Nat | T.Int)) -> - set env lit (Int16Lit (check_int16 env at s)) + commit env lit (Int16Lit (check_int16 env at s)) | T.Prim T.Int32, PreLit (s, (T.Nat | T.Int)) -> - set env lit (Int32Lit (check_int32 env at s)) + commit env lit (Int32Lit (check_int32 env at s)) | T.Prim T.Int64, PreLit (s, (T.Nat | T.Int)) -> - set env lit (Int64Lit (check_int64 env at s)) + commit env lit (Int64Lit (check_int64 env at s)) | T.Prim T.Float, PreLit (s, (T.Nat | T.Int | T.Float)) -> - set env lit (FloatLit (check_float env at s)) + commit env lit (FloatLit (check_float env at s)) | T.Prim T.Blob, PreLit (s, T.Text) -> - set env lit (BlobLit s) + commit env lit (BlobLit s) | t, _ -> let t' = T.Prim (infer_lit env lit at) in if not (sub env at t' t) then @@ -1667,13 +1673,13 @@ and infer_exp_and_promote env exp : T.typ * T.typ = and infer_exp_wrapper inf f env exp : T.typ = - assert (env.skip_note_typ || exp.note.note_typ = T.Pre); + assert (env.redo || exp.note.note_typ = T.Pre); let t = inf env exp in assert (t <> T.Pre); let t' = f t in - if not (env.pre || env.skip_note_typ) then begin + if not env.pre then begin let t'' = T.normalize t' in - assert (t'' <> T.Pre); + assert (env.redo || t'' <> T.Pre); let note_eff = A.infer_effect_exp exp in exp.note <- {note_typ = if env.viper_mode then t' else t''; note_eff} end; @@ -1715,29 +1721,29 @@ and infer_exp'' env exp : T.typ = let t1 = infer_exp_promote env exp1 in let t = Operator.type_unop op t1 in if not env.pre then begin - assert (env.skip_note_typ || !ot = T.Pre); + assert (env.redo || !ot = T.Pre); if not (Operator.has_unop op t) then error env exp.at "M0059" "operator is not defined for operand type%a" display_typ_expand t; - set env ot t + commit env ot t end; t | BinE (ot, exp1, op, exp2) -> let t1, t2 = infer_bin_exp env exp1 exp2 in let t = Operator.type_binop op (T.lub ~src_fields:env.srcs (T.promote t1) (T.promote t2)) in if not env.pre then begin - assert (env.skip_note_typ || !ot = T.Pre); + assert (env.redo || !ot = T.Pre); if not (Operator.has_binop op t) then error_bin_op env exp.at t1 t2 else if op = Operator.SubOp && eq env exp.at t T.nat then warn env exp.at "M0155" "operator may trap for inferred type%a" display_typ_expand t; - set env ot t + commit env ot t end; t | RelE (ot, exp1, op, exp2) -> if not env.pre then begin - assert (env.skip_note_typ || !ot = T.Pre); + assert (env.redo || !ot = T.Pre); let t1, t2 = infer_bin_exp env exp1 exp2 in let t = Operator.type_relop op (T.lub ~src_fields:env.srcs (T.promote t1) (T.promote t2)) in if not (Operator.has_relop op t) then @@ -1754,7 +1760,7 @@ and infer_exp'' env exp : T.typ = display_typ_expand t1 display_typ_expand t2 display_typ_expand t; - set env ot t + commit env ot t end; T.bool | ShowE (ot, exp1) -> @@ -1763,7 +1769,7 @@ and infer_exp'' env exp : T.typ = if not (Show.can_show t) then error env exp.at "M0063" "show is not defined for operand type%a" display_typ_expand t; - set env ot t + commit env ot t end; T.text | ToCandidE exps -> @@ -2330,14 +2336,12 @@ and check_exp_weak env t exp = check_exp {env with weak = true} t exp and check_exp env t exp = - assert (env.skip_note_typ || not env.pre); - assert (env.skip_note_typ || exp.note.note_typ = T.Pre); + assert (not env.pre); + assert (env.redo || exp.note.note_typ = T.Pre); assert (t <> T.Pre); let t' = check_exp' env (T.normalize t) exp in - if not (env.skip_note_typ) then begin - let e = A.infer_effect_exp exp in - exp.note <- {exp.note with note_typ = t'; note_eff = e} - end + let e = A.infer_effect_exp exp in + exp.note <- {exp.note with note_typ = t'; note_eff = e} and check_exp' env0 t exp : T.typ = let env = {env0 with in_prog = false; in_actor = false; context = exp.it :: env0.context } in @@ -2392,11 +2396,11 @@ and check_exp' env0 t exp : T.typ = | _ -> error env exp.at "M0090" "actor reference must have an actor type" end | UnE (ot, op, exp1), _ when Operator.has_unop op t -> - set env ot t; + commit env ot t; check_exp env t exp1; t | BinE (ot, exp1, op, exp2), _ when Operator.has_binop op t -> - set env ot t; + commit env ot t; check_exp env t exp1; check_exp env t exp2; if env.weak && op = Operator.SubOp && eq env exp.at t T.nat then @@ -2806,7 +2810,7 @@ and infer_call env exp1 inst (parenthesized, ref_exp2) at t_expect_opt = then wrong_call_args env tbs exp2.at t_args implicits_arity syntax_args else T.seq t_args in - if not env.pre then set env ref_exp2 exp2; (* TODO: is this good enough *) + if not env.pre then commit env ref_exp2 exp2; (* TODO: is this good enough *) let ts, t_arg', t_ret' = match tbs, inst.it with | [], (None | Some (_, [])) (* no inference required *) @@ -2818,22 +2822,19 @@ and infer_call env exp1 inst (parenthesized, ref_exp2) at t_expect_opt = let t_arg' = T.open_ ts t_arg in let t_ret' = T.open_ ts t_ret in - if not env.pre && typs <> [] && is_warning_enabled env "M0223" && - is_redundant_instantiation ts env (fun env' -> + let try_redundant = + (* TODO: refactor all this into try_redundant_instantiation *) + if not env.pre && typs <> [] && is_warning_enabled env "M0223" then try_redundant_instantiation ts env (fun env' -> infer_call_instantiation env' t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt extra_subtype_problems) - then ( + else None + in + (match try_redundant with + | Some result -> warn env inst.at "M0223" "redundant type instantiation"; - (* Continue as if there was no instantiation. Needed because: - 1. Correctly influences nested instantiations, avoiding emitting too many warnings, e.g. - When there are 2 nested instantiations, one of them might be necessary, - but in isolation both might be redundant. Emit a warning only for the 1st one) - 2. Infer again, but now without the skip_note_typ to commit the state - *) - let env = { env with weak = false } in - infer_call_instantiation env t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt extra_subtype_problems) - else ( + result + | None -> if not env.pre then - check_exp_strong env t_arg' exp2; + check_exp_strong { env with redo = true } t_arg' exp2; ts, t_arg', t_ret') | _::_, None -> (* implicit, infer *) infer_call_instantiation env t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt extra_subtype_problems @@ -3078,18 +3079,22 @@ and infer_call_instantiation env t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt | Some t -> Format.asprintf "\nto produce result of expected type%a" display_typ t) -and is_redundant_instantiation ts env infer_instantiation = +and try_redundant_instantiation ts env infer_instantiation : (T.typ list * T.typ * T.typ) option = assert (not env.pre); - (* Perf: Skip checking nested instantiations to ensure that every instantiation is checked for redundancy exactly once *) - if env.skip_note_typ then false else - match Diag.with_message_store (recover_opt (fun msgs -> - let env_without_errors = { env with msgs; skip_note_typ = true } in - let ts', _, _ = infer_instantiation env_without_errors in - List.length ts = List.length ts' && List.for_all2 (T.eq ?src_fields:None) ts ts' - )) + let reverts = ref [] in + let env = { env with reverts = Some reverts } in + let save = Diag.save_store env.msgs in + match Option.join (recover_opt (fun env -> + let (ts', _, _) as r = infer_instantiation env in + if List.length ts = List.length ts' && List.for_all2 (T.eq ?src_fields:None) ts ts' + then Some r else None) env) with - | Error _ -> false - | Ok (b, _) -> b + | Some result -> Some result + | None -> + (* Revert on failure. *) + List.iter (fun revert -> revert ()) !reverts; + Diag.load_store env.msgs save; + None and debug_print_infer_defer_split exp2 t_arg t2 subs deferred = print_endline (Printf.sprintf "exp2 : %s" (Source.read_region_with_markers exp2.at |> Option.value ~default:"")); @@ -3143,7 +3148,7 @@ and infer_pat_exhaustive warnOrError env pat : T.typ * Scope.val_env = t, ve and infer_pat name_types env pat : T.typ * Scope.val_env = - assert (env.skip_note_typ || pat.note = T.Pre); + assert (env.redo || pat.note = T.Pre); let t, ve = infer_pat' name_types env pat in if not env.pre then set_note env pat (T.normalize t); t, ve @@ -3256,7 +3261,7 @@ and check_pat env t pat : Scope.val_env = check_pat_aux env t pat Scope.Declaration and check_pat_aux env t pat val_kind : Scope.val_env = - assert (env.skip_note_typ || pat.note = T.Pre); + assert (env.redo || pat.note = T.Pre); if t = T.Pre then snd (infer_pat false env pat) else let t' = T.normalize t in let ve = check_pat_aux' env t' pat val_kind in @@ -4130,9 +4135,8 @@ and infer_dec env dec : T.typ = | TypD _ -> T.unit in - if not env.skip_note_typ then ( - let eff = A.infer_effect_dec dec in - dec.note <- {empty_typ_note with note_typ = t; note_eff = eff}); + let eff = A.infer_effect_dec dec in + dec.note <- {empty_typ_note with note_typ = t; note_eff = eff}; t @@ -4255,7 +4259,6 @@ and gather_dec env scope dec : Scope.t = let pre_k = T.Abs (pre_tbs, T.Pre) in let c = match id.note with | None -> - assert (not env.skip_note_typ); let c = Cons.fresh id.it pre_k in id.note <- Some c; c | Some c -> c in @@ -4429,7 +4432,6 @@ and infer_id_typdecs env at id c k : Scope.con_env = assert (match k with T.Abs (_, T.Pre) -> false | _ -> true); (match Cons.kind c with | T.Abs (_, T.Pre) -> - assert (not env.skip_note_typ); T.set_kind c k; id.note <- Some c | k' -> assert (eq_kind env at k' k) (* may diverge on expansive types *) ); @@ -4586,7 +4588,6 @@ let check_lib scope pkg_opt lib : Scope.t Diag.result = let { imports; body = cub; _ } = lib.it in let (imp_ds, ds) = CompUnit.decs_of_lib lib in let typ, _ = infer_block env (imp_ds @ ds) lib.at false in - assert (not env.skip_note_typ); List.iter2 (fun import imp_d -> import.note <- imp_d.note.note_typ) imports imp_ds; cub.note <- {empty_typ_note with note_typ = typ}; let imp_scope = match cub.it with diff --git a/test/run/ok/redundant-instantiations.tc.ok b/test/run/ok/redundant-instantiations.tc.ok index 9212efe47b0..b7e30c2ca8b 100644 --- a/test/run/ok/redundant-instantiations.tc.ok +++ b/test/run/ok/redundant-instantiations.tc.ok @@ -2,7 +2,7 @@ redundant-instantiations.mo:22.18-22.23: warning [M0223], redundant type instant redundant-instantiations.mo:31.18-31.23: warning [M0223], redundant type instantiation redundant-instantiations.mo:38.18-38.25: warning [M0223], redundant type instantiation redundant-instantiations.mo:45.18-45.24: warning [M0223], redundant type instantiation -redundant-instantiations.mo:52.24-52.30: warning [M0223], redundant type instantiation -redundant-instantiations.mo:54.26-54.32: warning [M0223], redundant type instantiation redundant-instantiations.mo:56.28-56.34: warning [M0223], redundant type instantiation +redundant-instantiations.mo:54.26-54.32: warning [M0223], redundant type instantiation +redundant-instantiations.mo:52.24-52.30: warning [M0223], redundant type instantiation redundant-instantiations.mo:66.35-66.45: warning [M0223], redundant type instantiation From 878cb79811e7924ff1638f003ad54aec432c2e0b Mon Sep 17 00:00:00 2001 From: Kamil Listopad Date: Tue, 28 Oct 2025 15:38:00 +0100 Subject: [PATCH 17/19] refactor --- src/mo_frontend/typing.ml | 23 ++++++++++------------- 1 file changed, 10 insertions(+), 13 deletions(-) diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index 6310cb86867..cdec9f18c3a 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -259,6 +259,8 @@ let info env at fmt = let is_warning_enabled env code = not env.errors_only && Flags.is_warning_enabled code +let is_warning_disabled env code = not (is_warning_enabled env code) + let check_deprecation env at desc id depr = match depr with | Some ("M0235" as code) -> @@ -2819,20 +2821,15 @@ and infer_call env exp1 inst (parenthesized, ref_exp2) at t_expect_opt = (* explicit instantiation, check argument against instantiated domain *) let typs = match inst.it with None -> [] | Some (_, typs) -> typs in let ts = check_inst_bounds env sort tbs typs t_ret at in - let t_arg' = T.open_ ts t_arg in - let t_ret' = T.open_ ts t_ret in - - let try_redundant = - (* TODO: refactor all this into try_redundant_instantiation *) - if not env.pre && typs <> [] && is_warning_enabled env "M0223" then try_redundant_instantiation ts env (fun env' -> - infer_call_instantiation env' t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt extra_subtype_problems) - else None - in - (match try_redundant with + (match try_redundant_instantiation typs ts env (fun env' -> + infer_call_instantiation env' t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt extra_subtype_problems) + with | Some result -> warn env inst.at "M0223" "redundant type instantiation"; result - | None -> + | None -> + let t_arg' = T.open_ ts t_arg in + let t_ret' = T.open_ ts t_ret in if not env.pre then check_exp_strong { env with redo = true } t_arg' exp2; ts, t_arg', t_ret') @@ -3079,8 +3076,8 @@ and infer_call_instantiation env t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt | Some t -> Format.asprintf "\nto produce result of expected type%a" display_typ t) -and try_redundant_instantiation ts env infer_instantiation : (T.typ list * T.typ * T.typ) option = - assert (not env.pre); +and try_redundant_instantiation typs ts env infer_instantiation : (T.typ list * T.typ * T.typ) option = + if env.pre || typs = [] || is_warning_disabled env "M0223" then None else let reverts = ref [] in let env = { env with reverts = Some reverts } in let save = Diag.save_store env.msgs in From 1961201b68bfc3e0027abcc2506045da77d4fd57 Mon Sep 17 00:00:00 2001 From: Kamil Listopad Date: Tue, 28 Oct 2025 16:53:19 +0100 Subject: [PATCH 18/19] just use reverts --- src/mo_frontend/typing.ml | 58 +++++++++++++++++++-------------------- 1 file changed, 29 insertions(+), 29 deletions(-) diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index cdec9f18c3a..f69c28df1af 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -58,9 +58,8 @@ type env = context : exp' list; (* [pre] phase skips thorough checks and avoids recording note types (and other internal state modifications) *) pre : bool; + (* [reverts] is used to revert the environment state after an extra analysis *) reverts : reverts ref option; - (* [redo] ignores and recalculates the state of the expressions *) - redo : bool; weak : bool; msgs : Diag.msg_store; scopes : Source.region T.ConEnv.t; @@ -88,7 +87,6 @@ let env_of_scope ?(viper_mode=false) msgs scope = context = []; pre = false; reverts = None; - redo = false; weak = false; msgs; scopes = T.ConEnv.empty; @@ -113,9 +111,11 @@ let commit env ref v = l := (fun () -> ref := old_v) :: !l); ref := v -let set_note env ap n = - (* if not env.skip_note_typ then *) - ap.note <- n +let commit_note env ap n = + env.reverts |> Option.iter (fun l -> + let old_v = ap.note in + l := (fun () -> ap.note <- old_v) :: !l); + ap.note <- n let get_identifiers identifiers = T.Env.fold (fun id _ set -> S.add id set) identifiers S.empty @@ -512,7 +512,7 @@ let check_import env at f ri = let rec check_obj_path env path : T.obj_sort * (T.field list) = match T.promote (check_obj_path' env path) with | T.Obj (s, fs) as t -> - path.note <- t; + commit_note env path t; (s, fs) | t -> error env path.at "M0023" @@ -552,7 +552,7 @@ and check_obj_path' env path : T.typ = let rec check_typ_path env path : T.con = let c = check_typ_path' env path in - path.note <- T.Typ c; + commit_note env path (T.Typ c); c and check_typ_path' env path : T.con = @@ -753,7 +753,7 @@ let infer_class_cap env obj_sort (tbs : T.bind list) cs = let rec check_typ env (typ : typ) : T.typ = let t = check_typ' env typ in - typ.note <- t; + commit_note env typ t; t and check_typ_item env typ_item = @@ -955,7 +955,7 @@ and check_typ_binds env typ_binds : T.con list * T.bind list * Scope.typ_env * S ) cs ks; let env' = add_typs env xs cs in let _ = List.map (fun typ_bind -> check_typ env' typ_bind.it.bound) typ_binds in - List.iter2 (fun typ_bind c -> typ_bind.note <- Some c) typ_binds cs; + List.iter2 (fun typ_bind c -> commit_note env typ_bind (Some c)) typ_binds cs; cs, tbs, te, T.ConSet.of_list cs and check_typ_bind env typ_bind : T.con * T.bind * Scope.typ_env * Scope.con_env = @@ -1675,15 +1675,15 @@ and infer_exp_and_promote env exp : T.typ * T.typ = and infer_exp_wrapper inf f env exp : T.typ = - assert (env.redo || exp.note.note_typ = T.Pre); + assert (exp.note.note_typ = T.Pre); let t = inf env exp in assert (t <> T.Pre); let t' = f t in if not env.pre then begin let t'' = T.normalize t' in - assert (env.redo || t'' <> T.Pre); + assert (t'' <> T.Pre); let note_eff = A.infer_effect_exp exp in - exp.note <- {note_typ = if env.viper_mode then t' else t''; note_eff} + commit_note env exp {note_typ = if env.viper_mode then t' else t''; note_eff} end; t' @@ -1708,7 +1708,7 @@ and infer_exp'' env exp : T.typ = if !Flags.compiled then error env id.at "M0056" "variable %s is in scope but not available in compiled code" id.it else t - | Some (t, _, _, Available) -> id.note <- (if T.is_mut t then Var else Const); t + | Some (t, _, _, Available) -> commit_note env id (if T.is_mut t then Var else Const); t | None -> error env id.at "M0057" "unbound variable %s%a%s" id.it display_vals env.vals @@ -1723,7 +1723,7 @@ and infer_exp'' env exp : T.typ = let t1 = infer_exp_promote env exp1 in let t = Operator.type_unop op t1 in if not env.pre then begin - assert (env.redo || !ot = T.Pre); + assert (!ot = T.Pre); if not (Operator.has_unop op t) then error env exp.at "M0059" "operator is not defined for operand type%a" display_typ_expand t; @@ -1734,7 +1734,7 @@ and infer_exp'' env exp : T.typ = let t1, t2 = infer_bin_exp env exp1 exp2 in let t = Operator.type_binop op (T.lub ~src_fields:env.srcs (T.promote t1) (T.promote t2)) in if not env.pre then begin - assert (env.redo || !ot = T.Pre); + assert (!ot = T.Pre); if not (Operator.has_binop op t) then error_bin_op env exp.at t1 t2 else if op = Operator.SubOp && eq env exp.at t T.nat then @@ -1745,7 +1745,7 @@ and infer_exp'' env exp : T.typ = t | RelE (ot, exp1, op, exp2) -> if not env.pre then begin - assert (env.redo || !ot = T.Pre); + assert (!ot = T.Pre); let t1, t2 = infer_bin_exp env exp1 exp2 in let t = Operator.type_relop op (T.lub ~src_fields:env.srcs (T.promote t1) (T.promote t2)) in if not (Operator.has_relop op t) then @@ -1925,7 +1925,7 @@ and infer_exp'' env exp : T.typ = let t1, ve1 = infer_pat_exhaustive (if T.is_shared_sort sort then local_error else warn) env' pat in let ve2 = T.Env.adjoin ve ve1 in let ts2 = List.map (check_typ_item env') ts2 in - set_note env typ (T.seq ts2); (* HACK *) + commit_note env typ (T.seq ts2); (* HACK *) let codom = T.codom c (fun () -> T.Con(List.hd cs,[])) ts2 in if not env.pre then begin let env'' = @@ -2339,11 +2339,11 @@ and check_exp_weak env t exp = and check_exp env t exp = assert (not env.pre); - assert (env.redo || exp.note.note_typ = T.Pre); + assert (exp.note.note_typ = T.Pre); assert (t <> T.Pre); let t' = check_exp' env (T.normalize t) exp in let e = A.infer_effect_exp exp in - exp.note <- {exp.note with note_typ = t'; note_eff = e} + commit_note env exp {exp.note with note_typ = t'; note_eff = e} and check_exp' env0 t exp : T.typ = let env = {env0 with in_prog = false; in_actor = false; context = exp.it :: env0.context } in @@ -2831,12 +2831,12 @@ and infer_call env exp1 inst (parenthesized, ref_exp2) at t_expect_opt = let t_arg' = T.open_ ts t_arg in let t_ret' = T.open_ ts t_ret in if not env.pre then - check_exp_strong { env with redo = true } t_arg' exp2; + check_exp_strong env t_arg' exp2; ts, t_arg', t_ret') | _::_, None -> (* implicit, infer *) infer_call_instantiation env t1 ctx_dot tbs t_arg t_ret exp2 at t_expect_opt extra_subtype_problems in - set_note env inst ts; + commit_note env inst ts; if not env.pre then begin if Type.is_shared_sort sort then begin if not (T.concrete t_arg') then @@ -3145,9 +3145,9 @@ and infer_pat_exhaustive warnOrError env pat : T.typ * Scope.val_env = t, ve and infer_pat name_types env pat : T.typ * Scope.val_env = - assert (env.redo || pat.note = T.Pre); + assert (pat.note = T.Pre); let t, ve = infer_pat' name_types env pat in - if not env.pre then set_note env pat (T.normalize t); + if not env.pre then commit_note env pat (T.normalize t); t, ve and infer_pat' name_types env pat : T.typ * Scope.val_env = @@ -3258,11 +3258,11 @@ and check_pat env t pat : Scope.val_env = check_pat_aux env t pat Scope.Declaration and check_pat_aux env t pat val_kind : Scope.val_env = - assert (env.redo || pat.note = T.Pre); + assert (pat.note = T.Pre); if t = T.Pre then snd (infer_pat false env pat) else let t' = T.normalize t in let ve = check_pat_aux' env t' pat val_kind in - if not env.pre then set_note env pat t'; + if not env.pre then commit_note env pat t'; ve and check_pat_aux' env t pat val_kind : Scope.val_env = @@ -3501,7 +3501,7 @@ and check_pat_fields_typ_dec env t tfs pfs te at : Scope.typ_env = match tfs, pf | _ -> match tf, pf with | T.{lab; typ = Typ t'; _}, { it = TypPF(id); _ } -> - id.note <- Some t'; + commit_note env id (Some t'); let te' = T.Env.add id.it t' te in begin match pfs' with | {it = TypPF(id'); at = at';_}::_ when id'.it = lab -> @@ -4133,7 +4133,7 @@ and infer_dec env dec : T.typ = T.unit in let eff = A.infer_effect_dec dec in - dec.note <- {empty_typ_note with note_typ = t; note_eff = eff}; + commit_note env dec {empty_typ_note with note_typ = t; note_eff = eff}; t @@ -4160,7 +4160,7 @@ and check_dec env t dec = match dec.it with | ExpD exp -> check_exp env t exp; - set_note env dec exp.note + commit_note env dec exp.note | _ -> let t' = infer_dec env dec in if not (eq env dec.at t T.unit || sub env dec.at t' t) then From 8778f702b9d71faefccc01dd1c75ca5f33de3be8 Mon Sep 17 00:00:00 2001 From: Kamil Listopad Date: Tue, 28 Oct 2025 17:13:05 +0100 Subject: [PATCH 19/19] clean --- src/mo_frontend/typing.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/mo_frontend/typing.ml b/src/mo_frontend/typing.ml index f69c28df1af..468dffcbac7 100644 --- a/src/mo_frontend/typing.ml +++ b/src/mo_frontend/typing.ml @@ -4255,8 +4255,7 @@ and gather_dec env scope dec : Scope.t = in let pre_k = T.Abs (pre_tbs, T.Pre) in let c = match id.note with - | None -> - let c = Cons.fresh id.it pre_k in id.note <- Some c; c + | None -> let c = Cons.fresh id.it pre_k in id.note <- Some c; c | Some c -> c in let val_env = match dec.it with @@ -4428,8 +4427,7 @@ and infer_dec_typdecs env dec : Scope.t = and infer_id_typdecs env at id c k : Scope.con_env = assert (match k with T.Abs (_, T.Pre) -> false | _ -> true); (match Cons.kind c with - | T.Abs (_, T.Pre) -> - T.set_kind c k; id.note <- Some c + | T.Abs (_, T.Pre) -> T.set_kind c k; id.note <- Some c | k' -> assert (eq_kind env at k' k) (* may diverge on expansive types *) ); T.ConSet.singleton c