diff --git a/FIX.org b/FIX.org index c3d4e47..9ea1c67 100644 --- a/FIX.org +++ b/FIX.org @@ -4909,3 +4909,143 @@ runtime/flan_rt.c comments, test/ (test_flan.ml, test_acceptance.ml, test_valgrind.ml and fifteen programs), vendor/edn and vendor/json, web, docs/BUILT.md, docs/overview.md, docs/SPIKE-DYNAMIC.md, spec-memory.md, NEXT.md and syntax-sketch.flan. sand.flan never used it. + +* A conversion under a bound, 2026-09-21 + +** The report +~(defn total [xs [$t]] i32 {:where [(integer? $t)]} ... (i32 (at xs i)) ...)~ +was refused with "i32 converts a number, found t". The bound says every type +the body is copied at is an integer, an integer is a number, and the +conversion is exactly what the bound exists to license. + +** The root cause, and it is narrower than "predicates are not consulted" +Arithmetic, comparison, min/max, the bitwise fold and the shifts all ask the +bound — each pairs an ~unconstrained ... ~needs:~ call with an ~|| generic_ty~ +escape, and the shifts had already been taught ~integer?~. The conversions +were the family nobody had gone back to. Three arms in lib/check.ml, all in +the cast block: + +1. ~is_cast~ (a machine type in head position) asked ~Types.is_numeric~ of the + operand and nothing else, so a variable — which has no type yet — fell + through to the refusal. This is the reported bug. +2. The enum target asked ~Types.Int _~ of the operand, the same way, so + ~(K n)~ inside a generic body was refused however the variable was bounded. +3. The *variable* target — ~(t x)~ — had the opposite defect. It asked the + bound of the target and then accepted any ~generic_ty~ operand, so a + second variable declared only ~ordered?~ passed the abstract pass on the + strength of a sentence about a different variable. That one was an + acceptance, not a refusal, and tightening it is part of this entry. + + It was not reachable, and saying so is the honest version. ~ordered?~ is + ~Types.is_comparable~, which admits numbers and enums and nothing else, + and every one of those converts at the concrete arm; a string is refused + at the instantiation before any of this. So no wrong program was ever + compiled through it. What it was is a hole that opens the day ~ordered?~ + admits a type that does not convert — which is the same future the rule + below refuses to bet against, and the best evidence for it: a check keyed + to the set a predicate denotes today is correct today and silently wrong + later, where one keyed to what the predicate claims stays correct across + the widening. + +** The rule +A conversion is legal at a bounded variable exactly when it is legal at every +type the bound admits, which is the repo rule that generic and concrete code +compute the same thing, applied to a set instead of a type. Read off the +concrete arm, that gives one predicate per target: + +- A machine-type target needs ~numeric?~. Every type it admits converts to + every numeric target today. +- An enum target needs ~integer?~. ~numeric?~ admits f32 and f64, and the + concrete arm refuses a float to an enum — sub-decision 3 of the cast block. +- ~ordered?~, ~equal?~ and ~hashable?~ admit nothing. + +And per predicate: + +- Under ~integer?~ every conversion is legal, the float targets included. + ~(f64 x)~ at an unknown-width integer is *not* value-preserving — i64 to + f64 rounds above 2^53 — and it is allowed anyway, because the written + ~(f64 i64-x)~ is allowed and a conversion has never claimed the value + survives. Refusing it at the variable would make the generic stricter than + the code it is copied into, which is the fork the rule forbids. +- Under ~numeric?~ every conversion to a number is legal, ~(i32 x)~ included, + and it may truncate a float. Same reasoning from the other side: ~(i32 + f64-x)~ truncates towards zero where the type is written, so the bound + cannot refuse what the copy would accept. The enum target is the one thing + ~numeric?~ does not buy. +- Under ~ordered?~ or ~equal?~ alone, refused. + +That last one is the only place the "legal at every admitted type" test does +not decide it, and it is worth naming rather than hiding. ~Types.is_comparable~ +admits numbers and enums and nothing else today, so every type ~ordered?~ +currently admits does in fact convert — the test taken literally would allow +it. It is still refused, because the predicate is a claim about ordering and +not about numbers: the day ~ordered?~ admits strings by a chosen collation +(plan.org, Types leaves that open), a conversion keyed to it would silently +start meaning something else. Predicates gate operations by what they say, +not by the set they happen to denote this week. ~hashable?~ makes the point +without any argument at all: it admits strings and structs now. + +** The diagnostics +The old line named the variable by its bare spelling, said only what was +wanted, and said nothing about the clause the reader would have to edit — +"i32 converts a number, found t" against a body whose signature says ~$t~. +The refusal now says what the variable is known to be and what to write: + + i32 converts a number. The where clause says t is ordered?, and that does + not make it a number — add (numeric? $t) to the where clause + + i32 converts a number. Nothing here says t is a number — write + {:where (numeric? $t)} at the head of the body + + K converts an integer to an enum. The where clause says t is numeric?, and + that does not make it an integer — add (integer? $t) to the where clause + +Both spellings compile as written, and the clause is spelled the way +~unconstrained~ already spells it so the family says it one way: a body with +no clause is handed the whole clause, a body that already has one is told +which predicate to add rather than a clause that would drop the predicates it +has. + +** Tests +test/test_flan.ml pins each conversion generic and concrete side by side — +the narrowing i32, the widening f64, an unsigned target, and the enum +direction — and each refusal against its whole message. +test/programs/int-generic.flan runs the reported program and its concrete +twin at -O2 and -O0. No x86 row was added: the checker decides more programs +are legal without changing what any of them emits, and the Cast they emit is +the one widening.flan already pins on x86. + +** Left alone, found while here +- ~(total v)~ where v is ~[3 i32]~ and the parameter is ~[$t]~ is refused, + and a written ~[i32]~ parameter refuses the same array with the same + reasoning. Not a fork; an array is not a slice, and the slice/as-slice lane + owns whatever changes there. +- ~i64->bytes~ takes its argument at ~~want:(Types.Int Types.I64)~, so a + written i32 or u8 is *accepted* — implicit widening reaches it — while a + ~$t~ under ~integer?~ is refused. That is not a fork either, and the reason + is the rule rather than symmetry: ~u64~ is refused concretely ("neither + widens into the other, so the conversion has to be written"), so ~integer?~ + admits a type at which the conversion is illegal, and a bound that admits + one such type cannot license the operation. ~bytes->i64~ has no argument + type to disagree about. Untouched. +- ~print~/~println~ over a bounded variable already defers to the + instantiation and needed nothing. + +** Open: there is now no generic enum → integer conversion +Worth recording as a loss rather than leaving the next reader to find it. +None of the five predicates admits enums while licensing a cast — ~numeric?~ +excludes them, and ~ordered?~ and ~equal?~ admit them but no longer convert. +Before this entry the one spelling that worked was ~(t x)~ with the *target* +bounded ~ordered?~, through the arm item 3 above closes, so the loss is real +and removing it is still right: it worked by not asking about the operand at +all. + +~enum?~ is the eventual answer and it is not a one-liner, which is why it is +written here rather than done here. It entails ~ordered?~ and ~equal?~ — +enums compare and are equal — and it does *not* entail ~numeric?~, because +arithmetic on an enum is refused where the type is written. So the cast rule +stops being one predicate per target and becomes a disjunction, ~numeric?~ or +~enum?~ for a machine-type target, and the refusal has to name whichever one +the reader meant. A cast *to* a variable bounded ~enum?~ is a second question +with its own answer. Each of those is a decision, not a fill-in, and the +author has not been asked. diff --git a/lib/check.ml b/lib/check.ml index a104795..fc60bfc 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -5674,6 +5674,59 @@ and not_numeric name what (a : Tast.expr) = else fail where "%s takes %s, found %s" name what (Types.to_string a.Tast.ty) +(* ── A conversion whose operand is a type variable ───────────────────── + [(i32 x)] where [x] is a [$t]. The concrete question — is this a number — + has no answer during the abstract pass, and asking it anyway is what + refused [(i32 (at xs i))] inside a body bounded [integer?]. The question + the bound can answer is the one asked here: does what the [where] clause + declares about the variable entail the predicate this conversion needs. + + Which predicate that is comes from the *target*, and the rule is the + concrete arm's rule read off a set rather than a type: a conversion legal + at every type the bound admits is legal at the variable, and one illegal at + any of them is refused. A number target needs [numeric?] — every type it + admits converts to every numeric target today, truncating or rounding by + the same rule a written f64 follows. An enum target needs [integer?], + because [numeric?] admits f32 and f64 and a float has no enum reading. + + [ordered?], [equal?] and [hashable?] are refused: they say what can be + compared, not what is a number, and nothing about a bound that only orders + says a conversion means anything. That they happen to admit only numbers + and enums today is a fact about [Types.is_comparable], not about what the + predicate claims — keying conversions to it would make widening [ordered?] + to strings a silent change to what converts. + + The message says what the variable is known to be and what to write. Both + spellings compile as written, and the clause spelling is [unconstrained]'s + so that the family says it one way: a body with no clause is given the + whole clause, and a body that already has one is told which predicate to + add rather than a clause that would drop the ones it has. *) +and cast_operand ctx loc name ~needs ~what ~is v = + if declares ctx.env.tvpreds v needs then () + else + let declared = + List.filter_map + (fun (p : Ast.pred) -> + if String.equal p.Ast.pvar v then Some p.Ast.pname else None) + ctx.env.tvpreds + in + let known = + match declared with + | [] -> Printf.sprintf "Nothing here says %s is %s" v is + | ps -> + Printf.sprintf + "The where clause says %s is %s, and that does not make it %s" v + (String.concat " and " ps) is + in + let fix = + if ctx.env.tvpreds = [] then + Printf.sprintf "write {:where (%s $%s)} at the head of the body" + needs v + else Printf.sprintf "add (%s $%s) to the where clause" needs v + in + Loc.failk "check/unconstrained-type-variable" loc + "%s converts %s. %s — %s" name what known fix + and fold_left_prim ctx ~want loc name p ~needs ok what args = let x, y, rest = match args with x :: y :: rest -> x, y, rest | _ -> assert false @@ -8062,6 +8115,13 @@ and named_call ?(qualified = false) ctx ~want loc name args = let a = check ctx (List.hd args) in (match a.Tast.ty with | Types.Int _ -> () + (* A type variable, answered by its bound rather than by a type it does + not have yet: [integer?] admits exactly the integer kinds, which is + what sub-decision 3 above asks for, and [numeric?] is a bound too wide + because it admits the floats that decision refuses. *) + | Types.Var v -> + cast_operand ctx loc name ~needs:"integer?" ~what:"an integer to an enum" + ~is:"an integer" v | other -> fail loc "%s converts an integer to an enum, found %s — an enum or a \ float goes through (i32 x) first" name @@ -8084,7 +8144,18 @@ and named_call ?(qualified = false) ctx ~want loc name args = let a = check ctx (List.hd args) in (match a.Tast.ty with | Types.Enum _ -> () - | t when Types.is_numeric t || generic_ty t -> () + | t when Types.is_numeric t -> () + (* The operand's own bound, asked the same way the target's was one line + up. Accepting every [generic_ty] here took the target's [numeric?] as + if it said something about the operand, so a second variable declared + only [ordered?] passed the abstract pass. Nothing wrong was ever + emitted — [ordered?] admits numbers and enums and both convert at the + instantiation — which is the point: the hole is only reachable the day + [ordered?] admits a type that does not, and that day is why the + question is asked of the predicate and not of the set it denotes. *) + | Types.Var v -> + cast_operand ctx loc name ~needs:"numeric?" ~what:"a number" + ~is:"a number" v | t -> fail loc "%s converts a number, found %s" name (Types.to_string t)); prim (Tast.Cast target) target [ a ] | _ when is_cast name && List.length args = 1 -> @@ -8098,6 +8169,12 @@ and named_call ?(qualified = false) ctx ~want loc name args = admits. *) | Types.Dyn -> () | t when Types.is_numeric t -> () + (* The operand of a conversion inside a generic body. The target is a + machine type, so what is in question is only the operand, and the + [where] clause is what answers it. *) + | Types.Var v -> + cast_operand ctx loc name ~needs:"numeric?" ~what:"a number" + ~is:"a number" v | t -> fail loc "%s converts a number, found %s" name (Types.to_string t)); (match a.Tast.ty with | Types.Dyn -> cast_dyn ctx loc target a diff --git a/spec-memory.md b/spec-memory.md index 358ad33..9a24af5 100644 --- a/spec-memory.md +++ b/spec-memory.md @@ -340,6 +340,24 @@ reaches through a container or function type is still bound exactly, because a slice's elements cannot be rewritten. An untyped literal is unaffected: it has no type of its own to keep. +**A conversion under a bound is legal exactly when it is legal at every type +the bound admits.** `(i32 x)` asks whether `x` is a number, and inside a +generic body no type is there to answer; the `where` clause answers for every +copy at once. `numeric?` is what a conversion to a machine type needs — +`integer?` entails it, so an `integer?` body converts too — and that covers +narrowing and widening alike: `(i32 x)` on a written `f64` truncates towards +zero and `(f64 x)` on a written `i64` rounds above 2^53, neither is refused +where the type is written, so neither is refused at the variable. A conversion +was never a claim that the value survives. The conversion *to* an enum needs +`integer?` exactly, because an enum is an `i32` and a float has no enum +reading, and `numeric?` would admit an `f32` copy the concrete rule refuses. +`ordered?`, `equal?` and `hashable?` admit no conversion at all: they say what +can be compared or keyed, not what is a number — and that is a claim about +what the predicate says, not about the set it denotes today, which currently +does admit only numbers and enums. The refusal names the predicate to write +(FIX.org 2026-09-21). One consequence is recorded there as open: no predicate +now licenses a generic enum → integer conversion. + **A type variable is not instantiated at `dyn`.** Two models answer "one body, many types" and they are not rivals: this one copies per written type at compile time, `defgeneric`/`defmethod` dispatch at run time on a value that diff --git a/test/programs/int-generic.flan b/test/programs/int-generic.flan index a5d8600..374b289 100644 --- a/test/programs/int-generic.flan +++ b/test/programs/int-generic.flan @@ -54,6 +54,45 @@ {:where (numeric? $t)} (+ a (+ b c))) +;; ── Conversions under a bound ────────────────────────────────────────── +;; A cast asks whether its operand is a number, and inside a generic body no +;; type is there to answer. The bound answers instead, for every copy at +;; once: integer? admits only integer kinds and every one of them converts, +;; so the body is checked once here and the conversion is the ordinary one in +;; each copy. This is the shape the bug report was written against — a sum +;; that narrows each element to the i32 it accumulates in. +(defn total [xs [$t]] i32 + {:where (integer? $t)} + (let [acc 0] + (dotimes [i (len xs)] (set acc (+ acc (i32 (at xs i))))) + acc)) + +;; The same rule widening. i64 → f64 rounds above 2^53 and i32 → f64 does +;; not, and neither is refused when the type is written out, so neither is +;; refused under the bound: a conversion is not a claim that the value +;; survives, it is the claim that the operand is a number. +(defn mean [xs [$t]] f64 + {:where (integer? $t)} + (let [sum 0.0] + (dotimes [i (len xs)] (set sum (+ sum (f64 (at xs i))))) + (/ sum (f64 (len xs))))) + +;; numeric? is the weaker bound and narrowing is legal under it too, because +;; it is legal at every type it admits: (i32 x) on a written f64 truncates +;; towards zero, and that is what the f32 copy of this does. +(defn truncate [x $t] i32 + {:where (numeric? $t)} + (i32 x)) + +;; The other direction, which is where the two bounds part company. An enum +;; is an i32 and a float has no enum reading, so this one needs integer? +;; exactly — numeric? would admit an f64 copy the concrete arm refuses. +(defenum Step [back -1 stay 0 forward 1]) + +(defn step-of [n $t] Step + {:where (integer? $t)} + (Step n)) + (defn main [] () ;; abs, one body, six widths. (println (abs (i8 -7))) @@ -109,4 +148,22 @@ (let [ns [5 3 9 1]] (match (index-of (slice ns 0 4) (i16 9)) (Some i) (println i) - _ (println -1)))) + _ (println -1))) + + ;; The conversions, generic and concrete side by side. Each pair is one + ;; conversion written twice — once at a bounded variable and once at the + ;; type a copy is made at — and the two answer the same number, which is + ;; the whole claim the bound makes. + (let [small [5 3 9 1] + wide [(i64 5) (i64 3) (i64 9) (i64 1)]] + (println (total (slice small 0 4))) + (println (total (slice wide 0 4))) + (println (mean (slice small 0 4))) + (println (mean (slice wide 0 4)))) + (println (truncate (i64 9))) + (println (truncate 2.75)) + (println (truncate -2.75)) + (println (i32 2.75)) + (println (step-of 1)) + (println (step-of (u8 0))) + (println (i32 (step-of (i64 -1))))) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index 2aa15d3..bd66636 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -2755,14 +2755,27 @@ let () = spells. Then the integer?-only operations at several widths, and last the join family: [true true], [6 6] and [42] are mixed widths at one $t answering identically in both argument orders, from one copy at - the wider type (FIX.org 2026-09-20). The closing [2] is an i16 scalar - widening into the i32 a slice fixed index-of's $t at — the one - direction a container-bound variable admits. *) + the wider type (FIX.org 2026-09-20). The [2] after them is an i16 + scalar widening into the i32 a slice fixed index-of's $t at — the one + direction a container-bound variable admits. + + The last eleven lines are the conversions. The two [18]s and the two + [4.5]s are one sum and one mean over an i32 slice and an i64 slice — + narrowing and widening inside a body bounded [integer?], each pinned + at two widths rather than against a written-type twin. [9 2 -2] is + (i32 x) at i64, f64 and a negative f64 under [numeric?], and it is the + one pair here that really is generic beside concrete: the bare [2] + after it is the written (i32 2.75), truncating towards zero to the + same number the copy does. The enum direction closes it, an integer + variable converting to a Step at two widths and back. The written-type + twins of the other three are in test_flan.ml, where the pairing is + every case. *) let int_generic_out = "7\n7\n7\n7\n7\n7\n-2147483648\n-9223372036854775808\n\ 0\n0\n1.5\n2.5\n\ 7\n15\n31\ntrue\nfalse\ntrue\n240\n9\n5\n-2\n301\n301\n\ - true\ntrue\n6\n6\n42\n2\n" + true\ntrue\n6\n6\n42\n2\n\ + 18\n18\n4.5\n4.5\n9\n2\n-2\n2\n:forward\n:stay\n-1\n" in outputs "integer? and the collapsed abs" "programs/int-generic.flan" int_generic_out; diff --git a/test/test_flan.ml b/test/test_flan.ml index 949f098..033f1c1 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -5385,6 +5385,81 @@ let () = ~needle:"admits no float type" "(defn h [x $t] $t {:where (integer? $t)} (+ x 1.5))"; + (* ── Conversions under a bound ─────────────────────────────────────── + A cast asks whether its operand is a number, and a type variable has no + type to answer with — so the bound answers, and the rule is the concrete + arm's rule read off the set a predicate admits: a conversion legal at + every type the bound admits is legal at the variable, and one illegal at + any of them is refused there. Each pair below is the same conversion + written twice, once generic and once concrete, and the two agree. *) + accepts "integer? admits (i32 x), the narrowing conversion" + "(defn to32 [x $t] i32 {:where (integer? $t)} (i32 x))"; + accepts "and the concrete conversion it stands for" + "(defn to32 [x i64] i32 (i32 x))"; + (* Widening an integer to a float is admitted for the reason every other + cast is: (f64 x) on a written i64 rounds above 2^53 and is not refused, + so the bound does not refuse it either. A conversion is not a promise + that the value survives. *) + accepts "integer? admits (f64 x), the widening one" + "(defn tof [x $t] f64 {:where (integer? $t)} (f64 x))"; + accepts "and the concrete widening it stands for" + "(defn tof [x i64] f64 (f64 x))"; + (* numeric? admits floats, so (i32 x) under it can truncate — which is + exactly what (i32 x) on a written f64 does, so refusing it at the + variable would make the generic stricter than the code it copies. *) + accepts "numeric? admits (i32 x), which may truncate a float" + "(defn to32 [x $t] i32 {:where (numeric? $t)} (i32 x))"; + accepts "and the concrete truncation it stands for" + "(defn to32 [x f64] i32 (i32 x))"; + accepts "integer? admits an unsigned target" + "(defn tou [x $t] u8 {:where (integer? $t)} (u8 x))"; + (* ordered?, equal? and hashable? say what can be compared or keyed, not + what is a number, so a conversion under one of them alone is refused — + and the message says which predicate to write. *) + rejects_check "ordered? does not admit a conversion" + ~needle:"The where clause says t is ordered?, and that does not make it \ + a number — add (numeric? $t) to the where clause" + "(defn to32 [x $t] i32 {:where (ordered? $t)} (i32 x))"; + rejects_check "nor does equal?" + ~needle:"add (numeric? $t) to the where clause" + "(defn to32 [x $t] i32 {:where (equal? $t)} (i32 x))"; + rejects_check "nor does hashable?" + ~needle:"add (numeric? $t) to the where clause" + "(defn to32 [x $t] i32 {:where (hashable? $t)} (i32 x))"; + (* With no clause at all the message hands over the whole clause rather + than a predicate to add to one that is not there. *) + rejects_check "an unbounded variable does not convert" + ~needle:"i32 converts a number. Nothing here says t is a number — write \ + {:where (numeric? $t)} at the head of the body" + "(defn to32 [x $t] i32 (i32 x))"; + (* The operand of a cast to a *variable* target is asked the same question + the target was: the target's bound says nothing about a second variable + standing in the argument. *) + accepts "a cast to a variable target takes a numeric? operand" + "(defn conv [x $u y $t] $t {:where [(numeric? $t) (numeric? $u)]} \ + (if (< y y) (t x) (t x)))"; + rejects_check "a cast to a variable target refuses an ordered? operand" + ~needle:"add (numeric? $u) to the where clause" + "(defn conv [x $u y $t] $t {:where [(numeric? $t) (ordered? $u)]} \ + (if (< y y) (t x) (t x)))"; + (* The enum direction, where the two numeric bounds part company: an enum + is an i32 and a float has no enum reading, so this conversion needs + integer? exactly — numeric? would admit an f64 copy that the concrete + arm two lines below refuses. *) + accepts "integer? admits the conversion to an enum" + "(defenum K [lo -1 hi 1])\n\ + (defn as-k [n $t] K {:where (integer? $t)} (K n))"; + rejects_check "numeric? does not, because it admits floats" + ~needle:"K converts an integer to an enum. The where clause says t is \ + numeric?, and that does not make it an integer — add \ + (integer? $t) to the where clause" + "(defenum K [lo -1 hi 1])\n\ + (defn as-k [n $t] K {:where (numeric? $t)} (K n))"; + rejects_check "and the concrete float it stands for is refused too" + ~needle:"K converts an integer to an enum, found f64" + "(defenum K [lo -1 hi 1])\n\ + (defn as-k [n f64] K (K n))"; + accepts "a variable read twice under one predicate" "(defn twice [a $t] bool {:where (ordered? $t)} (< a a))"; rejects_check "a predicate nobody has heard of"