A number widens where no value can change, and a trial leaves no trace
This commit is contained in:
commit
d737625a3f
375
FIX.org
375
FIX.org
@ -2897,3 +2897,378 @@ takes a location first, so the class name would have been read as a length.
|
||||
*~dune build~ does not compile ~flan_dyn.c~* — it is a string the compiler
|
||||
carries and hands to clang at ~flan run~ — so a green build is not evidence
|
||||
about that file at all. ~dune test~ is, and so is running any program.
|
||||
* Implicit widening, 2026-09-20 — "go with C"
|
||||
Answers DISCUSS.org's *implicit numeric conversions with a warning flag,
|
||||
instead of hard errors*. The ask there was a warn-instead-of-refuse mode; the
|
||||
answer is narrower and needs no mode and no flag.
|
||||
|
||||
*The decision.* Implicit numeric *widening* is legal — every conversion that
|
||||
cannot change the number. *Narrowing stays a hard error everywhere*, with no
|
||||
flag that turns it into a warning. Odin's position roughly; Rust's
|
||||
no-conversions-at-all position is rejected, and so is C's, which is what
|
||||
DISCUSS.org's ~-Wconversion~ middle ground would have reproduced.
|
||||
|
||||
So there is no second type-checking mode, which was the objection in the note:
|
||||
one predicate says which conversions exist, one helper inserts the ~Cast~ for
|
||||
them, and everything else in the checker is unchanged.
|
||||
|
||||
** The lattice
|
||||
~Types.widens_to ~from ~into~ (lib/types.ml). One rule decides every row: a
|
||||
conversion is admitted exactly when no value of the source can come out the
|
||||
other side as a different number.
|
||||
|
||||
| from | widens implicitly into |
|
||||
|-------------+-------------------------------------------|
|
||||
| ~i8~ | ~i16~ ~i32~ ~i64~ ~f32~ ~f64~ |
|
||||
| ~i16~ | ~i32~ ~i64~ ~f32~ ~f64~ |
|
||||
| ~i32~ | ~i64~ ~f64~ |
|
||||
| ~i64~ | — (nothing) |
|
||||
| ~u8~ | ~u16~ ~u32~ ~u64~ ~i16~ ~i32~ ~i64~ ~f32~ ~f64~ |
|
||||
| ~u16~ | ~u32~ ~u64~ ~i32~ ~i64~ ~f32~ ~f64~ |
|
||||
| ~u32~ | ~u64~ ~i64~ ~f64~ |
|
||||
| ~u64~ | — (nothing) |
|
||||
| ~f32~ | ~f64~ |
|
||||
| ~f64~ | — (nothing) |
|
||||
|
||||
Read off the rule, one clause at a time:
|
||||
|
||||
- *Same signedness, strictly wider* — the uncontroversial half.
|
||||
- *Unsigned into strictly wider signed* — ~u8~→~i16~, ~u32~→~i64~. Every
|
||||
value of the source is a value of the target, so it is in.
|
||||
- *Signed into unsigned* — never, at any width: the negatives have nowhere to
|
||||
go.
|
||||
- *Equal width across signedness* (~i32~→~u32~, ~u32~→~i32~) — never, for the
|
||||
same reason. Half the range would have to move.
|
||||
- *Integer into float, exact only.* An ~f64~ significand is 53 bits, so
|
||||
everything 32 bits and under reaches it and ~i64~/~u64~ do not — 2^53+1 is
|
||||
not an ~f64~. An ~f32~ significand is 24 bits, so only the 8- and 16-bit
|
||||
integers reach it. Odin allows any integer into any float; this is the
|
||||
tighter rule deliberately. A program that wants ~i64~→~f64~ writes ~(f64 x)~.
|
||||
Loosening this later adds programs; tightening it later would break them,
|
||||
which is why the loose version is not the one that landed.
|
||||
- *~dyn~ is not in the lattice.* Crossing into and out of a box is
|
||||
~box~/~unbox~ and is untouched — in particular a ~dyn~ still only unboxes to
|
||||
~i64~/~f64~/~bool~, and a narrower want there is still the refusal
|
||||
lib/check.ml's ~unbox~ has always given.
|
||||
- *Containers are invariant.* A ~[i32]~ is not a ~[i64]~, a ~(Vec i32)~ is not
|
||||
a ~(Vec i64)~, an ~[8 u8]~ is not an ~[8 u16]~. Widening rewrites a value
|
||||
with a ~Cast~; there is no value to rewrite in a slice that does not own its
|
||||
bytes, and rewriting a ~Vec~ would mean allocating a second one.
|
||||
- ~bool~ and an ~Enum~ are not numbers and are not on the list. A keyword still
|
||||
resolves against an enum and a bare integer still does not fit one.
|
||||
|
||||
*Not expressed as a loosening of ~equal~ or ~fits~*, deliberately.
|
||||
~widens_to~ is a separate predicate precisely so that admitting a conversion
|
||||
is always paired with inserting the ~Cast~ that performs it. Had ~fits~ been
|
||||
loosened, every site that accepts a value without rewriting it would hand the
|
||||
backends a node whose type lies about the bits it holds.
|
||||
|
||||
** Where it applies
|
||||
~Check.expect~ (lib/check.ml) is the single place a wanted type meets a
|
||||
produced one, so one arm there covers the whole surface: argument passing,
|
||||
return position, ~let~ and ~defvar~ with an annotation, struct field
|
||||
initialisers, ~Vec~ pushes, ~set!~, every C import's parameters. Nothing else
|
||||
had to learn about widening except the binary operators, which have no
|
||||
"wanted type" to meet.
|
||||
|
||||
** The join rule for binary operators
|
||||
Both operands of a binary operator have one type, and the old comment said
|
||||
"there is no implicit widening, so one side has to decide it". The
|
||||
decides-rule generalises rather than disappearing:
|
||||
|
||||
1. *An expectation still wins, and it reaches the operands.* When the site
|
||||
wants a type — ~(defn f [] i64 (+ a b))~ — that want is threaded into both
|
||||
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, 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~.
|
||||
4. *Equal-width cross-sign still refuses.* ~(+ i32-var u32-var)~ has no join —
|
||||
neither widens into the other — and the message names the cast to write.
|
||||
|
||||
~join~ is not a real lattice and is not meant to be: ~(i32, u32)~ has no
|
||||
answer, and inventing ~i64~ for it would pick a type neither operand was
|
||||
written at.
|
||||
|
||||
*Folds are still folds.* ~(+ a b c)~ is ~((a + b) + c)~, so the join is
|
||||
pairwise and left-to-right: the first pair settles a type and the third
|
||||
operand is checked against it. ~(+ i8 i8 i64)~ therefore still refuses, where
|
||||
~(+ i64 i8 i8)~ passes. Left to stand rather than joined across the whole
|
||||
argument list, because changing that would change what ~(- a b c)~ means, not
|
||||
only what it admits.
|
||||
|
||||
*Shifts are carved out.* ~<<~ and ~>>~ do not take the plain join: the value
|
||||
decides, and the count widens to the value's type. Under the general rule
|
||||
~(<< u8-var i32-count)~ would widen the *value* to ~i32~ and the result type
|
||||
and the wrap width would silently follow the count's declared type — and the
|
||||
emitter's poison mask is keyed to the value's width. A count wider than the
|
||||
value is refused and says so.
|
||||
|
||||
** Const folding is unchanged, and was never the thing it looked like
|
||||
The ~defconst~ integer folder (~const_int~, lib/check.ml) runs on the *AST*,
|
||||
before anything has a type, and carries one ~int64~ per constant with no width
|
||||
attached. So it already folded across widths and still does —
|
||||
~(defconst w i32 4)~ times ~(defconst h i64 5)~ has always been a constant 20,
|
||||
usable as an array length — and widening neither added a fold nor removed one.
|
||||
Measured, not assumed.
|
||||
|
||||
The one thing that did change is at the edges rather than in the folder: it
|
||||
answers nothing for a ~Call~ whose operator is not one of the five arithmetic
|
||||
names, and a written cast is such a call. So ~(* w (i64 h))~ was not a
|
||||
constant and ~(* w h)~ is — which means dropping a cast that widening made
|
||||
unnecessary can turn a run-time computation into an array length. That is
|
||||
widening adding a program, the same as everywhere else, and needed no change
|
||||
here.
|
||||
|
||||
** No overload resolution to disturb
|
||||
Worth saying plainly, because widening is exactly the change that breaks
|
||||
overloading in a language that has it: this one does not. Every builtin is
|
||||
dispatched by *name* in ~named_call~ — there is no set of candidates to pick
|
||||
between, so widening cannot change which one fires and cannot make a call
|
||||
ambiguous. ~min~/~max~ and the arithmetic builtins looked like they keyed on
|
||||
types, and what they actually do is check a predicate (~ordered?~,
|
||||
~numeric?~) against the type the operands already agreed on. Widening changes
|
||||
what they agree on and nothing about the dispatch.
|
||||
|
||||
** Sites changed, and sites kept
|
||||
Changed, three of them and no more:
|
||||
- lib/types.ml — ~widens_to~ and ~join~, new. ~equal~ and ~fits~ untouched.
|
||||
- ~Check.expect~ — one arm, which is the entire annotation surface.
|
||||
- ~Check.binary~ — the join, and ~~join:false~ for the shifts.
|
||||
|
||||
Kept, with the message saying *narrowing* rather than "no conversions":
|
||||
- ~Check.unbox~'s per-width refusal at the dyn boundary. A dyn carries one
|
||||
integer width and one float width, so there is no narrower source to widen
|
||||
from and nothing on the lattice reaches it; what it refuses is a truncation
|
||||
at the one boundary where the value's type was already uncertain, and that
|
||||
is as true as it was.
|
||||
- Every numeric refusal that survives ~expect~ now carries ~numeric_note~,
|
||||
which tells the two surviving cases apart: a narrowing names the cast and
|
||||
points out that the other direction is free, and an equal-width cross-signed
|
||||
pair is told that neither direction exists.
|
||||
|
||||
Comments rewritten rather than left to rot, each now stating the new invariant
|
||||
rather than the old one: lib/types.ml's header, ~equal~'s note (why widening
|
||||
is deliberately *not* a loosening of it), ~Check.unbox~, ~Check.binary~, the
|
||||
bitwise and shift arms, the ~embed~ two-spellings argument (which turns out
|
||||
never to have rested on widening at all — it rests on containers not
|
||||
converting), lib/prelude.ml's ~print~ note and both ~sum-~ notes,
|
||||
docs/BUILT.md's ~gravity~ and ~#load~ paragraphs, test/programs/embed.flan,
|
||||
and the ~+~, ~bit-and~, ~<<~, ~>>~ and ~min~ lines of the ~builtins~ table.
|
||||
Left alone: docs/SPIKE-*.md and docs/handoffs/*, which are dated records of
|
||||
what was true when they were written.
|
||||
|
||||
** What was run
|
||||
- ~dune test --root . --force~ — exit 0, 0 FAIL lines, on the lane *and* in a
|
||||
trial-merged tree. Through most of this lane it exited 1 instead, from
|
||||
~test_dev.ml~'s ~trap_park~ rows racing and dying with
|
||||
~Fatal error: exception Flan.Wire.Closed~ at ~dev-trap-null-alloc~ — measured
|
||||
on an untouched worktree at dev-loop's tip with nothing of this lane in it,
|
||||
and written up above under "Found while running it". Another lane has since
|
||||
fixed it (~trap_park stops dying on the abort race~), so the green run is a
|
||||
real green run rather than a lucky one.
|
||||
|
||||
One *other* ~test_dev.ml~ row failed twice across seven runs of identical
|
||||
code — "the merged program never bound ...agent.sock", a daemon that did not
|
||||
come up in time — and was green on every run either side, on the lane and in
|
||||
the merged tree. The second failure named its own cause: the corpus sweep was
|
||||
compiling in another worktree on the same machine, and the row gives the
|
||||
daemon a fixed window to bind in. Run on an idle machine it is green.
|
||||
Recorded rather than chased: it is a socket bind in the agent fixture, this
|
||||
lane touches neither the agent nor the dyn side, and it looks like the same
|
||||
family as the ~trap_park~ race that was just fixed, one row further along —
|
||||
a timeout that is generous when nothing else is running and is not
|
||||
otherwise.
|
||||
- test/programs/widening.flan, new, with three acceptance rows — default, -O0
|
||||
and ~--x86~ — and its output diffed by hand across the two backends before
|
||||
the rows were written. Byte-identical.
|
||||
- The lattice's edges pinned in test_flan.ml: what widens, what does not, the
|
||||
two calls that could have gone the other way (int-into-float exact-only, and
|
||||
equal-width cross-signedness), container invariance, the join in both
|
||||
operand orders, the literal rule still standing, and the shift carve-out in
|
||||
both directions.
|
||||
- *Verified in a trial-merged tree, not only on the lane.* dev-loop moved
|
||||
eight times while this was open, and the acceptance rows, the full suite and
|
||||
the sweep were re-run against the last of them. The branch caught up by
|
||||
rebase until the notes file made that expensive — every commit of this lane
|
||||
touches FIX.org and so conflicted with every landing that also did — and
|
||||
finishes with an ordinary merge of dev-loop into the lane instead, resolved
|
||||
once. The merge back into dev-loop is clean, and was built, run and tested
|
||||
as a merged tree rather than only on the branch.
|
||||
- *The corpus sweep, base against lane.* Headless programs (test/programs/)
|
||||
were compiled, ~check~ed and run, and the diff of the whole lot is a single
|
||||
pure addition: widening.flan's own rows. Not one existing program's
|
||||
diagnostics, output or exit status moved.
|
||||
|
||||
The thirteen test programs that import ~vendor:raylib~ were not run either,
|
||||
for the same reason, and got the same treatment as examples/ below:
|
||||
~check~'s diagnostics are identical on both sides, LLVM ~emit~ is
|
||||
byte-identical, and the x86 difference is the prelude-line strings and
|
||||
nothing else.
|
||||
|
||||
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 — 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 ~<prelude>: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
|
||||
prelude line number makes both backends byte-identical everywhere.
|
||||
- A global-initialiser check by hand, both backends: a widened ~defvar~
|
||||
initialiser, a widened struct field in a struct literal, a widened array
|
||||
element, and a widened ~set~. The concern was that a ~Cast~ in an
|
||||
initialiser would stop being an LLVM constant; it does not, and the two
|
||||
backends print the same six lines. A ~defconst~ of a float *from* an integer
|
||||
constant is refused, with the existing "must be a compile-time constant"
|
||||
sentence — the folder is integers-only and says so.
|
||||
|
||||
** What this lane did not do
|
||||
- ~dyn~ is untouched in both directions.
|
||||
- No ~Vec~, slice or array element type converts, and nothing was added that
|
||||
could make one.
|
||||
- The ~@x86~ and ~@sanitize~ sweeps were not run; per the sweep policy they
|
||||
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 the context and puts it 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.
|
||||
|
||||
*The first version of that fix restored six chosen fields, and the choice was
|
||||
wrong.* Review round three found three more, and the worst of them inverts the
|
||||
symptom: where a leaked binding produces a false *accept*, a leaked window
|
||||
produces a false *refusal*.
|
||||
|
||||
- ~in_frames~. ~check_frames~ sets it, threads the expectation into the body's
|
||||
last form, and clears it on the way out. A trial abandoned inside that
|
||||
window leaves the flag stuck, so
|
||||
|
||||
: (println (+ i32-x (handler-bind [] i64-y)))
|
||||
: (return 0)
|
||||
|
||||
— which compiled before this lane and compiles again now — was refused with
|
||||
"return is not allowed inside handler-bind yet", pointing at a line with no
|
||||
~handler-bind~ within sight of it. A valid program refused for a reason that
|
||||
is not in the program.
|
||||
- ~loops~, the same window via ~loop~: a leaked ~Lrecur~ made an invalid
|
||||
~break~ answer "the nearest loop is a (loop ...), which answers with the
|
||||
value of its body" instead of "break is only allowed inside a loop". No bad
|
||||
accept, a thoroughly misleading refusal.
|
||||
- ~defer_block~, message text only, and leaked with ~loops~.
|
||||
|
||||
*So the subset was replaced by the whole record.* ~trial~ now restores every
|
||||
mutable field of ~ctx~ — the three above, the six from round two, and
|
||||
~defer_ok~, ~tail~ and ~outer_what~, which would self-heal on their own and
|
||||
are restored anyway, because "this one cannot currently leak" is precisely the
|
||||
reasoning that produced two rounds of leaks. The destructuring is closed and
|
||||
carries ~[@warning "+9"]~, so adding a field to ~ctx~ stops ~trial~ compiling
|
||||
until somebody decides about it. *Verified that the guard guards*: removing
|
||||
one field from the pattern by hand fails the build, naming the field.
|
||||
|
||||
One thing is deliberately not restored, and it is on ~env~ rather than ~ctx~:
|
||||
an abandoned trial that lifted a function out of an ~fn~ literal leaves it in
|
||||
~env.lifted~. That is dead and harmless — 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 into the module as a function nobody calls. Left because
|
||||
~env~ is the program's table rather than this form's, and rewinding it would
|
||||
mean deciding what else on ~env~ a trial may have touched; the one piece of
|
||||
~env~ state that genuinely needs rewinding, the generic instantiation cache,
|
||||
already rewinds itself in ~instantiate~.
|
||||
|
||||
All five symptoms pinned — the two accepts, the shadow, the unknown name, and
|
||||
the loop diagnostic.
|
||||
|
||||
*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.
|
||||
|
||||
@ -806,7 +806,8 @@ fact without cutting anything in half. See "The browser is the third target" bel
|
||||
**Three edits were made to sand.flan's own text** when it was ported, and they are language decisions rather than fixes:
|
||||
|
||||
- `(defconst gravity 0.05)` → `(defconst gravity f32 0.05)`. An untyped float constant is `f64`, `velocity` is `[f32]`,
|
||||
and there is no implicit widening.
|
||||
and `f64` into `f32` is a narrowing — still written, and still written after implicit widening landed (FIX.org
|
||||
2026-09-20), because widening is only the conversions that cannot change the number and this one can.
|
||||
- `(defvar current-color u32)` → `i32`. It is an index into `colors`, and `(len colors)` is an `i32`.
|
||||
- `(defn main [])` is unchanged — the short form, as plan.org says.
|
||||
|
||||
@ -3934,8 +3935,9 @@ compile-time constant*. Both of emit.ml's string emitters take the bytes and ign
|
||||
constant either way and this one is a constant a global can hold.
|
||||
|
||||
**Two spellings, not one form that changes type with its context.** Odin threads a `type_hint` everywhere and can
|
||||
afford `#load("p")` to mean a `string` here and a `[]u8` there. With structural equality, no implicit widening and no
|
||||
coercion anywhere, the same text meaning two types would be a wart, so `string` is written down when it is wanted. The
|
||||
afford `#load("p")` to mean a `string` here and a `[]u8` there. With structural equality and no conversion between one
|
||||
container and another — implicit widening is numbers only — the same text meaning two types would be a wart, so
|
||||
`string` is written down when it is wanted. The
|
||||
site's expectation is a fallback only and nothing depends on it.
|
||||
|
||||
**The path is a literal and resolves relative to the file the form is written in.** Both are Odin's rules and for
|
||||
|
||||
310
lib/check.ml
310
lib/check.ml
@ -20,6 +20,19 @@
|
||||
|
||||
let fail = Loc.fail
|
||||
|
||||
(* "A literal could not be built at the type this site asked for": 300 at a u8,
|
||||
1.5 at an i32, 3000000000 at the i32 an unconstrained integer defaults to.
|
||||
|
||||
It is kinded rather than left generic because one caller has to tell this
|
||||
refusal apart from every other one. [binary] retries a refused operand
|
||||
against the other operand's type (FIX.org 2026-09-20, implicit widening),
|
||||
and it must not retry *this* one: a literal takes its width from the other
|
||||
side and always could, so a literal that does not fit is the program's
|
||||
mistake and not a pair of types that failed to meet. Without the kind the
|
||||
retry turns (+ u8-thing 300) into i32 arithmetic, which is a different
|
||||
language from the one the author decided on. *)
|
||||
let literal_at_want = "check/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. *)
|
||||
@ -2035,12 +2048,19 @@ let unbox loc (want : Types.t) (e : Tast.expr) : Tast.expr =
|
||||
value was a bool, so what comes back is 0 or 1. *)
|
||||
widen loc Types.Bool (need "flan_dyn_need_bool" (Types.Int Types.I32))
|
||||
(* Every other width is refused rather than served by a need_i64 and a
|
||||
truncation. This language has no implicit narrowing anywhere, and putting
|
||||
one at the boundary where a value's type was *already* uncertain is the
|
||||
worst place in the program to start: the annotation would read as a check
|
||||
and would be a silent discard of the high bits. The ABI grows a per-width
|
||||
entry point when there is a reason to; until then the spelling that works
|
||||
is an i64 and an explicit conversion after it. *)
|
||||
truncation. Narrowing is written or it does not happen — that survives
|
||||
widening becoming implicit (FIX.org 2026-09-20) untouched, and this is the
|
||||
boundary where it matters most: the value's type was *already* uncertain
|
||||
here, so an annotation that quietly discarded the high bits would read as
|
||||
a check and be the opposite of one.
|
||||
|
||||
Nor does widening reach this arm from the other side. The box carries one
|
||||
integer width and one float width, so there is no narrower source here to
|
||||
widen from — a u32 want is asking the i64 in the box to fit in half of
|
||||
itself, which is the refusal above and not a conversion the lattice has.
|
||||
The ABI grows a per-width entry point when there is a reason to; until
|
||||
then the spelling that works is an i64 and a written conversion after
|
||||
it. *)
|
||||
| Types.Int _ | Types.Float _ ->
|
||||
no_dyn_yet loc ~into:false want
|
||||
(Printf.sprintf
|
||||
@ -2201,14 +2221,43 @@ let unbox_option ctx loc (t : Types.t) (got : Tast.expr) : Tast.expr =
|
||||
mk loc oty
|
||||
(Tast.Let ([ (s, got) ], [ mk loc oty (Tast.If (not_nil, some, none)) ]))
|
||||
|
||||
(* What a numeric mismatch has left to say, now that widening is silent.
|
||||
FIX.org 2026-09-20, "Implicit widening": every conversion that cannot change
|
||||
the number happens by itself, so a numeric pair that still reaches a refusal
|
||||
is one of exactly two things, and this tells them apart.
|
||||
|
||||
Either the wanted type is *narrower* — the conversion can lose, which is
|
||||
what the language has always refused to do without being told, and the
|
||||
sentence names the cast and points out that the other direction needed
|
||||
nothing. Or there is no direction at all: i32 and u32 are the same width and
|
||||
each holds values the other cannot, so neither widens and the program has to
|
||||
say which half it means to keep.
|
||||
|
||||
Written once and used by both refusals that can report one — [expect]'s, and
|
||||
the binary operators' when their two operands have no join. *)
|
||||
let numeric_note ~(want : Types.t) ~(got : Types.t) =
|
||||
if not (Types.is_numeric want && Types.is_numeric got) then ""
|
||||
else if Types.widens_to ~from:want ~into:got then
|
||||
Printf.sprintf
|
||||
" — %s into %s can lose, so it has to be written: (%s x). The other way \
|
||||
round, %s widens into %s by itself"
|
||||
(Types.to_string got) (Types.to_string want) (Types.to_string want)
|
||||
(Types.to_string want) (Types.to_string got)
|
||||
else
|
||||
Printf.sprintf
|
||||
" — neither widens into the other, so the conversion has to be written: \
|
||||
(%s x)"
|
||||
(Types.to_string want)
|
||||
|
||||
let expect ctx loc ~want (got : Tast.expr) =
|
||||
match want with
|
||||
| None -> got
|
||||
| Some w ->
|
||||
(* The boundary, and the only implicit conversion in the language. It runs
|
||||
before [fits] rather than instead of it: what comes back is an ordinary
|
||||
expression of the wanted type, and if the coercion did not produce one
|
||||
the usual message is still the one that reports it. *)
|
||||
(* The boundary: where a wanted type meets a produced one, and the one
|
||||
place the language's implicit conversions live. It runs before [fits]
|
||||
rather than instead of it: what comes back is an ordinary expression of
|
||||
the wanted type, and if the coercion did not produce one the usual
|
||||
message is still the one that reports it. *)
|
||||
let got =
|
||||
match w, got.Tast.ty with
|
||||
| Types.Dyn, Types.Dyn -> got
|
||||
@ -2226,6 +2275,19 @@ let expect ctx loc ~want (got : Tast.expr) =
|
||||
(Types.to_string w)
|
||||
| _, Types.Dyn when Types.fits ~expected:w ~actual:Types.Dyn -> got
|
||||
| _, Types.Dyn -> unbox loc w got
|
||||
(* 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 defvar with a type, a struct field
|
||||
initialiser, a push into a Vec and a C import's parameter all get it
|
||||
here at once and none of them had to learn about it.
|
||||
|
||||
The conversion is performed, not waved through: [widen] emits the same
|
||||
[Cast] node the written (i64 x) emits, so the backends sext or zext by
|
||||
the *source* type's signedness and nothing downstream sees a node
|
||||
whose type disagrees with its bits. [widens_to] is what keeps that
|
||||
honest — it admits only conversions that cannot change the number, so
|
||||
the cast this inserts is one no program can tell happened. *)
|
||||
| _ when Types.widens_to ~from:got.Tast.ty ~into:w -> widen loc w got
|
||||
| _ -> got
|
||||
in
|
||||
if Types.fits ~expected:w ~actual:got.Tast.ty then got
|
||||
@ -2233,9 +2295,15 @@ let expect ctx loc ~want (got : Tast.expr) =
|
||||
(* Kinded so that the one caller who knows more — a call argument, which
|
||||
can name the function and the parameter — can recognise this exact
|
||||
refusal at this exact span and say the rest. Every other reader of a
|
||||
diagnostic ignores [kind]. *)
|
||||
Loc.failk "check/type-mismatch" loc "expected %s, found %s"
|
||||
diagnostic ignores [kind].
|
||||
|
||||
[numeric_note] is the rest of the sentence when both sides are
|
||||
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"
|
||||
(Types.to_string w) (Types.to_string got.Tast.ty)
|
||||
(numeric_note ~want:w ~got:got.Tast.ty)
|
||||
|
||||
(* 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
|
||||
@ -2646,7 +2714,7 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
|
||||
match want with
|
||||
| Some (Types.Float k) -> k
|
||||
| Some other when other <> Types.Never ->
|
||||
fail loc "expected %s, found the float literal %g"
|
||||
Loc.failk literal_at_want loc "expected %s, found the float literal %g"
|
||||
(Types.to_string other) x
|
||||
| _ -> Types.F64
|
||||
in
|
||||
@ -2993,7 +3061,7 @@ and int_literal loc ~want ?(default = Types.I32) n =
|
||||
| Some (Types.Float k) ->
|
||||
mk loc (Types.Float k) (Tast.Float (Int64.to_float n, k))
|
||||
| Some other when other <> Types.Never ->
|
||||
fail loc "expected %s, found the integer literal %Ld"
|
||||
Loc.failk literal_at_want loc "expected %s, found the integer literal %Ld"
|
||||
(Types.to_string other) n
|
||||
| _ -> mk loc (Types.Int default) (Tast.Int (in_range loc default n, default))
|
||||
|
||||
@ -3020,7 +3088,8 @@ and in_range loc k n =
|
||||
&& Int64.compare n (Int64.shift_left 1L bits) < 0
|
||||
in
|
||||
if ok then n
|
||||
else fail loc "%Ld does not fit in %s" n (Types.ikind_name k)
|
||||
else Loc.failk literal_at_want loc "%Ld does not fit in %s" n
|
||||
(Types.ikind_name k)
|
||||
|
||||
(* The arms that are names rather than calls, and the same rule holds for them:
|
||||
each is in [builtins] below, and test_flan reads this match to check it. *)
|
||||
@ -5453,8 +5522,10 @@ and named_call ctx ~want loc name args =
|
||||
(* Same truthiness as [if]: a dyn argument is negated on nil/false vs.
|
||||
everything else, not narrowed to a strict bool first. *)
|
||||
prim Tast.Not Types.Bool [ check_truthy ctx (List.hd args) ]
|
||||
(* Bitwise operators are integers-only, and the shift count has the same type
|
||||
as the value shifted — there is no implicit widening anywhere else either. *)
|
||||
(* Bitwise operators are integers-only. They take the ordinary join — an
|
||||
operand that widens into the other does, so (bit-and u8-flags u32-mask) is
|
||||
a u32 and — and the shifts below do not, which is the one carve-out
|
||||
widening has (FIX.org 2026-09-20). *)
|
||||
| "bit-and" | "bit-or" | "bit-xor" ->
|
||||
let p = match name with
|
||||
| "bit-and" -> Tast.BitAnd | "bit-or" -> Tast.BitOr
|
||||
@ -5465,11 +5536,20 @@ and named_call ctx ~want loc name args =
|
||||
(function Types.Int _ -> true | _ -> false) "integers" args
|
||||
(* The shifts stay at two, and not only because a shift chain reads badly:
|
||||
each count would be checked against the same width below, so (<< x 30 30)
|
||||
would pass two legal shifts and still shift the value away entirely. *)
|
||||
would pass two legal shifts and still shift the value away entirely.
|
||||
|
||||
[~join:false] is the one place widening is deliberately not symmetric.
|
||||
The count still widens *to* the value's type — (<< i64-x u8-n) is fine —
|
||||
but the value never widens to the count's, which the general rule would do
|
||||
for (<< u8-x i32-n). It would be the wrong answer twice over: the result's
|
||||
type and the width the shift wraps at would be taken from a number that is
|
||||
only saying how far, and the range check just below, along with [emit]'s
|
||||
mask, is keyed to the *value's* width. A count wider than the value is
|
||||
refused and is told to write the cast. *)
|
||||
| "<<" | ">>" ->
|
||||
let p = if String.equal name "<<" then Tast.Shl else Tast.Shr in
|
||||
arity ctx loc name 2 args;
|
||||
let a, b = binary ctx name loc ~want:(numeric_want want) args in
|
||||
let a, b = binary ctx ~join:false name loc ~want:(numeric_want want) args in
|
||||
(match a.Tast.ty with
|
||||
| Types.Int _ -> ()
|
||||
| other -> fail loc "%s takes integers, found %s" name
|
||||
@ -6466,9 +6546,11 @@ and named_call ctx ~want loc name args =
|
||||
let as_bytes () = mk loc (Types.Slice (Types.Int Types.U8)) (Tast.Str data) in
|
||||
(* Two spellings rather than one that changes type with its context.
|
||||
Odin threads a type_hint everywhere and can afford (embed "p") to
|
||||
mean a string here and a []u8 there; with structural equality and no
|
||||
implicit widening anywhere, the same text meaning two types would be
|
||||
a wart. [want] is a fallback only, and nothing depends on it. *)
|
||||
mean a string here and a []u8 there; with structural equality and a
|
||||
container that never converts to another container -- implicit
|
||||
widening is numbers only, FIX.org 2026-09-20 -- the same text meaning
|
||||
two types would be a wart. [want] is a fallback only, and nothing
|
||||
depends on it. *)
|
||||
(match args with
|
||||
| [ _; { Ast.e = Ast.Var "string"; _ } ] ->
|
||||
expect ctx loc ~want (as_string ())
|
||||
@ -7506,11 +7588,133 @@ and byte_slice ctx (a : Ast.expr) =
|
||||
and numeric_want want =
|
||||
match want with Some (Types.Int _ | Types.Float _) -> want | _ -> None
|
||||
|
||||
(* Both operands of a binary operator have one type, and there is no implicit
|
||||
widening, so one side has to decide it. Check the side that carries the most
|
||||
information first: a non-literal over a literal, and a float literal over an
|
||||
integer one, since an integer constant converts to a float and not back. *)
|
||||
and binary ctx ?(dyn_ok = false) name loc ~want args =
|
||||
(* Both operands of a binary operator have one type, so one side has to decide
|
||||
it. Check the side that carries the most information first: a non-literal
|
||||
over a literal, and a float literal over an integer one, since an integer
|
||||
constant converts to a float and not back.
|
||||
|
||||
Widening (FIX.org 2026-09-20) does not retire that rule, it finishes it.
|
||||
Three things decide, in this order:
|
||||
|
||||
1. An expectation, if the site has one, and it reaches *both* operands. So
|
||||
(defn f [] i64 (+ a b)) over two i32s widens each operand and adds at
|
||||
i64, rather than adding at i32 and widening the sum. That is the better
|
||||
of the two readings and it costs nothing to prefer it, because no program
|
||||
that compiled before can reach it — the pair used to be a refusal.
|
||||
2. A literal, exactly as before: it takes its width from the other operand,
|
||||
so (+ x 1) over a u64 x is still u64 arithmetic and (let [h fnv-offset])
|
||||
over a u64 defconst still means what it meant. [needs_want] is what marks
|
||||
the forms this applies to and it is untouched.
|
||||
3. Otherwise the *wider* side decides — [Types.join], whichever operand the
|
||||
other widens into, with a [Cast] put on the narrower one. (+ i32-var
|
||||
i64-var) is an i64 add. Equal width across signedness has no join, by
|
||||
construction: neither i32 nor u32 widens into the other, and the refusal
|
||||
says which cast to write.
|
||||
|
||||
The mechanism for 3 is a *trial*: ask y for [a]'s type, and if that refusal
|
||||
is the one widening was invented for, look again the other way round. Two
|
||||
things have to be true for a trial to be honest, and both are below.
|
||||
|
||||
[trial] is the first. Checking is not a function of its argument — it
|
||||
allocates frame slots and it opens scopes — so a check that is abandoned
|
||||
has to leave no trace, and [scoped] cannot help: it restores the scope on
|
||||
the way *out*, which an exception does not take. Without this a binding
|
||||
from the abandoned pass outlives it, which is visible as a name that should
|
||||
be unknown resolving anyway, and worse, as a shadow: the inner binding of
|
||||
(let [t ...] ... (let [t ...] t) ... t) survives into the outer t's slot
|
||||
with nothing ever stored in it. That is an uninitialised read, produced by
|
||||
a program the compiler accepted.
|
||||
|
||||
[literal_at_want] is the second. A trial that refused because a *literal*
|
||||
could not be built at the wanted type is not a pair of types that failed to
|
||||
meet — the literal had no type of its own to bring — so looking again would
|
||||
answer with the literal's default and quietly move (+ u8-thing 300) to i32.
|
||||
Rule 2 above is not a description of the old language kept for continuity;
|
||||
it is what the author decided, and the kind is how the trial obeys it. *)
|
||||
and trial ctx f =
|
||||
(* Everything a check writes into the context, put back if the check is
|
||||
abandoned — and it is *everything* on purpose, not a chosen subset.
|
||||
|
||||
Picking the fields that looked like they mattered was tried twice and was
|
||||
wrong twice. [scope] and the slot fields were the first round, found as an
|
||||
uninitialised read. The second round was worse, because the symptom was
|
||||
the other way up: a form that opens a window and closes it on the way out
|
||||
— [check_frames] setting [in_frames], [loop] pushing onto [loops] — leaves
|
||||
that window *open* when a trial inside it is abandoned, and then refuses
|
||||
a perfectly good program.
|
||||
|
||||
(println (+ i32-x (handler-bind [] i64-y)))
|
||||
(return 0)
|
||||
|
||||
compiled before this lane and was refused after it, with "return is not
|
||||
allowed inside handler-bind yet" pointing at a line with no handler-bind
|
||||
anywhere near it. A false refusal is not a lesser bug than a false accept;
|
||||
it is just quieter about being one.
|
||||
|
||||
So the rule here is not judgement, it is the whole record. Three fields
|
||||
would have self-healed anyway — [defer_ok] and [tail] are read and cleared
|
||||
on entry to [check], [outer_what] is never written after the context is
|
||||
built — and they are restored regardless, because "this one cannot
|
||||
currently leak" is exactly the reasoning that produced two rounds of
|
||||
leaks. The destructuring below is closed and warning 9 is turned on for
|
||||
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 already rolls itself back, in [instantiate].
|
||||
|
||||
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
|
||||
resource failure into a wrong answer. *)
|
||||
let[@warning "+9"] { env = _; ret = _; slots; slot_tys; slot_names; scope;
|
||||
defers; defer_slot; defer_ok; defer_block; outer = _;
|
||||
outer_what; in_frames; loops; tail; in_defer;
|
||||
owner = _ } = ctx in
|
||||
match f () with
|
||||
| r -> Ok r
|
||||
| exception Loc.Error d ->
|
||||
ctx.slots <- slots; ctx.slot_tys <- slot_tys;
|
||||
ctx.slot_names <- slot_names; ctx.scope <- scope;
|
||||
ctx.defers <- defers; ctx.defer_slot <- defer_slot;
|
||||
ctx.defer_ok <- defer_ok; ctx.defer_block <- defer_block;
|
||||
ctx.outer_what <- outer_what; ctx.in_frames <- in_frames;
|
||||
ctx.loops <- loops; ctx.tail <- tail; ctx.in_defer <- in_defer;
|
||||
Error d
|
||||
|
||||
(* 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
|
||||
having a second opinion on. *)
|
||||
and reconsiderable (d : Loc.diag) = not (String.equal d.Loc.kind literal_at_want)
|
||||
|
||||
(* [a] was checked, y refused [a]'s type, and [b] is y on its own terms — held
|
||||
by the caller when it has one, taken here when it does not. If the pair has
|
||||
a join it can only be [b]'s type (had it been [a]'s, the trial would have
|
||||
passed), so [a] is the operand that moves. *)
|
||||
and join_widen (a : Tast.expr) (b : Tast.expr) =
|
||||
match Types.join a.Tast.ty b.Tast.ty with
|
||||
| Some t when not (Types.equal t a.Tast.ty) ->
|
||||
Some (widen a.Tast.loc t a, widen b.Tast.loc t b)
|
||||
| _ -> None
|
||||
|
||||
and join_pair ctx (a : Tast.expr) (y : Ast.expr) (d : Loc.diag) =
|
||||
(* Check y on its own terms to find out whether it was simply the wider
|
||||
operand. This trial is guarded too: if y cannot check without an
|
||||
expectation at all — [None], [(zeroed)] — the original refusal is the one
|
||||
reported, so no form loses the expectation it used to get. *)
|
||||
match trial ctx (fun () -> check ctx y) with
|
||||
| Error _ -> raise (Loc.Error d)
|
||||
| Ok b ->
|
||||
(match join_widen a b with
|
||||
| Some pair -> pair
|
||||
| None -> raise (Loc.Error d))
|
||||
|
||||
and binary ctx ?(dyn_ok = false) ?(join = true) name loc ~want args =
|
||||
match args with
|
||||
| [ x; y ] ->
|
||||
let y_decides =
|
||||
@ -7556,12 +7760,36 @@ and binary ctx ?(dyn_ok = false) name loc ~want args =
|
||||
if a.Tast.ty = Types.Dyn || b.Tast.ty = Types.Dyn
|
||||
|| Types.equal a.Tast.ty b.Tast.ty
|
||||
then a, b
|
||||
else a, check ctx ~want:a.Tast.ty y
|
||||
(* Asking y for [a]'s type stays the first thing tried, and not only for
|
||||
continuity: y was checked above with no expectation at all, and an
|
||||
expectation is information. A sum of two products handed to an f32
|
||||
function is the case — test/programs/math.flan does it — because every
|
||||
literal inside those products defaults to f64 on its own terms, so
|
||||
reading the join off the two unexpected halves would answer f64 for a
|
||||
form the site asked to be f32. The re-check builds them at f32 as it
|
||||
always did.
|
||||
|
||||
[b] is only used when that re-check refuses, which is the direction
|
||||
[expect] cannot serve: a is the narrower operand and it is the one
|
||||
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
|
||||
| Ok b' -> a, b'
|
||||
| Error d ->
|
||||
(match
|
||||
if join && reconsiderable d then join_widen a b else None
|
||||
with
|
||||
| Some pair -> pair
|
||||
| None -> raise (Loc.Error d)))
|
||||
end
|
||||
else begin
|
||||
let a = check ctx ?want x in
|
||||
let b = check ctx ~want:a.Tast.ty y in
|
||||
a, b
|
||||
match trial ctx (fun () -> check ctx ~want:a.Tast.ty y) with
|
||||
| Ok b -> a, b
|
||||
| Error d ->
|
||||
if join && reconsiderable d then join_pair ctx a y d
|
||||
else raise (Loc.Error d)
|
||||
end
|
||||
| _ -> fail loc "%s takes two arguments" name
|
||||
|
||||
@ -7594,8 +7822,9 @@ and binary ctx ?(dyn_ok = false) name loc ~want args =
|
||||
let builtins : (string * string * string) list =
|
||||
[ (* arithmetic and comparison *)
|
||||
("+", "+ [numeric? ...] numeric?",
|
||||
"Sum, folded left over two or more operands that share one numeric \
|
||||
type — nothing widens implicitly.");
|
||||
"Sum, folded left over two or more operands. Two operands of different \
|
||||
numeric types meet at the wider one when that cannot lose — i32 and i64 \
|
||||
add at i64 — and i32 with u32 has no such type and is refused.");
|
||||
("-", "- [numeric? ...] numeric?",
|
||||
"Difference, folded left: (- a b c) is ((a - b) - c).");
|
||||
("*", "* [numeric? ...] numeric?",
|
||||
@ -7620,20 +7849,23 @@ let builtins : (string * string * string) list =
|
||||
("not", "not [bool] bool",
|
||||
"Negates a bool. Nothing else in this language is a truth value.");
|
||||
("bit-and", "bit-and [int ...] int",
|
||||
"Bitwise and, folded left. Integers only, and every operand has the \
|
||||
same width.");
|
||||
"Bitwise and, folded left. Integers only; operands of different widths \
|
||||
meet at the wider one, the way + does.");
|
||||
("bit-or", "bit-or [int ...] int", "Bitwise or, folded left over integers.");
|
||||
("bit-xor", "bit-xor [int ...] int",
|
||||
"Bitwise exclusive or, folded left over integers.");
|
||||
("<<", "<< [int int] int",
|
||||
"Left shift. The count has the shifted value's own type, and a literal \
|
||||
count at or past its width is refused — LLVM calls that poison.");
|
||||
"Left shift. The value's type decides — a narrower count widens to it, a \
|
||||
wider one is refused — and a literal count at or past the value's width \
|
||||
is refused too, because LLVM calls that poison.");
|
||||
(">>", ">> [int int] int",
|
||||
"Right shift, by a count of the value's own type; a literal count at or \
|
||||
past the width is refused, as it is for <<.");
|
||||
"Right shift. The value's type decides and the count widens to it, never \
|
||||
the reverse; a literal count at or past the width is refused, as it is \
|
||||
for <<.");
|
||||
("min", "min [ordered? ...] ordered?",
|
||||
"The smallest of two or more operands, each of them evaluated exactly \
|
||||
once however many there are.");
|
||||
once however many there are. Two widths meet at the wider: (min i8-x \
|
||||
i16-y) is an i16.");
|
||||
("max", "max [ordered? ...] ordered?",
|
||||
"The largest of two or more operands, each evaluated exactly once.");
|
||||
("zeroed", "zeroed [] T",
|
||||
|
||||
@ -31,12 +31,14 @@
|
||||
is strictly the better call for every one of them. [print] is the same walk
|
||||
as [println] without the trailing newline, so it covers the no-newline case
|
||||
that was the family's remaining excuse (see [show] in
|
||||
test/programs/slices.flan). And because this language has no implicit
|
||||
widening, [(print-i64 x)] forced an explicit [(i64 x)] at every site;
|
||||
[(print x)] takes the value as it is. That is not only shorter: the cast
|
||||
through the signed printer turned a [u64] above 2^63 into a negative
|
||||
number, where [print] routes it through [flan_u64_to_bytes] and prints what
|
||||
it actually holds. *)
|
||||
test/programs/slices.flan). And [(print-i64 x)] forced an explicit
|
||||
[(i64 x)] at every site, where [(print x)] takes the value as it is. That
|
||||
is not only shorter: the cast through the signed printer turned a [u64]
|
||||
above 2^63 into a negative number, where [print] routes it through
|
||||
[flan_u64_to_bytes] and prints what it actually holds. Implicit widening
|
||||
(FIX.org 2026-09-20) would have removed the cast at a [u8] or an [i32] site
|
||||
on its own, but not at that one -- a [u64] widens into nothing at all, and
|
||||
the printer it was being forced through was the wrong one. *)
|
||||
|
||||
let source = {flan|
|
||||
;; The condition every allocating operation signals when the allocator cannot
|
||||
@ -470,17 +472,20 @@ let source = {flan|
|
||||
;; sum is the one shape a type variable cannot express, and it is worth being
|
||||
;; precise about why rather than leaving two near-identical functions looking
|
||||
;; like an oversight. Each of these *widens*: sum-i32 accumulates in i64 and
|
||||
;; sum-f32 in f64, with an explicit cast per element, because there is no
|
||||
;; implicit widening anywhere in the language and summing a screenful into the
|
||||
;; element's own type is how a total silently wraps or absorbs. "The wider
|
||||
;; sum-f32 in f64, because summing a screenful into the element's own type is
|
||||
;; how a total silently wraps or absorbs. The per-element casts no longer have
|
||||
;; to be written to say so — an i32 widens into an i64 by itself, FIX.org
|
||||
;; 2026-09-20 — and they stay because what these two functions exist to show is
|
||||
;; that the accumulator is a different type from the element. "The wider
|
||||
;; type $t accumulates into" is a function from types to types — an associated
|
||||
;; type, or a constraint system of a kind {:where} is not — and a generic sum
|
||||
;; that took its accumulator and its + as parameters would be reduce, which is
|
||||
;; above.
|
||||
|
||||
;; Accumulates in i64 and each element is widened explicitly — there is no
|
||||
;; implicit widening anywhere in the language, and summing a screenful of i32
|
||||
;; into an i32 is how a total silently wraps.
|
||||
;; Accumulates in i64, because summing a screenful of i32 into an i32 is how a
|
||||
;; total silently wraps. The per-element (i64 ...) would happen on its own now;
|
||||
;; it is written to keep the accumulator's type visible at the line that feeds
|
||||
;; it.
|
||||
(defn sum-i32 [s [i32]] i64
|
||||
(let [t (i64 0)]
|
||||
(dotimes [i (len s)]
|
||||
|
||||
67
lib/types.ml
67
lib/types.ml
@ -9,8 +9,11 @@
|
||||
have to have it. That rejection lives in [Check]; this module only names
|
||||
the shape. *)
|
||||
|
||||
(* Machine integer types. Signedness and width are both part of the type —
|
||||
there is no implicit widening anywhere, per plan.org. *)
|
||||
(* Machine integer types. Signedness and width are both part of the type, and
|
||||
two of them are the same type only when both halves match. A value may move
|
||||
to a type that cannot lose it — see [widens_to] at the bottom of this file,
|
||||
FIX.org 2026-09-20 — and never the other way: narrowing is written or it
|
||||
does not happen. *)
|
||||
type ikind = I8 | I16 | I32 | I64 | U8 | U16 | U32 | U64
|
||||
|
||||
type fkind = F32 | F64
|
||||
@ -115,9 +118,13 @@ let ikind_name k =
|
||||
|
||||
let fkind_name = function F32 -> "f32" | F64 -> "f64"
|
||||
|
||||
(* Structural equality is the whole story: no subtyping, no coercion between
|
||||
machine types, no variance. Written out rather than using [=] so that adding
|
||||
a case with a function or a mutable field cannot silently break it. *)
|
||||
(* Structural equality is the whole story for *identity*: no subtyping, no
|
||||
variance, and nothing here bends to admit a conversion. Implicit widening
|
||||
(below) is deliberately not expressed as a loosening of this function or of
|
||||
[fits] — it is a separate predicate that every caller must pair with a
|
||||
[Cast] on the value, so a node's type never lies about the bits it holds.
|
||||
Written out rather than using [=] so that adding a case with a function or
|
||||
a mutable field cannot silently break it. *)
|
||||
let rec equal a b =
|
||||
match a, b with
|
||||
| Int x, Int y -> x = y
|
||||
@ -202,3 +209,53 @@ let is_equatable = function String -> true | t -> is_comparable t
|
||||
place anything resembling subtyping exists. *)
|
||||
let fits ~expected ~actual =
|
||||
match actual with Never -> true | _ -> equal expected actual
|
||||
|
||||
(* ── Implicit widening, FIX.org 2026-09-20 ────────────────────────────
|
||||
Which numeric types a value may move to without the program saying so.
|
||||
One rule decides every entry: the conversion is admitted exactly when no
|
||||
value of the source type can come out the other side as a different number.
|
||||
Narrowing is not on this list and never will be — [(u32 x)] is how an i64
|
||||
becomes a u32, because that one can lose.
|
||||
|
||||
Read out of that rule:
|
||||
|
||||
- Same signedness, strictly wider: i8→i16→i32→i64, u8→u16→u32→u64.
|
||||
- Unsigned into a strictly wider signed: u8→i16, u8/u16→i32, u8/u16/u32→i64.
|
||||
Every u32 fits in an i64, so nothing is lost. The mirror never holds:
|
||||
signed into unsigned drops the negatives, at any width.
|
||||
- Equal width across signedness (i32→u32, u32→i32) is refused for the same
|
||||
reason — one of the two halves of the range has nowhere to go.
|
||||
- f32→f64.
|
||||
- Integer into float only where the float's significand covers the integer
|
||||
exactly: f64 has 53 bits, so i8/i16/i32/u8/u16/u32 reach it and i64/u64 do
|
||||
not (2^53+1 is not an f64); f32 has 24, so only i8/i16/u8/u16 reach it.
|
||||
Odin is looser here and lets any integer into any float. This is the
|
||||
tighter rule on purpose: a program that wants the lossy one writes (f64 x)
|
||||
and says so, and loosening later adds programs where tightening later
|
||||
would break them.
|
||||
|
||||
Nothing else participates. [Bool] is not a number, an [Enum] is its own type
|
||||
whose whole point is that a bare integer does not fit it, [Dyn] crosses by
|
||||
boxing and unboxing rather than by this, and a container is invariant: a
|
||||
[Vec i32] is not a [Vec i64] and a [[i32]] is not a [[i64]], because the
|
||||
elements would each have to be rewritten and a slice does not own its
|
||||
bytes. *)
|
||||
let widens_to ~(from : t) ~(into : t) =
|
||||
match from, into with
|
||||
| Int a, Int b ->
|
||||
if signed a = signed b then bits b > bits a
|
||||
else (not (signed a)) && signed b && bits b > bits a
|
||||
| Float F32, Float F64 -> true
|
||||
| Int a, Float b -> bits a <= (match b with F64 -> 32 | F32 -> 16)
|
||||
| _ -> false
|
||||
|
||||
(* The type a binary operator's two operands meet at: whichever of the pair the
|
||||
other one widens into, and nothing otherwise. That is total and it is not a
|
||||
real lattice — (i32, u32) has no answer here, and inventing i64 for it would
|
||||
be picking a type neither operand was written at. Equal types answer
|
||||
themselves, so a caller can use this without checking for that first. *)
|
||||
let join a b =
|
||||
if equal a b then Some a
|
||||
else if widens_to ~from:a ~into:b then Some b
|
||||
else if widens_to ~from:b ~into:a then Some a
|
||||
else None
|
||||
|
||||
@ -1468,10 +1468,12 @@ int64_t flan_dyn_need_i64(flan_dyn v) {
|
||||
}
|
||||
|
||||
/* A float, and an int is not one. Refusing the widening is the decision, not
|
||||
* an omission: typed Flan has no implicit widening anywhere — [(print-i64 x)]
|
||||
* used to force an explicit [(i64 x)] at every site — and a boundary that
|
||||
* quietly turned an int into a float would be the one place in the language
|
||||
* where a *value* changed type without anybody writing it down. The dyn
|
||||
* an omission. The typed language does widen an integer into a float, but only
|
||||
* where the float holds every value of it exactly — an i32 into an f64, never
|
||||
* an i64 (FIX.org 2026-09-20). This boundary has no such guarantee to offer:
|
||||
* the box carries one integer width and it is i64, so "an int here" means the
|
||||
* widest one, which is exactly the conversion the typed lattice refuses. The
|
||||
* dyn
|
||||
* *operators* promote, because arithmetic between a 2 and a 2.5 has an obvious
|
||||
* answer and refusing it makes dynamic code worse; the boundary into a typed
|
||||
* f64 parameter does not, because there the annotation is somebody's stated
|
||||
|
||||
@ -112,10 +112,12 @@ flan_dyn flan_dyn_vec_new(void) {
|
||||
/* ── Arithmetic ────────────────────────────────────────────────────── */
|
||||
|
||||
/* Two numbers promote to f64 when either is one, which is the rule a reader
|
||||
* expects of a dynamic language and is not the rule the typed language uses.
|
||||
* The typed language has no implicit widening at all; here there is no
|
||||
* annotation to have been written, so refusing would leave (+ 1 2.5) with no
|
||||
* spelling that works. */
|
||||
* expects of a dynamic language and is still not the rule the typed language
|
||||
* uses. The typed side widens only where nothing can be lost, and an i64 into
|
||||
* an f64 can (FIX.org 2026-09-20), so (+ i64-x 2.5) is written there and is
|
||||
* promoted here. The difference is not an oversight on either side: here there
|
||||
* is no annotation to have been written, so refusing would leave (+ 1 2.5)
|
||||
* with no spelling that works. */
|
||||
static int numeric(cell *c) { return c->tag == T_I64 || c->tag == T_F64; }
|
||||
static double as_f(cell *c) { return c->tag == T_I64 ? (double)c->u.i : c->u.f; }
|
||||
|
||||
|
||||
@ -23,8 +23,9 @@
|
||||
(print (string a))) ; hello from a
|
||||
|
||||
;; `string` is the second spelling, not a different meaning for the same
|
||||
;; text. With structural equality and no implicit widening, one form that
|
||||
;; changes type with its context would be a wart.
|
||||
;; text. With structural equality and nothing that converts one container
|
||||
;; into another -- implicit widening is numbers only -- one form that changes
|
||||
;; type with its context would be a wart.
|
||||
(println (embed "assets/b.bin" string)) ; BBB
|
||||
|
||||
;; Byte-exact, including bytes no text encoding would survive: emit.ml's
|
||||
|
||||
109
test/programs/widening.flan
Normal file
109
test/programs/widening.flan
Normal file
@ -0,0 +1,109 @@
|
||||
;;;; Implicit widening, and the only thing worth pinning about it: the bits.
|
||||
;;;; FIX.org 2026-09-20, "Implicit widening".
|
||||
;;;;
|
||||
;;;; A widening conversion is admitted exactly when it cannot change the
|
||||
;;;; number, so every row here has an answer that is also the answer the source
|
||||
;;;; type had. Which means the test is entirely about the *emitted* cast being
|
||||
;;;; the right one: a sign-extension where the source is signed, a
|
||||
;;;; zero-extension where it is not, and the float conversions picking sitofp
|
||||
;;;; against uitofp by the same rule. Each of those is a separate instruction
|
||||
;;;; on both backends and choosing the wrong one gives a wrong number rather
|
||||
;;;; than a wrong type, which no type test would catch.
|
||||
;;;;
|
||||
;;;; The rows are picked so that a mistake is visible in the printed value:
|
||||
;;;;
|
||||
;;;; -5 i8 to i64 sext; a zext prints 251
|
||||
;;;; -1 i32 to i64 sext; a zext prints 4294967295
|
||||
;;;; 255 u8 to i16 zext; a sext prints -1
|
||||
;;;; 4000000000 u32 zext to i64; a sext prints -294967296
|
||||
;;;; 4294967295 u32 to f64, exact; a signed conversion prints -1
|
||||
;;;; -2000000000 i32 to f64; a uitofp prints 2294967296
|
||||
;;;;
|
||||
;;;; Everything goes through a global rather than a literal, because a literal
|
||||
;;;; is built at the wanted width by the literal rule and would never reach a
|
||||
;;;; cast at all.
|
||||
|
||||
(defvar w-i8neg i8 -5)
|
||||
(defvar w-i8pos i8 127)
|
||||
(defvar w-i16neg i16 -300)
|
||||
(defvar w-i32neg i32 -2000000000)
|
||||
(defvar w-i32one i32 1)
|
||||
(defvar w-i32all i32 -1)
|
||||
(defvar w-u8max u8 255)
|
||||
(defvar w-u16max u16 65535)
|
||||
(defvar w-u32big u32 4000000000)
|
||||
(defvar w-u32max u32 4294967295)
|
||||
(defvar w-i64big i64 5000000000)
|
||||
(defvar w-f32half f32 0.5)
|
||||
|
||||
;; Widening at a parameter. Each of these is a plain typed function and the
|
||||
;; call sites below hand it a narrower type with no cast written anywhere.
|
||||
(defn w-take-i64 [x i64] i64 x)
|
||||
(defn w-take-i16 [x i16] i16 x)
|
||||
(defn w-take-u64 [x u64] u64 x)
|
||||
(defn w-take-f64 [x f64] f64 x)
|
||||
(defn w-take-f32 [x f32] f32 x)
|
||||
|
||||
;; Widening at a return position: the body is an i32 and the signature is i64.
|
||||
(defn w-ret-widened [] i64 w-i32neg)
|
||||
|
||||
;; Widening in a binary operator, both orders. The first is the direction
|
||||
;; [expect] already served; the second is the one the join rule added.
|
||||
(defn w-add-wide-first [] i64 (+ w-i64big w-i32one))
|
||||
(defn w-add-narrow-first [] i64 (+ w-i32one w-i64big))
|
||||
|
||||
(defn main [args [string]] i32
|
||||
;; ── integer to integer ──────────────────────────────────────────
|
||||
(println (w-take-i64 w-i8neg)) ;; -5
|
||||
(println (w-take-i64 w-i8pos)) ;; 127
|
||||
(println (w-take-i64 w-i16neg)) ;; -300
|
||||
(println (w-take-i64 w-i32all)) ;; -1
|
||||
(println (w-take-i64 w-i32neg)) ;; -2000000000
|
||||
(println (w-take-i16 w-u8max)) ;; 255
|
||||
(println (w-take-i64 w-u8max)) ;; 255
|
||||
(println (w-take-i64 w-u16max)) ;; 65535
|
||||
(println (w-take-i64 w-u32big)) ;; 4000000000
|
||||
(println (w-take-i64 w-u32max)) ;; 4294967295
|
||||
(println (w-take-u64 w-u32big)) ;; 4000000000
|
||||
(println (w-take-u64 w-u8max)) ;; 255
|
||||
|
||||
;; ── a widened return ────────────────────────────────────────────
|
||||
(println (w-ret-widened)) ;; -2000000000
|
||||
|
||||
;; ── integer to float, exact only ────────────────────────────────
|
||||
(println (w-take-f64 w-i32neg)) ;; -2000000000.0
|
||||
(println (w-take-f64 w-u32max)) ;; 4294967295.0
|
||||
(println (w-take-f64 w-i8neg)) ;; -5.0
|
||||
(println (w-take-f32 w-i16neg)) ;; -300.0
|
||||
(println (w-take-f32 w-u16max)) ;; 65535.0
|
||||
|
||||
;; The printer answers %g, which rounds an f64 long before the bits it is
|
||||
;; carrying run out, so the exactness the int-to-float boundary is chosen for
|
||||
;; is asserted by subtraction rather than by reading the digits. Each of
|
||||
;; these is the difference between the widened value and the number it is
|
||||
;; supposed to be, and a conversion that lost anything answers something
|
||||
;; other than the last unit.
|
||||
(println (- (w-take-f64 w-u32max) 4294967294.0)) ;; 1
|
||||
(println (- (w-take-f64 w-i32neg) -1999999999.0)) ;; -1
|
||||
(println (- (w-take-f32 w-u16max) 65534.0)) ;; 1
|
||||
|
||||
;; ── float to float ──────────────────────────────────────────────
|
||||
(println (w-take-f64 w-f32half)) ;; 0.5
|
||||
|
||||
;; ── the binary join, both operand orders ────────────────────────
|
||||
(println (w-add-wide-first)) ;; 5000000001
|
||||
(println (w-add-narrow-first)) ;; 5000000001
|
||||
;; The narrower operand is the first one, and the sum is an i64 even though
|
||||
;; nothing on this line is annotated.
|
||||
(println (+ w-i32neg w-i64big)) ;; 3000000000
|
||||
;; A comparison joins the same way, and the widened -1 must still be -1.
|
||||
(println (< w-i32all w-i64big)) ;; true
|
||||
;; min and max over two widths answer at the wider one.
|
||||
(println (max w-i8neg w-i16neg)) ;; -5
|
||||
(println (min w-i8neg w-i32neg)) ;; -2000000000
|
||||
;; A count narrower than the value widens to it; the value's width decides.
|
||||
(println (<< w-i64big w-i8pos)) ;; 0 -- masked to 127 mod 64 = 63
|
||||
;; An expectation reaches the operands, so this adds at i64 rather than
|
||||
;; wrapping at i32 and widening the sum afterwards.
|
||||
(println (w-take-i64 (+ w-i32neg w-i32neg))) ;; -4000000000
|
||||
0)
|
||||
@ -542,6 +542,58 @@ let () =
|
||||
outputs "the rest of libm, both widths" "programs/math3.flan" math3_out;
|
||||
outputs ~opt:"-O0" "the rest of libm, both widths, -O0"
|
||||
"programs/math3.flan" math3_out;
|
||||
(* Implicit widening, FIX.org 2026-09-20. The type side of it needs no
|
||||
program — a refusal that stopped happening is a compile that succeeds —
|
||||
so what this asserts is the *bits*: every row is a value whose printed
|
||||
form differs depending on which extension instruction the backend chose.
|
||||
-5 as an i8 reaching an i64 prints 251 under a zero-extension; a u8 255
|
||||
reaching an i16 prints -1 under a sign-extension; a u32 four billion
|
||||
reaching an i64 prints a negative number under a sign-extension. The
|
||||
three subtraction rows are the int-to-float boundary, asserted by
|
||||
difference because %g rounds long before an f64's bits run out.
|
||||
|
||||
Run on both backends and on the unoptimised build, because the choice is
|
||||
made three separate times: emit.ml picks sext/zext/sitofp/uitofp by the
|
||||
source type's signedness, and x86.ml gets there by a load that extends
|
||||
by the same rule and a cvtsi2sd on the register it left behind. *)
|
||||
let widening_out =
|
||||
"-5\n\
|
||||
127\n\
|
||||
-300\n\
|
||||
-1\n\
|
||||
-2000000000\n\
|
||||
255\n\
|
||||
255\n\
|
||||
65535\n\
|
||||
4000000000\n\
|
||||
4294967295\n\
|
||||
4000000000\n\
|
||||
255\n\
|
||||
-2000000000\n\
|
||||
-2e+09\n\
|
||||
4.29497e+09\n\
|
||||
-5\n\
|
||||
-300\n\
|
||||
65535\n\
|
||||
1\n\
|
||||
-1\n\
|
||||
1\n\
|
||||
0.5\n\
|
||||
5000000001\n\
|
||||
5000000001\n\
|
||||
3000000000\n\
|
||||
true\n\
|
||||
-5\n\
|
||||
-2000000000\n\
|
||||
0\n\
|
||||
-4000000000\n"
|
||||
in
|
||||
outputs "implicit widening, and which extension it emits"
|
||||
"programs/widening.flan" widening_out;
|
||||
outputs ~opt:"-O0" "implicit widening, -O0" "programs/widening.flan"
|
||||
widening_out;
|
||||
outputs ~x86:true "implicit widening, --x86" "programs/widening.flan"
|
||||
widening_out;
|
||||
(* The clock and the environment. Every line of that program's output is
|
||||
an invariant — a monotonicity, a date range, a sleep that did not
|
||||
return early — and not a reading, because the same file is in the
|
||||
|
||||
@ -930,6 +930,141 @@ let () =
|
||||
rejects_check "float literal into an int"
|
||||
"(defn f [] i32 (+ 1 0.5))" ~needle:"expected i32";
|
||||
|
||||
(* ── Implicit widening, FIX.org 2026-09-20 ─────────────────────────
|
||||
The lattice, pinned at its edges rather than row by row: what is in, what
|
||||
is out, and the two boundaries that were a judgement call and could be
|
||||
argued the other way — int-into-float admitting only the exact ones, and
|
||||
equal-width cross-signedness admitting nothing.
|
||||
|
||||
[programs/widening.flan] is the other half and asserts the bits; these
|
||||
assert which programs exist. *)
|
||||
accepts "same signedness widens"
|
||||
"(defvar a i32) (defn g [x i64] ()) (defn f [] () (g a))";
|
||||
accepts "unsigned widens into a wider signed"
|
||||
"(defvar a u32) (defn g [x i64] ()) (defn f [] () (g a))";
|
||||
accepts "u8 widens into i16"
|
||||
"(defvar a u8) (defn g [x i16] ()) (defn f [] () (g a))";
|
||||
accepts "f32 widens into f64"
|
||||
"(defvar a f32) (defn g [x f64] ()) (defn f [] () (g a))";
|
||||
(* Narrowing is the thing that did not change, and the message has to say
|
||||
narrowing rather than "these are different types" — it also names the
|
||||
direction that needs nothing, because that is the half a reader coming
|
||||
from the old rule will not expect. *)
|
||||
rejects_check "narrowing is still refused, and says so"
|
||||
"(defvar a i64) (defn g [x i32] ()) (defn f [] () (g a))"
|
||||
~needle:"i64 into i32 can lose";
|
||||
rejects_check "and says the other direction is free"
|
||||
"(defvar a i64) (defn g [x i32] ()) (defn f [] () (g a))"
|
||||
~needle:"i32 widens into i64 by itself";
|
||||
rejects_check "float narrowing is refused too"
|
||||
"(defvar a f64) (defn g [x f32] ()) (defn f [] () (g a))"
|
||||
~needle:"f64 into f32 can lose";
|
||||
(* Equal width across signedness: each holds values the other cannot, so
|
||||
there is no direction at all and the message says that instead. *)
|
||||
rejects_check "signed does not reach the same-width unsigned"
|
||||
"(defvar a i32) (defn g [x u32] ()) (defn f [] () (g a))"
|
||||
~needle:"neither widens into the other";
|
||||
rejects_check "and a signed value never reaches an unsigned, wider or not"
|
||||
"(defvar a i32) (defn g [x u64] ()) (defn f [] () (g a))"
|
||||
~needle:"neither widens into the other";
|
||||
(* Int into float, exact only. This is where the rule is tighter than
|
||||
Odin's, which admits any integer into any float; i64 has values no f64
|
||||
holds, so it is out, and the cast is written. *)
|
||||
accepts "i32 reaches f64 exactly"
|
||||
"(defvar a i32) (defn g [x f64] ()) (defn f [] () (g a))";
|
||||
accepts "u32 reaches f64 exactly"
|
||||
"(defvar a u32) (defn g [x f64] ()) (defn f [] () (g a))";
|
||||
accepts "i16 reaches f32 exactly"
|
||||
"(defvar a i16) (defn g [x f32] ()) (defn f [] () (g a))";
|
||||
rejects_check "i64 does not reach f64 — above 2^53 it would round"
|
||||
"(defvar a i64) (defn g [x f64] ()) (defn f [] () (g a))"
|
||||
~needle:"(f64 x)";
|
||||
rejects_check "i32 does not reach f32 — above 2^24 it would round"
|
||||
"(defvar a i32) (defn g [x f32] ()) (defn f [] () (g a))"
|
||||
~needle:"(f32 x)";
|
||||
(* Containers are invariant: widening rewrites a value with a cast, and
|
||||
there is no value to rewrite in a slice that does not own its bytes. *)
|
||||
rejects_check "a slice of i32 is not a slice of i64"
|
||||
"(defn g [s [i64]] ()) (defn f [t [i32]] () (g t))"
|
||||
~needle:"expected [i64]";
|
||||
|
||||
(* The binary join. The wider operand decides, in either written order, and
|
||||
an equal-width cross-signed pair still has nothing to decide on. *)
|
||||
accepts "the wider operand decides, wider written first"
|
||||
"(defvar a i64) (defvar b i32) (defn f [] i64 (+ a b))";
|
||||
accepts "and decides when it is written second"
|
||||
"(defvar a i64) (defvar b i32) (defn f [] i64 (+ b a))";
|
||||
accepts "min and max join the same way"
|
||||
"(defvar a i8) (defvar b i16) (defn f [] i16 (max a b))";
|
||||
rejects_check "i32 and u32 have no join"
|
||||
"(defvar a i32) (defvar b u32) (defn f [] i32 (+ a b))"
|
||||
~needle:"neither widens into the other";
|
||||
(* The literal rule is untouched, which is what keeps a u64 constant's
|
||||
arithmetic at u64 rather than defaulting the 1 to an i32. *)
|
||||
accepts "a literal still takes the other operand's type"
|
||||
"(defconst fnv u64 0xcbf29ce484222325) (defn f [] u64 (+ fnv 1))";
|
||||
(* The form DISCUSS.org's note named: an unannotated let of a u64 constant.
|
||||
It binds a u64 and nothing about widening reaches it — a let with no type
|
||||
has no expectation to widen against, and the constant is what it says. *)
|
||||
accepts "an unannotated let of a u64 constant still binds a u64"
|
||||
"(defconst fnv u64 0xcbf29ce484222325) \
|
||||
(defn f [] u64 (let [h fnv] (* h 2)))";
|
||||
(* A literal that does not fit is the program's mistake, not a pair of types
|
||||
that failed to meet, so the join must not reconsider it — the operand it
|
||||
would reconsider against is the one the literal was supposed to take its
|
||||
width *from*. Both spellings: the literal written as the operand, and the
|
||||
literal buried in one. *)
|
||||
rejects_check "a literal that does not fit is still refused"
|
||||
"(defvar m u8) (defn f [] u8 (+ m 300))" ~needle:"300 does not fit in u8";
|
||||
rejects_check "and is refused inside an operand too"
|
||||
"(defvar m u8) (defn f [] u8 (+ m (+ 300 1)))"
|
||||
~needle:"300 does not fit in u8";
|
||||
rejects_check "a float literal still cannot stand where an int is wanted"
|
||||
"(defvar n i32) (defn f [] i32 (+ n 1.5))"
|
||||
~needle:"found the float literal 1.5";
|
||||
accepts "a literal that does fit still takes the operand's type"
|
||||
"(defvar m u8) (defn f [] u8 (+ m 200))";
|
||||
|
||||
(* The join reconsiders a refused operand, and a reconsidered pass must leave
|
||||
nothing behind. [scoped] cannot see to that — it puts the scope back on
|
||||
the way out, which an exception does not take — so [binary] snapshots and
|
||||
restores around each trial. Both symptoms of not doing it: a binding that
|
||||
outlives the pass that made it, and the same binding *shadowing* a live
|
||||
one, which is an uninitialised read in a program the compiler accepted. *)
|
||||
(* The other half, and the one that bites harder: a form that opens a window
|
||||
and closes it on the way out leaves it *open* when a trial inside it is
|
||||
abandoned, and then refuses a program that is fine. Both windows — the
|
||||
frames [handler-bind] establishes, and the loop [loop] pushes — with the
|
||||
refusal each would wrongly produce written as the second half of the
|
||||
test, so a regression shows up as the message coming back rather than as
|
||||
a silent accept. *)
|
||||
accepts "an abandoned trial inside handler-bind does not leave its frames up"
|
||||
"(defvar n i32) (defvar w i64) \
|
||||
(defn f [] i32 (println (+ n (handler-bind [] w))) (return 0))";
|
||||
accepts "nor does one inside a loop leave the loop up"
|
||||
"(defvar n i32) (defvar w i64) \
|
||||
(defn f [] i32 (println (+ n (loop [i 0] w))) (defer (println 1)) 0)";
|
||||
rejects_check "and a break outside every loop still says so plainly"
|
||||
"(defvar n i32) (defvar w i64) \
|
||||
(defn f [] i32 (println (+ n (loop [i 0] w))) (break) 0)"
|
||||
~needle:"break is only allowed inside a loop";
|
||||
rejects_check "an abandoned trial leaves no binding behind"
|
||||
"(defvar n i32) (defvar w i64) \
|
||||
(defn f [] i32 (println (+ n (let [q w] q))) (println q) 0)"
|
||||
~needle:"unknown name q";
|
||||
accepts "and does not shadow the binding it was nested in"
|
||||
"(defvar n i32) (defvar w i64) \
|
||||
(defn f [] i32 (let [t n] (println (+ n (let [t w] t))) (println t)) 0)";
|
||||
|
||||
(* Shifts are the carve-out: the value's type decides and the count widens
|
||||
to it, never the reverse, because the result's width and the poison check
|
||||
both belong to the value. *)
|
||||
accepts "a narrower count widens to the value"
|
||||
"(defvar v i64) (defvar n u8) (defn f [] i64 (<< v n))";
|
||||
rejects_check "a wider count does not drag the value up with it"
|
||||
"(defvar v u8) (defvar n i32) (defn f [] u8 (<< v n))"
|
||||
~needle:"expected u8";
|
||||
|
||||
(* ── Bidirectional flow ────────────────────────────────────────── *)
|
||||
accepts "return type types the literal" "(defn f [] u8 0)";
|
||||
accepts "return type types None" "(defn f [] (Option f64) None)";
|
||||
@ -2697,13 +2832,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
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user