From ed7258c80f9e5cf41e06dc735d1b5449f554a894 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Fri, 25 Sep 2026 21:26:56 +0700 Subject: [PATCH] An abandoned check puts back everything it wrote into the environment, an else arm refused on its own terms is not blamed for the then arm's type, and a match's arms meet at the same join as an if's --- TODO.org | 4 +- lib/check.ml | 220 ++++++++++++++++++++----------- spec-syntax.md | 2 +- test/programs/trial-generic.flan | 23 ++++ test/test_acceptance.ml | 6 + test/test_flan.ml | 38 ++++++ 6 files changed, 213 insertions(+), 80 deletions(-) create mode 100644 test/programs/trial-generic.flan diff --git a/TODO.org b/TODO.org index bf8a0edd..648ac94b 100644 --- a/TODO.org +++ b/TODO.org @@ -43,10 +43,10 @@ The body's own type, never a call site's; parameters are never inferred, and a cycle among =_= functions is refused by name unless it gives =()=. Rules out use-directed inference. -** DONE An if's arms meet at one join, whichever is written first +** DONE An if's or match's arms meet at one join, whichever is written first CLOSED: [2026-09-25] Lossless widening, const, and dyn beside anything, the same for =_= exits. -Rules out the then arm deciding the type the else arm is checked at. +Rules out the first arm deciding the type the others are checked at. ** DONE def, defonce and defconst are the three forms CLOSED: [2026-09-20] diff --git a/lib/check.ml b/lib/check.ml index ebc96bc2..4a25a489 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -364,6 +364,64 @@ let new_env () = { guard_next = false; } +(* Everything checking may write into [env], taken so that a check which is + abandoned — a trial, a probe, a return type read and thrown away, a + tolerated body — can be undone as one piece. Partial undo is the bug this + exists for: rewinding [lifted] and not the generic cache left a copy made + during a trial with the lambda it lifted gone, which is a link error. So + the whole record is named, closed with warning 9: a new field stops this + compiling until it is decided here. + + Taken on every trial, so it copies only what a body's check writes: the + struct table and its locations (a generic struct's copy, a closure's + environment), the struct-copy tables, and the generic cache, whose copies' + entries in [fns] are the only ones a body adds. The rest is written by the + declaration passes alone, before any body is checked, and is marked so. *) +let snapshot_env env : unit -> unit = + let[@warning "+9"] { structs; locs; copies; insts; lifted; instances; + tyvars; subst; tvpreds; chain; deferred; lenvars; + len_placeholder; schain; in_field; recovering; + recovered; poison; speculating; guard_next; + fns = _ (* through [insts], below *); + (* Declaration passes only. *) + datas = _; unions = _; cases = _; aliases = _; + consts = _; enums = _; parents = _; externs = _; + extern_locs = _; fparams = _; fn_locs = _; + privates = _; globals = _; global_locs = _; + generics = _; gsigs = _; refused_generics = _; + gstructs = _; broken = _; glens = _; classes = _; + tracks = _; inferred = _; infer_failed = _ } = env in + let keep t = + let c = Hashtbl.copy t in + fun () -> Hashtbl.reset t; Hashtbl.iter (Hashtbl.add t) c + in + let tables = [ keep structs; keep locs; keep copies; keep struct_apps ] in + let cache = Hashtbl.fold (fun g r acc -> (g, r, !r) :: acc) insts [] in + fun () -> + List.iter (fun undo -> undo ()) tables; + (* A copy made since goes from [fns] with its cache entry. *) + Hashtbl.filter_map_inplace + (fun g r -> + match List.find_opt (fun (h, _, _) -> String.equal g h) cache with + | None -> + List.iter (fun (_, _, sym) -> Hashtbl.remove env.fns sym) !r; + None + | Some (_, _, before) -> + List.iter + (fun ((_, _, sym) as e) -> + if not (List.memq e before) then Hashtbl.remove env.fns sym) + !r; + r := before; + Some r) + insts; + env.lifted <- lifted; env.instances <- instances; env.tyvars <- tyvars; + env.subst <- subst; env.tvpreds <- tvpreds; env.chain <- chain; + env.deferred <- deferred; env.lenvars <- lenvars; + env.len_placeholder <- len_placeholder; env.schain <- schain; + env.in_field <- in_field; env.recovering <- recovering; + env.recovered <- recovered; env.poison <- poison; + env.speculating <- speculating; env.guard_next <- guard_next + (* A refusal [collect] can go on past: kept while a whole-file check is collecting, in the order found, and raised otherwise. *) let defer_or_raise env (d : Loc.diag) = @@ -7042,18 +7100,38 @@ and check_if_once ctx ~tail ?want loc c t e = || t.Tast.ty = Types.Bool || and_sentinel e || lone_literal e then None else - (* A trial not kept leaves nothing: [trial] puts the context back - when it raises, and what it lifted goes here. *) - let lifted = ctx.env.lifted in + (* A trial not kept leaves nothing: [trial] puts the context and + the environment back when it raises. *) + let not_kept = "check/arm-not-kept" in + let alone () = branch ctx (fun () -> in_tail (fun () -> check ctx e)) in match trial ctx (fun () -> - let v = branch ctx (fun () -> in_tail (fun () -> check ctx e)) in + let v = alone () in match arm_join t.Tast.ty v.Tast.ty with | Some j when Types.equal v.Tast.ty j -> v - | _ -> raise (Loc.Error (Loc.diag v.Tast.loc "not kept"))) + | _ -> raise (Loc.Error (Loc.diag ~kind:not_kept v.Tast.loc ""))) with | Ok v -> Some (v.Tast.ty, v) - | Error _ -> ctx.env.lifted <- lifted; None + | Error d when String.equal d.Loc.kind not_kept -> None + | Error _ -> + (* Refused on its own terms. If the then arm's type is what it + needed — [nil], a bare struct — the arm is checked at it below; + if it is refused there too, its own error is the real one, so it + is checked for real on its own terms and nothing is invented + about a type it was never going to have. *) + (match + trial ctx (fun () -> + branch ctx (fun () -> + in_tail (fun () -> check ctx ~want:t.Tast.ty e))) + with + | Ok _ -> None + | Error _ -> + let v = alone () in + (match arm_join t.Tast.ty v.Tast.ty with + | Some j -> Some (j, expect ctx v.Tast.loc ~want:(Some j) v) + | None -> + fail loc "the branches of this if have different types: %s and %s" + (Types.to_string t.Tast.ty) (Types.to_string v.Tast.ty))) in match joined with | Some (j, v) -> @@ -8469,6 +8547,13 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms = | Some t when not (Types.equal t (Types.Int Types.I32)) -> want := Some t | _ -> ()) | [] -> ()); + (* With nothing expected, the arms meet at [arm_join], as an [if]'s do, in + whatever order they are written: each typed arm is checked on its own + terms, the join so far grows with it, and every arm is brought to the + final join at the end. An arm that needs an expectation — [nil], a bare + struct — is checked at the join so far, as it was at the first arm's + type before. *) + let free = !want = None in let order = let idx = List.mapi (fun i r -> (i, r)) resolved in if !want <> None then idx @@ -8511,12 +8596,43 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms = (* Every arm is the tail, exactly as an [if]'s two arms are. Restored here because checking the scrutinee withdrew it. *) ctx.tail <- tail; - let body = block ctx ?want:!want a.Ast.aloc a.Ast.body in - if !want = None && body.Tast.ty <> Types.Never then - want := Some body.Tast.ty; + let arm = (a, ctor, binds) in + let body = + if free && !want <> None && not (literal_arm arm) then + let at w () = block ctx ?want:w a.Ast.aloc a.Ast.body in + match trial ctx (at None) with + | Ok b -> b + | Error _ -> + (* Refused on its own terms: the join is what it needed, + or, refused there too, its own error is the real one. *) + (match trial ctx (at !want) with + | Ok _ -> at !want () + | Error _ -> at None ()) + else block ctx ?want:!want a.Ast.aloc a.Ast.body + in + (if body.Tast.ty <> Types.Never then + match !want with + | None -> want := Some body.Tast.ty + | Some w when free -> + (match arm_join w body.Tast.ty with + | Some j -> want := Some j + | None -> ()) + | Some _ -> ()); { Tast.acase = ctor; binds; abody = [ body ] })) order in + let checked = + match free, !want with + | true, Some j -> + List.map + (fun (i, (arm : Tast.arm)) -> + match arm.Tast.abody with + | [ b ] when not (Types.equal b.Tast.ty j || b.Tast.ty = Types.Never) -> + (i, { arm with Tast.abody = [ expect ctx b.Tast.loc ~want:(Some j) b ] }) + | _ -> (i, arm)) + checked + | _ -> checked + in let arms = List.map snd (List.sort (fun (i, _) (j, _) -> compare i j) checked) in @@ -13178,24 +13294,10 @@ and trial ctx f = it, so a new field on [ctx] stops this function compiling until somebody decides about it, rather than joining the list of things nobody noticed. - What is *not* restored, once, deliberately: [env.lifted] keeps whatever - function an abandoned trial lifted out of an [fn] literal. It is dead — - the names are [fn//N] handed out by count, so the live pass gets - fresh ones and nothing refers to the orphan — and it rides along into the - module as a function nobody calls. Left alone because [env] is the - program's table and not this form's, and rewinding it would mean deciding - what else on [env] a trial may have touched. - - The generic instantiation cache is the other table a trial reaches, and - it does not rewind either. [instantiate] rewinds a copy whose *body* - refused, which is a different event from a copy the caller abandoned — - and the abandoned one does not need rewinding. A generic call's - instantiation is read off its arguments and never off the ambient want: - an unbound variable is checked with no expectation at all, and a bound - one does not widen. So the trial and the live pass ask [instantiate] for - the same types, the second ask is a cache hit on the first, and exactly - one copy exists either way. Pinned in test_flan, "a generic inside an - abandoned trial". + [env] is put back the same way, whole, by [snapshot_env]: a function + lifted, a generic copy made and cached, a struct registered — all of it + goes together, since keeping one of a pair without the other is how a + copy ends up calling a lambda that was never emitted. Only [Loc.Error] is caught. A timeout or a stack overflow is not a refusal to reconsider, and silently continuing past one would turn a @@ -13205,9 +13307,11 @@ and trial ctx f = outer_what; caught; place_ok; envslot; parent = _; in_frames; loops; tail; in_defer; owner = _ } = ctx in + let undo = snapshot_env ctx.env in match speculate ctx.env f with | r -> Ok r | exception Loc.Error d -> + undo (); ctx.slots <- slots; ctx.slot_tys <- slot_tys; ctx.slot_names <- slot_names; ctx.scope <- scope; ctx.defers <- defers; ctx.defer_slot <- defer_slot; @@ -14798,39 +14902,18 @@ and check_generic env (fn : Ast.fn) = arms is refused between exits, in the same words. None gives (); no value beside a value is refused, since () does not take a value's place. *) and read_return env (fn : Ast.fn) params = - (* One check of the body against [ret], thrown away: what it lifted goes, - and so do the copies it asked for if it failed, as [tolerant] does. *) + (* One check of the body against [ret], thrown away with everything it + wrote into [env] ([snapshot_env]); pass two checks it again for real. *) let attempt ret = - let lifted = env.lifted and instances = env.instances in - let insts = Hashtbl.fold (fun g r acc -> (g, r, !r) :: acc) env.insts [] in + let undo = snapshot_env env in let seen = !infer_seen in infer_seen := []; - let restore ~copies = - env.lifted <- lifted; - infer_seen := seen; - if copies then begin - Hashtbl.filter_map_inplace - (fun g r -> - match List.find_opt (fun (h, _, _) -> String.equal g h) insts with - | None -> - List.iter (fun (_, _, sym) -> Hashtbl.remove env.fns sym) !r; - None - | Some (_, _, before) -> - List.iter - (fun ((_, _, sym) as e) -> - if not (List.memq e before) then Hashtbl.remove env.fns sym) - !r; - r := before; - Some r) - env.insts; - env.instances <- instances - end - in + let restore () = undo (); infer_seen := seen in match speculate env (fun () -> check_fn ~sign:(params, ret) env fn) with - | exception e -> restore ~copies:true; raise e + | exception e -> restore (); raise e | tf -> let returns = List.rev !infer_seen in - restore ~copies:false; + restore (); (tf, returns) in let tf, returns = attempt infer_ret in @@ -16170,33 +16253,16 @@ let build_program ~keep_going ?tolerate ?previous (decls : Ast.decl list) : match tolerate with | None -> f () | Some ok -> - let lifted = env.lifted and instances = env.instances in - (* The generic-copy cache as well as the copies. A copy the failed body - asked for would otherwise stay cached, and the next body asking for - it would be handed the name of a copy the program does not have. *) - let insts = - Hashtbl.fold (fun g r acc -> (g, r, !r) :: acc) env.insts [] - in + (* Everything the failed body wrote into [env] goes with it + ([snapshot_env]): a copy it asked for would otherwise stay cached, + and the next body asking for it would be handed the name of a copy + the program does not have. *) + let undo = snapshot_env env in (match f () with | x -> x | exception ((Loc.Error d | Loc.Errors (d :: _)) as e) -> if ok env name d then begin - Hashtbl.filter_map_inplace - (fun g r -> - match List.find_opt (fun (h, _, _) -> String.equal g h) insts with - | None -> - List.iter (fun (_, _, sym) -> Hashtbl.remove env.fns sym) !r; - None - | Some (_, _, before) -> - List.iter - (fun ((_, _, sym) as e) -> - if not (List.memq e before) then Hashtbl.remove env.fns sym) - !r; - r := before; - Some r) - env.insts; - env.lifted <- lifted; - env.instances <- instances; + undo (); tolerated := name :: !tolerated; None end diff --git a/spec-syntax.md b/spec-syntax.md index d22fce65..5494a565 100644 --- a/spec-syntax.md +++ b/spec-syntax.md @@ -55,7 +55,7 @@ warns about; the new syntax must not inherit it. **The return type is inferred when omitted.** Body-local only, as `docs/SPIKE-INFERENCE.md` ("The cheap first step" and "Verdict") scopes it: - the return type is the body's type; a `dyn` body gives `dyn`; the exits (the - last form and each `return`) meet exactly as an `if`'s arms do, through one + last form and each `return`) meet exactly as an `if`'s or `match`'s arms do, through one join and in any order: lossless widening, the read-only side of a const difference, `dyn` beside anything; a literal takes the other exits' type and what `if` refuses is refused; no value gives `()`. diff --git a/test/programs/trial-generic.flan b/test/programs/trial-generic.flan new file mode 100644 index 00000000..9ae05f20 --- /dev/null +++ b/test/programs/trial-generic.flan @@ -0,0 +1,23 @@ +;;;; A generic copy first made while an if's else arm is tried on its own, +;;;; then kept when the arm is checked again: whatever the copy lifted — a +;;;; lambda, a condition's message printer — has to be kept with it, or the +;;;; program links against a function nobody emitted. + +(defstruct MyErr :parent Error [code i32 why string]) + +(defn ap [x i32 f (Fn [i32] i32)] i32 (f x)) + +(defn g [x $t] i32 (ap 21 (fn [y] (+ y y)))) + +(defn h [x $t] i32 + (when (< 21 0) (error (MyErr {.code 3 .why "negative"}))) + 21) + +(defn pick [c bool a i64 b i32] i64 (let [v (if c a (g b))] v)) + +(defn pick2 [c bool a i64 b i32] i64 (let [v (if c a (h b))] v)) + +(defn main [] i32 + (println (pick false 1 21)) + (println (pick2 false 1 21)) + 0) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index 1c703e47..427c33f5 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -570,6 +570,12 @@ let () = "programs/return-defer.flan" rd_out; outputs ~x86:true "a return computes its value before its defers, x86" "programs/return-defer.flan" rd_out; + (* A generic copy made during an abandoned trial keeps what it lifted. *) + outputs "a trial's generic copy keeps its lambda and its message printer" + "programs/trial-generic.flan" "42\n21\n"; + outputs ~x86:true + "a trial's generic copy keeps its lambda and its message printer, x86" + "programs/trial-generic.flan" "42\n21\n"; (* Constant arithmetic folds before a bounded variable checks it. *) let fold_out = "10\n0\n7.5\n7\n" in outputs "constant arithmetic at a bounded variable" diff --git a/test/test_flan.ml b/test/test_flan.ml index 611e35c6..0a011ceb 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -7632,6 +7632,24 @@ let () = "(when c (return a)) b", "f [bool (Ptr i32) (Ptr const i32)] (Ptr const i32)"); ("exits dyn then a literal", "[c bool d dyn]", "(when c (return d)) 1", "f [bool dyn] dyn"); ("exits nil then a literal", "[c bool]", "(when c (return nil)) 1", "f [bool] dyn") ]; + (* A match's arms meet at the same join, in either order. *) + List.iter + (fun (what, sg, body, want) -> + reads_as what ("(defn f " ^ sg ^ " _ " ^ body ^ ")" ^ main) "f" want) + [ ("match i32 then i64", "[o (Option i32) x i32 y i64]", + "(match o (Some q) x None y)", "f [(Option i32) i32 i64] i64"); + ("match i64 then i32", "[o (Option i32) x i32 y i64]", + "(match o (Some q) y None x)", "f [(Option i32) i32 i64] i64"); + ("match i8 then dyn", "[o (Option i32) x i8 y dyn]", + "(match o (Some q) x None y)", "f [(Option i32) i8 dyn] dyn"); + ("match writable then read-only", "[o (Option i32) x [u8] y [const u8]]", + "(match o (Some q) x None y)", "f [(Option i32) [u8] [const u8]] [const u8]"); + ("match literal arms, i32 then i64", "[n i32 x i32 y i64]", + "(match n 1 x _ y)", "f [i32 i32 i64] i64"); + ("match a typed arm and a literal arm", "[o (Option i32) x i8]", + "(match o (Some q) x None 1)", "f [(Option i32) i8] i8"); + ("match an arm that needs the join", "[o (Option i32) d dyn]", + "(match o (Some q) d None nil)", "f [(Option i32) dyn] dyn") ]; reads_as "an f32 exit and a float literal" ("(defn f [x f32] _ (when (< x 0.0) (return x)) 0.0)" ^ main) "f" "f [f32] f32"; reads_as "a function that calls itself and gives nothing is ()" @@ -7727,6 +7745,26 @@ let () = rejects_check "a constant computed by a _ function, as by a written one" ~needle:"a constant's value must be a compile-time constant — the constant K is computed" "(defn five [] _ 5)\n(defconst K (five))\n(defn main [] i32 0)"; + (* An else arm refused on its own terms is not also blamed for a type it + was never going to have. *) + (let n = + match + program "(defn g [c bool a i32 b i64] i64 (let [v (if c a (+ b (nope2 1)))] v))\n\ + (defn main [] i32 0)" + |> Check.program_all + with + | _ -> 0 + | exception Loc.Error _ -> 1 + | exception Loc.Errors ds -> List.length ds + in + if n <> 1 then begin + incr failures; + Printf.printf "FAIL an else arm's own error alone: %d errors\n" n + end); + rejects_check "an else arm's own error is the one reported" + ~needle:"unknown function nope2" + "(defn g [c bool a i32 b i64] i64 (let [v (if c a (+ b (nope2 1)))] v))\n\ + (defn main [] i32 0)"; rejects_check "some under an inferred return" ~needle:"Write the return type: (Option T)" "(defn f [o (Option i32)] _ (+ 1 (some o)))\n(defn main [] ())";