From ff88b9dad6075774b9f68f5baf2ab4380ef2d154 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Fri, 25 Sep 2026 17:09:13 +0700 Subject: [PATCH 1/9] A defn whose return slot is _ (or a .fln fn with no arrow) takes its return type from its own body, recursion through such functions is refused by name, and a stale caller of one is told which line changed its type --- TODO.org | 5 + emacs/flan.el | 4 + lib/ast.ml | 5 + lib/check.ml | 316 +++++++++++++++++++++++++++++++++-- lib/cimport.ml | 1 + lib/dev.ml | 7 +- lib/indent_printer.ml | 6 +- lib/indent_reader.ml | 16 +- lib/load.ml | 2 + lib/parse.ml | 18 +- lib/session.ml | 50 ++++-- lib/shim.ml | 2 + spec-syntax.md | 13 +- test/programs/dev-infer.flan | 20 +++ test/syntax/infer/main.flan | 27 +++ test/syntax/infer/main.fln | 28 ++++ test/test_flan.ml | 74 ++++++++ test/test_session.ml | 56 +++++++ test/test_syntax.ml | 12 +- 19 files changed, 619 insertions(+), 43 deletions(-) create mode 100644 test/programs/dev-infer.flan create mode 100644 test/syntax/infer/main.flan create mode 100644 test/syntax/infer/main.fln diff --git a/TODO.org b/TODO.org index d2c3d726..728dd885 100644 --- a/TODO.org +++ b/TODO.org @@ -37,6 +37,11 @@ A =defn= writes its return type, and unit is =()=. The parse ambiguity a missing slot would open is real, and =()= does not collapse into =dyn=. Rules out the optional return slot. +** DONE A return type is read off the body only when the slot says =_= +CLOSED: [2026-09-25] +The body's own type, never a call site's; parameters are never inferred, and a +cycle among =_= functions is refused by name. Rules out use-directed inference. + ** DONE def, defonce and defconst are the three forms CLOSED: [2026-09-20] =def= is Common Lisp's =defparameter= and re-initialises on every run; =defonce= diff --git a/emacs/flan.el b/emacs/flan.el index 614e91b2..ed118760 100644 --- a/emacs/flan.el +++ b/emacs/flan.el @@ -2448,6 +2448,10 @@ of the tenth name tells you neither how many there were nor which." (concat (format "this call to %s was compiled for %s, and %s is defined as %s. " callee compiled callee (plist-get site :current)) + ;; Set when CALLEE's return type is read off its body, which nobody + ;; wrote, so the line that changed it is named. + (when-let* ((cause (plist-get site :cause))) + (concat cause ". ")) (if (plist-get site :running) ;; `main' is the one caller no evaluation can reach: the program is ;; inside the body it started with and never calls it again. diff --git a/lib/ast.ml b/lib/ast.ml index bc5f0d67..9ec98ec4 100644 --- a/lib/ast.ml +++ b/lib/ast.ml @@ -24,6 +24,11 @@ and texpr_kind = them identically — the difference is a fact about the value, and it is [Check.resolve] that turns it into one. *) | Tfn of bool * texpr list * texpr + (* [_]: the type is read off the body. Only a [defn]'s return slot has a + body to read it off, and [Check.resolve] refuses it everywhere else. A + constructor rather than [ret = None] because [None] already means () + for [declare] and the shim. *) + | Tinfer (* An array length is an integer or a compile-time constant's name. *) and len = diff --git a/lib/check.ml b/lib/check.ml index 9ca97cf7..0f1e68c4 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -211,6 +211,9 @@ type env = { the declare-c forms before [Shim.expand] rewrites them. Keyed by the Flan name a program calls. *) tracks : (string, Shim.track) Hashtbl.t; + (* Every [defn] whose return type was read off its body ([_]), with the + form that decided it — what a stale-caller warning points at. *) + inferred : (string, Loc.t) Hashtbl.t; } let new_env () = { @@ -243,6 +246,7 @@ let new_env () = { in_field = false; classes = Hashtbl.create 8; tracks = Hashtbl.create 16; + inferred = Hashtbl.create 8; } (* Where a named type was declared, and what it has, as a note. @@ -1217,6 +1221,13 @@ let tyvar_in_scope env n = let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t = let loc = t.Ast.tloc in match t.Ast.t with + (* The one slot that takes [_] never reaches here: [collect] reads it off + the body first. So every [_] that does is in a slot with no body behind + it. *) + | Ast.Tinfer -> + Loc.failk "check/infer-misplaced" loc + "_ here asks for a type to be read off a function body, and only a \ + defn's return slot has a body to read. Write the type out" | Ast.Tname "const" -> fail loc "const is not a type on its own — it marks one that can only be read, \ @@ -1557,7 +1568,7 @@ let missing_return_type env (fn : Ast.fn) = "%s has no return type: (%s ...) stands where the return type goes, \ and %s is not a type. The return type is written between the \ parameter vector and the body, and a function that returns nothing \ - writes () there" + writes () there, or _ to read it off the body" fn.Ast.name head head | _ -> () @@ -1632,6 +1643,13 @@ let pair_params ?(also = fun _ -> false) env (items : Ast.pitem list) Loc.failk "check/parameter-named-type" loc "%s names a type, so it cannot also be this parameter's name. Write \ [name %s], or rename the parameter" n n + (* [_] reads a type off a body, and a parameter has none to read. *) + | Ast.Pname (n, _) :: Ast.Pname ("_", tloc) :: _ -> + Loc.failk "check/infer-misplaced" tloc + "_ here asks for %s's type to be read off a body, and a parameter's \ + type is never read off anything. Write its type, or leave it out \ + and %s is dyn" + n n | Ast.Pname (n, loc) :: Ast.Ptype t :: rest -> { Ast.fname = n; fty = t; floc = loc } :: go rest | Ast.Pname (n, loc) :: Ast.Pname (t, tloc) :: rest when is_type_name env t -> @@ -2023,6 +2041,7 @@ let signature_tyvars (fn : Ast.fn) = not over type constructors. A [$t] inside the arguments is ordinary. *) | Ast.Tapp (_, args) -> List.iter ty args | Ast.Tfn (_, ps, r) -> List.iter ty ps; ty r + | Ast.Tinfer -> () in List.iter (fun (p : Ast.field) -> ty p.Ast.fty) fn.Ast.params; (match fn.Ast.ret with Some r -> ty r | None -> ()); @@ -3527,6 +3546,13 @@ let hash_ty = Types.Int Types.U64 Each caller calls it again rather than sharing one value: [slots] and [slot_tys] are counted up per frame, and two frames that shared a context would share a slot counter. *) +(* The return type a body is checked against while it is being read for + one ([_] in a defn's return slot; see [infer_returns]). Compared by + address, so no type written anywhere is ever mistaken for it. What each + [return] in that body gives is pushed on [infer_seen]. *) +let infer_ret = Types.Named "_" +let infer_seen : (Types.t * Loc.t) list ref = ref [] + let invented_ctx env ret = { env; ret; slots = 0; slot_tys = []; slot_names = []; scope = []; defers = []; defer_slot = None; outer = []; outer_what = None; caught = []; place_ok = false; envslot = None; parent = None; in_frames = None; loops = []; tail = false; @@ -4411,6 +4437,17 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr = "return is not allowed inside %s yet" (match ctx.in_frames with Some n -> n | None -> assert false) + | Ast.Return v when ctx.ret == infer_ret -> + let v = Option.map (check ctx) v in + infer_seen := + (match v with + | Some (x : Tast.expr) -> (x.Tast.ty, loc) + | None -> (Types.Unit, loc)) + :: !infer_seen; + (match ctx.defers, v with + | [], _ -> mk loc Types.Never (Tast.Return v) + (* Thrown away after, so the order the defers run in is not built. *) + | ds, _ -> mk loc Types.Never (Tast.Do (ds @ [ mk loc Types.Never (Tast.Return v) ]))) | Ast.Return v -> let v = match v with @@ -4549,6 +4586,11 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr = (* Unwrap Some, else early-return None from the enclosing function, so the enclosing function must itself return an Option (plan.org). *) (match ctx.ret with + | _ when ctx.ret == infer_ret -> + Loc.failk "check/infer-some" loc + "some returns None from the function when there is nothing, and \ + this function's return type is read off its body, which cannot \ + say what the Option holds. Write the return type: (Option T)" | Types.Option _ -> let v = check ctx v in (match v.Tast.ty with @@ -12596,7 +12638,19 @@ let collect env (decls : Ast.decl list) = List.map (fun (p : Ast.field) -> resolve env p.Ast.fty) fn.Ast.params in let ret = - match fn.Ast.ret with None -> Types.Unit | Some t -> resolve env t + match fn.Ast.ret with + | None -> Some Types.Unit + (* Read off the body by [infer_returns], once every written + signature is in [fns]; until then the name has none. *) + | Some { Ast.t = Ast.Tinfer; tloc } -> + if vars <> [] then + Loc.failk "check/infer-generic" tloc + "%s is generic, and _ asks for its return type to be read \ + off one body — but each call site makes its own copy. \ + Write the return type, in terms of the $ variables" + fn.Ast.name; + None + | Some t -> Some (resolve env t) in env.tyvars <- []; env.tvpreds <- []; @@ -12604,11 +12658,14 @@ let collect env (decls : Ast.decl list) = Hashtbl.replace env.privates fn.Ast.name (fn.Ast.nloc, fn.Ast.fprivate); if vars = [] then begin - Hashtbl.replace env.fns fn.Ast.name (params, ret); + Option.iter + (fun ret -> Hashtbl.replace env.fns fn.Ast.name (params, ret)) + ret; Hashtbl.replace env.fparams fn.Ast.name fn.Ast.params; Hashtbl.replace env.fn_locs fn.Ast.name fn.Ast.nloc end else begin + let ret = Option.get ret in Hashtbl.replace env.generics fn.Ast.name fn; Hashtbl.replace env.gsigs fn.Ast.name (vars, params, ret) end @@ -12770,8 +12827,10 @@ let check_union_members env = (* ── Declarations: pass 2, check bodies ────────────────────────────── *) -let rec check_fn env (fn : Ast.fn) : Tast.fn = - let params, ret = Hashtbl.find env.fns fn.Ast.name in +let rec check_fn ?sign env (fn : Ast.fn) : Tast.fn = + let params, ret = + match sign with Some s -> s | None -> Hashtbl.find env.fns fn.Ast.name + in let ctx = { (invented_ctx env ret) with owner = fn.Ast.name } in List.iter2 (fun (p : Ast.field) ty -> @@ -12795,13 +12854,16 @@ let rec check_fn env (fn : Ast.fn) : Tast.fn = let body = match fn.Ast.fbody with | [] -> - if Types.equal ret Types.Unit then [] + if Types.equal ret Types.Unit || ret == infer_ret then [] else fail fn.Ast.nloc "%s returns %s but has no body" fn.Ast.name (Types.to_string ret) | body -> (* The last form is the return value, unless the function returns Unit, in which case whatever it evaluates to is discarded. *) - let want = if Types.equal ret Types.Unit then None else Some ret in + let want = + if Types.equal ret Types.Unit || ret == infer_ret then None + else Some ret + in (* Every form here is at the top level of the function body, so every one of them may carry a [defer] — and so may a form inside a [let] written here, which is what [ctx.defer_ok] carries down. [check] registers it @@ -12838,6 +12900,8 @@ let rec check_fn env (fn : Ast.fn) : Tast.fn = in match ctx.defers with | [] -> body + (* A body read only for its type is thrown away after. *) + | _ when ret == infer_ret -> body (* A body that never falls off the end — its last form a [return], say — has no fall-off path to put the defers on, and a copy of them there is code after a terminator. *) @@ -12908,6 +12972,233 @@ and check_generic env (fn : Ast.fn) = | _ -> finish () | exception e -> finish (); raise e) +(* ── Return types read off the body ([_]) ──────────────────────────── + Between the two passes: every written signature is in [fns], and a [defn] + whose return slot is [_] gets its entry here, from its own body and + nothing else — never a call site (docs/SPIKE-INFERENCE.md, "The cheap + first step"). Its parameters are written, so the body checks exactly as it + would with the type written, and the Tast is thrown away: pass two checks + the body again against the type found, which is what keeps literals and + [return]s coerced the way a written signature would coerce them. + + One such body may call another, so the bodies are read callees first and + then to a fixpoint, the untyped-[defconst] loop's shape. A cycle among + them never settles and is refused by name; a body that calls its own name + is the cycle of one. *) + +(* The type one body gives, and the form that decided it: the last form and + every [return], ignoring what never arrives. All alike give that type; + none gives (); any two that differ give dyn, decided by the first one to + differ. *) +and read_return env (fn : Ast.fn) params = + 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 seen = !infer_seen in + infer_seen := []; + let restore ~copies = + env.lifted <- lifted; + infer_seen := seen; + if copies then begin + (* A copy a failed read asked for goes with it, as [tolerant] does. *) + 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 + match check_fn ~sign:(params, infer_ret) env fn with + | exception e -> restore ~copies:true; raise e + | tf -> + let returns = List.rev !infer_seen in + restore ~copies:false; + let last = + match List.rev tf.Tast.body with + | (x : Tast.expr) :: _ -> [ (x.Tast.ty, x.Tast.loc) ] + | [] -> [] + in + let arrive = + List.filter + (fun (t, _) -> not (Types.equal t Types.Never)) + (returns @ last) + in + (* Nothing boxes (), so a way out with no value beside one with a value + has no type to share — dyn included. *) + let unit (t, _) = Types.equal t Types.Unit in + (match List.find_opt unit arrive, List.find_opt (fun x -> not (unit x)) arrive with + | Some (_, bare), Some (t, valued) -> + Loc.failk "check/infer-mixed" bare + ~notes:[ Loc.note valued ("this gives " ^ Types.to_string t) ] + "%s gives no value here and %s on another path, and its return \ + type is read off its body. Give this path a value too, or write \ + the return type" + fn.Ast.name (Types.to_string t) + | _ -> ()); + (match arrive with + | [] -> (Types.Unit, fn.Ast.nloc) + | (t, l) :: rest -> + (match List.find_opt (fun (u, _) -> not (Types.equal t u)) rest with + | None -> (t, l) + | Some (_, l') -> (Types.Dyn, l'))) + +and infer_returns ?tolerate ?(previous = fun _ -> None) env + (decls : Ast.decl list) = + let pending = + List.filter_map + (fun (d : Ast.decl) -> + match d.Ast.d with + | Ast.Defn ({ Ast.ret = Some { Ast.t = Ast.Tinfer; _ }; _ } as fn) + when not (Hashtbl.mem env.gsigs fn.Ast.name) -> + Some fn + | _ -> None) + decls + in + if pending <> [] then begin + let names = List.map (fun (fn : Ast.fn) -> fn.Ast.name) pending in + (* The other pending names each body mentions, with where. A local of + the same name is counted too, which only matters once the fixpoint + has stalled on a real error, and then only to pick which to show. *) + let calls (fn : Ast.fn) = + let acc = ref [] in + List.iter (Load.expr_uses acc) fn.Ast.fbody; + List.filter (fun (n, _) -> List.mem n names) (List.rev !acc) + in + let deps = List.map (fun (fn : Ast.fn) -> (fn.Ast.name, calls fn)) pending in + let byname = List.map (fun (fn : Ast.fn) -> (fn.Ast.name, fn)) pending in + (* Callees first, so a program with no cycle settles in one round. *) + let order = + let visited = Hashtbl.create 16 and out = ref [] in + let rec visit n = + if not (Hashtbl.mem visited n) then begin + Hashtbl.replace visited n (); + List.iter (fun (m, _) -> visit m) (List.assoc n deps); + out := List.assoc n byname :: !out + end + in + List.iter visit names; + List.rev !out + in + let params_of (fn : Ast.fn) = + List.map (fun (p : Ast.field) -> resolve env p.Ast.fty) fn.Ast.params + in + let settle (fn : Ast.fn) = + let params = params_of fn in + let ret, cause = read_return env fn params in + Hashtbl.replace env.fns fn.Ast.name (params, ret); + Hashtbl.replace env.inferred fn.Ast.name cause + in + let rec rounds left = + let still = + List.filter + (fun fn -> + match settle fn with + | () -> false + | exception Loc.Error _ -> true) + left + in + if still <> [] && List.length still < List.length left then rounds still + else still + in + (* A body [tolerate] excuses keeps the signature it was compiled with, + [previous]'s, the way pass two keeps its compiled body: it is a stale + caller, not a change. *) + let excused (fn : Ast.fn) = + match settle fn with + | () -> () + | exception (Loc.Error d as e) -> + (match tolerate, previous fn.Ast.name with + | Some ok, Some (params, ret) when ok env fn.Ast.name d -> + Hashtbl.replace env.fns fn.Ast.name (params, ret) + | _ -> raise e) + in + let rec stalled left = + let stuck = rounds left in + if stuck <> [] then refuse stuck + and refuse stuck = + let stuck_names = List.map (fun (fn : Ast.fn) -> fn.Ast.name) stuck in + let waits n = + List.filter (fun (m, _) -> List.mem m stuck_names) (List.assoc n deps) + in + (* One that waits on nothing else stuck failed on its own body: check + it again, unswallowed, and its own error is the report. *) + (match List.find_opt (fun n -> waits n = []) stuck_names with + | Some n -> + excused (List.assoc n byname); + stalled (List.filter (fun (fn : Ast.fn) -> fn.Ast.name <> n) stuck) + | None -> + (* Every one waits on another, so following the first wait from + any of them comes back round: that loop is the cycle. *) + let rec walk path n = + if List.mem n path then + let rec from = function + | m :: rest when m = n -> m :: rest + | _ :: rest -> from rest + | [] -> [] + in + from (List.rev path) + else walk (n :: path) (fst (List.hd (waits n))) + in + let cycle = walk [] (List.hd stuck_names) in + (* Told from the one written first, which is where a reader of the + file meets the loop. *) + let cycle = + let index n = + let rec at i = function + | [] -> max_int + | m :: rest -> if m = n then i else at (i + 1) rest + in + at 0 names + in + let start = + List.fold_left (fun a n -> if index n < index a then n else a) + (List.hd cycle) cycle + in + let rec rot = function + | m :: rest when m <> start -> rot (rest @ [ m ]) + | l -> l + in + rot cycle + in + let first = List.hd cycle in + let fn = List.assoc first byname in + let next i = List.nth cycle ((i + 1) mod List.length cycle) in + let notes = + List.mapi + (fun i n -> + let callee = next i in + let at = List.assoc callee (waits n) in + Loc.note at + (if n = callee then n ^ " calls itself here" + else Printf.sprintf "%s calls %s here" n callee)) + cycle + in + (match cycle with + | [ n ] -> + Loc.failk "check/infer-recursive" fn.Ast.nloc ~notes + "%s calls itself, so its return type cannot be read off its \ + body. Write the return type in its signature" n + | _ -> + Loc.failk "check/infer-recursive" fn.Ast.nloc ~notes + "%s call each other (%s), so %s of their return types can \ + be read off their bodies. Write the return type of one of \ + them in its signature" + (String.concat " and " cycle) + (String.concat " → " (cycle @ [ first ])) + (if List.length cycle = 2 then "neither" else "none"))) + in + stalled order + end + (* The knot from [instantiate]: a call site makes a copy, and making one is checking a function. *) let () = check_fn_ref := check_fn @@ -13949,7 +14240,7 @@ let shadow_prelude (prelude : Ast.decl list) (decls : Ast.decl list) = in (prelude @ decls, warnings) -let build_program ~keep_going ?tolerate (decls : Ast.decl list) : +let build_program ~keep_going ?tolerate ?previous (decls : Ast.decl list) : Tast.program * env * string list = let env = new_env () in (* ── A declaration left as it was compiled ─────────────────────────── @@ -14045,6 +14336,7 @@ let build_program ~keep_going ?tolerate (decls : Ast.decl list) : let decls = collect env decls in check_finite env; check_union_members env; + infer_returns ?tolerate ?previous env decls; let s = Loc.sink ~on:keep_going in ignore (Loc.caught s (fun () -> check_main env decls)); (* Every generic body, checked once with its variables left abstract, and @@ -14144,8 +14436,8 @@ let program_with_env (decls : Ast.decl list) : Tast.program * env = (** The same, with [tolerate] deciding which body failures leave a declaration out rather than refuse it — see [build_program]. The names left out come back beside the program; nothing else about it changes. *) -let program_tolerant ~tolerate (decls : Ast.decl list) = - build_program ~keep_going:false ~tolerate decls +let program_tolerant ~tolerate ?previous (decls : Ast.decl list) = + build_program ~keep_going:false ~tolerate ?previous decls let program (decls : Ast.decl list) : Tast.program = let p, _, _ = build_program ~keep_going:false decls in @@ -14537,3 +14829,7 @@ let memory_sites ?file (p : Tast.program) : Loc.diag list = | false, true -> 1 | _ -> Loc.before a.Loc.dloc b.Loc.dloc) (List.rev !found) + +(* The form that decided an inferred return type, for a name whose return + slot was [_]; [None] for one whose type was written. *) +let inferred_cause env name = Hashtbl.find_opt env.inferred name diff --git a/lib/cimport.ml b/lib/cimport.ml index 9fea9ebe..4b47262e 100644 --- a/lib/cimport.ml +++ b/lib/cimport.ml @@ -416,6 +416,7 @@ let rec ty_source (t : Ast.texpr) = | Ast.Tfn (env, ps, r) -> Printf.sprintf "(%s [%s] %s)" (if env then "Fn" else "CFn") (String.concat " " (List.map ty_source ps)) (ty_source r) + | Ast.Tinfer -> "_" let tname n = ty (Ast.Tname n) diff --git a/lib/dev.ml b/lib/dev.ml index 0f4e7e86..00c6700d 100644 --- a/lib/dev.ml +++ b/lib/dev.ml @@ -989,12 +989,15 @@ let stale_field (ss : Session.stale list) = (List.map (fun (x : Session.stale) -> Printf.sprintf - "(:loc %s :caller %s :callee %s :compiled %s :current %s%s)" + "(:loc %s :caller %s :callee %s :compiled %s :current %s%s%s)" (Wire.quote (Loc.to_string x.Session.at)) (Wire.quote x.Session.caller) (Wire.quote x.Session.target) (Wire.quote x.Session.compiled) (Wire.quote x.Session.current) - (if x.Session.running then " :running t" else "")) + (if x.Session.running then " :running t" else "") + (match x.Session.cause with + | Some c -> " :cause " ^ Wire.quote c + | None -> "")) ss) ] let eval ?forms ?base ?(extra = []) t ~code ~origin ~pause = diff --git a/lib/indent_printer.ml b/lib/indent_printer.ml index eb3bfd38..84fbc811 100644 --- a/lib/indent_printer.ml +++ b/lib/indent_printer.ml @@ -577,8 +577,10 @@ and sugar n ~last (f : Form.t) : string list option = | _ -> ("", body) in let head = - i ^ (if d = "defn" then "fn " else "fn- ") ^ name ^ "(" ^ pt ^ ") -> " - ^ ty ret ^ where_ + i ^ (if d = "defn" then "fn " else "fn- ") ^ name ^ "(" ^ pt ^ ")" + (* [_] is what the reader makes of no arrow at all. *) + ^ (match ret.v with Form.Sym "_" -> "" | _ -> " -> " ^ ty ret) + ^ where_ in (match body with | [] -> Some [ head ] diff --git a/lib/indent_reader.ml b/lib/indent_reader.ml index a5ea3a81..af77e655 100644 --- a/lib/indent_reader.ml +++ b/lib/indent_reader.ml @@ -1159,16 +1159,12 @@ and header (s : st) w : Form.t = let lp = glued_lp p ~what:"the parameters, in parentheses glued to the name" in let ps = params p lp in let rp = last p in - let ret = + (* No arrow reads the return type off the body: the paren syntax's [_] + (spec-syntax.md §3.5). *) + let ret, ret_text = match (peek p).tok with - | NAME "->" -> ignore (advance p); ty p - | _ -> - let n = match name.v with Form.Sym n -> n | _ -> "" in - failk "return-type" rp.loc - "fn %s has no return type after its parameters, and a .fln \ - function states one for now. Write it after an arrow: fn %s(...) \ - -> i32, or -> dyn, or -> () when it returns nothing" - n n + | NAME "->" -> ignore (advance p); let r = ty p in (r, text_of r) + | _ -> (sym rp.loc "_", ")") in let where_clause = match (peek p).tok with @@ -1201,7 +1197,7 @@ and header (s : st) w : Form.t = | NEWLINE -> ignore (advance p); if (peek p).tok = INDENT then block s ~after:"fn" else [] - | _ -> stray p ~after:(text_of ret) + | _ -> stray p ~after:ret_text in named (if w = "fn" then "defn" else "defn-") (name :: Form.make (Form.Vec ps) lp.loc :: ret :: (where_clause @ body)) diff --git a/lib/load.ml b/lib/load.ml index 70bb75cb..17c323c2 100644 --- a/lib/load.ml +++ b/lib/load.ml @@ -218,6 +218,7 @@ let rec rename_texpr owned alias (t : Ast.texpr) : Ast.texpr = | Ast.Tfn (env, ps, r) -> Ast.Tfn (env, List.map (rename_texpr owned alias) ps, rename_texpr owned alias r) + | Ast.Tinfer -> Ast.Tinfer in { t with Ast.t = k } @@ -802,6 +803,7 @@ let rec texpr_uses acc (t : Ast.texpr) = | Ast.Tmap (k, v) -> texpr_uses acc k; texpr_uses acc v | Ast.Tapp (_, args) -> List.iter (texpr_uses acc) args | Ast.Tfn (_, ps, r) -> List.iter (texpr_uses acc) ps; texpr_uses acc r + | Ast.Tinfer -> () let rec expr_uses acc (e : Ast.expr) = let go = expr_uses acc in diff --git a/lib/parse.ml b/lib/parse.ml index e5190994..ba533003 100644 --- a/lib/parse.ml +++ b/lib/parse.ml @@ -88,6 +88,7 @@ let rec texpr (f : Form.t) : Ast.texpr = point: it is what [()] parses to, and what the resolver, the shim and the emitter go on speaking. *) | Sym "Unit" -> fail f "unit is written (), not Unit" + | Sym "_" -> mk Ast.Tinfer | Sym s -> mk (Ast.Tname s) (* [const T] is matched before [n T], which it would otherwise be: [const] is a reserved name exactly so that no constant can be called that and @@ -1498,12 +1499,14 @@ let rec decl (f : Form.t) : Ast.decl = leads, and the slot's own clause follows it. *) Loc.failk "parse/return-type-expected" inner "%s — this is the return type, which every defn states, and a \ - function that returns nothing writes ()" msg + function that returns nothing writes (), or _ to read it off \ + the body" msg else Loc.failk "parse/return-type-expected" ret.Form.loc ~notes:[ Loc.note inner msg ] "the return type goes here, and this is %s — every defn states \ - one, and a function that returns nothing writes ()" + one, and a function that returns nothing writes (), or _ to \ + read it off the body" (Form.to_string ret) in let fwhere, body = constraints body in @@ -1513,7 +1516,8 @@ let rec decl (f : Form.t) : Ast.decl = | _ -> fail f "%s is (%s name [param Type ...] ReturnType body ...). The return \ - type is not optional; a function that returns nothing writes ()" + type is not optional; a function that returns nothing writes (), \ + and _ reads it off the body" head head) (* ── The dyn side's classes and generic functions ────────────────── @@ -1556,6 +1560,14 @@ let rec decl (f : Form.t) : Ast.decl = (match args with | n :: { v = Vec ps; _ } :: ret :: body when if generic then body = [] else body <> [] -> + (* Every method answers through this one signature, so no single + body can say what it returns. *) + if ret.v = Sym "_" then + Loc.failk "parse/infer-generic" ret.loc + "_ asks for the return type to be read off a body, and %s's \ + methods each have their own. Write the type every method \ + returns, or dyn" + which; mk ((if generic then (fun fn -> Ast.Defgeneric fn) else fun fn -> Ast.Defmulti fn) { Ast.name = dname n; params = dyn_params which ps; praw = None; diff --git a/lib/session.ml b/lib/session.ml index d79508bc..36642efd 100644 --- a/lib/session.ml +++ b/lib/session.ml @@ -37,7 +37,7 @@ the signature that function had when this body was compiled, and where the call is written. A function value taken by name is a site too — the dev build checks the signature where the address is taken. *) -type site = { callee : string; csig : string; sloc : Loc.t } +type site = { callee : string; csig : string; cret : Types.t; sloc : Loc.t } (* What the session knows about one compiled body: the declaration it belongs to — itself, the function a clause was lifted out of, or the generic a copy @@ -58,6 +58,9 @@ type stale = { again, so compiling [main] again cannot reach it. Changing the callee back or re-running the program does. *) running : bool; + (* When [target]'s return type is read off its body and that is what + changed: which way, and the line that decided it. *) + cause : string option; } type t = { @@ -119,13 +122,15 @@ let sites_of (p : Tast.program) (fn : Tast.fn) = let sigs = Hashtbl.create 64 in List.iter (fun (f : Tast.fn) -> - Hashtbl.replace sigs f.Tast.name (Emit.sig_text f.Tast.params f.Tast.ret)) + Hashtbl.replace sigs f.Tast.name + (Emit.sig_text f.Tast.params f.Tast.ret, f.Tast.ret)) p.Tast.fns; let found = ref [] in let see (e : Tast.expr) = let at m = match Hashtbl.find_opt sigs m with - | Some csig -> found := { callee = m; csig; sloc = e.Tast.loc } :: !found + | Some (csig, cret) -> + found := { callee = m; csig; cret; sloc = e.Tast.loc } :: !found | None -> () in match e.Tast.e with @@ -162,13 +167,26 @@ let record_built env (p : Tast.program) (fns : Tast.fn list) m = it was compiled for, in source order. A callee [p] does not have is skipped rather than reported: nothing could have been installed under it since, so the cell still holds what the site was compiled against. *) -let stale_sites ?(live = SM.empty) ?(running = false) built (p : Tast.program) : - stale list = - let sigs = Hashtbl.create 64 in +let stale_sites ?(live = SM.empty) ?(running = false) + ?(inferred = fun _ -> None) built (p : Tast.program) : stale list = + let sigs = Hashtbl.create 64 and rets = Hashtbl.create 64 in List.iter (fun (f : Tast.fn) -> - Hashtbl.replace sigs f.Tast.name (Emit.sig_text f.Tast.params f.Tast.ret)) + Hashtbl.replace sigs f.Tast.name (Emit.sig_text f.Tast.params f.Tast.ret); + Hashtbl.replace rets f.Tast.name f.Tast.ret) p.Tast.fns; + (* Nobody wrote an inferred return type, so a change to one is said in + terms of the line that made it. *) + let cause (st : site) = + match inferred st.callee, Hashtbl.find_opt rets st.callee with + | Some (l : Loc.t), Some now when not (Types.equal now st.cret) -> + Some + (Printf.sprintf "%s now returns %s, not %s, because of line %d%s" + st.callee (Types.to_string now) (Types.to_string st.cret) l.Loc.line + (if String.equal l.Loc.file st.sloc.Loc.file then "" + else " of " ^ Filename.basename l.Loc.file)) + | _ -> None + in (* Named by the declaration a body belongs to: a clause lifted out of [step] is [step]'s call, and a generic's copy is the generic's. *) let from ~kept m acc = @@ -180,7 +198,8 @@ let stale_sites ?(live = SM.empty) ?(running = false) built (p : Tast.program) : match Hashtbl.find_opt sigs st.callee with | Some now when not (String.equal now st.csig) -> { caller = b.owner; target = st.callee; compiled = st.csig; - current = now; at = st.sloc; running } :: acc + current = now; at = st.sloc; running; cause = cause st } + :: acc | _ -> acc) acc b.sites) m acc @@ -969,7 +988,16 @@ let eval ?(origin = "") ?base ?forms ?pause ?(running = true) t src : chan t.built in let program, env, tolerated = - Check.program_tolerant ~tolerate:stale_owner decls + (* A tolerated body whose return type is read off it keeps the + signature the process has for it. *) + Check.program_tolerant ~tolerate:stale_owner + ~previous:(fun n -> + List.find_map + (fun (f : Tast.fn) -> + if String.equal f.Tast.name n then Some (f.Tast.params, f.Tast.ret) + else None) + t.program.Tast.fns) + decls in let program = if tolerated = [] then program @@ -1296,7 +1324,9 @@ let eval ?(origin = "") ?base ?forms ?pause ?(running = true) t src : chan { ir; x86 = t.x86; names; fns; installs = fns <> [] || allocates || consts <> [] || run_thunk <> None; - stale = stale_sites ~live ~running built program } + stale = + stale_sites ~live ~running ~inferred:(Check.inferred_cause env) built + program } (* ── Evaluating an expression ──────────────────────────────────────── *) diff --git a/lib/shim.ml b/lib/shim.ml index c3070b04..26be806b 100644 --- a/lib/shim.ml +++ b/lib/shim.ml @@ -254,6 +254,8 @@ let rec cty env ~needed ~loc ~what (t : Ast.texpr) : string = what | Ast.Tfn _ -> fail loc "%s is a function type, and a C callback is not implemented" what + | Ast.Tinfer -> + fail loc "%s is _, and a C signature writes every type out" what | Ast.Tapp (n, _) -> fail loc "%s is %s, which is not a type this shim generator knows" what n diff --git a/spec-syntax.md b/spec-syntax.md index c62dcd24..c3838ddf 100644 --- a/spec-syntax.md +++ b/spec-syntax.md @@ -232,8 +232,9 @@ Each item: the proposal, then the reason in one line. - `fn name(a: i32, b) -> R` plus a block; `fn name(a) = expr` for one expression. Reads `(defn name [a i32 b dyn] R …)`. A `{:where …}` constraint - becomes `where ordered?($t)` after the return type. **Built**, with `-> R` - required until step 6; several predicates are `where p, q`. + becomes `where ordered?($t)` after the return type. **Built**; with no + `-> R` the return is `_`, read off the body. Several predicates are + `where p, q`. - `def x = v`, `def x: T = v`, `once x: T`, `once x = v`, `const n = 3`, `def scratch: [4 u8] = uninit`. **Built.** `def x = v` and `once x = v` read with `dyn`; `const n = 3` reads `(defconst n 3)`, its type inferred as today. @@ -315,8 +316,7 @@ Each step lands on its own, with `dune test --root .` green. indent stack, then a parser to `Form.t`. Start with what `sand.flan` and `algorithms.flan` need, then the fallback, then the sugar in section 2 in order of corpus frequency (`set`, `let`, `+`, `at`, `=`, - `if`, `dotimes`, …). Until step 6 lands, a `.fln` function must write - `-> T`; omitting it is refused with a message saying inference is coming. + `if`, `dotimes`, …). **Test:** hand-convert `algorithms.flan` and `sand.flan` to `.fln`; the forms read from each pair must be equal, ignoring locations. 2. **Switch readers by extension** at every program-source entry point: @@ -358,6 +358,11 @@ Each step lands on its own, with `dune test --root .` green. (`ast.ml:491-492`). 6. **Return-type inference** in `Check`, with the recursion refusal and the stale-caller cause. This is independent of steps 1-5 once the marker exists. + **Built** (`Check.infer_returns`). `_` is refused outside a `defn`'s return + slot, in a generic's, and in `defgeneric`/`defmulti`'s (`defmethod` has no + return slot). Two ways out of one body with a value on one and none on the + other are refused rather than made `dyn`, since `()` does not box. A stale + body with `_` keeps the signature it was compiled with. Out of scope: dropping macros, built-in replacements for `with-*`/`defedn`, printing diagnostics in the new syntax, converting the prelude or vendor diff --git a/test/programs/dev-infer.flan b/test/programs/dev-infer.flan new file mode 100644 index 00000000..25d39c7b --- /dev/null +++ b/test/programs/dev-infer.flan @@ -0,0 +1,20 @@ +;;;; Return types read off the body, for the stale-caller warning's cause. +;;;; [speed]'s type is inferred and the tests change its body so that it +;;;; returns something else. [run] is a written caller, [relay] an inferred +;;;; one that returns what [speed] returns, and [sum] an inferred one whose +;;;; body stops checking once [speed] returns an f64: [twice] takes an i32. + +(defn speed [x i32] _ + (* x 2)) + +(defn run [] i32 (speed 3)) + +(defn relay [x i32] _ (speed x)) + +(defn twice [x i32] i32 (* x 2)) + +(defn sum [x i32] _ (twice (speed x)) (speed x)) + +(defn use-relay [] i32 (+ (relay 1) (sum 1))) + +(defn main [] i32 (+ (run) (use-relay))) diff --git a/test/syntax/infer/main.flan b/test/syntax/infer/main.flan new file mode 100644 index 00000000..69dccae0 --- /dev/null +++ b/test/syntax/infer/main.flan @@ -0,0 +1,27 @@ +;; Return types read off the body: _ in the return slot here, no arrow in +;; main.fln. Each shape the rule has: one type, a call's type, two types +;; (dyn), nothing (()), and a return that never falls off the end. + +(defn add [x i32 y i32] _ (+ x y)) + +(defn half [x f64] _ (/ x 2.0)) + +(defn quarter [x f64] _ (half (half x))) + +(defn pick [c bool] _ + (when c (return 1)) + 2.5) + +(defn say [x i32] _ (println x)) + +(defn- floor0 [x i32] _ + (if (< x 0) (return 0) x)) + +(defn main [] i32 + (println (add 1 2)) + (println (quarter 10.0)) + (println (pick true)) + (println (pick false)) + (say 4) + (println (floor0 -3) (floor0 5)) + 0) diff --git a/test/syntax/infer/main.fln b/test/syntax/infer/main.fln new file mode 100644 index 00000000..6ce6975a --- /dev/null +++ b/test/syntax/infer/main.fln @@ -0,0 +1,28 @@ +;; Return types read off the body: no arrow here, _ in the return slot in +;; main.flan. Each shape the rule has: one type, a call's type, two types +;; (dyn), nothing (()), and a return that never falls off the end. + +fn add(x: i32, y: i32) = x + y + +fn half(x: f64) = x / 2.0 + +fn quarter(x: f64) = half(half(x)) + +fn pick(c: bool) + if c + return 1 + 2.5 + +fn say(x: i32) = println(x) + +fn- floor0(x: i32) + if x < 0 then return 0 else x + +fn main() -> i32 + println(add(1, 2)) + println(quarter(10.0)) + println(pick(true)) + println(pick(false)) + say(4) + println(floor0(-3), floor0(5)) + 0 diff --git a/test/test_flan.ml b/test/test_flan.ml index 4d0f57f7..65da5f42 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -7078,4 +7078,78 @@ let () = accepts "calc-me.flan type checks" (In_channel.with_open_bin "../calc-me.flan" In_channel.input_all); + + (* ── Return types read off the body ([_]) ──────────────────────── *) + (* What each shape reads as, by the signature the editor is shown. *) + (let sign src name = + match checked src with + | p -> + (match List.find_opt (fun (f : Tast.fn) -> f.Tast.name = name) p.Tast.fns with + | Some f -> Dev.signature_of_fn f + | None -> "missing") + | exception Loc.Error { Loc.dmsg = m; _ } -> "refused: " ^ m + in + let reads_as what src name want = + let got = sign src name in + if got <> want then begin + incr failures; + Printf.printf "FAIL %s\n got: %s\n wanted: %s\n" what got want + end + in + let main = "\n(defn main [] ())" in + reads_as "an inferred return is the body's type" + ("(defn f [x i32] _ (+ x 1))" ^ main) "f" "f [i32] i32"; + reads_as "an inferred return follows a call to another" + ("(defn g [x f64] _ (f x))\n(defn f [x f64] _ (* x 2.0))" ^ main) "g" "g [f64] f64"; + reads_as "two types give dyn" + ("(defn f [c bool] _ (when c (return 1)) 2.5)" ^ main) "f" "f [bool] dyn"; + reads_as "a dyn body gives dyn" ("(defn f [x] _ x)" ^ main) "f" "f [dyn] dyn"; + reads_as "no value gives ()" ("(defn f [x i32] _ (println x))" ^ main) "f" "f [i32] ()"; + reads_as "an empty body gives ()" ("(defn f [] _)" ^ main) "f" "f [] ()"; + reads_as "a return that never falls off the end" + ("(defn f [x i32] _ (if (< x 0) (return 0) x))" ^ main) "f" "f [i32] i32"; + reads_as "a local that shares a name is not a call" + ("(defn f [x i32] _ (let [f 2] (+ x f)))" ^ main) "f" "f [i32] i32"; + reads_as "defn- reads it too" ("(defn- f [x i32] _ x)" ^ main) "f" "f [i32] i32"); + rejects_check "an inferred function that calls itself" + ~needle:"fact calls itself, so its return type cannot be read off its body" + "(defn fact [n i32] _ (if (< n 2) 1 (* n (fact (- n 1)))))\n(defn main [] ())"; + rejects_check "inferred functions that call each other, named in order" + ~needle:"ev and od call each other (ev → od → ev), so neither" + "(defn top [n i32] _ (ev n))\n\ + (defn ev [n i32] _ (if (= n 0) true (od (- n 1))))\n\ + (defn od [n i32] _ (if (= n 0) false (ev (- n 1))))\n\ + (defn main [] ())"; + rejects_check "a cycle of three is named whole" + ~needle:"a and b and c call each other (a → b → c → a), so none" + "(defn a [n i32] _ (b n))\n(defn b [n i32] _ (c n))\n\ + (defn c [n i32] _ (a n))\n(defn main [] ())"; + accepts "a written return type breaks the cycle" + "(defn ev [n i32] bool (if (= n 0) true (od (- n 1))))\n\ + (defn od [n i32] _ (if (= n 0) false (ev (- n 1))))\n\ + (defn main [] ())"; + rejects_check "a body error behind an inferred return is its own" + ~needle:"expected i32, found string" + "(defn f [x i32] _ (+ x \"a\"))\n(defn g [x i32] _ (f x))\n(defn main [] ())"; + rejects_check "no value on one path and a value on another" + ~needle:"f gives no value here and i32 on another path" + "(defn f [x i32] _ (when (> x 0) (return 1)) (println 2))\n(defn main [] ())"; + 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 [] ())"; + rejects_check "_ in a generic's return slot" ~needle:"f is generic, and _" + "(defn f [x $t] _ x)\n(defn main [] ())"; + rejects_check "_ as a parameter type" + ~needle:"_ here asks for x's type to be read off a body" + "(defn f [x _] i32 3)\n(defn main [] ())"; + rejects_check "_ as a field type" ~needle:"only a defn's return slot" + "(defstruct P [x _])\n(defn main [] ())"; + rejects_check "_ in a function type" ~needle:"only a defn's return slot" + "(defn main [] () (let [f (the (Fn [i32] _) (fn [x] x))] (f 1)))"; + rejects_check "_ in a declare" ~needle:"only a defn's return slot" + "(declare cabs [x i32] _ \"abs\")\n(defn main [] ())"; + parse_rejects "_ in a defgeneric's return slot" + ~needle:"defgeneric's methods each have their own" + "(defgeneric area [s] _)"; + Test_support.report () diff --git a/test/test_session.ml b/test/test_session.ml index 5af415c9..ffe2a9f9 100644 --- a/test/test_session.ml +++ b/test/test_session.ml @@ -1764,4 +1764,60 @@ let () = | _ -> fail "a package's bare name resolved from the program's own file" | exception Loc.Error _ -> ()); + (* ── A return type read off the body changes ─────────────────────── + [speed]'s return slot is [_], and a new body makes it an f64. It + installs like a written change, and each stale caller says why the + signature moved and which line moved it: nobody wrote the old or the + new type. [relay] returns what [speed] returns, so its own signature + moves too and its caller is named for that, at [relay]'s line. [sum] + no longer checks, and is a stale caller like [run]: it keeps the + signature it was compiled with. *) + (let t, _ = Session.create ~file:"programs/dev-infer.flan" () in + match + Session.eval ~origin:"programs/dev-infer.flan" t + "(defn speed [x i32] _\n (* (f64 x) 2.5))" + with + | exception Loc.Error { Loc.dmsg = m; _ } -> + fail "an inferred return type that changed was refused: %s" m + | c -> + if not (List.mem "speed" c.Session.fns) then + fail "the inferred change was not installed"; + let got = + List.map + (fun (x : Session.stale) -> + (x.Session.caller, x.Session.target, + Option.value x.Session.cause ~default:"-")) + c.Session.stale + in + let want = + [ ("run", "speed", "speed now returns f64, not i32, because of line 2"); + ("relay", "speed", "speed now returns f64, not i32, because of line 2"); + ("sum", "speed", "speed now returns f64, not i32, because of line 2"); + ("sum", "speed", "speed now returns f64, not i32, because of line 2"); + ("use-relay", "relay", + "relay now returns f64, not i32, because of line 12") ] + in + if got <> want then + fail "the stale callers of an inferred change were %s" + (String.concat "; " + (List.map (fun (a, b, c) -> Printf.sprintf "%s->%s (%s)" a b c) got)); + (match + List.find_opt + (fun (f : Tast.fn) -> f.Tast.name = "sum") + t.Session.program.Tast.fns + with + | Some f when Types.equal f.Tast.ret (Types.Int Types.I32) -> () + | Some f -> + fail "the stale inferred caller sum now returns %s" + (Types.to_string f.Tast.ret) + | None -> fail "the stale inferred caller sum left the program")); + (* A written return type that changes names no cause. *) + (let t, _ = Session.create ~file:"programs/dev-stale.flan" () in + match Session.eval t "(defn scale [x i64] i32 (i32 x))" with + | exception Loc.Error { Loc.dmsg = m; _ } -> fail "a written change: %s" m + | c -> + if List.exists (fun (x : Session.stale) -> x.Session.cause <> None) + c.Session.stale + then fail "a written return type's change named a cause"); + Test_support.report ~label:"session" () diff --git a/test/test_syntax.ml b/test/test_syntax.ml index d8dc6426..70422f0f 100644 --- a/test/test_syntax.ml +++ b/test/test_syntax.ml @@ -83,6 +83,7 @@ let pair flan fln = let () = pair "syntax/algorithms.flan" "syntax/algorithms.fln"; pair "../sand.flan" "syntax/sand.fln"; + pair "syntax/infer/main.flan" "syntax/infer/main.fln"; (* Checked, never run: sand opens a window. *) List.iter (fun f -> @@ -286,7 +287,10 @@ let () = "fn g(h: Fn(i32, i32) -> bool) -> () = h(1, 2)" "(defn g [h (Fn [i32 i32] bool)] () (h 1 2))"; reads "untyped parameter is dyn" "fn id(x) -> dyn = x" "(defn id [x dyn] dyn x)"; - refuses "no return type" "fn f(x)\n x" "indent/return-type" "-> i32"; + reads "no arrow infers the return" "fn f(x)\n x" "(defn f [x dyn] _ x)"; + reads "no arrow, one expression" "fn f(x: i32) = x + 1" "(defn f [x i32] _ (+ x 1))"; + reads "no arrow, with where" "fn f(x: $t) where ordered?($t) = x" + "(defn f [x $t] _ {:where (ordered? $t)} x)"; (* Characters, lexed before brackets and separators. *) reads "character literals" "x = [\\( \\, \\space \\)]" "(set x [\\( \\, \\space \\)])"; reads "character arguments" "f(\\,, \\))" "(f \\, \\))"; @@ -552,7 +556,11 @@ let run_both path want = let () = if Test_support.have "clang" then begin run_both "syntax/mixed/main.flan" "12\n12\n0\n55\n"; - run_both "syntax/mixed/main.fln" "25\n7\nfar\n3\n" + run_both "syntax/mixed/main.fln" "25\n7\nfar\n3\n"; + (* Return types read off the body, in both spellings of [_]. *) + List.iter + (fun p -> run_both p "3\n2.5\n1\n2.5\n4\n0 5\n") + [ "syntax/infer/main.flan"; "syntax/infer/main.fln" ] end else print_endline "syntax: no clang, the import programs are not built" From 8fdf8513fd8a5fceb951e275b79ba23fc320759a Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Fri, 25 Sep 2026 20:17:44 +0700 Subject: [PATCH 2/9] A _ body's errors are reported with every other error in the file, a literal return takes the type of the other exits, and a recursive _ function that gives nothing returns () --- TODO.org | 3 +- lib/check.ml | 243 ++++++++++++++++++++++++------------ spec-syntax.md | 4 +- test/syntax/infer/main.flan | 19 ++- test/syntax/infer/main.fln | 20 ++- test/test_flan.ml | 42 ++++++- test/test_syntax.ml | 2 +- 7 files changed, 244 insertions(+), 89 deletions(-) diff --git a/TODO.org b/TODO.org index 145ceafe..87c5a67c 100644 --- a/TODO.org +++ b/TODO.org @@ -40,7 +40,8 @@ optional return slot. ** DONE A return type is read off the body only when the slot says =_= CLOSED: [2026-09-25] The body's own type, never a call site's; parameters are never inferred, and a -cycle among =_= functions is refused by name. Rules out use-directed inference. +cycle among =_= functions is refused by name unless it gives =()=. Rules out +use-directed inference. ** DONE def, defonce and defconst are the three forms CLOSED: [2026-09-20] diff --git a/lib/check.ml b/lib/check.ml index 9c43282d..d149172d 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -214,6 +214,11 @@ type env = { (* Every [defn] whose return type was read off its body ([_]), with the form that decided it — what a stale-caller warning points at. *) inferred : (string, Loc.t) Hashtbl.t; + (* The [_] bodies whose type could not be read because of an error of + their own, while every error is being collected. Each stands in [fns] + as Never, a call to one stands as a poison, and pass two reports the + body's errors once. *) + infer_failed : (string, unit) Hashtbl.t; (* Recovery: checking goes on past a refused subexpression. See [check]. [recovering] is on only while a whole-file or session check is collecting every error; [recovered] is what it found, newest first; [poison] counts @@ -260,6 +265,7 @@ let new_env () = { classes = Hashtbl.create 8; tracks = Hashtbl.create 16; inferred = Hashtbl.create 8; + infer_failed = Hashtbl.create 4; recovering = false; recovered = []; poison = 0; @@ -4479,7 +4485,7 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr = else begin let seen = env.poison in let caused () = - env.recovered <> [] + (env.recovered <> [] || Hashtbl.length env.infer_failed > 0) && (env.poison > seen || want = Some Types.Never) in match check_plain ctx ?want e with @@ -11334,6 +11340,13 @@ and ordinary_call ctx ~want loc name args = lifted body captures it by value and then calls the copy. [peek_outer] rather than [capture] in the guard, because a guard must not take a copy on its way to deciding what a form means. *) + (* A [_] function whose body failed has no return type to give; its own + errors are reported with its body, so a call to it stands in. *) + | _ when ctx.env.recovering && Hashtbl.mem ctx.env.infer_failed name + && lookup ctx name = None -> + List.iter (fun a -> ignore (check ctx a)) args; + ctx.env.poison <- ctx.env.poison + 1; + poison loc (* A local bound to a refused initialiser's stand-in, called: the refusal is already reported, so the call stands in too, its arguments still checked. *) @@ -13475,6 +13488,16 @@ let rec check_fn ?sign env (fn : Ast.fn) : Tast.fn = let params, ret = match sign with Some s -> s | None -> Hashtbl.find env.fns fn.Ast.name in + (* A [_] body whose type could not be read stands in [fns] as Never (see + [infer_returns]); pass two reads it the same way again, so its errors + are reported here, once, with every other body's. *) + let ret = + match sign, fn.Ast.ret with + | None, Some { Ast.t = Ast.Tinfer; _ } + when Hashtbl.mem env.infer_failed fn.Ast.name -> + infer_ret + | _ -> ret + in let ctx = { (invented_ctx env ret) with owner = fn.Ast.name } in List.iter2 (fun (p : Ast.field) ty -> @@ -13667,68 +13690,91 @@ and check_generic env (fn : Ast.fn) = (* The type one body gives, and the form that decided it: the last form and every [return], ignoring what never arrives. All alike give that type; - none gives (); any two that differ give dyn, decided by the first one to - differ. *) + none gives (). When they differ, each one's type is tried as the return + type the body is checked against, last form first, so a literal takes the + type of the other exits the way an [if]'s arms do; the first that checks + is the type. When none does, they meet in dyn. *) and read_return env (fn : Ast.fn) params = - 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 seen = !infer_seen in - infer_seen := []; - let restore ~copies = - env.lifted <- lifted; - infer_seen := seen; - if copies then begin - (* A copy a failed read asked for goes with it, as [tolerant] does. *) - 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 + (* 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. *) + 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 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 + match speculate env (fun () -> check_fn ~sign:(params, ret) env fn) with + | exception e -> restore ~copies:true; raise e + | tf -> + let returns = List.rev !infer_seen in + restore ~copies:false; + (tf, returns) in - match speculate env (fun () -> check_fn ~sign:(params, infer_ret) env fn) with - | exception e -> restore ~copies:true; raise e - | tf -> - let returns = List.rev !infer_seen in - restore ~copies:false; - let last = - match List.rev tf.Tast.body with - | (x : Tast.expr) :: _ -> [ (x.Tast.ty, x.Tast.loc) ] - | [] -> [] + let tf, returns = attempt infer_ret in + let last = + match List.rev tf.Tast.body with + | (x : Tast.expr) :: _ -> [ (x.Tast.ty, x.Tast.loc) ] + | [] -> [] + in + let arrive = + List.filter (fun (t, _) -> not (Types.equal t Types.Never)) (returns @ last) + in + match arrive with + | [] -> (Types.Unit, fn.Ast.nloc) + | (t, l) :: rest + when not (List.exists (fun (u, _) -> not (Types.equal t u)) rest) -> + (t, l) + | _ -> + let candidates = + List.fold_left + (fun acc (t, l) -> + if List.exists (fun (u, _) -> Types.equal t u) acc then acc + else acc @ [ (t, l) ]) + [] (List.rev arrive) in - let arrive = - List.filter - (fun (t, _) -> not (Types.equal t Types.Never)) - (returns @ last) + let fits (t, _) = + match attempt t with _ -> true | exception Loc.Error _ -> false in - (* Two types meet in dyn only if both box into it, and () and a struct - do not: said here, with both ways out, rather than as a boxing - refusal at one of them in pass two. *) - let boxes (t, _) = - match t with - | Types.Int _ | Types.Float _ | Types.Bool | Types.String | Types.Dyn -> - true - | _ -> false - in - (match arrive with - | (t0, _) :: _ - when List.exists (fun (u, _) -> not (Types.equal t0 u)) arrive -> + (match List.find_opt fits candidates with + | Some found -> found + | None -> + (* Two types meet in dyn only if both box into it, and () and a + struct do not: said here, with both ways out, rather than as a + boxing refusal at one of them in pass two. *) + let boxes (t, _) = + match t with + | Types.Int _ | Types.Float _ | Types.Bool | Types.String + | Types.Dyn -> true + | _ -> false + in (match List.find_opt (fun x -> not (boxes x)) arrive with | Some (bad, at) -> let other, oloc = List.find (fun (u, _) -> not (Types.equal u bad)) arrive in - let notes = [ Loc.note oloc ("this gives " ^ Types.to_string other) ] in + let notes = + [ Loc.note oloc ("this gives " ^ Types.to_string other) ] + in if Types.equal bad Types.Unit then Loc.failk "check/infer-mixed" at ~notes "%s gives no value here and %s on another path, and its \ @@ -13743,16 +13789,12 @@ and read_return env (fn : Ast.fn) params = return type" fn.Ast.name (Types.to_string bad) (Types.to_string other) (Types.to_string bad) - | None -> ()) - | _ -> ()); - (match arrive with - | [] -> (Types.Unit, fn.Ast.nloc) - | (t, l) :: rest -> - (match List.find_opt (fun (u, _) -> not (Types.equal t u)) rest with - | None -> (t, l) - | Some (_, l') -> (Types.Dyn, l'))) + | None -> + let t, _ = List.hd arrive in + let _, l' = List.find (fun (u, _) -> not (Types.equal t u)) arrive in + (Types.Dyn, l'))) -and infer_returns ?tolerate ?(previous = fun _ -> None) env +and infer_returns ~keep_going ?tolerate ?(previous = fun _ -> None) env (decls : Ast.decl list) = let pending = List.filter_map @@ -13798,21 +13840,21 @@ and infer_returns ?tolerate ?(previous = fun _ -> None) env Hashtbl.replace env.fns fn.Ast.name (params, ret); Hashtbl.replace env.inferred fn.Ast.name cause in - let rec rounds left = - let still = - List.filter - (fun fn -> - match settle fn with - | () -> false - | exception Loc.Error _ -> true) - left - in - if still <> [] && List.length still < List.length left then rounds still - else still - in (* A body [tolerate] excuses keeps the signature it was compiled with, [previous]'s, the way pass two keeps its compiled body: it is a stale caller, not a change. *) + (* A body that fails for its own reasons is left to pass two, which + reports its errors with every other body's. Until then it stands as + Never, which fits anywhere, so its callers are not refused for its + sake; a [_] body that calls it cannot be read either, and waits the + same way. *) + let failed = env.infer_failed in + let fail_quietly (fn : Ast.fn) = + Hashtbl.replace failed fn.Ast.name (); + Hashtbl.replace env.fns fn.Ast.name (params_of fn, Types.Never) + in + (* Only while every error is collected: a check that stops at the first + reports this body's own, here. *) let excused (fn : Ast.fn) = match settle fn with | () -> () @@ -13820,7 +13862,49 @@ and infer_returns ?tolerate ?(previous = fun _ -> None) env (match tolerate, previous fn.Ast.name with | Some ok, Some (params, ret) when ok env fn.Ast.name d -> Hashtbl.replace env.fns fn.Ast.name (params, ret) - | _ -> raise e) + | _ -> if keep_going then fail_quietly fn else raise e) + in + let rec rounds left = + let still = + List.filter + (fun (fn : Ast.fn) -> + if List.exists (fun (m, _) -> Hashtbl.mem failed m) + (List.assoc fn.Ast.name deps) + then begin fail_quietly fn; false end + else + match settle fn with + | () -> false + | exception Loc.Error _ -> true) + left + in + if still <> [] && List.length still < List.length left then rounds still + else still + in + (* A loop of [_] bodies that give no value on any way out — a + countdown that calls itself — is (): each is read with the others + taken as (), and kept only when every one of them gives () back. *) + let units stuck = + List.iter + (fun (fn : Ast.fn) -> + Hashtbl.replace env.fns fn.Ast.name (params_of fn, Types.Unit)) + stuck; + let all_unit = + List.for_all + (fun (fn : Ast.fn) -> + match read_return env fn (params_of fn) with + | t, cause when Types.equal t Types.Unit -> + Hashtbl.replace env.inferred fn.Ast.name cause; true + | _ -> false + | exception Loc.Error _ -> false) + stuck + in + if not all_unit then + List.iter + (fun (fn : Ast.fn) -> + Hashtbl.remove env.fns fn.Ast.name; + Hashtbl.remove env.inferred fn.Ast.name) + stuck; + all_unit in let rec stalled left = let stuck = rounds left in @@ -13870,6 +13954,11 @@ and infer_returns ?tolerate ?(previous = fun _ -> None) env in rot cycle in + if units (List.map (fun n -> List.assoc n byname) cycle) then + stalled + (List.filter + (fun (fn : Ast.fn) -> not (List.mem fn.Ast.name cycle)) stuck) + else let first = List.hd cycle in let fn = List.assoc first byname in let next i = List.nth cycle ((i + 1) mod List.length cycle) in @@ -15051,7 +15140,7 @@ let build_program ~keep_going ?tolerate ?previous (decls : Ast.decl list) : (List.rev !pairing_warnings); check_finite env; check_union_members env; - infer_returns ?tolerate ?previous env decls; + infer_returns ~keep_going ?tolerate ?previous env decls; let s = Loc.sink ~on:keep_going in ignore (Loc.caught s (fun () -> check_main env decls)); (* Every generic body, checked once with its variables left abstract, and diff --git a/spec-syntax.md b/spec-syntax.md index 9b327b3e..0f2de937 100644 --- a/spec-syntax.md +++ b/spec-syntax.md @@ -363,7 +363,9 @@ Each step lands on its own, with `dune test --root .` green. slot, in a generic's, and in `defgeneric`/`defmulti`'s (`defmethod` has no return slot). Two ways out of one body whose types differ and cannot both box (a value and `()`, a number and a struct) are refused rather than made - `dyn`. A stale + `dyn`. Exits of different types are first tried at each other's type, so a + literal `return 0` beside an `i64` gives `i64`. A self- or mutually + recursive group whose every exit gives `()` is `()`. A stale body with `_` keeps the signature it was compiled with. Out of scope: dropping macros, built-in replacements for `with-*`/`defedn`, diff --git a/test/syntax/infer/main.flan b/test/syntax/infer/main.flan index 69dccae0..b197b9ad 100644 --- a/test/syntax/infer/main.flan +++ b/test/syntax/infer/main.flan @@ -1,6 +1,8 @@ ;; Return types read off the body: _ in the return slot here, no arrow in -;; main.fln. Each shape the rule has: one type, a call's type, two types -;; (dyn), nothing (()), and a return that never falls off the end. +;; main.fln. Each shape the rule has: one type, a call's type, a literal +;; that takes the other exit's type, two types (dyn), nothing (()), a return +;; that never falls off the end, and a function that calls itself and gives +;; nothing. (defn add [x i32 y i32] _ (+ x y)) @@ -12,16 +14,27 @@ (when c (return 1)) 2.5) +(defn label [c bool] _ + (when c (return "yes")) + 0) + (defn say [x i32] _ (println x)) (defn- floor0 [x i32] _ (if (< x 0) (return 0) x)) +(defn countdown [n i32] _ + (when (> n 0) + (println n) + (countdown (- n 1)))) + (defn main [] i32 (println (add 1 2)) (println (quarter 10.0)) - (println (pick true)) + (println (+ (pick true) 0.5)) (println (pick false)) + (println (label true) (label false)) (say 4) (println (floor0 -3) (floor0 5)) + (countdown 2) 0) diff --git a/test/syntax/infer/main.fln b/test/syntax/infer/main.fln index 6ce6975a..8ade8d50 100644 --- a/test/syntax/infer/main.fln +++ b/test/syntax/infer/main.fln @@ -1,6 +1,8 @@ ;; Return types read off the body: no arrow here, _ in the return slot in -;; main.flan. Each shape the rule has: one type, a call's type, two types -;; (dyn), nothing (()), and a return that never falls off the end. +;; main.flan. Each shape the rule has: one type, a call's type, a literal +;; that takes the other exit's type, two types (dyn), nothing (()), a return +;; that never falls off the end, and a function that calls itself and gives +;; nothing. fn add(x: i32, y: i32) = x + y @@ -13,16 +15,28 @@ fn pick(c: bool) return 1 2.5 +fn label(c: bool) + if c + return "yes" + 0 + fn say(x: i32) = println(x) fn- floor0(x: i32) if x < 0 then return 0 else x +fn countdown(n: i32) + if n > 0 + println(n) + countdown(n - 1) + fn main() -> i32 println(add(1, 2)) println(quarter(10.0)) - println(pick(true)) + println(pick(true) + 0.5) println(pick(false)) + println(label(true), label(false)) say(4) println(floor0(-3), floor0(5)) + countdown(2) 0 diff --git a/test/test_flan.ml b/test/test_flan.ml index 5d255063..b3c2a9e3 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -7320,8 +7320,19 @@ let () = ("(defn f [x i32] _ (+ x 1))" ^ main) "f" "f [i32] i32"; reads_as "an inferred return follows a call to another" ("(defn g [x f64] _ (f x))\n(defn f [x f64] _ (* x 2.0))" ^ main) "g" "g [f64] f64"; + reads_as "a literal return takes the other exit's type" + ("(defn f [c bool] _ (when c (return 1)) 2.5)" ^ main) "f" "f [bool] f64"; + reads_as "a literal return takes a parameter's type" + ("(defn f [x i64] _ (when (< x 0) (return 0)) x)" ^ main) "f" "f [i64] i64"; + reads_as "a literal return takes an f32" + ("(defn f [c bool x f32] _ (when c (return 1)) x)" ^ main) "f" "f [bool f32] f32"; reads_as "two types give dyn" - ("(defn f [c bool] _ (when c (return 1)) 2.5)" ^ main) "f" "f [bool] dyn"; + ("(defn f [c bool] _ (when c (return \"s\")) 2)" ^ main) "f" "f [bool] dyn"; + reads_as "a function that calls itself and gives nothing is ()" + ("(defn f [n i32] _ (when (> n 0) (println n) (f (- n 1))))" ^ main) "f" "f [i32] ()"; + reads_as "two that call each other and give nothing are ()" + ("(defn ev [n i32] _ (when (> n 0) (od (- n 1))))\n\ + (defn od [n i32] _ (when (> n 0) (ev (- n 1))))" ^ main) "od" "od [i32] ()"; reads_as "a dyn body gives dyn" ("(defn f [x] _ x)" ^ main) "f" "f [dyn] dyn"; reads_as "no value gives ()" ("(defn f [x i32] _ (println x))" ^ main) "f" "f [i32] ()"; reads_as "an empty body gives ()" ("(defn f [] _)" ^ main) "f" "f [] ()"; @@ -7341,8 +7352,8 @@ let () = (defn main [] ())"; rejects_check "a cycle of three is named whole" ~needle:"a and b and c call each other (a → b → c → a), so none" - "(defn a [n i32] _ (b n))\n(defn b [n i32] _ (c n))\n\ - (defn c [n i32] _ (a n))\n(defn main [] ())"; + "(defn a [n i32] _ (+ 1 (b n)))\n(defn b [n i32] _ (+ 1 (c n)))\n\ + (defn c [n i32] _ (+ 1 (a n)))\n(defn main [] ())"; accepts "a written return type breaks the cycle" "(defn ev [n i32] bool (if (= n 0) true (od (- n 1))))\n\ (defn od [n i32] _ (if (= n 0) false (ev (- n 1))))\n\ @@ -7357,6 +7368,31 @@ let () = ~needle:"f gives P here and i32 on another path" "(defstruct P [x i32])\n\ (defn f [c bool] _ (when c (return (P {.x 1}))) 2)\n(defn main [] ())"; + (* Every error in the file is still reported, a [_] body's included, and + a call to a [_] function whose body failed adds none of its own. *) + (let count src = + match program src |> Check.program_all with + | _ -> 0 + | exception Loc.Error _ -> 1 + | exception Loc.Errors ds -> List.length ds + in + let errors what src n = + let got = count src in + if got <> n then begin + incr failures; + Printf.printf "FAIL %s: %d errors, wanted %d\n" what got n + end + in + errors "a _ body's error does not hide the others" + "(defn bad1 [x i32] _ (+ x \"s\"))\n\ + (defn bad2 [x i32] i32 (+ x \"t\"))\n\ + (defn bad3 [x i32] i32 (undefined-thing x))\n(defn main [] i32 0)" 3; + errors "every error in one _ body" + "(defn bad1 [x i32] _ (+ x \"s\") (foo) (bar))\n(defn main [] i32 0)" 3; + errors "a call to a failed _ body adds nothing" + "(defn bad1 [x i32] _ (+ x \"s\"))\n(defn g [x i32] _ (bad1 x))\n\ + (defn h [x i32] i32 (+ 1 (g x)))\n\ + (defn main [] i32 (println (bad1 1)) 0)" 1); 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 [] ())"; diff --git a/test/test_syntax.ml b/test/test_syntax.ml index 429a0afb..4f6414f6 100644 --- a/test/test_syntax.ml +++ b/test/test_syntax.ml @@ -564,7 +564,7 @@ let () = run_both "syntax/mixed/main.fln" "25\n7\nfar\n3\n"; (* Return types read off the body, in both spellings of [_]. *) List.iter - (fun p -> run_both p "3\n2.5\n1\n2.5\n4\n0 5\n") + (fun p -> run_both p "3\n2.5\n1.5\n2.5\nyes 0\n4\n0 5\n2\n1\n") [ "syntax/infer/main.flan"; "syntax/infer/main.fln" ] end else print_endline "syntax: no clang, the import programs are not built" From df7078d586b64719e805891893088438ac09d87d Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Fri, 25 Sep 2026 20:37:50 +0700 Subject: [PATCH 3/9] A _ function's exits combine exactly as an if's arms do, a refused _ body or loop is collected with every other error, and the placeholder type never leaves the checker --- lib/check.ml | 157 ++++++++++++++++++++---------------- spec-syntax.md | 14 ++-- test/syntax/infer/main.flan | 8 +- test/syntax/infer/main.fln | 8 +- test/test_flan.ml | 37 +++++++-- 5 files changed, 134 insertions(+), 90 deletions(-) diff --git a/lib/check.ml b/lib/check.ml index d149172d..94812188 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -218,7 +218,7 @@ type env = { their own, while every error is being collected. Each stands in [fns] as Never, a call to one stands as a poison, and pass two reports the body's errors once. *) - infer_failed : (string, unit) Hashtbl.t; + infer_failed : (string, Loc.diag option) Hashtbl.t; (* Recovery: checking goes on past a refused subexpression. See [check]. [recovering] is on only while a whole-file or session check is collecting every error; [recovered] is what it found, newest first; [poison] counts @@ -3690,7 +3690,7 @@ let hash_ty = Types.Int Types.U64 address, so no type written anywhere is ever mistaken for it. What each [return] in that body gives is pushed on [infer_seen]. *) let infer_ret = Types.Named "_" -let infer_seen : (Types.t * Loc.t) list ref = ref [] +let infer_seen : (Types.t * Loc.t * bool) list ref = ref [] (* What a refused subexpression stands as while recovering. [Zero] of [Never] is a value nothing else builds, so it is recognisable; see [check]. *) let poison loc = { Tast.e = Tast.Zero Types.Never; ty = Types.Never; loc } @@ -4788,11 +4788,12 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr = (match ctx.in_frames with Some n -> n | None -> assert false) | Ast.Return v when ctx.ret == infer_ret -> + let lit = match v with Some x -> lone_literal x | None -> false in let v = Option.map (check ctx) v in infer_seen := (match v with - | Some (x : Tast.expr) -> (x.Tast.ty, loc) - | None -> (Types.Unit, loc)) + | Some (x : Tast.expr) -> (x.Tast.ty, loc, lit) + | None -> (Types.Unit, loc, false)) :: !infer_seen; (match ctx.defers, v with | [], _ -> mk loc Types.Never (Tast.Return v) @@ -13644,6 +13645,15 @@ let rec check_fn ?sign env (fn : Ast.fn) : Tast.fn = | None -> ctx.defers | Some s -> guarded_defers s ctx.defers); fenv = None; fparent = None; floc = fn.Ast.nloc } + |> fun (tf : Tast.fn) -> + if sign = None && ret == infer_ret then + (* Pass two over a [_] body pass one could not read: its errors are + raised above; a body that checks has the refusal pass one made about + its exits, or waited on one that did, and stands as Never. *) + match Hashtbl.find_opt env.infer_failed fn.Ast.name with + | Some (Some d) -> raise (Loc.Error d) + | _ -> { tf with Tast.ret = Types.Never } + else tf (* The generic body, checked once with its variables abstract. Nothing is kept — the [Tast.fn] it produces is thrown away, and so is anything it lifted — @@ -13688,12 +13698,15 @@ and check_generic env (fn : Ast.fn) = them never settles and is refused by name; a body that calls its own name is the cycle of one. *) -(* The type one body gives, and the form that decided it: the last form and - every [return], ignoring what never arrives. All alike give that type; - none gives (). When they differ, each one's type is tried as the return - type the body is checked against, last form first, so a literal takes the - type of the other exits the way an [if]'s arms do; the first that checks - is the type. When none does, they meet in dyn. *) +(* The type one body gives, and the form that decided it. The exits — the + last form and every [return], less what never arrives — combine the way + an [if]'s arms do ([check_if_once]): the first one that is not a lone + literal decides and the literals take its type, a bool meets a dyn at + dyn, and literals alone meet at the wider of their own types. The body is + then checked against that type exactly as a written one would be, so + whatever [if] refuses between its 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. *) @@ -13732,67 +13745,48 @@ and read_return env (fn : Ast.fn) params = in let tf, returns = attempt infer_ret in let last = - match List.rev tf.Tast.body with - | (x : Tast.expr) :: _ -> [ (x.Tast.ty, x.Tast.loc) ] - | [] -> [] + match List.rev tf.Tast.body, List.rev fn.Ast.fbody with + | (x : Tast.expr) :: _, (a : Ast.expr) :: _ -> + [ (x.Tast.ty, x.Tast.loc, lone_literal a) ] + | (x : Tast.expr) :: _, [] -> [ (x.Tast.ty, x.Tast.loc, false) ] + | [], _ -> [] in let arrive = - List.filter (fun (t, _) -> not (Types.equal t Types.Never)) (returns @ last) + List.filter (fun (t, _, _) -> not (Types.equal t Types.Never)) (returns @ last) in + let unit (t, _, _) = Types.equal t Types.Unit in + (match List.find_opt unit arrive, List.find_opt (fun x -> not (unit x)) arrive with + | Some (_, bare, _), Some (t, valued, _) -> + Loc.failk "check/infer-mixed" bare + ~notes:[ Loc.note valued ("this gives " ^ Types.to_string t) ] + "%s gives no value here and %s on another path, and its return \ + type is read off its body. Give this path a value too, or write \ + the return type" + fn.Ast.name (Types.to_string t) + | _ -> ()); match arrive with | [] -> (Types.Unit, fn.Ast.nloc) - | (t, l) :: rest - when not (List.exists (fun (u, _) -> not (Types.equal t u)) rest) -> + | (t, l, _) :: rest + when not (List.exists (fun (u, _, _) -> not (Types.equal t u)) rest) -> (t, l) - | _ -> - let candidates = - List.fold_left - (fun acc (t, l) -> - if List.exists (fun (u, _) -> Types.equal t u) acc then acc - else acc @ [ (t, l) ]) - [] (List.rev arrive) + | (t0, l0, _) :: _ -> + let decided = + match List.filter (fun (_, _, lit) -> not lit) arrive with + | (Types.Bool, l, _) :: others + when List.exists (fun (u, _, _) -> Types.equal u Types.Dyn) others -> + (Types.Dyn, l) + | (t, l, _) :: _ -> (t, l) + | [] -> + let joined = + List.fold_left + (fun acc (u, _, _) -> + match acc with Some a -> Types.join a u | None -> None) + (Some t0) arrive + in + (Option.value joined ~default:t0, l0) in - let fits (t, _) = - match attempt t with _ -> true | exception Loc.Error _ -> false - in - (match List.find_opt fits candidates with - | Some found -> found - | None -> - (* Two types meet in dyn only if both box into it, and () and a - struct do not: said here, with both ways out, rather than as a - boxing refusal at one of them in pass two. *) - let boxes (t, _) = - match t with - | Types.Int _ | Types.Float _ | Types.Bool | Types.String - | Types.Dyn -> true - | _ -> false - in - (match List.find_opt (fun x -> not (boxes x)) arrive with - | Some (bad, at) -> - let other, oloc = - List.find (fun (u, _) -> not (Types.equal u bad)) arrive - in - let notes = - [ Loc.note oloc ("this gives " ^ Types.to_string other) ] - in - if Types.equal bad Types.Unit then - Loc.failk "check/infer-mixed" at ~notes - "%s gives no value here and %s on another path, and its \ - return type is read off its body. Give this path a value \ - too, or write the return type" - fn.Ast.name (Types.to_string other) - else - Loc.failk "check/infer-mixed" at ~notes - "%s gives %s here and %s on another path, and its return type \ - is read off its body. Two types meet only in dyn, and %s does \ - not box into it. Give every path one type, or write the \ - return type" - fn.Ast.name (Types.to_string bad) (Types.to_string other) - (Types.to_string bad) - | None -> - let t, _ = List.hd arrive in - let _, l' = List.find (fun (u, _) -> not (Types.equal t u)) arrive in - (Types.Dyn, l'))) + ignore (attempt (fst decided)); + decided and infer_returns ~keep_going ?tolerate ?(previous = fun _ -> None) env (decls : Ast.decl list) = @@ -13849,8 +13843,8 @@ and infer_returns ~keep_going ?tolerate ?(previous = fun _ -> None) env sake; a [_] body that calls it cannot be read either, and waits the same way. *) let failed = env.infer_failed in - let fail_quietly (fn : Ast.fn) = - Hashtbl.replace failed fn.Ast.name (); + let fail_quietly ?refusal (fn : Ast.fn) = + Hashtbl.replace failed fn.Ast.name refusal; Hashtbl.replace env.fns fn.Ast.name (params_of fn, Types.Never) in (* Only while every error is collected: a check that stops at the first @@ -13862,7 +13856,7 @@ and infer_returns ~keep_going ?tolerate ?(previous = fun _ -> None) env (match tolerate, previous fn.Ast.name with | Some ok, Some (params, ret) when ok env fn.Ast.name d -> Hashtbl.replace env.fns fn.Ast.name (params, ret) - | _ -> if keep_going then fail_quietly fn else raise e) + | _ -> if keep_going then fail_quietly ~refusal:d fn else raise e) in let rec rounds left = let still = @@ -13972,6 +13966,9 @@ and infer_returns ~keep_going ?tolerate ?(previous = fun _ -> None) env else Printf.sprintf "%s calls %s here" n callee)) cycle in + (* Collected like any refusal when every error is: the loop's + first member carries it into pass two, the rest stand quietly. *) + match (match cycle with | [ n ] -> Loc.failk "check/infer-recursive" fn.Ast.nloc ~notes @@ -13984,7 +13981,20 @@ and infer_returns ~keep_going ?tolerate ?(previous = fun _ -> None) env them in its signature" (String.concat " and " cycle) (String.concat " → " (cycle @ [ first ])) - (if List.length cycle = 2 then "neither" else "none"))) + (if List.length cycle = 2 then "neither" else "none")) + with + | () -> () + | exception (Loc.Error d as e) -> + if not keep_going then raise e; + List.iter + (fun n -> + fail_quietly + ?refusal:(if n = first then Some d else None) + (List.assoc n byname)) + cycle; + stalled + (List.filter + (fun (fn : Ast.fn) -> not (List.mem fn.Ast.name cycle)) stuck)) in stalled order end @@ -15199,6 +15209,17 @@ let build_program ~keep_going ?tolerate ?previous (decls : Ast.decl list) : (Loc.entry ~mark:'~' ~label:"warning: " d.Loc.dloc d.Loc.dmsg)) (List.rev !grow_warnings); Loc.finish s; + (* The placeholder a [_] body is read against is never a type anything + downstream may see; a signature carrying it would be emitted as a + struct named _. *) + List.iter + (fun (f : Tast.fn) -> + if f.Tast.ret == infer_ret + || List.exists (fun t -> t == infer_ret) f.Tast.params + then + fail f.Tast.floc "internal: %s left the checker with its return \ + type unread" f.Tast.name) + fns; (* The handler clauses lifted out along the way. They are ordinary functions from here down; nothing in the backend knows they were written inside something else. *) diff --git a/spec-syntax.md b/spec-syntax.md index 0f2de937..050bdfd8 100644 --- a/spec-syntax.md +++ b/spec-syntax.md @@ -54,8 +54,10 @@ 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`; `return`s of - different types give `dyn`; no value gives `()`. +- the return type is the body's type; a `dyn` body gives `dyn`; the exits (the + last form and each `return`) combine exactly as an `if`'s arms do, so a + literal takes the other exits' type and what `if` refuses is refused; no + value gives `()`. - it reads only the function's own body, never a call site. - a self-recursive or mutually recursive function must write its return type. Refuse by name, naming the whole cycle. The corpus has 17 self-recursive @@ -361,11 +363,9 @@ Each step lands on its own, with `dune test --root .` green. stale-caller cause. This is independent of steps 1-5 once the marker exists. **Built** (`Check.infer_returns`). `_` is refused outside a `defn`'s return slot, in a generic's, and in `defgeneric`/`defmulti`'s (`defmethod` has no - return slot). Two ways out of one body whose types differ and cannot both - box (a value and `()`, a number and a struct) are refused rather than made - `dyn`. Exits of different types are first tried at each other's type, so a - literal `return 0` beside an `i64` gives `i64`. A self- or mutually - recursive group whose every exit gives `()` is `()`. A stale + return slot). An exit with no value beside one with a value is refused. A + self- or mutually recursive group whose every exit gives `()` is `()`. A + stale body with `_` keeps the signature it was compiled with. Out of scope: dropping macros, built-in replacements for `with-*`/`defedn`, diff --git a/test/syntax/infer/main.flan b/test/syntax/infer/main.flan index b197b9ad..02e896d7 100644 --- a/test/syntax/infer/main.flan +++ b/test/syntax/infer/main.flan @@ -1,6 +1,6 @@ ;; Return types read off the body: _ in the return slot here, no arrow in ;; main.fln. Each shape the rule has: one type, a call's type, a literal -;; that takes the other exit's type, two types (dyn), nothing (()), a return +;; that takes the other exit's type, a dyn beside a literal, nothing (()), a return ;; that never falls off the end, and a function that calls itself and gives ;; nothing. @@ -14,8 +14,8 @@ (when c (return 1)) 2.5) -(defn label [c bool] _ - (when c (return "yes")) +(defn label [c bool d dyn] _ + (when c (return d)) 0) (defn say [x i32] _ (println x)) @@ -33,7 +33,7 @@ (println (quarter 10.0)) (println (+ (pick true) 0.5)) (println (pick false)) - (println (label true) (label false)) + (println (label true "yes") (label false "yes")) (say 4) (println (floor0 -3) (floor0 5)) (countdown 2) diff --git a/test/syntax/infer/main.fln b/test/syntax/infer/main.fln index 8ade8d50..bdcfe51c 100644 --- a/test/syntax/infer/main.fln +++ b/test/syntax/infer/main.fln @@ -1,6 +1,6 @@ ;; Return types read off the body: no arrow here, _ in the return slot in ;; main.flan. Each shape the rule has: one type, a call's type, a literal -;; that takes the other exit's type, two types (dyn), nothing (()), a return +;; that takes the other exit's type, a dyn beside a literal, nothing (()), a return ;; that never falls off the end, and a function that calls itself and gives ;; nothing. @@ -15,9 +15,9 @@ fn pick(c: bool) return 1 2.5 -fn label(c: bool) +fn label(c: bool, d) if c - return "yes" + return d 0 fn say(x: i32) = println(x) @@ -35,7 +35,7 @@ fn main() -> i32 println(quarter(10.0)) println(pick(true) + 0.5) println(pick(false)) - println(label(true), label(false)) + println(label(true, "yes"), label(false, "yes")) say(4) println(floor0(-3), floor0(5)) countdown(2) diff --git a/test/test_flan.ml b/test/test_flan.ml index b3c2a9e3..ea94d0d5 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -7326,8 +7326,12 @@ let () = ("(defn f [x i64] _ (when (< x 0) (return 0)) x)" ^ main) "f" "f [i64] i64"; reads_as "a literal return takes an f32" ("(defn f [c bool x f32] _ (when c (return 1)) x)" ^ main) "f" "f [bool f32] f32"; - reads_as "two types give dyn" - ("(defn f [c bool] _ (when c (return \"s\")) 2)" ^ main) "f" "f [bool] dyn"; + reads_as "a dyn exit beside a literal gives dyn" + ("(defn f [d dyn c bool] _ (when c (return d)) 1)" ^ main) "f" "f [dyn bool] dyn"; + reads_as "a literal before the typed exit still takes its type" + ("(defn f [x i16] _ (when (< x 0) (return x)) 0)" ^ main) "f" "f [i16] i16"; + 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 ()" ("(defn f [n i32] _ (when (> n 0) (println n) (f (- n 1))))" ^ main) "f" "f [i32] ()"; reads_as "two that call each other and give nothing are ()" @@ -7364,10 +7368,6 @@ let () = rejects_check "no value on one path and a value on another" ~needle:"f gives no value here and i32 on another path" "(defn f [x i32] _ (when (> x 0) (return 1)) (println 2))\n(defn main [] ())"; - rejects_check "a struct on one path and a number on another" - ~needle:"f gives P here and i32 on another path" - "(defstruct P [x i32])\n\ - (defn f [c bool] _ (when c (return (P {.x 1}))) 2)\n(defn main [] ())"; (* Every error in the file is still reported, a [_] body's included, and a call to a [_] function whose body failed adds none of its own. *) (let count src = @@ -7392,7 +7392,30 @@ let () = errors "a call to a failed _ body adds nothing" "(defn bad1 [x i32] _ (+ x \"s\"))\n(defn g [x i32] _ (bad1 x))\n\ (defn h [x i32] i32 (+ 1 (g x)))\n\ - (defn main [] i32 (println (bad1 1)) 0)" 1); + (defn main [] i32 (println (bad1 1)) 0)" 1; + errors "a refused loop does not hide the others" + "(defn a [n i32] _ (if (> n 0) (b (- n 1)) 5))\n(defn b [n i32] _ (a n))\n\ + (defn z [n i32] i32 (+ n \"q\"))\n(defn main [] i32 (a 3) 0)" 2; + errors "a refused exit does not hide the others" + "(defn u [c bool] _ (when c (return)) 1)\n\ + (defn z [n i32] i32 (+ n \"q\"))\n(defn main [] i32 (u true) 0)" 2); + (* Exits meet as an if's arms do, and are refused where those are. *) + rejects_check "a struct exit and a literal exit" + ~needle:"expected Pt, found the integer literal 1" + "(defstruct Pt [x i32 y i32])\n\ + (defn m [c bool] _ (when c (return (Pt {.x 1 .y 2}))) 1)\n(defn main [] ())"; + rejects_check "no value on one exit and a value on the other" + ~needle:"u gives no value here and i32 on another path" + "(defn u [c bool] _ (when c (return)) 1)\n(defn main [] ())"; + rejects_check "an i32 exit and an i64 exit, as if refuses them" + ~needle:"expected i32, found i64" + "(defn f [x i32 y i64 c bool] _ (when c (return x)) y)\n(defn main [] ())"; + rejects_check "a literal that does not fit the typed exit" + ~needle:"300 does not fit in u8" + "(defn f [c bool] _ (when c (return 300)) (u8 2))\n(defn main [] ())"; + rejects_check "a string exit and a number exit" + ~needle:"expected string, found the integer literal 1" + "(defn f [c bool] _ (when c (return \"s\")) 1)\n(defn main [] ())"; 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 [] ())"; From f76d0d6e9fbeb9d89487ba99774793faeefc6572 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Fri, 25 Sep 2026 21:02:26 +0700 Subject: [PATCH 4/9] An if's arms and a _ function's exits meet at one join in any order, a return inside the last form counts where it is written, and a constant computed by a _ function is refused as with a written type --- TODO.org | 5 ++ lib/check.ml | 164 +++++++++++++++++++++++++++++++++++----------- spec-syntax.md | 7 +- test/test_flan.ml | 39 ++++++++++- 4 files changed, 169 insertions(+), 46 deletions(-) diff --git a/TODO.org b/TODO.org index b2cfc7d6..1cec2704 100644 --- a/TODO.org +++ b/TODO.org @@ -43,6 +43,11 @@ 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 +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. + ** DONE def, defonce and defconst are the three forms CLOSED: [2026-09-20] =def= is Common Lisp's =defparameter= and re-initialises on every run; =defonce= diff --git a/lib/check.ml b/lib/check.ml index e633bc81..b1ef029f 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -4161,6 +4161,24 @@ let hash_ty = Types.Int Types.U64 address, so no type written anywhere is ever mistaken for it. What each [return] in that body gives is pushed on [infer_seen]. *) let infer_ret = Types.Named "_" + +(* The type two arms meet at — an [if]'s two, or two exits of a [_] body — + the same whichever comes first: the wider where one widens into the other + without loss ([Types.join]), the read-only where they differ only in const, + and dyn where either is dyn, the other boxed. [None] is a refusal. *) +let arm_join (a : Types.t) (b : Types.t) = + if Types.equal a Types.Never then Some b + else if Types.equal b Types.Never then Some a + else + match Types.join a b with + | Some j -> Some j + | None -> + match Types.const_join a b with + | Some j -> Some j + | None -> + (match a, b with + | Types.Dyn, _ | _, Types.Dyn -> Some Types.Dyn + | _ -> None) let infer_seen : (Types.t * Loc.t * bool) list ref = ref [] (* What a refused subexpression stands as while recovering. [Zero] of [Never] is a value nothing else builds, so it is recognisable; see [check]. *) @@ -7009,6 +7027,34 @@ and check_if_once ctx ~tail ?want loc c t e = bool as before, for that path's messages. A chain whose arms all fit is checked once; a refused one re-checks each level below the refusal once more, the square of its depth. *) + (* The else arm on its own terms, when nothing is wanted: the two arms + meet at [arm_join], so the order they are written in decides nothing. + Kept when it has the then arm's type, or when the then arm is the one + that moves; when the else arm moves it is checked again below at the + then arm's type, so its literals are typed there as before. *) + let joined = + if want <> None || free_join || t.Tast.ty = Types.Never + || 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 + match + trial ctx (fun () -> + let v = branch ctx (fun () -> in_tail (fun () -> check ctx e)) 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"))) + with + | Ok v -> Some (v.Tast.ty, v) + | Error _ -> ctx.env.lifted <- lifted; None + in + match joined with + | Some (j, v) -> + let t = expect ctx t.Tast.loc ~want:(Some j) t in + mk loc j (Tast.If (c, t, v)) + | None -> let own_else = if want = None && t.Tast.ty = Types.Bool then match @@ -13628,6 +13674,32 @@ let check_parents env = | None -> ()) env.parents +(* Untyped constants to a fixpoint, and for the same reason: one untyped + constant may be defined in terms of another declared after it. A constant + that still does not check once no progress is left has a real error, so + the last round is run without swallowing it. *) +let settle_consts env consts = + let infer (_, v) = (check (invented_ctx env Types.Unit) v).Tast.ty in + let pending = ref consts in + let rec settle () = + let left = + List.filter + (fun ((n, _) as c) -> + match speculate env (fun () -> infer c) with + | ty -> Hashtbl.replace env.globals n (ty, true); false + | exception Loc.Error _ -> true) + !pending + in + let progressed = List.length left < List.length !pending in + pending := left; + if progressed && left <> [] then settle () + in + settle (); + List.iter (fun c -> ignore (infer c)) !pending + +(* Set by [collect], read by [build_program] once [infer_returns] ran. *) +let consts_after_infer : (string * Ast.expr) list ref = ref [] + let collect env (decls : Ast.decl list) = (* One pass over every declaration kind before any of the others, because the tables below are per-kind — structs, data types, aliases, enums, functions @@ -14155,27 +14227,27 @@ let collect env (decls : Ast.decl list) = "internal: a method of %s reached the checker unexpanded — \ Classes.expand did not run over this declaration list" m.Ast.mgen) decls; - (* Also to a fixpoint, and for the same reason: one untyped constant may be - defined in terms of another declared after it. A constant that still does - not check once no progress is left has a real error, so the last round is - run without swallowing it. *) - let infer (_, v) = (check (invented_ctx env Types.Unit) v).Tast.ty in - let pending = ref (List.rev !untyped) in - let rec settle () = - let left = - List.filter - (fun ((n, _) as c) -> - match speculate env (fun () -> infer c) with - | ty -> Hashtbl.replace env.globals n (ty, true); false - | exception Loc.Error _ -> true) - !pending - in - let progressed = List.length left < List.length !pending in - pending := left; - if progressed && left <> [] then settle () + (* The untyped constants ([settle_consts]). One that calls a [_] function + waits for [infer_returns], which needs every signature this pass + registers; it is settled after that, and its refusal is the one a + written return type would get. *) + let inferred_names = + List.filter_map + (fun (d : Ast.decl) -> + match d.Ast.d with + | Ast.Defn { Ast.name; ret = Some { Ast.t = Ast.Tinfer; _ }; _ } -> + Some name + | _ -> None) + decls in - settle (); - List.iter (fun c -> ignore (infer c)) !pending; + let waits (_, v) = + let acc = ref [] in + Load.expr_uses acc v; + List.exists (fun (n, _) -> List.mem n inferred_names) !acc + in + let late, now = List.partition waits (List.rev !untyped) in + consts_after_infer := late; + settle_consts env now; check_parents env; (* The paired declarations, handed back so that pass two checks the bodies of the same functions whose signatures this pass registered. Pairing needs the @@ -14539,14 +14611,13 @@ and check_generic env (fn : Ast.fn) = is the cycle of one. *) (* The type one body gives, and the form that decided it. The exits — the - last form and every [return], less what never arrives — combine the way - an [if]'s arms do ([check_if_once]): the first one that is not a lone - literal decides and the literals take its type, a bool meets a dyn at - dyn, and literals alone meet at the wider of their own types. The body is - then checked against that type exactly as a written one would be, so - whatever [if] refuses between its 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. *) + last form and every [return], less what never arrives — meet at + [arm_join], the function an [if]'s arms meet at, in any order: the typed + ones decide and the lone literals take their type; literals alone meet at + the wider of their own types. The body is then checked against that type + exactly as a written one would be, so whatever [if] refuses between its + 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. *) @@ -14610,20 +14681,30 @@ and read_return env (fn : Ast.fn) params = when not (List.exists (fun (u, _, _) -> not (Types.equal t u)) rest) -> (t, l) | (t0, l0, _) :: _ -> - let decided = - match List.filter (fun (_, _, lit) -> not lit) arrive with - | (Types.Bool, l, _) :: others - when List.exists (fun (u, _, _) -> Types.equal u Types.Dyn) others -> - (Types.Dyn, l) - | (t, l, _) :: _ -> (t, l) - | [] -> - let joined = + (* Where no join exists the first typed exit's type is the one checked + against, so the refusal is the one [if] gives its else arm. *) + let meet = function + | [] -> None + | ((t, l, _) :: _) as xs -> + let j = List.fold_left - (fun acc (u, _, _) -> - match acc with Some a -> Types.join a u | None -> None) - (Some t0) arrive + (fun acc (u, _, _) -> Option.bind acc (fun a -> arm_join a u)) + (Some t) xs in - (Option.value joined ~default:t0, l0) + let at = + match j with + | Some j -> + (match List.find_opt (fun (u, _, _) -> Types.equal u j) xs with + | Some (_, l', _) -> l' + | None -> l) + | None -> l + in + Some (Option.value j ~default:t, at) + in + let decided = + match meet (List.filter (fun (_, _, lit) -> not lit) arrive) with + | Some d -> d + | None -> Option.value (meet arrive) ~default:(t0, l0) in ignore (attempt (fst decided)); decided @@ -15992,6 +16073,9 @@ let build_program ~keep_going ?tolerate ?previous (decls : Ast.decl list) : check_finite env; check_union_members env; infer_returns ~keep_going ?tolerate ?previous env decls; + (let late = !consts_after_infer in + consts_after_infer := []; + settle_consts env late); let s = Loc.sink ~on:keep_going in (match env.deferred with | Some ds -> s.Loc.found <- ds; env.deferred <- None diff --git a/spec-syntax.md b/spec-syntax.md index 050bdfd8..77c9ef40 100644 --- a/spec-syntax.md +++ b/spec-syntax.md @@ -55,9 +55,10 @@ 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`) combine exactly as an `if`'s arms do, so a - literal takes the other exits' type and what `if` refuses is refused; no - value gives `()`. + last form and each `return`) meet exactly as an `if`'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 `()`. - it reads only the function's own body, never a call site. - a self-recursive or mutually recursive function must write its return type. Refuse by name, naming the whole cycle. The corpus has 17 self-recursive diff --git a/test/test_flan.ml b/test/test_flan.ml index 9527f95d..502a2e35 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -7531,6 +7531,30 @@ let () = ("(defn f [d dyn c bool] _ (when c (return d)) 1)" ^ main) "f" "f [dyn bool] dyn"; reads_as "a literal before the typed exit still takes its type" ("(defn f [x i16] _ (when (< x 0) (return x)) 0)" ^ main) "f" "f [i16] i16"; + (* Arms and exits meet at one join, whichever comes first. *) + List.iter + (fun (what, sg, body, want) -> + reads_as what ("(defn f " ^ sg ^ " _ " ^ body ^ ")" ^ main) "f" want) + [ ("if i32 then i64", "[c bool x i32 y i64]", "(if c x y)", "f [bool i32 i64] i64"); + ("if i64 then i32", "[c bool x i32 y i64]", "(if c y x)", "f [bool i32 i64] i64"); + ("if f32 then f64", "[c bool x f32 y f64]", "(if c x y)", "f [bool f32 f64] f64"); + ("if u8 then i32", "[c bool x u8 y i32]", "(if c x y)", "f [bool u8 i32] i32"); + ("if dyn then i8", "[c bool x i8 d dyn]", "(if c d x)", "f [bool i8 dyn] dyn"); + ("if i8 then dyn", "[c bool x i8 d dyn]", "(if c x d)", "f [bool i8 dyn] dyn"); + ("if i64 then dyn", "[c bool x i64 d dyn]", "(if c x d)", "f [bool i64 dyn] dyn"); + ("if i8 then a literal", "[c bool x i8]", "(if c x 1)", "f [bool i8] i8"); + ("exits i32 then i64", "[c bool x i32 y i64]", "(when c (return x)) y", "f [bool i32 i64] i64"); + ("exits i64 then i32", "[c bool x i32 y i64]", "(when c (return y)) x", "f [bool i32 i64] i64"); + ("a return inside the last form, in source order", "[c bool x i64 y i32]", + "(if c x (return y))", "f [bool i64 i32] i64"); + ("exits writable then read-only slice", "[c bool a [u8] b [const u8]]", + "(when c (return a)) b", "f [bool [u8] [const u8]] [const u8]"); + ("exits read-only then writable slice", "[c bool a [u8] b [const u8]]", + "(when c (return b)) a", "f [bool [u8] [const u8]] [const u8]"); + ("exits writable then read-only pointer", "[c bool a (Ptr i32) b (Ptr const i32)]", + "(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") ]; 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 ()" @@ -7608,15 +7632,24 @@ let () = rejects_check "no value on one exit and a value on the other" ~needle:"u gives no value here and i32 on another path" "(defn u [c bool] _ (when c (return)) 1)\n(defn main [] ())"; - rejects_check "an i32 exit and an i64 exit, as if refuses them" - ~needle:"expected i32, found i64" - "(defn f [x i32 y i64 c bool] _ (when c (return x)) y)\n(defn main [] ())"; + rejects_check "an i32 exit and a u32 exit, which neither widens into" + ~needle:"expected i32, found u32" + "(defn f [x i32 y u32 c bool] _ (when c (return x)) y)\n(defn main [] ())"; + rejects_check "a u32 exit and an i32 exit, the other order" + ~needle:"expected u32, found i32" + "(defn f [x i32 y u32 c bool] _ (when c (return y)) x)\n(defn main [] ())"; + rejects_check "an if over i32 and u32, either order" + ~needle:"expected i32, found u32" + "(defn f [x i32 y u32 c bool] i32 (let [v (if c x y)] 0))\n(defn main [] ())"; rejects_check "a literal that does not fit the typed exit" ~needle:"300 does not fit in u8" "(defn f [c bool] _ (when c (return 300)) (u8 2))\n(defn main [] ())"; rejects_check "a string exit and a number exit" ~needle:"expected string, found the integer literal 1" "(defn f [c bool] _ (when c (return \"s\")) 1)\n(defn main [] ())"; + 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)"; 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 [] ())"; From ed7258c80f9e5cf41e06dc735d1b5449f554a894 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Fri, 25 Sep 2026 21:26:56 +0700 Subject: [PATCH 5/9] 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 [] ())"; From ff0679cbb15f8e616afd438aebeeefefe49c14de Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Fri, 25 Sep 2026 22:14:06 +0700 Subject: [PATCH 6/9] An if's else arm is checked once and brought to the join, an abandoned check undoes only what it wrote, and an arm refused at the join says why at its value --- lib/check.ml | 234 ++++++++++++++++++++++++++++------------------ test/test_flan.ml | 63 +++++++++++++ 2 files changed, 206 insertions(+), 91 deletions(-) diff --git a/lib/check.ml b/lib/check.ml index bbc78dd1..0defb97b 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -34,6 +34,12 @@ let fail = Loc.fail language from the one the author decided on. *) let literal_at_want = "check/literal-at-want" +(* A refusal that is two types failing to meet, a literal's included: what + an arm checked at another arm's type says when the two simply differ. *) +let is_mismatch (d : Loc.diag) = + String.equal d.Loc.kind "check/type-mismatch" + || String.equal d.Loc.kind literal_at_want + (* [List.map]'s evaluation order is unspecified, and checking allocates frame slots as a side effect. Left-to-right is required, not a preference: a later let binding sees an earlier one, and slot numbering must be reproducible. *) @@ -121,6 +127,35 @@ type gstruct = { program asks for the copy itself. *) let struct_apps : (string, string * Types.t list) Hashtbl.t = Hashtbl.create 16 +(* The undo journal a check that may be abandoned writes into: every table + write a body's check makes goes through [jreplace]/[jremove]/[jset], which + note how to take it back while a [snapshot_env] is open. So abandoning a + check costs what it wrote, not the size of the tables it could have. *) +let journal : (unit -> unit) list ref = ref [] +let journal_open = ref 0 + +let jot undo = if !journal_open > 0 then journal := undo :: !journal + +let jreplace tbl k v = + (if !journal_open > 0 then + let old = Hashtbl.find_opt tbl k in + jot (fun () -> + match old with + | Some o -> Hashtbl.replace tbl k o + | None -> Hashtbl.remove tbl k)); + Hashtbl.replace tbl k v + +let jremove tbl k = + (if !journal_open > 0 then + match Hashtbl.find_opt tbl k with + | Some o -> jot (fun () -> Hashtbl.replace tbl k o) + | None -> ()); + Hashtbl.remove tbl k + +let jset r v = + (if !journal_open > 0 then let old = !r in jot (fun () -> r := old)); + r := v + (* The length every length variable has inside a generic body's abstract pass. Large so that no constant index into such an array is refused as out of bounds there, and within i32 so that [(length a)] is an ordinary index. @@ -364,25 +399,25 @@ 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 +(* A check that may be abandoned — a trial, a probe, a return type read and + thrown away, a tolerated body — opens one of these: [undo] puts back + everything it wrote into [env], [keep] closes it and leaves the writes, + which an enclosing one can still undo. 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 *); + The tables a body's check writes go through the journal ([jreplace]); + the lists and flags are held here, which costs nothing; the rest is + written by the declaration passes alone, before any body is checked. *) +let snapshot_env env : (unit -> unit) * (unit -> unit) = + let[@warning "+9"] { lifted; instances; tyvars; subst; tvpreds; chain; + deferred; lenvars; len_placeholder; schain; in_field; + recovering; recovered; poison; speculating; + guard_next; + (* Journaled at their writes. *) + structs = _; locs = _; copies = _; insts = _; fns = _; (* Declaration passes only. *) datas = _; unions = _; cases = _; aliases = _; consts = _; enums = _; parents = _; externs = _; @@ -391,29 +426,22 @@ let snapshot_env env : unit -> unit = 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 + incr journal_open; + let mark = !journal in + let close () = + decr journal_open; + if !journal_open = 0 then journal := [] 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; + let undo () = + let rec back l = + if l != mark then + match l with + | u :: rest -> u (); back rest + | [] -> () + in + back !journal; + journal := mark; + close (); env.lifted <- lifted; env.instances <- instances; env.tyvars <- tyvars; env.subst <- subst; env.tvpreds <- tvpreds; env.chain <- chain; env.deferred <- deferred; env.lenvars <- lenvars; @@ -421,6 +449,8 @@ let snapshot_env env : unit -> unit = env.in_field <- in_field; env.recovering <- recovering; env.recovered <- recovered; env.poison <- poison; env.speculating <- speculating; env.guard_next <- guard_next + in + (undo, close) (* A refusal [collect] can go on past: kept while a whole-file check is collecting, in the order found, and raised otherwise. *) @@ -1469,7 +1499,7 @@ let struct_app g args = args) in if not (Hashtbl.mem struct_apps key) then begin - Hashtbl.replace struct_apps key (g, args); + jreplace struct_apps key (g, args); Hashtbl.replace Types.display key (Printf.sprintf "(%s %s)" g (String.concat " " (List.map Types.to_string args))) @@ -1710,8 +1740,8 @@ and struct_copy ?(at_definition = false) env loc name targs = let key = struct_app name targs in if Hashtbl.mem env.copies key then key else if Hashtbl.mem env.broken name then begin - Hashtbl.replace env.copies key (List.exists generic_arg targs); - Hashtbl.replace env.structs key { Tast.sname = key; fields = [] }; + jreplace env.copies key (List.exists generic_arg targs); + jreplace env.structs key { Tast.sname = key; fields = [] }; key end else begin @@ -1745,9 +1775,9 @@ and struct_copy ?(at_definition = false) env loc name targs = let generic = List.exists generic_arg targs in (* In before its fields, so a field that names the same copy through a pointer — [(defstruct Node [next (Ptr (Node $t))])] — finds it. *) - Hashtbl.replace env.copies key generic; - Hashtbl.replace env.structs key { Tast.sname = key; fields = [] }; - Hashtbl.replace env.locs key g.gloc; + jreplace env.copies key generic; + jreplace env.structs key { Tast.sname = key; fields = [] }; + jreplace env.locs key g.gloc; let saved = (env.subst, env.tyvars, env.lenvars, env.tvpreds, env.len_placeholder, env.in_field, env.schain) @@ -1775,13 +1805,13 @@ and struct_copy ?(at_definition = false) env loc name targs = with | fields -> restore (); - Hashtbl.replace env.structs key { Tast.sname = key; fields }; + jreplace env.structs key { Tast.sname = key; fields }; finite_from env key; key | exception e -> restore (); - Hashtbl.remove env.copies key; - Hashtbl.remove env.structs key; + jremove env.copies key; + jremove env.structs key; (* A field refused inside the template says nothing about which use asked for this copy; the note names it, one per level of copies. *) (match e with @@ -3011,7 +3041,7 @@ let close_over ~fname (octx : ctx) (fctx : ctx) loc = (fun (n, ((b : binding), _)) -> { Tast.fname = n; fty = b.bty }) caught in - Hashtbl.replace fctx.env.structs ename { Tast.sname = ename; fields }; + jreplace fctx.env.structs ename { Tast.sname = ename; fields }; let ety = Types.Named ename in let eslot = fresh_slot fctx (Types.Ptr (Types.Mut, ety)) in let binds = @@ -7367,47 +7397,42 @@ and check_if_once ctx ~tail ?want loc c t e = is checked once; a refused one re-checks each level below the refusal once more, the square of its depth. *) (* The else arm on its own terms, when nothing is wanted: the two arms - meet at [arm_join], so the order they are written in decides nothing. - Kept when it has the then arm's type, or when the then arm is the one - that moves; when the else arm moves it is checked again below at the - then arm's type, so its literals are typed there as before. *) + meet at [arm_join], so the order they are written in decides nothing, + and both are brought to the join as checked — the arm is never checked + twice, which in a chain of ifs would be twice per level. *) let joined = if want <> None || free_join || t.Tast.ty = Types.Never || t.Tast.ty = Types.Bool || and_sentinel e || lone_literal e then None else - (* 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 = 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 ~kind:not_kept v.Tast.loc ""))) - with - | Ok v -> Some (v.Tast.ty, v) - | 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 alone with + | Ok v -> + (match arm_join t.Tast.ty v.Tast.ty with + | Some j -> Some (j, expect ctx v.Tast.loc ~want:(Some j) v) + (* No join: the refusal [if] gives its else arm. *) + | None -> + Some (t.Tast.ty, expect ctx v.Tast.loc ~want:(Some t.Tast.ty) v)) + | Error own -> + (* Refused on its own terms. The then arm's type may be what it + needed — [nil], a bare struct — and it is checked at it below, + whose refusal is then the one said. Only when that refusal is a + mismatch and the arm's own is not — an unknown name, say — is + the arm's own error the real one, so 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 _ -> + | Error d + when is_mismatch d && not (is_mismatch own) -> 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))) + Some (t.Tast.ty, expect ctx v.Tast.loc ~want:(Some t.Tast.ty) v)) + | _ -> None) in match joined with | Some (j, v) -> @@ -8878,12 +8903,16 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms = 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. *) + | Error own -> + (* Refused on its own terms: the join may be what it + needed, and its refusal at the join is then the one + said — unless that refusal is a mismatch and the arm's + own is not, when the arm's own error is the real one. *) (match trial ctx (at !want) with - | Ok _ -> at !want () - | Error _ -> at None ()) + | Error d + when is_mismatch d && not (is_mismatch own) -> + at None () + | _ -> at !want ()) else block ctx ?want:!want a.Ast.aloc a.Ast.body in (if body.Tast.ty <> Types.Never then @@ -8900,11 +8929,32 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms = let checked = match free, !want with | true, Some j -> + (* Said at the arm's value, its last form, as a refusal checked at the + join would have been — not at its pattern. *) + let rec value (x : Ast.expr) = + match x.Ast.e with + | Ast.Do (_ :: _ as xs) | Ast.Let (_, (_ :: _ as xs)) -> + value (List.hd (List.rev xs)) + | _ -> x.Ast.loc + in + let value_loc i = + let (a : Ast.arm), _, _ = List.nth resolved i in + match List.rev a.Ast.body with + | x :: _ -> value x + | [] -> a.Ast.aloc + in + (* Each arm refused on its own, so every arm that cannot meet the join + is said, as each would be checked at it. *) 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 ] }) + let at = value_loc i in + let b = + try expect ctx at ~want:(Some j) b + with Loc.Error d -> refuse_or_poison ctx.env at d + in + (i, { arm with Tast.abody = [ b ] }) | _ -> (i, arm)) checked | _ -> checked @@ -13346,7 +13396,7 @@ and instantiate env loc gname vars subst cparams cret = let cache = match Hashtbl.find_opt env.insts gname with | Some r -> r - | None -> let r = ref [] in Hashtbl.replace env.insts gname r; r + | None -> let r = ref [] in jreplace env.insts gname r; r in let same (ps, r, _) = List.length ps = List.length cparams @@ -13392,8 +13442,8 @@ and instantiate env loc gname vars subst cparams cret = (* The entry goes in *before* the body is checked, which is what makes a recursive generic function terminate: the call to itself at the same types finds this and does not generate a second copy. *) - cache := (cparams, cret, sym) :: !cache; - Hashtbl.replace env.fns sym (cparams, cret); + jset cache ((cparams, cret, sym) :: !cache); + jreplace env.fns sym (cparams, cret); let saved_subst = env.subst and saved_vars = env.tyvars and saved_preds = env.tvpreds and saved_chain = env.chain in (* Inside the copy there are no variables left: [resolve_name] answers @@ -13481,8 +13531,8 @@ and instantiate env loc gname vars subst cparams cret = (* A copy whose body did not check is not a copy. Both entries go back out, so a second call at the same types is the same refusal again rather than a cache hit on a function that does not exist. *) - cache := List.filter (fun (_, _, s) -> s <> sym) !cache; - Hashtbl.remove env.fns sym; + jset cache (List.filter (fun (_, _, s) -> s <> sym) !cache); + jremove env.fns sym; raise e in env.instances <- tfn :: env.instances; @@ -13583,9 +13633,9 @@ 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 + let undo, keep = snapshot_env ctx.env in match speculate ctx.env f with - | r -> Ok r + | r -> keep (); Ok r | exception Loc.Error d -> undo (); ctx.slots <- slots; ctx.slot_tys <- slot_tys; @@ -13596,6 +13646,7 @@ and trial ctx f = ctx.caught <- caught; ctx.place_ok <- place_ok; ctx.envslot <- envslot; ctx.loops <- loops; ctx.tail <- tail; ctx.in_defer <- in_defer; Error d + | exception e -> keep (); raise e (* Whether the trial's refusal is one worth reconsidering. A literal that did not fit is not, and neither is a refusal a program cannot make any use of @@ -15147,9 +15198,9 @@ and check_generic env (fn : Ast.fn) = [env.tvpreds] whether the variable was declared to support it, and every instantiation asks the concrete type the same question again. *) env.tvpreds <- fn.Ast.fwhere; - Hashtbl.replace env.fns fn.Ast.name (params, ret); + jreplace env.fns fn.Ast.name (params, ret); let finish () = - Hashtbl.remove env.fns fn.Ast.name; + jremove env.fns fn.Ast.name; env.lifted <- saved_lifted; env.tyvars <- saved_vars; env.tvpreds <- saved_preds; @@ -15186,7 +15237,7 @@ and read_return env (fn : Ast.fn) params = (* 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 undo = snapshot_env env in + let undo, _ = snapshot_env env in let seen = !infer_seen in infer_seen := []; let restore () = undo (); infer_seen := seen in @@ -16538,16 +16589,17 @@ let build_program ~keep_going ?tolerate ?previous (decls : Ast.decl list) : ([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 + let undo, keep = snapshot_env env in (match f () with - | x -> x + | x -> keep (); x | exception ((Loc.Error d | Loc.Errors (d :: _)) as e) -> if ok env name d then begin undo (); tolerated := name :: !tolerated; None end - else raise e) + else (keep (); raise e) + | exception e -> keep (); raise e) in let decls, prelude_warnings = shadow_prelude (Parse.program (Prelude.forms ())) decls diff --git a/test/test_flan.ml b/test/test_flan.ml index 3bb133a9..9ff4d3de 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -7862,6 +7862,69 @@ let () = incr failures; Printf.printf "FAIL an else arm's own error alone: %d errors\n" n end); + (* An arm that needs the other's type, and is refused at it too, says why + at that type — not that it has no type on its own. *) + rejects_check "a bare struct else arm with an unknown name in it" + ~needle:"unknown name q2" + "(defstruct P [x i32 y i32])\n\ + (defn b3 [c bool p P] i32 (let [v (if c p {.x q2 .y 2})] (.y v)))\n\ + (defn main [] i32 0)"; + rejects_check "a bare struct match arm with an unknown name in it" + ~needle:"unknown name q2" + "(defstruct P [x i32 y i32])\n\ + (defn a3 [o (Option i32) p P] i32 \ + (let [v (match o (Some q) p None {.x q2 .y 2})] (.y v)))\n\ + (defn main [] i32 0)"; + (* A match arm that does not meet the others is refused at its value. *) + (match + checked + "(defn m4 [o (Option i32) x i8] i32 \ + (let [v (match o (Some q) x None (do (println \"a\") \"lit\"))] 0))\n\ + (defn main [] i32 0)" + with + | _ -> check "a match arm of another type is refused" false + | exception Loc.Error { Loc.dloc; dmsg; _ } -> + check "a match arm of another type is refused at its value" + (dloc.Loc.col = 87 && contains dmsg "expected i8, found string")); + (* Nested arms that meet at a wider type are checked once each, not once + per level above them. *) + (let nest kind depth = + let rec go k e = + if k = 0 then e + else + go (k - 1) + (match kind with + | `If -> Printf.sprintf "(if c a (+ (idg b) (i32 %s)))" e + | `Match -> + Printf.sprintf "(match o (Some q) a None (+ (idg b) (i32 %s)))" e) + in + go depth "(i32 b)" + in + let structs = + String.concat "" + (List.init 300 (Printf.sprintf "(defstruct S%d [a i32 b i64])\n")) + in + List.iter + (fun (kind, sg, what) -> + let src = + "(defn idg [x $t] $t x)\n" ^ structs + ^ "(defn f " ^ sg ^ " i64 (let [v " ^ nest kind 20 ^ "] v))\n\ + (defn g " ^ sg ^ " _ " ^ nest kind 20 ^ ")" + in + let t0 = Unix.gettimeofday () in + match checked src with + | p -> + check (what ^ " twenty deep checks fast") + (Unix.gettimeofday () -. t0 < 3.0); + check (what ^ " twenty deep meets at i64") + (List.exists + (fun (f : Tast.fn) -> + f.Tast.name = "g" && Types.equal f.Tast.ret (Types.Int Types.I64)) + p.Tast.fns) + | exception Loc.Error { Loc.dmsg; _ } -> + check (what ^ " twenty deep checks: " ^ dmsg) false) + [ (`If, "[c bool a i64 b i32]", "an if"); + (`Match, "[o (Option i32) a i64 b i32]", "a match") ]); 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\ From 3e504deb6f36da73a64a0fa32014d44f860fe163 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Fri, 25 Sep 2026 23:10:16 +0700 Subject: [PATCH 7/9] An arm is checked at the other arm's type first and meets it at the join only when refused there, so every program master accepts keeps its type and value while arms still meet in either order --- TODO.org | 5 +- lib/check.ml | 199 ++++++++++++++++++++++++++++-------- spec-syntax.md | 9 +- test/programs/arm-want.flan | 25 +++++ test/test_acceptance.ml | 8 ++ test/test_flan.ml | 48 ++++++++- 6 files changed, 245 insertions(+), 49 deletions(-) create mode 100644 test/programs/arm-want.flan diff --git a/TODO.org b/TODO.org index 32899497..1a23c947 100644 --- a/TODO.org +++ b/TODO.org @@ -64,8 +64,9 @@ use-directed inference. ** 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 first arm deciding the type the others are checked at. +Each arm is asked the other's type first; only a refusal meets at the join +(lossless widening, const, dyn beside a dyn value), the same for =_= exits. +Rules out the first arm's type refusing a wider second arm. ** DONE def, defonce and defconst are the three forms CLOSED: [2026-09-20] diff --git a/lib/check.ml b/lib/check.ml index 47b9586c..fcae594f 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -3000,6 +3000,23 @@ let rec literal_arith (e : Ast.expr) : int64 option = over literals alone. *) let lone_literal (e : Ast.expr) = is_literal e || literal_arith e <> None +(* A value whose type comes only from defaults — a literal, [nil], [(Some 3)], + arithmetic over literals, a [do] ending in one — so it takes the type of whatever + meets it. An arm of this kind is checked after the others, at their type, + and never decides a join. *) +let rec adapts (e : Ast.expr) = + lone_literal e + || (match e.Ast.e with + | Ast.Var "nil" -> true + | Ast.Call ({ Ast.e = Ast.Var "Some"; _ }, [ x ]) -> adapts x + | Ast.Call ({ Ast.e = Ast.Var ("+" | "-" | "*" | "/" | "%"); _ }, + (_ :: _ as xs)) -> + List.for_all adapts xs + | Ast.Do (_ :: _ as xs) | Ast.Let (_, (_ :: _ as xs)) -> + adapts (List.hd (List.rev xs)) + | Ast.If (_, a, Some b) -> adapts a && adapts b + | _ -> false) + (* The environment for a lifted body, built once its own body has been checked and [caught] is therefore final. spec-memory.md's case 2, and the whole of @@ -5324,6 +5341,28 @@ let if_failed : Hashtbl.create 16 let if_depth = ref 0 +(* An arm refused at the other arm's type, keyed the same way: the arm is + then checked on its own terms, and an [if] above it that checks it again + — its own trial, then for real — finds the refusal here rather than + walking the arm to it once more, which in a chain nested in else arms + would be twice per level. Cleared for each program. *) +let arm_failed : + (Loc.t, + Ast.expr * ((string * binding) list * Types.t) * Types.t * Loc.diag) + Hashtbl.t = + Hashtbl.create 16 + +(* A dyn value opened at a typed want: the box, and the want it was opened + at. Two arms that meet this way meet at dyn — the typed one is boxed, not + the dyn one opened — whichever is written first. *) +let not_kept = "check/arm-not-kept" + +let opened_dyn (v : Tast.expr) = + match v.Tast.e with + | Tast.Prim (Tast.Rt ("flan_dyn_need_i64" | "flan_dyn_need_f64"), [ inner ]) + when Types.equal inner.Tast.ty Types.Dyn -> Some inner + | _ -> None + (* A Vec or a Map parameter is a copy of the caller's header — Odin's rule — so growing it reallocates a block only this function's copy points at, and @@ -5724,7 +5763,7 @@ and check_value ctx ?want (e : Ast.expr) : Tast.expr = (match ctx.in_frames with Some n -> n | None -> assert false) | Ast.Return v when ctx.ret == infer_ret -> - let lit = match v with Some x -> lone_literal x | None -> false in + let lit = match v with Some x -> adapts x | None -> false in let v = Option.map (check ctx) v in infer_seen := (match v with @@ -7431,7 +7470,7 @@ and check_if_once ctx ~tail ?want loc c t e = let t = branch ctx (fun () -> in_tail (fun () -> check ctx ?want t)) in let e = branch ctx (fun () -> in_tail (fun () -> check ctx ?want e)) in mk loc t.Tast.ty (Tast.If (c, t, e)) - | Some e when want = None && lone_literal t && not (lone_literal e) + | Some e when want = None && adapts t && not (adapts e) && not (and_sentinel e) -> (* A literal has no type of its own until something asks, so with no expectation the other arm decides: [(if c 4000000 n)] over an i64 [n] @@ -7461,43 +7500,75 @@ and check_if_once ctx ~tail ?want loc c t e = bool as before, for that path's messages. A chain whose arms all fit is checked once; a refused one re-checks each level below the refusal once more, the square of its depth. *) - (* The else arm on its own terms, when nothing is wanted: the two arms - meet at [arm_join], so the order they are written in decides nothing, - and both are brought to the join as checked — the arm is never checked - twice, which in a chain of ifs would be twice per level. *) + (* The else arm at the then arm's type first, as it always was: a value + that takes its type from what is asked of it — [(+ b 1)] beside an + i64, [nil] beside an Option — is asked the then arm's. Only when that + is refused as a mismatch is it checked on its own terms, and the two + meet at [arm_join], so [(if c x32 y64)] is the i64 [(if c y64 x32)] + is. A dyn opened at the then arm's type is not a meeting: the two + meet at dyn, as they do the other way round. The arm is checked once + each way at most, and a refusal at the then arm's type is kept + ([arm_failed]) for the ifs above that check it again. *) let joined = if want <> None || free_join || t.Tast.ty = Types.Never || t.Tast.ty = Types.Bool || and_sentinel e || lone_literal e then None else let alone () = branch ctx (fun () -> in_tail (fun () -> check ctx e)) in - match trial ctx alone with + let key = (ctx.scope, ctx.ret) in + let at_then () = + match + List.find_opt + (fun (n, (sc, r), w, _) -> + n == e && r == ctx.ret && Types.equal w t.Tast.ty + && same_scope sc ctx.scope) + (Hashtbl.find_all arm_failed e.Ast.loc) + with + | Some (_, _, _, d) -> Error d + | None -> + match + trial ctx (fun () -> + branch ctx (fun () -> + in_tail (fun () -> check ctx ~want:t.Tast.ty e))) + with + | Ok v -> Ok v + | Error d -> + Hashtbl.add arm_failed e.Ast.loc (e, key, t.Tast.ty, d); + Error d + in + let meet v = + match arm_join t.Tast.ty v.Tast.ty with + | Some j -> Some (j, expect ctx v.Tast.loc ~want:(Some j) v) + | None -> None + in + match at_then () with | Ok v -> - (match arm_join t.Tast.ty v.Tast.ty with - | Some j -> Some (j, expect ctx v.Tast.loc ~want:(Some j) v) - (* No join: the refusal [if] gives its else arm. *) - | None -> - Some (t.Tast.ty, expect ctx v.Tast.loc ~want:(Some t.Tast.ty) v)) - | Error own -> - (* Refused on its own terms. The then arm's type may be what it - needed — [nil], a bare struct — and it is checked at it below, - whose refusal is then the one said. Only when that refusal is a - mismatch and the arm's own is not — an unknown name, say — is - the arm's own error the real one, so nothing is invented about a - type it was never going to have. *) + (match opened_dyn v with + | Some box -> Some (Types.Dyn, box) + | None -> Some (t.Tast.ty, v)) + | Error _ when adapts e -> None + | Error d -> + (* A mismatch, or a dyn the then arm's type could not open: the + arm on its own terms meets the then arm. Anything else refused + it at the then arm's type, and that refusal is said. *) (match trial ctx (fun () -> - branch ctx (fun () -> - in_tail (fun () -> check ctx ~want:t.Tast.ty e))) + let v = alone () in + if is_mismatch d || Types.equal v.Tast.ty Types.Dyn then v + else raise (Loc.Error (Loc.diag ~kind:not_kept v.Tast.loc ""))) with - | Error d - when is_mismatch d && not (is_mismatch own) -> + | Ok v -> meet v + | Error own when String.equal own.Loc.kind not_kept -> None + (* Refused on its own terms too, and not as a mismatch — an + unknown name, say: that is the real error, and nothing is said + about a type the arm was never going to have. *) + | Error own when is_mismatch d && not (is_mismatch own) -> 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) + (match meet v with + | Some r -> Some r | None -> Some (t.Tast.ty, expect ctx v.Tast.loc ~want:(Some t.Tast.ty) v)) - | _ -> None) + | Error _ -> None) in match joined with | Some (j, v) -> @@ -8928,7 +8999,7 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms = the others, as an [if]'s literal arm does. The order is only the order they are checked in; they are put back in source order below. *) let literal_arm ((a : Ast.arm), _, _) = - match List.rev a.Ast.body with last :: _ -> lone_literal last | [] -> false + match List.rev a.Ast.body with last :: _ -> adapts last | [] -> false in (* Every arm a literal: they meet at the wider of their own types, as an [if]'s two do. *) @@ -9002,19 +9073,47 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms = let arm = (a, ctor, binds) in let body = if free && !want <> None && not (literal_arm arm) then + (* As an [if]'s else arm: at the join so far first, on its + own terms only when that is refused as a mismatch. *) let at w () = block ctx ?want:w a.Ast.aloc a.Ast.body in - match trial ctx (at None) with - | Ok b -> b - | Error own -> - (* Refused on its own terms: the join may be what it - needed, and its refusal at the join is then the one - said — unless that refusal is a mismatch and the arm's - own is not, when the arm's own error is the real one. *) - (match trial ctx (at !want) with - | Error d - when is_mismatch d && not (is_mismatch own) -> + let w = Option.get !want in + let head = List.hd a.Ast.body in + let at_join () = + match + List.find_opt + (fun (n, (sc, r), w', _) -> + n == head && r == ctx.ret && Types.equal w' w + && same_scope sc ctx.scope) + (Hashtbl.find_all arm_failed head.Ast.loc) + with + | Some (_, _, _, d) -> Error d + | None -> + (match trial ctx (at (Some w)) with + | Ok b -> Ok b + | Error d -> + Hashtbl.add arm_failed head.Ast.loc + (head, (ctx.scope, ctx.ret), w, d); + Error d) + in + match at_join () with + | Ok b -> + (match opened_dyn b with + | Some box -> want := Some Types.Dyn; box + | None -> b) + | Error d -> + (match + trial ctx (fun () -> + let b = at None () in + if is_mismatch d || Types.equal b.Tast.ty Types.Dyn then b + else + raise (Loc.Error (Loc.diag ~kind:not_kept b.Tast.loc ""))) + with + | Ok b -> b + | Error own when String.equal own.Loc.kind not_kept -> + at !want () + | Error own when is_mismatch d && not (is_mismatch own) -> at None () - | _ -> at !want ()) + | Error _ -> at !want ()) else block ctx ?want:!want a.Ast.aloc a.Ast.body in (if body.Tast.ty <> Types.Never then @@ -13928,6 +14027,21 @@ and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args = type, so [(+ x 1)] over a dyn x goes on building an i64 one. *) else if dyn_ok && not (needs_want y) then begin let a = check ctx ?want x in + (* y at [a]'s type first, and on its own terms only if that is + refused: checking it both ways every time made a chain of these + nested in their second operands twice as slow per level. A dyn + opened at [a]'s type is seen for what it was. *) + let at_a = + if a.Tast.ty = Types.Dyn then None + else + match trial ctx (fun () -> check ctx ~want:a.Tast.ty y) with + | Ok b' -> Some (Ok b') + | Error d -> Some (Error d) + in + match at_a with + | Some (Ok b') -> + (match opened_dyn b' with Some box -> a, box | None -> a, b') + | _ -> let b = check ctx y in (* Nothing dyn about this pair after all, so it is put back the way the typed path built it. Re-checking only when the types actually differ @@ -13949,7 +14063,11 @@ and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args = that has to move. Nothing is checked a third time — the own-terms [b] already in hand is the answer. *) else - (match trial ctx (fun () -> check ctx ~want:a.Tast.ty y) with + (match + match at_a with + | Some (Error d) -> Error d + | _ -> trial ctx (fun () -> check ctx ~want:a.Tast.ty y) + with | Ok b' -> a, b' | Error d -> (match @@ -15524,7 +15642,7 @@ and read_return env (fn : Ast.fn) params = let last = match List.rev tf.Tast.body, List.rev fn.Ast.fbody with | (x : Tast.expr) :: _, (a : Ast.expr) :: _ -> - [ (x.Tast.ty, x.Tast.loc, lone_literal a) ] + [ (x.Tast.ty, x.Tast.loc, adapts a) ] | (x : Tast.expr) :: _, [] -> [ (x.Tast.ty, x.Tast.loc, false) ] | [], _ -> [] in @@ -16837,6 +16955,7 @@ let shadow_prelude (prelude : Ast.decl list) (decls : Ast.decl list) = let build_program ~keep_going ?tolerate ?previous (decls : Ast.decl list) : Tast.program * env * string list = let env = new_env () in + Hashtbl.reset arm_failed; (* ── A declaration left as it was compiled ─────────────────────────── A dev session installs a function whose signature changed, and a caller compiled against the old one is still in the running program and diff --git a/spec-syntax.md b/spec-syntax.md index ffd35efc..53f4fe3d 100644 --- a/spec-syntax.md +++ b/spec-syntax.md @@ -55,10 +55,11 @@ 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 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 `()`. + last form and each `return`) meet exactly as an `if`'s or `match`'s arms do, + in any order: each is asked the others' type first, so a literal, `nil` or + arithmetic takes it; only arms that are refused that way meet at the join + (lossless widening, the read-only side of a const difference, `dyn` beside + a genuinely dyn value); what `if` refuses is refused; no value gives `()`. - it reads only the function's own body, never a call site. - a self-recursive or mutually recursive function must write its return type. Refuse by name, naming the whole cycle. The corpus has 17 self-recursive diff --git a/test/programs/arm-want.flan b/test/programs/arm-want.flan new file mode 100644 index 00000000..58cf9dce --- /dev/null +++ b/test/programs/arm-want.flan @@ -0,0 +1,25 @@ +;;;; An arm is checked at the other arm's type first: arithmetic in a +;;;; narrower arm is done at the wider type, not done narrow and widened, and +;;;; nil beside an Option is None, whichever arm comes first. + +(defn wd [c bool a i64 b i32] i64 (let [v (if c a (+ b 1))] v)) +(defn wd2 [c bool a i64 b i32] i64 (if c a (+ b 1))) +(defn wd4 [c bool a i64 b i32] i64 (let [v (if c a (* b b))] v)) +(defn wd5 [o (Option i32) a i64 b i32] i64 (let [v (match o (Some q) a None (+ b 1))] v)) +(defn wd6 [c bool a f64 b i32] f64 (let [v (if c a (/ b 2))] v)) +(defn wd7 [c bool a i64 b i32] _ (when c (return a)) (+ b 1)) + +(defn n1 [c bool p (Option i64)] i64 (let [v (if c nil p)] (match v (Some q) q None -1))) +(defn n2 [o (Option i32) p (Option i64)] i64 + (let [v (match o None nil (Some z) p)] (match v (Some q) q None -1))) + +(defn main [] i32 + (println (wd false 0 2147483647)) + (println (wd2 false 0 2147483647)) + (println (wd4 false 0 100000)) + (println (wd5 None 0 2147483647)) + (println (wd6 false 0.0 3)) + (println (wd7 false 0 2147483647)) + (println (n1 false (Some 5)) (n1 true (Some 5))) + (println (n2 (Some 1) (Some 5)) (n2 None (Some 5))) + 0) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index 72cb2fe5..cb0e7202 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -590,6 +590,14 @@ 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; + (* An arm is checked at the other arm's type first. *) + let aw_out = + "2147483648\n2147483648\n10000000000\n2147483648\n1.5\n2147483648\n\ + 5 -1\n5 -1\n" + in + outputs "an arm takes the other arm's type" "programs/arm-want.flan" aw_out; + outputs ~x86:true "an arm takes the other arm's type, x86" + "programs/arm-want.flan" aw_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"; diff --git a/test/test_flan.ml b/test/test_flan.ml index 02fe3813..da911778 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -7984,7 +7984,8 @@ let () = check "a match arm of another type is refused at its value" (dloc.Loc.col = 87 && contains dmsg "expected i8, found string")); (* Nested arms that meet at a wider type are checked once each, not once - per level above them. *) + per level above them — when the else arm fits the then arm's type, and + when it is wider, so that every level's first attempt is refused. *) (let nest kind depth = let rec go k e = if k = 0 then e @@ -7993,7 +7994,10 @@ let () = (match kind with | `If -> Printf.sprintf "(if c a (+ (idg b) (i32 %s)))" e | `Match -> - Printf.sprintf "(match o (Some q) a None (+ (idg b) (i32 %s)))" e) + Printf.sprintf "(match o (Some q) a None (+ (idg b) (i32 %s)))" e + | `If_wider -> Printf.sprintf "(if c b (+ a (i64 %s)))" e + | `Match_wider -> + Printf.sprintf "(match o (Some q) b None (+ a (i64 %s)))" e) in go depth "(i32 b)" in @@ -8021,7 +8025,45 @@ let () = | exception Loc.Error { Loc.dmsg; _ } -> check (what ^ " twenty deep checks: " ^ dmsg) false) [ (`If, "[c bool a i64 b i32]", "an if"); - (`Match, "[o (Option i32) a i64 b i32]", "a match") ]); + (`Match, "[o (Option i32) a i64 b i32]", "a match"); + (`If_wider, "[c bool a i64 b i32]", "an if whose else arm is wider"); + (`Match_wider, "[o (Option i32) a i64 b i32]", + "a match whose last arm is wider") ]); + (* An arm is asked the other arm's type first, so a value that takes its + type from what is asked — nil, (Some 3), arithmetic — gets it, and the + two meet the same way whichever is written first. *) + (let reads_as_top what src name want = + let got = + match checked src with + | p -> + (match List.find_opt (fun (f : Tast.fn) -> f.Tast.name = name) p.Tast.fns with + | Some f -> Dev.signature_of_fn f + | None -> "missing") + | exception Loc.Error { Loc.dmsg = m; _ } -> "refused: " ^ m + in + if got <> want then begin + incr failures; + Printf.printf "FAIL %s\n got: %s\n wanted: %s\n" what got want + end + in + List.iter + (fun (what, sg, body, want) -> + reads_as_top what ("(defn f " ^ sg ^ " _ " ^ body ^ ")\n(defn main [] ())") "f" want) + [ ("nil beside an Option", "[c bool p (Option i64)]", "(if c p nil)", + "f [bool (Option i64)] (Option i64)"); + ("nil first beside an Option", "[c bool p (Option i64)]", "(if c nil p)", + "f [bool (Option i64)] (Option i64)"); + ("(Some 3) beside an Option", "[c bool p (Option i64)]", "(if c p (Some 3))", + "f [bool (Option i64)] (Option i64)"); + ("float arithmetic beside an f32", "[c bool p f32]", "(if c p (* 2.0 3.0))", + "f [bool f32] f32"); + ("a do ending in a literal beside a u8", "[c bool p u8]", + "(if c p (do (println 1) 7))", "f [bool u8] u8"); + ("a match's nil arm first", "[o (Option i32) p (Option i64)]", + "(match o None nil (Some z) p)", "f [(Option i32) (Option i64)] (Option i64)") ]); + rejects_check "nil beside a string, as before" + ~needle:"string" + "(defn f [c bool s string] string (let [v (if c s nil)] v))\n(defn main [] ())"; 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\ From 263214e6392d10d0e51d215930e3db310414a52a Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Fri, 25 Sep 2026 23:43:14 +0700 Subject: [PATCH 8/9] A dyn opened by an expectation is marked where it is opened, so a bool or an Option beside a dyn stays a dyn, and an operand refused at a type is not asked again, so nested sums and matches check in linear time --- lib/check.ml | 73 +++++++++++++++++++++++++++++------ test/programs/dyn-opened.flan | 25 ++++++++++++ test/test_acceptance.ml | 5 +++ test/test_flan.ml | 28 ++++++++++++++ 4 files changed, 120 insertions(+), 11 deletions(-) create mode 100644 test/programs/dyn-opened.flan diff --git a/lib/check.ml b/lib/check.ml index fcae594f..8b0aa8a3 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -4108,6 +4108,17 @@ let box loc (e : Tast.expr) : Tast.expr = | Types.LArray _ -> no_dyn_yet loc ~into:true e.Tast.ty "" +(* Every dyn an expectation opened ([expect]'s dyn arm), by the node that + opened it, and the box: what lets a caller that asked for a typed value + see that the value was a dyn, whichever opening the want picked. Keyed by + identity and held weakly, so it is gone with the tree. *) +module Opened = Ephemeron.K1.Make (struct + type t = Tast.expr + let equal = ( == ) + let hash = Hashtbl.hash + end) +let opened_by_want : Tast.expr Opened.t = Opened.create 16 + let unbox loc (want : Types.t) (e : Tast.expr) : Tast.expr = let need sym ty = rt loc ty sym [ e ] in match want with @@ -4485,6 +4496,10 @@ let expect ctx loc ~want (got : Tast.expr) = | Types.Dyn, Types.Dyn -> got | Types.Dyn, Types.Option t -> box_option ctx loc t got | Types.Dyn, _ -> box loc got + | Types.Option t, Types.Dyn when not (is_nil_lit got) -> + let opened = unbox_option ctx loc t got in + Opened.replace opened_by_want opened got; + opened | Types.Option t, Types.Dyn -> unbox_option ctx loc t got (* A bare T has no None to become, and this nil is one the checker can actually see — the literal, written right where the mismatch is. @@ -4496,7 +4511,10 @@ let expect ctx loc ~want (got : Tast.expr) = or to dyn itself; wrap the type in Option, or keep the value dyn" (Types.to_string w) | _, Types.Dyn when Types.fits ~expected:w ~actual:Types.Dyn -> got - | _, Types.Dyn -> unbox loc w got + | _, Types.Dyn -> + let opened = unbox loc w got in + Opened.replace opened_by_want opened got; + opened (* Implicit widening, and this single arm is the whole of its surface. [expect] is called by every site that annotates and by nothing else, so an argument, a return, a let or defonce with a type, a struct field @@ -5357,11 +5375,21 @@ let arm_failed : the dyn one opened — whichever is written first. *) let not_kept = "check/arm-not-kept" -let opened_dyn (v : Tast.expr) = +let rec opened_dyn (v : Tast.expr) = match v.Tast.e with - | Tast.Prim (Tast.Rt ("flan_dyn_need_i64" | "flan_dyn_need_f64"), [ inner ]) - when Types.equal inner.Tast.ty Types.Dyn -> Some inner - | _ -> None + (* A block — a match arm's body — opened its last form. *) + | Tast.Do (_ :: _ as xs) -> + let rec split = function + | [ l ] -> ([], l) + | x :: r -> let i, l = split r in (x :: i, l) + | [] -> assert false + in + let init, last = split xs in + Option.map + (fun (box : Tast.expr) -> + { v with Tast.e = Tast.Do (init @ [ box ]); ty = Types.Dyn }) + (opened_dyn last) + | _ -> Opened.find_opt opened_by_want v (* A Vec or a Map parameter is a copy of the caller's header — Odin's rule — @@ -13988,6 +14016,25 @@ and join_pair ctx (a : Tast.expr) (y : Ast.expr) (d : Loc.diag) = | Some pair -> pair | None -> raise (Loc.Error d)) +(* [y] checked at [w] in a trial, and a refusal kept ([arm_failed]) so the + same operand asked again at the same type, in the same scope, is refused + without being walked: a chain of these nested in their second operands is + asked once per level above it. *) +and trial_at ctx (y : Ast.expr) (w : Types.t) = + match + List.find_opt + (fun (n, (sc, r), w', _) -> + n == y && r == ctx.ret && Types.equal w' w && same_scope sc ctx.scope) + (Hashtbl.find_all arm_failed y.Ast.loc) + with + | Some (_, _, _, d) -> Error d + | None -> + (match trial ctx (fun () -> check ctx ~want:w y) with + | Ok b -> Ok b + | Error d -> + Hashtbl.add arm_failed y.Ast.loc (y, (ctx.scope, ctx.ret), w, d); + Error d) + and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args = match args with | [ x; y ] -> @@ -14034,9 +14081,7 @@ and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args = let at_a = if a.Tast.ty = Types.Dyn then None else - match trial ctx (fun () -> check ctx ~want:a.Tast.ty y) with - | Ok b' -> Some (Ok b') - | Error d -> Some (Error d) + Some (trial_at ctx y a.Tast.ty) in match at_a with | Some (Ok b') -> @@ -14066,7 +14111,7 @@ and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args = (match match at_a with | Some (Error d) -> Error d - | _ -> trial ctx (fun () -> check ctx ~want:a.Tast.ty y) + | _ -> trial_at ctx y a.Tast.ty with | Ok b' -> a, b' | Error d -> @@ -14078,10 +14123,16 @@ and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args = end else begin let a = check ctx ?want x in - match trial ctx (fun () -> check ctx ~want:a.Tast.ty y) with + match trial_at ctx y a.Tast.ty with | Ok b -> a, b | Error d -> - if join && reconsiderable d then join_pair ctx a y d + (* The join moves [a] to something wider, and [a] already has the + type asked of the whole: that can only be refused, so y is not + walked on its own terms to find it out. *) + let doomed = + match want with Some w -> Types.equal a.Tast.ty w | None -> false + in + if join && reconsiderable d && not doomed then join_pair ctx a y d else raise (Loc.Error d) end | _ -> fail loc "%s takes two arguments" name diff --git a/test/programs/dyn-opened.flan b/test/programs/dyn-opened.flan new file mode 100644 index 00000000..529b3db5 --- /dev/null +++ b/test/programs/dyn-opened.flan @@ -0,0 +1,25 @@ +;;;; A dyn beside a typed value is compared, added and joined as a dyn, in +;;;; either order, whichever conversion asking for the typed value would have +;;;; opened it with — a bool compared with a dyn int is false, not a trap. + +(defn as-dyn [d dyn] dyn d) +(defn eqb [b bool d dyn] bool (= b d)) +(defn eqi [b i64 d dyn] bool (= b d)) +(defn addf [b f64 d dyn] dyn (+ b d)) +(defn addi [b i64 d dyn] dyn (+ b d)) +(defn mb [o (Option i32) b bool d dyn] dyn (let [v (match o (Some q) b None d)] v)) +(defn mb2 [o (Option i32) b bool d dyn] dyn (let [v (match o None d (Some q) b)] v)) +(defn ib [c bool b bool d dyn] dyn (let [v (if c b d)] v)) +(defn ib2 [c bool b bool d dyn] dyn (let [v (if c d b)] v)) + +(defn main [] i32 + (println (eqb true (as-dyn 1))) + (println (eqb true (as-dyn true))) + (println (eqi 1 (as-dyn 1.0))) + (println (addi 1 (as-dyn 1.5))) + (println (addf 1.0 (as-dyn 2))) + (println (mb None true (as-dyn 5))) + (println (mb2 None true (as-dyn 5))) + (println (ib false true (as-dyn 5))) + (println (ib2 true true (as-dyn 5))) + 0) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index a470865d..af5a600d 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -590,6 +590,11 @@ 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 dyn opened by the other operand's or arm's type is seen as a dyn. *) + let do_out = "false\ntrue\ntrue\n2.5\n3\n5\n5\n5\n5\n" in + outputs "a dyn beside a typed value stays a dyn" "programs/dyn-opened.flan" do_out; + outputs ~x86:true "a dyn beside a typed value stays a dyn, x86" + "programs/dyn-opened.flan" do_out; (* An arm is checked at the other arm's type first. *) let aw_out = "2147483648\n2147483648\n10000000000\n2147483648\n1.5\n2147483648\n\ diff --git a/test/test_flan.ml b/test/test_flan.ml index da911778..c186c9dd 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -8061,6 +8061,34 @@ let () = "(if c p (do (println 1) 7))", "f [bool u8] u8"); ("a match's nil arm first", "[o (Option i32) p (Option i64)]", "(match o None nil (Some z) p)", "f [(Option i32) (Option i64)] (Option i64)") ]); + (* Thirty deep, each level's first try refused: a chain of matches whose + last arm is wider, and sums nested in their second operands. *) + List.iter + (fun (what, src) -> + let t0 = Unix.gettimeofday () in + (match checked src with + | _ -> () + | exception Loc.Error { Loc.dmsg; _ } -> check (what ^ ": " ^ dmsg) false); + check (what ^ " checks fast") (Unix.gettimeofday () -. t0 < 3.0)) + (let nest f = let rec go k e = if k = 0 then e else go (k - 1) (f e) in go 30 in + [ ("thirty matches whose last arm is wider", + "(defn f [o (Option i32) a i64 b i32] i64 (let [v " + ^ nest (Printf.sprintf "(match o (Some q) (+ q 1) None (+ b %s))") "a" + ^ "] v))"); + ("thirty matches with the narrow arm last", + "(defn f [o (Option i32) a i64 b i32] i64 (let [v " + ^ nest (Printf.sprintf "(match o None b (Some q) (+ b %s))") "a" + ^ "] v))"); + ("thirty matches over a dyn at the bottom", + "(defn f [o (Option i32) d dyn b i32] dyn (let [v " + ^ nest (Printf.sprintf "(match o (Some q) q None (+ b %s))") "d" + ^ "] v))"); + ("thirty sums nested in their second operands", + "(defn f [a i64 b i32] i64 (let [v " + ^ nest (Printf.sprintf "(+ b %s)") "a" ^ "] v))") ]); + rejects_check "an Option compared with a dyn, as before" + ~needle:"(Option i64) does not cross into dyn yet" + "(defn eqo [b (Option i64) d dyn] bool (= b d))\n(defn main [] ())"; rejects_check "nil beside a string, as before" ~needle:"string" "(defn f [c bool s string] string (let [v (if c s nil)] v))\n(defn main [] ())"; From 40eb57a5b6955fdffb54d2ea5ce9623f6b02767c Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sat, 26 Sep 2026 00:09:42 +0700 Subject: [PATCH 9/9] A dyn opened in any value position of an operand or an arm makes it meet as a dyn, found by the one walk of value positions the frame-escape check also uses --- lib/check.ml | 103 ++++++++++++++++++++--------------- lib/tast.ml | 38 +++++++++++++ test/programs/dyn-tails.flan | 88 ++++++++++++++++++++++++++++++ test/test_acceptance.ml | 5 ++ 4 files changed, 190 insertions(+), 44 deletions(-) create mode 100644 test/programs/dyn-tails.flan diff --git a/lib/check.ml b/lib/check.ml index 8b0aa8a3..766e7642 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -3944,26 +3944,11 @@ let refuse_frame_escapes (f : Tast.fn) = else String.capitalize_ascii who) verb (what hit) target whose who fix in - let rec tails (e : Tast.expr) = - match e.Tast.e with - | Tast.Do es | Tast.Let (_, es) | Tast.WithAlloc (_, es) - | Tast.Handled (_, es) -> - (match List.rev es with x :: _ -> tails x | [] -> ()) - (* A restart clause is a branch of this function whose value is the - form's value when that restart is taken. *) - | Tast.RestartCase (cs, body) -> - List.iter - (fun (c : Tast.rclause) -> - match List.rev c.Tast.rbody with x :: _ -> tails x | [] -> ()) - cs; - tails body - | Tast.If (_, a, b) -> tails a; tails b - | Tast.Match (_, arms) -> - List.iter - (fun (a : Tast.arm) -> - match List.rev a.Tast.abody with x :: _ -> tails x | [] -> ()) - arms - | _ -> + (* Every value position of the body, walked by [Tast.iter_tails]: a + restart clause is a branch of this function whose value is the form's + value when that restart is taken, and it is on that list. *) + let tails = + Tast.iter_tails (fun (e : Tast.expr) -> Option.iter (fail ~verb:"returns" ~target:"" ~fix_slice:(fun c -> @@ -3976,7 +3961,7 @@ let refuse_frame_escapes (f : Tast.fn) = else "Return the value, of type " ^ t ^ ", instead of its address: drop the addr")) - (escapes 0 e) + (escapes 0 e)) in (* Only a store into the global itself can be fixed by changing the global's type; for a field, an element or a push, the value's type @@ -4119,6 +4104,15 @@ module Opened = Ephemeron.K1.Make (struct end) let opened_by_want : Tast.expr Opened.t = Opened.create 16 +(* What an [expect] mismatch found, by the refusal: the type a caller that + skipped a join can still name the way the join would have. *) +module Found = Ephemeron.K1.Make (struct + type t = Loc.diag + let equal = ( == ) + let hash = Hashtbl.hash + end) +let mismatch_found : Types.t Found.t = Found.create 16 + let unbox loc (want : Types.t) (e : Tast.expr) : Tast.expr = let need sym ty = rt loc ty sym [ e ] in match want with @@ -4560,10 +4554,14 @@ let expect ctx loc ~want (got : Tast.expr) = numbers, and it is on this message rather than beside it because a reader who has just been told i64 and i32 are different types needs to be told, in the same breath, which direction needed nothing. *) - Loc.failk "check/type-mismatch" loc "expected %s, found %s%s%s" - (Types.to_string w) (Types.to_string got.Tast.ty) - (numeric_note ~want:w ~got:got.Tast.ty) - (const_note ctx.env ~want:w ~got:got.Tast.ty) + (try + Loc.failk "check/type-mismatch" loc "expected %s, found %s%s%s" + (Types.to_string w) (Types.to_string got.Tast.ty) + (numeric_note ~want:w ~got:got.Tast.ty) + (const_note ctx.env ~want:w ~got:got.Tast.ty) + with Loc.Error d -> + Found.replace mismatch_found d got.Tast.ty; + raise (Loc.Error d)) (* Something a [break] may not jump out of, named so the refusal can say which. See [lentry]: it is a barrier and not a blanket refusal, so a loop written @@ -5375,21 +5373,25 @@ let arm_failed : the dyn one opened — whichever is written first. *) let not_kept = "check/arm-not-kept" -let rec opened_dyn (v : Tast.expr) = - match v.Tast.e with - (* A block — a match arm's body — opened its last form. *) - | Tast.Do (_ :: _ as xs) -> - let rec split = function - | [ l ] -> ([], l) - | x :: r -> let i, l = split r in (x :: i, l) - | [] -> assert false - in - let init, last = split xs in - Option.map - (fun (box : Tast.expr) -> - { v with Tast.e = Tast.Do (init @ [ box ]); ty = Types.Dyn }) - (opened_dyn last) - | _ -> Opened.find_opt opened_by_want v +let to_dyn ctx (x : Tast.expr) = expect ctx x.Tast.loc ~want:(Some Types.Dyn) x + +let opened_dyn ~(box : Tast.expr -> Tast.expr) (v : Tast.expr) = + (* An opening is a value position of its own, whatever shape the + conversion built. *) + let stop x = Opened.mem opened_by_want x in + let any = ref false in + Tast.iter_tails ~stop (fun x -> if stop x then any := true) v; + if not !any then None + else + (* Every value position meets at dyn: an opened one is put back to the + box it opened, and any other is boxed. *) + Some + (Tast.map_tails ~stop ~ty:Types.Dyn + (fun x -> + match Opened.find_opt opened_by_want x with + | Some b -> b + | None -> box x) + v) (* A Vec or a Map parameter is a copy of the caller's header — Odin's rule — @@ -7571,7 +7573,7 @@ and check_if_once ctx ~tail ?want loc c t e = in match at_then () with | Ok v -> - (match opened_dyn v with + (match opened_dyn ~box:(to_dyn ctx) v with | Some box -> Some (Types.Dyn, box) | None -> Some (t.Tast.ty, v)) | Error _ when adapts e -> None @@ -9125,7 +9127,7 @@ and check_match ctx ?(tail = false) ?want loc scrutinee arms = in match at_join () with | Ok b -> - (match opened_dyn b with + (match opened_dyn ~box:(to_dyn ctx) b with | Some box -> want := Some Types.Dyn; box | None -> b) | Error d -> @@ -14085,7 +14087,7 @@ and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args = in match at_a with | Some (Ok b') -> - (match opened_dyn b' with Some box -> a, box | None -> a, b') + (match opened_dyn ~box:(to_dyn ctx) b' with Some box -> a, box | None -> a, b') | _ -> let b = check ctx y in (* Nothing dyn about this pair after all, so it is put back the way the @@ -14133,7 +14135,20 @@ and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args = match want with Some w -> Types.equal a.Tast.ty w | None -> false in if join && reconsiderable d && not doomed then join_pair ctx a y d - else raise (Loc.Error d) + else + (* Doomed: said the way the join would have been refused — the + pair at the wider type, at this form — when y's own refusal + names the wider type it found. *) + match want, (if doomed then Found.find_opt mismatch_found d else None) with + | Some w, Some found + when String.equal d.Loc.dloc.Loc.file y.Ast.loc.Loc.file + && d.Loc.dloc = y.Ast.loc -> + (match Types.join w found with + | Some j when not (Types.equal j w) -> + ignore (expect ctx loc ~want:(Some w) (mk loc j Tast.Unit)); + raise (Loc.Error d) + | _ -> raise (Loc.Error d)) + | _ -> raise (Loc.Error d) end | _ -> fail loc "%s takes two arguments" name diff --git a/lib/tast.ml b/lib/tast.ml index c6eda366..cba851e2 100644 --- a/lib/tast.ml +++ b/lib/tast.ml @@ -471,6 +471,44 @@ let is_watch_guard (c : expr) = | Prim (Ne, [ { e = Prim (Rt s, _); _ }; _ ]) -> String.equal s watch_begin | _ -> false +(* The value positions of an expression: the forms whose value is the + expression's value — a block's last form, both arms of an [if], every + arm of a [match] and of a [restart-case]. Everything that asks "what does + this expression answer with" walks these, so a form that carries a value + through from one of its parts is added here once. [map_tails ~ty] rebuilds + the expression with each value position replaced by [f] of it and every + form on the way given [ty]; a position that never arrives (its type + Never) is left alone unless [all]. A form [stop] answers yes for is taken + as a value position whole, not looked into. *) +let rec map_tails ?(all = false) ?(stop = fun _ -> false) ?ty (f : expr -> expr) + (e : expr) : expr = + let go = map_tails ~all ~stop ?ty f in + let last es = + match List.rev es with + | x :: rest -> List.rev (go x :: rest) + | [] -> es + in + let retype k = + let t = match ty with Some t -> t | None -> e.ty in + { e with e = k; ty = (if e.ty = Types.Never then e.ty else t) } + in + if stop e then f e else + match e.e with + | Do es -> retype (Do (last es)) + | Let (bs, es) -> retype (Let (bs, last es)) + | WithAlloc (a, es) -> retype (WithAlloc (a, last es)) + | Handled (hs, es) -> retype (Handled (hs, last es)) + | If (c, a, b) -> retype (If (c, go a, go b)) + | Match (sc, arms) -> + retype (Match (sc, List.map (fun a -> { a with abody = last a.abody }) arms)) + | RestartCase (cs, body) -> + retype + (RestartCase (List.map (fun c -> { c with rbody = last c.rbody }) cs, go body)) + | _ -> if e.ty = Types.Never && not all then e else f e + +let iter_tails ?stop (f : expr -> unit) (e : expr) = + ignore (map_tails ~all:true ?stop (fun x -> f x; x) e) + let rec walk (f : expr -> unit) (e : expr) = f e; let go = walk f in diff --git a/test/programs/dyn-tails.flan b/test/programs/dyn-tails.flan new file mode 100644 index 00000000..dc73e56a --- /dev/null +++ b/test/programs/dyn-tails.flan @@ -0,0 +1,88 @@ +;;;; A dyn in any value position of an operand or an arm — the last form +;;;; of a let, either arm of an if, an arm of a match, the operand an and +;;;; or an or answers with — meets its typed partner as a dyn, so what the +;;;; runtime compares or adds is the dyn value and nothing traps. + +(defn as-dyn [d dyn] dyn d) + +(defn a1-t [c bool i i64 d dyn] dyn (+ i (let [z 1] d))) +(defn a2-t [c bool i i64 d dyn] dyn (+ i (if c d d))) +(defn a3-t [c bool i i64 d dyn] dyn (+ i (if c d 2))) +(defn a4-t [c bool i i64 d dyn] dyn (= i (if c d 2))) +(defn a5-t [c bool i i64 d dyn] dyn (* i (match (Some 1) (Some q) d None d))) +(defn a6-t [c bool i i64 d dyn] dyn (let [v (if c i (let [z 1] d))] v)) +(defn a7-t [c bool i i64 d dyn] dyn (let [v (match (Some 1) (Some q) i None (let [z 1] d))] v)) +(defn a8-t [c bool i i64 d dyn] dyn (let [v (match (Some 1) None i (Some q) (if c d d))] v)) +(defn a9-t [c bool i i64 d dyn] dyn (- i (do (println 0) d))) +(defn o1-t [c bool b bool i i64 d dyn] dyn (= b (and d))) +(defn o2-t [c bool b bool i i64 d dyn] dyn (= b (or d))) +(defn o3-t [c bool b bool i i64 d dyn] dyn (= b (and c d))) +(defn o4-t [c bool b bool i i64 d dyn] dyn (= b (not d))) +(defn o6-t [c bool b bool i i64 d dyn] dyn (let [v (if c b (and d))] v)) +(defn w1-t [c bool b bool d dyn] bool (= b (do (println 0) d))) +(defn w2-t [c bool b bool d dyn] bool (= b (let [z 1] d))) +(defn w3-t [c bool b bool d dyn] bool (= b (if c d d))) +(defn w4-t [c bool b bool d dyn] bool (= b (if c d false))) +(defn w5-t [c bool b bool d dyn] bool (= b (if c false d))) +(defn w6-t [c bool b bool d dyn] bool (= b (match (Some 1) (Some q) d None d))) +(defn w7-t [c bool b bool d dyn] bool (= (do d) b)) +(defn w9-t [c bool b bool d dyn] bool (= b (cond c d :else d))) +(defn w10-t [c bool b bool d dyn] bool (= b (as-dyn d))) +(defn w11-t [c bool b bool d dyn] bool (let [v (if c b (let [z 1] d))] (= v v))) +(defn w12-t [c bool b bool d dyn] bool (= b (if c (do d) (do d)))) +(defn w13-t [c bool b bool d dyn] bool (!= b (let [z 1] (println z) d))) + +(defn main [] i32 + (println (a1-t true 1 (as-dyn 1.5))) + (println (a1-t false 1 (as-dyn 1.5))) + (println (a2-t true 1 (as-dyn 1.5))) + (println (a2-t false 1 (as-dyn 1.5))) + (println (a3-t true 1 (as-dyn 1.5))) + (println (a3-t false 1 (as-dyn 1.5))) + (println (a4-t true 1 (as-dyn 1.5))) + (println (a4-t false 1 (as-dyn 1.5))) + (println (a5-t true 1 (as-dyn 1.5))) + (println (a5-t false 1 (as-dyn 1.5))) + (println (a6-t true 1 (as-dyn 1.5))) + (println (a6-t false 1 (as-dyn 1.5))) + (println (a7-t true 1 (as-dyn 1.5))) + (println (a7-t false 1 (as-dyn 1.5))) + (println (a8-t true 1 (as-dyn 1.5))) + (println (a8-t false 1 (as-dyn 1.5))) + (println (a9-t true 1 (as-dyn 1.5))) + (println (a9-t false 1 (as-dyn 1.5))) + (println (o1-t true true 1 (as-dyn 1))) + (println (o1-t true true 1 (as-dyn true))) + (println (o2-t true true 1 (as-dyn 1))) + (println (o2-t true true 1 (as-dyn true))) + (println (o3-t true true 1 (as-dyn 1))) + (println (o3-t true true 1 (as-dyn true))) + (println (o4-t true true 1 (as-dyn 1))) + (println (o4-t true true 1 (as-dyn true))) + (println (o6-t true true 1 (as-dyn 1))) + (println (o6-t true true 1 (as-dyn true))) + (println (w1-t true true (as-dyn 5))) + (println (w1-t false true (as-dyn 5))) + (println (w2-t true true (as-dyn 5))) + (println (w2-t false true (as-dyn 5))) + (println (w3-t true true (as-dyn 5))) + (println (w3-t false true (as-dyn 5))) + (println (w4-t true true (as-dyn 5))) + (println (w4-t false true (as-dyn 5))) + (println (w5-t true true (as-dyn 5))) + (println (w5-t false true (as-dyn 5))) + (println (w6-t true true (as-dyn 5))) + (println (w6-t false true (as-dyn 5))) + (println (w7-t true true (as-dyn 5))) + (println (w7-t false true (as-dyn 5))) + (println (w9-t true true (as-dyn 5))) + (println (w9-t false true (as-dyn 5))) + (println (w10-t true true (as-dyn 5))) + (println (w10-t false true (as-dyn 5))) + (println (w11-t true true (as-dyn 5))) + (println (w11-t false true (as-dyn 5))) + (println (w12-t true true (as-dyn 5))) + (println (w12-t false true (as-dyn 5))) + (println (w13-t true true (as-dyn 5))) + (println (w13-t false true (as-dyn 5))) + 0) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index af5a600d..f12aca6d 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -590,6 +590,11 @@ 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 dyn in any value position of an operand or an arm is a dyn. *) + let dt_out = "2.5\n2.5\n2.5\n2.5\n2.5\n3\nfalse\nfalse\n1.5\n1.5\n1\n1.5\n1\n1\n1.5\n1.5\n0\n-0.5\n0\n-0.5\nfalse\ntrue\nfalse\ntrue\nfalse\ntrue\nfalse\nfalse\ntrue\ntrue\n0\nfalse\n0\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\nfalse\ntrue\ntrue\nfalse\nfalse\n1\ntrue\n1\ntrue\n" in + outputs "a dyn in a value position stays a dyn" "programs/dyn-tails.flan" dt_out; + outputs ~x86:true "a dyn in a value position stays a dyn, x86" + "programs/dyn-tails.flan" dt_out; (* A dyn opened by the other operand's or arm's type is seen as a dyn. *) let do_out = "false\ntrue\ntrue\n2.5\n3\n5\n5\n5\n5\n" in outputs "a dyn beside a typed value stays a dyn" "programs/dyn-opened.flan" do_out;