JosephFerano/flan
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

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

Browse Source
This commit is contained in:
Joseph Ferano 2026-09-25 21:26:56 +07:00
parent 0fc258c434
commit ed7258c80f
6 changed files with 213 additions and 80 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
TODO.org
View File

@ -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]

220
lib/check.ml
View File

@ -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/<owner>/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

2
spec-syntax.md
View File

@ -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 `()`.

23
test/programs/trial-generic.flan Normal file
View File

@ -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)

6
test/test_acceptance.ml
View File

@ -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"

38
test/test_flan.ml
View File

@ -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 [] ())";