From b4dbbb67ab97ff92b82d76eadb9e7ca0dcfa3986 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sun, 20 Sep 2026 19:25:17 +0700 Subject: [PATCH] The review's three findings, and the lanes this one landed on top of --- FIX.org | 105 +++++++++++++++++++++++++++++++++++++++++++--- test/test_flan.ml | 20 +++++---- 2 files changed, 112 insertions(+), 13 deletions(-) diff --git a/FIX.org b/FIX.org index 57a8b61..bc02ade 100644 --- a/FIX.org +++ b/FIX.org @@ -2526,11 +2526,26 @@ decides-rule generalises rather than disappearing: operands as before, and now widens them. The addition happens at ~i64~, not at ~i32~ followed by a widened result. That is the better of the two and it is only reachable by programs that did not compile before. -2. *Literals decide exactly as they did.* ~y_decides~ and ~needs_want~ are - untouched: a literal takes its width from the other operand, a float - literal outranks an integer one. ~(+ x 1)~ over a ~u64~ ~x~ still builds a - ~u64~ one, which is what keeps ~(let [h fnv-offset])~ with a ~u64~ - ~defconst~ meaning exactly what it meant. +2. *Literals decide exactly as they did, and this one had to be defended.* + ~y_decides~ and ~needs_want~ are untouched: a literal takes its width from + the other operand, a float literal outranks an integer one. ~(+ x 1)~ over a + ~u64~ ~x~ still builds a ~u64~ one, which is what keeps + ~(let [h fnv-offset])~ with a ~u64~ ~defconst~ meaning exactly what it + meant. + + Saying so was not enough. The join is implemented as a *trial* — ask the + second operand for the first's type, and reconsider if it refuses — and the + first version of it reconsidered a literal too, which silently moved + ~(+ u8-thing 300)~ from "300 does not fit in u8" to i32 arithmetic + answering 555, asymmetric in the operand order, and ~(+ i32-x 1.5)~ to an + f64 add. That is a different language from the one decided on. A literal + that does not fit is the program's mistake and not a pair of types that + failed to meet — the literal had no type of its own to bring — so the three + refusals that say so (~in_range~, and the integer and float literal arms of + ~check~) now carry the kind ~check/literal-at-want~, and the trial re-raises + on sight of it rather than looking again. Pinned four ways: the literal as + the operand, the literal buried inside one, the float-literal spelling, and + a literal that *does* fit still taking the operand's type. 3. *Otherwise the wider side decides* — ~Types.join~: whichever operand the other widens into, with the loser wrapped in a ~Cast~ to it. ~(+ i32-var i64-var)~ is ~i64~ and is newly legal. ~(min i8-var i16-var)~ is ~i16~. @@ -2638,7 +2653,10 @@ what was true when they were written. examples/ were *not run*. They link raylib and every one of them opens a real window on the author's desktop, so the comparison there is ~check~'s exit status and diagnostics plus a byte-diff of ~emit~ and ~emit --x86~. - LLVM output is byte-identical for all of them. The x86 output differs in 28 + LLVM output is byte-identical for all of them — after the same + prelude-line normalisation the x86 comparison needs, which the LLVM diff gets + for free because it spells those strings out as text where x86 emits them as + ~.byte~ data. The x86 output differs in 28 of them and every differing byte is inside a ~:line:col~ string — this lane's comment rewrites moved prelude source lines by three, and the x86 backend spells those strings out as ~.byte~ data. Normalising the @@ -2659,3 +2677,78 @@ what was true when they were written. belong to the batch after several lanes land. The individual ~--x86~ builds the policy does require were run, and are the acceptance row and the sweep above. + +** Review round two: what the first version got wrong +Three findings, all in the mechanism rather than in the lattice, and all from +the same root — the join is implemented as a *trial* (ask the second operand +for the first operand's type; reconsider only if that refuses), and a trial +that catches an exception is not free the way a trial that returns an option +is. + +*1. An abandoned trial left its bindings behind.* ~scoped~ restores +~ctx.scope~ on the way out, and an exception does not take that way out — so +every binding the abandoned pass made survived into the enclosing scope. Two +symptoms, and the second is the serious one: + +- a name that should be unknown resolved anyway, and +- the abandoned binding *shadowed* a live one. ~(let [t i32-x] (println (+ + i32-x (let [t i64-y] t))) (println t))~ printed the sum and then ~0~ — the + outer ~t~ read through the dead inner binding's slot, which nothing ever + stored into. An uninitialised stack read, in a program the compiler + accepted, on both backends. + +Fixed with ~trial~, which snapshots ~scope~, ~slots~, ~slot_tys~, +~slot_names~, ~defers~ and ~defer_slot~ and puts all six back when the trial +refuses. ~scoped~ itself is untouched — it is shared by every scope-opening +form in the file and this is not its problem to solve. ~trial~ also narrows +the catch to ~Loc.Error~: a timeout or a stack overflow is not a refusal to +reconsider, and continuing past one would turn a resource failure into a wrong +answer. Both symptoms pinned. + +*2. The trial reconsidered literals.* Written up under the join rule above. +The short version: ~(+ u8-thing 300)~ compiled, at i32, answering 555. The +decision was literals-unchanged and now the code says so, by kind rather than +by hope. + +*3. Three globals collided with the prelude.* The dogfood batch added +~u8-max~, ~u16-max~ and ~u32-max~ as prelude ~defconst~s while this lane was +open, and the acceptance program had defined its own. The textual merge was +clean and all three acceptance rows died on "defined twice" in the merged +tree, which is precisely the failure a per-lane ~dune test~ cannot see. Every +global and function in test/programs/widening.flan now carries a ~w-~ prefix, +and the rows were re-run in a trial-merged tree rather than only on the lane. + +** Collisions with the lanes that landed underneath +Three, each read by hand rather than trusted to the auto-merge: + +- *The diagnostics lane* kinded ~expect~'s mismatch as + ~check/type-mismatch~ so a call-argument site can recognise it. Its wording + and its mechanism win; ~numeric_note~ rides on the same message, because a + reader who has just been told i64 and i32 are different types needs telling + in the same breath which direction needed nothing. +- *The struct lane* added ~check_bare~ and ~positional_struct~. No overlap: + it calls ~expect~, this lane added an arm inside it. The intersection — a + struct literal whose field initialisers widen — was compiled and run on both + backends by hand. +- *The int/float alias lane* pinned ~(+ int-var i64-var)~ as a type error, + with a comment saying the pin was written as identity so it would survive + whatever the widening table grew into. It was not written that way — it + pinned a refusal and a message — and it is the one refusal pin in the suite + this lane makes legal. Rewritten to pin identity for real: the mixed form is + accepted at i64 under ~int~ exactly as under ~i32~, and the narrowing back + into ~int~ is still refused, naming ~i32~ because that is what ~int~ erases + to. + +** Stale claims elsewhere, and one left alone +~runtime/flan_dyn.c~'s ~flan_dyn_need_f64~ note and +~runtime/flan_dyn_stub.c~'s arithmetic note both said the typed language has +no implicit widening at all. Rewritten, and the rewrite is not a hedge: the +typed language *does* widen an integer into a float now, but only the exact +ones, and the dyn box carries integers at i64 — the one width that reaches no +float on the lattice. So both boundaries refuse exactly what they refused, for +a reason that is now stated correctly. + +~web/index.html~ (two places) makes the same stale claim. *Left alone +deliberately*: the website has its own rewrite lane, and a marketing page is +not the place for this lane to be making edits it cannot test. Flagged here so +that lane picks it up. diff --git a/test/test_flan.ml b/test/test_flan.ml index 4d1c557..c7545cc 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -2815,13 +2815,19 @@ let () = "(defn f [] int 1.5)" ~needle:"expected i32"; rejects_check "and one under float names f32" "(defn f [] float (f64 1.0))" ~needle:"expected f32"; - (* Widening needs no entry for [int] because [int] *is* [i32]: the mixed - arithmetic that i32 refuses, int refuses identically and by the same - message. Pinned as identity rather than as a widening rule, so it says - the same thing whatever the widening table grows into. *) - rejects_check "int mixes with i64 exactly as i32 does" - "(defvar a int) (defvar b i64) (defn f [] i64 (+ a b))" - ~needle:"expected i64, found i32"; + (* Widening needs no entry for [int] because [int] *is* [i32], and this pin + says exactly that and nothing about what the widening table holds. It used + to read the other way round — the mixed arithmetic that i32 *refuses*, + int refuses identically — which was true when it was written and stopped + being true when implicit widening landed (FIX.org 2026-09-20): an i32 and + an i64 now meet at i64, so the same form under [int] has to be accepted, + and accepted at i64. Kept pointing at identity by pinning both directions: + the one that widens, and the one that still cannot. *) + accepts "int mixes with i64 exactly as i32 does" + "(defvar a int) (defvar b i64) (defn f [] i64 (+ a b))"; + rejects_check "and refuses the narrowing exactly as i32 does" + "(defvar a int) (defvar b i64) (defn f [] int (+ a b))" + ~needle:"expected i32, found i64"; (* A program that declared the alias itself — which this one's author did, before it was builtin. True as written, it is the no-op it says it is; pointed anywhere else it is refused, because the alias table is never