From 879a43995105c4df1fdf1d9dece4370ea29d561d Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sun, 20 Sep 2026 20:21:41 +0700 Subject: [PATCH] A written zero stands where a numeric type variable stands pos? over every numeric type from one definition was the motivating example for milestone 5 and was the one thing the landed generics could not write: (> x 0) refused with "expected t, found the integer literal 0", because int_literal had no arm for a want that is a type variable. It has one now, and the bound is what makes it sound rather than optimistic. Every type numeric? admits is an integer or a float, and an untyped integer constant is usable at all of them, so there is no instantiation of a numeric? variable at which the literal has no meaning. Under a weaker bound there is -- ordered? admits an enum -- so numeric? is what is asked for and the refusal names it. The float literal is refused at a type variable even under numeric?, and that asymmetry is the concrete arms' own: an integer constant is usable where a float is wanted and a float literal is never usable where an integer is wanted, so a body written with 0.5 has no meaning at the integer half of its own bound. Refusing at the definition is what the abstract pass is for; the alternative is a surprise at whichever call site first asks for i32. The node the abstract pass builds is never emitted. Each copy re-checks the same form with the variable substituted, and that is where the literal is built at the concrete width and range-checked -- so (+ x 300) is fine at i32 and a refusal at u8, and u8 is where it is refused. --- lib/check.ml | 60 +++++++++++++++++++++++++++++++++++-- test/programs/generics.flan | 42 ++++++++++++++++++++++++++ test/test_acceptance.ml | 11 ++++++- test/test_flan.ml | 33 ++++++++++++++++++++ 4 files changed, 142 insertions(+), 4 deletions(-) diff --git a/lib/check.ml b/lib/check.ml index fcc0244..8138d16 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -2701,8 +2701,10 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr = let tail = ctx.tail in ctx.tail <- false; match e.Ast.e with - | Ast.Int n -> int_literal loc ~want n - | Ast.Byte b -> int_literal loc ~want ~default:Types.U8 (Int64.of_int b) + | Ast.Int n -> int_literal loc ~want ~preds:ctx.env.tvpreds n + | Ast.Byte b -> + int_literal loc ~want ~preds:ctx.env.tvpreds ~default:Types.U8 + (Int64.of_int b) (* The float literal's own dyn case, for the reason the integer's has one: the ABI carries one width and the literal is built at it. f64 is already what an unconstrained float literal defaults to, so this only has to stop @@ -2713,6 +2715,27 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr = let k = match want with | Some (Types.Float k) -> k + (* A float literal at a type variable, refused even under [numeric?] — + the asymmetry with the integer literal above is deliberate and is the + same asymmetry the concrete arms already have. An untyped integer + constant is usable wherever a float is wanted; a float literal is + never usable where an integer is wanted (Odin's rule, stated at the + [Int] case). So [numeric?] admits integers, and a body written with a + float literal has no meaning at the integer half of its own bound. + Refusing here keeps that a refusal at the definition rather than one + that surprises whichever call site first instantiates at [i32]. *) + | Some (Types.Var v) -> + Loc.failk literal_at_want loc + "the float literal %g cannot stand where $%s is wanted: %s may be \ + instantiated at an integer type, and a float literal is never \ + usable where an integer is wanted. Write the constant as an \ + integer literal — that one is admitted under {:where (numeric? \ + $%s)} at every numeric type — or take the value as a parameter" + x v + (if declares ctx.env.tvpreds v "numeric?" then + Printf.sprintf "{:where (numeric? $%s)} admits integers too, so $%s" v v + else Printf.sprintf "$%s" v) + v | Some other when other <> Types.Never -> Loc.failk literal_at_want loc "expected %s, found the float literal %g" (Types.to_string other) x @@ -3043,9 +3066,29 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr = ctx.defer_block; register_defer ctx loc forms -and int_literal loc ~want ?(default = Types.I32) n = +and int_literal loc ~want ?(preds = []) ?(default = Types.I32) n = match want with | Some (Types.Int k) -> mk loc (Types.Int k) (Tast.Int (in_range loc k n, k)) + (* An integer literal where a *type variable* is wanted: the abstract pass + over a generic body, checking [(> x 0)] or [(+ x 1)] with [x] at [$t]. + + It is admitted exactly when [$t] is declared [numeric?], and that bound is + what makes it sound rather than optimistic: every type [numeric?] admits + is an integer or a float, and an untyped integer constant is usable at all + of them — the same rule the [Float k] arm below encodes for a concrete + float. So there is no instantiation of a [numeric?] variable at which this + literal has no meaning, which is the promise the abstract pass exists to + make. + + The node built here is never emitted. A generic body produces no code; the + instantiation re-checks the same form with [$t] substituted, and then the + [Int k] or [Float k] arm above builds the literal at the concrete type and + runs the range check. [I64] is the placeholder width and is chosen only so + that a value too wide for [I32] survives the abstract pass to be ranged at + the instantiation that actually has a type — [(defn f [x $t] $t (+ x 300))] + is fine at [i32] and a refusal at [u8], and [u8] is where it is refused. *) + | Some (Types.Var v) when declares preds v "numeric?" -> + mk loc (Types.Var v) (Tast.Int (n, Types.I64)) (* A literal in dyn position takes i64 and not the i32 an unconstrained one defaults to. This is where "dyn integers are i64" stops being a statement about the ABI and becomes one about the language: [(defvar x dyn 5)] holds @@ -3060,6 +3103,17 @@ and int_literal loc ~want ?(default = Types.I32) n = Odin. A float literal is never usable where an integer is wanted. *) | Some (Types.Float k) -> mk loc (Types.Float k) (Tast.Float (Int64.to_float n, k)) + (* The same position without the bound. An unconstrained variable supports + only what every type supports, and holding a number is not that, so the + refusal names the bound that would admit it rather than reporting a type + mismatch the programmer cannot act on. *) + | Some (Types.Var v) -> + Loc.failk literal_at_want loc + "the integer literal %Ld cannot stand where $%s is wanted: an \ + unconstrained type variable may be instantiated at a type that holds \ + no number. Declare the bound — {:where (numeric? $%s)} — and the \ + literal is admitted at every type $%s can then be" + n v v v | Some other when other <> Types.Never -> Loc.failk literal_at_want loc "expected %s, found the integer literal %Ld" (Types.to_string other) n diff --git a/test/programs/generics.flan b/test/programs/generics.flan index 87ed185..12ddee7 100644 --- a/test/programs/generics.flan +++ b/test/programs/generics.flan @@ -50,6 +50,33 @@ {:where (ordered? $t)} (min (max x lo) hi)) +;; An integer *literal* where the type variable is wanted, which is what the +;; author's motivating family needs: one pos? over every numeric type rather +;; than one per width. The literal is admitted because {:where (numeric? $t)} +;; is declared, and the bound is what makes it sound rather than optimistic — +;; every type numeric? admits is an integer or a float, and an untyped integer +;; constant is usable at all of them, so there is no instantiation at which +;; this 0 has no meaning. Without the clause it is refused at the definition; +;; see the rejects in test_flan.ml. +;; +;; The literal is never emitted from here. The abstract pass builds a +;; placeholder and throws it away with the rest of the body; each copy +;; re-checks (> x 0) with $t substituted, and *that* is where the literal is +;; built at the concrete width and range-checked. +(defn pos? [x $t] bool {:where (numeric? $t)} (> x 0)) +(defn neg? [x $t] bool {:where (numeric? $t)} (< x 0)) +(defn zero-p? [x $t] bool {:where (numeric? $t)} (= x 0)) + +;; The same literal in arithmetic rather than comparison, and answering $t +;; rather than bool, so the placeholder has to survive being the operand of a +;; Prim and being returned. +(defn next-after [x $t] $t {:where (numeric? $t)} (+ x 1)) + +;; The range check is the instantiation's and not the definition's: 300 is +;; fine at i32 and would be a refusal at u8, and u8 is where it is refused. +;; This one is only ever asked for at i32. +(defn plus-300 [x $t] $t {:where (numeric? $t)} (+ x 300)) + ;; Two variables, and the second is determined by its own argument. (defn fst [a $t b $u] $t (do b a)) @@ -131,6 +158,21 @@ (println (clamp-to 0.5 1.0 9.0)) (println (fst 8 true)) + ;; The literal-at-a-type-variable family, at six numeric types from three + ;; written bodies. i32, i64, u8, u16, f32 and f64 all reach the same 0 and + ;; the same 1. + (println (pos? 3)) + (println (neg? (i8 -3))) + (println (zero-p? (u8 0))) + (println (zero-p? 0.0)) + (println (pos? (u16 1))) + (println (neg? (f32 -0.5))) + (println (next-after 3)) + (println (next-after (i64 10))) + (println (next-after 2.5)) + (println (next-after (u8 254))) + (println (plus-300 1)) + (show 3) (show 4.5) (show "text") diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index 542b2f9..f84c9e9 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -2584,9 +2584,18 @@ let () = scalar types because a default that is returned and one that is discarded are two different lowerings, and the last pair — [2 0] — is the same pair at a $t that owns storage, where each answer is a header - onto whichever of the two buffers the branch chose. *) + onto whichever of the two buffers the branch chose. + + The six [true]s and the five numbers after the first [8] are the + literal-at-a-type-variable family: three written bodies — pos?/neg?/ + zero-p?, next-after and plus-300 — reaching i8, u8, u16, i32, i64, f32 + and f64. [255] is next-after at u8 and is the one that would say + whether the placeholder width the abstract pass builds had leaked into + a copy; [301] is plus-300 at i32, whose range check belongs to the copy + and not to the definition. *) let generics_out = "3\n4.5\ntrue\n7\n5\n-1\n5\n42\n3\n1\n10\n1\n8\n\ + true\ntrue\ntrue\ntrue\ntrue\ntrue\n4\n11\n3.5\n255\n301\n\ 3\n4.5\ntext\n1\n2.5\n9\n36\n2\n2.5\n0\n\ 0\n-1\n2.5\n0\ntrue\nfalse\ntrue\n2\n0\n\ 3\n3\n0\n21\n7\n3\n4.5\n" diff --git a/test/test_flan.ml b/test/test_flan.ml index 077a74b..aef9577 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -4711,6 +4711,39 @@ let () = accepts "and is accepted when it is" "(defn outer [s [$t]] () {:where (ordered? $t)} (sort s))"; + (* ── A numeric literal where a type variable is wanted ────────────── + The author's motivating family — one pos? over every numeric type from + one definition — needs a written 0 to stand where $t stands. The bound + is what makes it sound: every type [numeric?] admits is an integer or a + float, and an untyped integer constant is usable at all of them, so + there is no instantiation of a [numeric?] variable at which the literal + has no meaning. That is the whole rule, and the four pins below are its + two halves and its one asymmetry. *) + accepts "an integer literal stands where a numeric? type variable is wanted" + "(defn pos? [x $t] bool {:where (numeric? $t)} (> x 0))"; + accepts "and in arithmetic, answering the variable" + "(defn next [x $t] $t {:where (numeric? $t)} (+ x 1))"; + (* [numeric?] is what admits it and nothing weaker does. [ordered?] admits + an enum, which holds no number, so a literal under it has an + instantiation at which it means nothing — and the refusal below is what + stops that reaching the call site. *) + rejects_check "an unconstrained type variable admits no literal" + ~needle:"may be instantiated at a type that holds no number" + "(defn f [x $t] bool (> x 0))"; + rejects_check "and ordered? is not the bound that admits one" + ~needle:"Declare the bound" + "(defn f [x $t] bool {:where (ordered? $t)} (> x 0))"; + (* The asymmetry, and it is the concrete arms' asymmetry rather than a new + one: an untyped integer constant is usable where a float is wanted, and + a float literal is never usable where an integer is wanted. [numeric?] + covers both halves of the numbers, so a body written with a float + literal has no meaning at the integer half of its own bound. Refused at + the definition, which is where the abstract pass promises refusals + arrive — not at whichever call site first asks for i32. *) + rejects_check "a float literal is refused at a type variable even under numeric?" + ~needle:"may be instantiated at an integer type" + "(defn half [x $t] $t {:where (numeric? $t)} (* x 0.5))"; + (* A map key that is a type variable has no hash and no equality to emit: they are chosen from the concrete type, which does not exist yet. So the map operations join print and println on the list of forms the abstract