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

Merge branch 'lane-m5-generics' into dev-loop

Browse Source 
# Conflicts:
#	FIX.org
This commit is contained in:
Joseph Ferano 2026-09-20 21:09:30 +07:00
commit c20a4b90dc
11 changed files with 938 additions and 36 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

237
FIX.org
View File

@ -3229,9 +3229,13 @@ an abandoned trial that lifted a function out of an ~fn~ literal leaves it in
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~.
mean deciding what else on ~env~ a trial may have touched.
[Corrected by the milestone-5 lane, below: the generic instantiation cache
does not rewind itself either, and does not need to. ~instantiate~ rewinds a
copy whose *body* refused, which is a different event from a copy the caller
abandoned. The abandoned one is harmless because the trial and the live pass
cannot disagree about which copy to make.]
All five symptoms pinned — the two accepts, the shadow, the unknown name, and
the loop diagnostic.
@ -3558,3 +3562,230 @@ them exactly as it skips the shadowing guard; nothing in that test changed.
and ~@sanitize~ sweeps were not run here — the new corpus row is registered
for the x86 survey through the existing ~programs/*.flan~ glob and will be
compared on the next sweep.
* Milestone 5, and the sweep behind it, 2026-09-20
** What was already there
Almost all of it, and the first finding of this lane is that finding.
docs/SPIKE-GENERICS.md carries a banner saying so — "it stopped being current
when generics landed for real, on 2026-09-13" — and the code agrees:
~$t~ binds and bare ~t~ reads; ~collect~ puts a generic signature in ~gsigs~
and keeps it out of ~env.fns~; ~generic_call~ binds left to right,
substituting each binding into the parameters still to come; ~instantiate~
caches by ~Types.equal~ on the concrete parameter list; the body is checked
once abstractly so a refusal lands at the definition; ~{:where~ carries four
predicates with an entailment table; ~runaway~ caps the depth; a copy is an
ordinary ~Tast.fn~ with a cell, so both backends were untouched then and are
untouched now; and ~Check.instantiations~ expands a redefined generic's name
for ~Session.eval~, which test_session pins at four shapes including a copy
the running process was never built with.
So this lane is not "start M5". It is the four things M5 did not reach, and
the sweep the author asked for.
** 1. A written zero may stand where a numeric type variable stands
The one thing the landed generics could not express was the family the whole
feature was asked for:
#+begin_src lisp
(defn pos? [x $t] bool {:where (numeric? $t)} (> x 0))
#+end_src
~(> x 0)~ was 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 anything weaker there is —
~ordered?~ admits an enum, which holds no number — 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 rather than a new rule: an 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 ~0.5~ has no meaning at the integer half of
its own bound, and refusing at the definition is what the abstract pass is
for.
Nothing built here is emitted. The abstract pass builds a placeholder at i64
and throws it away with the rest of the body; 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.
** 2. Generics and implicit widening
*Decided: implicit widening does not cross a generic binding.*
Widening landed days after generics did, and the rule the two of them left
between them read off the order the arguments were written in:
#+begin_src lisp
(defn eq2? [a $t b $t] bool {:where (equal? $t)} (= a b))
(eq2? (i8 3) (i64 3)) ; refused — i64 into i8 can lose
(eq2? (i64 3) (i8 3)) ; accepted — $t was i64 already, the i8 widened in
#+end_src
Same two values, same function, one copy at i8 refused and one copy at i64
generated. Neither answer is unsound — a widen cannot change a number — so
this is not a bug report; it is a decision nobody had taken, because the two
features had never been in the tree at the same time.
Taken: a concrete argument at a variable an earlier argument already bound has
to be that type. Both orders refuse now, with one sentence naming the binding,
the argument and the cast to write.
*Why refuse rather than join.* Letting the pair meet at the wider type is the
other coherent rule, and it is the better one if the ergonomics ask for it.
It can be added later without invalidating a single program written under this
rule. The reverse is not true. Refusing is the direction that can be walked
back, and with two features that had never met, that is the direction to be
wrong in.
The rule costs almost nothing, because ~Types.widens_to~ admits only numeric
scalars: a variable bound inside ~[$t]~ or ~(Fn [$t $t] bool)~ leaves a
parameter no widening ever applied to, so ~sort-by~ and the whole fn-literal
path are untouched by construction. Two exceptions keep the ergonomics —
an untyped literal has no type of its own to keep, so it still takes the
variable's; and a form with no type without a want (~(zeroed)~) is asked for
its natural type through a ~trial~ and falls back to the want when that
refuses.
*** And the composition with the trial machinery, which is the reason to care
A binary operator whose operands disagree re-checks the right one at the left
one's type inside a ~trial~, so a generic call written there is checked twice,
once in a pass that is thrown away. An instantiation made during the discarded
pass does *not* go back out: ~instantiate~ rewinds a copy whose body refused,
which is a different event.
It does not have to, and the reason is this lane's own rule rather than luck.
*A generic call's instantiation is read off its arguments and never off the
ambient want* — an unbound variable is checked with no expectation at all, and
a bound one no longer widens — so the trial and the live pass ask
~instantiate~ for the same types, the second ask is a cache hit on the first,
and exactly one copy exists either way. Pinned by counting copies in the
checked program, not by reading the comment.
The widening lane's own note said the instantiation cache "already rewinds
itself"; it does not, and the entry above has been corrected in place.
** 3. A type variable is not instantiated at dyn
*Decided: refused, at the binding.*
Nothing stopped it before, because ~dyn~ is an ordinary case of ~Types.t~ and
substituted like any other type. The copy was then made and walked into the
dyn answers that are not all there, and the refusal arrived from inside the
generic's own source: ~(or-else (Some d) e)~ over two dyns was reported
against ~<prelude>:385~, about a descriptor the collector cannot build for
~(Option dyn)~ — a line the caller did not write and cannot act on. Every
such case is this refusal arriving late and in the wrong place.
The message does not only say no. Two models answer "one body, many types"
here and they are not rivals: this one copies per written type at compile
time, ~defgeneric~/~defmethod~ dispatch at run time on a value that carries
its own. A dyn argument is asking the second question of the first machinery,
so the sentence names the other spelling.
Only the unbounded half is new — a variable carrying a ~{:where}~ clause was
already refused by ~pred_holds~, and that refusal is left in front of this one
deliberately, because it names the predicate the signature wrote down.
*Open, and the author's:* whether dyn should eventually flow through a
generic at all. Refusing now is the walk-backable direction for the same
reason as the widening decision.
** 4. Three messages about milestone 5, from a milestone that arrived
Swept, and they were not all the same kind of stale.
- ~check.ml~'s unknown-lowercase-type arm reported "generic code over the
type variable X is not implemented yet — milestone 5 work". Generics are
implemented, and ~resolve_name~ consults ~env.tyvars~ and ~env.subst~ long
before anything reaches that arm, so a lowercase name arriving there is a
typo too far from any type to guess at, or a type variable nobody
introduced. It names the sigil that would introduce it.
- The type resolver's "X takes no type arguments — generics are milestone 5"
and the value-position fork's "a type given type arguments is generic code,
which is milestone 5" are about the *other* half, which is genuinely
unbuilt: ~Types.Named~ is a bare string with no room for parameters, and
giving it some is a change to ~Types.t~ and therefore to the layout
calculator, both backends, ~Render~ and DWARF. Both now say a generic
*type* is not there yet and point at the generic function that is. Nothing
was built for them.
Three test needles moved with them.
** 5. The prelude sweep — what collapsed, what did not
*Added:* ~pos?~, ~neg?~, ~zero?~. Three questions about a number's sign, one
body each, answering at i8 through u64 and at both float widths. They were
never written before because without a type variable they are three functions
per width; they are writable now because of item 1 above and not because of
the type variable alone.
*Declined, with the real reason written where the old one was:*
- ~abs-i32~/~abs-i64~ stay two functions. The comment's old reason — "there
are no generics over the numeric types" — is false now, and the generic
body checks and runs at every integer width. What stops it is the float
half of its own bound: ~numeric?~ is the only predicate that admits a
written ~0~ and it admits f32/f64 too, and ~(if (< x 0) (- 0 x) x)~ is the
wrong abs for a float — it hands back a negative zero. The float pair is
libm's ~fabs~ for exactly that reason. *The collapse waits on a bound that
spells "an integer type".*
- ~min~/~max~ stay builtins. Not a type-system limit: they are variadic, and
each step slots both of its sides so every operand is evaluated exactly
once. A binary prelude generic would have to be nested at the call site,
which puts the double evaluation back. Their generic half was never missing
— ~ordered?~ already admits them in any body that declares it.
*** An ~integer?~ predicate — recorded, not built
It would collapse ~abs~, and it would let ~%~, the bitwise operators and the
shifts be written over a variable. It is four lines in ~pred_holds~,
~predicate_names~ and ~pred_entails~ (declared ~integer?~ gives ~numeric?~,
~ordered?~ and ~equal?~). It is not built here because adding a predicate is
language surface — the vocabulary a programmer writes — and that is the
author's call, not a lane's.
** What this lane did not build, deliberately
- *Generic types.* ~(defstruct Pair [a $t b $t])~ cannot be spelled, and
the price is in the spike: ~Types.t~ and every backend. Out of scope, and
the two messages above now say so accurately.
- *"In instantiation of" notes.* A refusal inside a copy points at the
generic's source with no note saying which call site asked for that type.
~Check.instantiation_origin~ exists and ~session.ml~ already uses it for
compatibility reports, so the data is there; wiring it into every ~fail~
under an instantiation is the spike's "bulky, not hard" bucket and is a
lane of its own. Two of the three places it mattered most are closed by
items 2 and 3 above, which move those refusals to the call site outright.
- *~$n~ in length position.* Same price as generic types, smaller prize.
** Pins added
Cross-package generics (~programs/pkg-generic.flan~ and a new
~pkgs/gen~ package — one generic at two element types, one calling another in
its own package at its own variable so the transitive copy is generated from a
call site two files away, and a local generic calling across the boundary at
its own ~$t~), both backends and -O0; the package bound refused at the call
with the clause quoted; the literal family at six numeric types in the
generics corpus row; the prelude's three under their real names including
~zero?~ at ~-0.0~; both widening orders refusing; the written conversion and
the untyped literal still accepted; the fn-literal path unaffected; ~(zeroed)~
still getting its want; ~$t~ at dyn and at ~(Option dyn)~; a bounded variable
still refused by its bound; the abandoned-trial copy count; and the three
reworded messages.
Dev-loop reload needed nothing: test_session already pins ~C-c C-c~ on a
generic installing its copies, the callee side, the absence of a stale cache
across two evaluations, and a redefinition that needs a copy the process was
never built with.
** One stale claim flagged, not touched
plan.org's Types section still lists *five* predicates and describes
~copyable?~ and "a type variable is move-only by default" at length.
spec-memory.md's Generics section already records that ~copyable?~ went with
the second repeal, and ~predicate_names~ in check.ml has four. plan.org is the
one that is behind. Left alone deliberately: it is the ownership-repeal lane's
sentence to retire, not this one's, and it is flagged here so that lane picks
it up.
spec-memory.md's Generics section gained the three rules this lane decided —
the literal under ~numeric?~, the widening boundary, and dyn — because the
spike banner names that section and plan.org's Types as the current account,
and all three are observable from a program.

260
lib/check.ml
View File

@ -904,8 +904,19 @@ let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
| "Map", _ -> fail loc "(Map K V) takes exactly two types"
| "Result", _ -> unimplemented loc "(Result T E)" 6
| _ ->
(* Not generics, which are here: a *function* is generic over [$t] and
instantiated per call site. This is a parameterised named type —
[(Pair i32 f64)] — and that is a different thing and is not built.
[Types.Named] is a bare string with no parameters, so there is
nowhere to put the arguments, and giving it some is a change to
[Types.t] and therefore to the layout calculator, both backends,
[Render] and the DWARF path. docs/SPIKE-GENERICS.md, question 4,
prices it and leaves it out. *)
fail loc
"%s takes no type arguments — generics are milestone 5" name)
"%s takes no type arguments. A generic *function* is written with \
[$t] in its parameter vector and copied per call site; a generic \
*type* — (%s ...) — is not there yet"
name name)
(* One edit away from a type that exists — a substitution, an insertion, a
deletion or a transposition of neighbours. Bounded at one, because two edits
@ -1001,12 +1012,26 @@ and resolve_name env ~seen loc n =
| _ when near_miss env n <> None ->
Loc.failk "check/unknown-type" loc "unknown type %s — did you mean %s?" n
(Option.get (near_miss env n))
(* Lowercase is a type variable, Capitalized is concrete — no sigil
(plan.org, Types). A variable parses, but nothing at milestone 2 can
give a value one, so it is rejected here rather than later. *)
(* An unknown lowercase name, and the sentence it gets used to be that
generics were milestone 5 work. They are not: [$t] binds a type
variable and bare [t] uses one, and [resolve_name] has already
consulted [env.tyvars] and [env.subst] before anything reaches here.
So a lowercase name arriving at this arm is one of exactly two
things, and the message names both rather than sending somebody to a
schedule.
Either it is a typo too far from any type to be guessed at — the
near-miss arm above catches the one-edit ones — or it is a type
variable that was never introduced, which is the sigil's whole
purpose to notice: without the binding site a mistyped type name
silently became a type parameter and made the signature more
permissive than it was written to be. *)
| _ when n <> "" && n.[0] = Char.lowercase_ascii n.[0] ->
unimplemented loc
(Printf.sprintf "generic code over the type variable %s" n) 5
Loc.failk "check/unknown-type" loc
"unknown type %s. A lowercase name is a type variable only where a \
defn signature introduced it — write $%s in the parameter vector \
to introduce one, and %s reads it from there"
n n n
| _ -> Loc.failk "check/unknown-type" loc "unknown type %s" n
and array_len env loc = function
@ -1424,6 +1449,19 @@ let rec generic_ty (t : Types.t) =
| Types.Fn (ps, r) -> List.exists generic_ty ps || generic_ty r
| _ -> false
(* Does a type a call site bound a variable to reach a [dyn] anywhere? See the
refusal in [generic_call]: [dyn] is a concrete type and substitutes like any
other, so nothing stopped a copy being made at it, and the copies walked
straight into holes the rest of the language has no [dyn] answer for yet. *)
let rec reaches_dyn (t : Types.t) =
match t with
| Types.Dyn -> true
| Types.Slice e | Types.Array (_, e) | Types.Ptr e | Types.Vec e
| Types.Option e -> reaches_dyn e
| Types.Map (k, v) -> reaches_dyn k || reaches_dyn v
| Types.Fn (ps, r) -> List.exists reaches_dyn ps || reaches_dyn r
| _ -> false
(* The refusal plan.org's Types section asks for, in one place so that every
operator says the same thing: with no constraints a type variable supports
only what *every* type supports, so [=], [<], [+] and [hash] over one are
@ -2751,8 +2789,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
@ -2763,6 +2803,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
@ -3093,9 +3154,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
@ -3110,6 +3191,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
@ -5678,7 +5770,17 @@ and named_call ?(qualified = false) ctx ~want loc name args =
in
let a, b = binary ctx name loc ~want:(numeric_want want) [ x; y ] in
(* [min] and [max] are [<] with a pick, so [ordered?] is what they want —
not [numeric?]. A generic that declares [ordered?] gets both. *)
not [numeric?]. A generic that declares [ordered?] gets both.
They stay builtins now that generics could express them, and the reason
is the two lines above rather than the type system: they are variadic,
and each step puts both of its sides in slots so that every operand is
evaluated exactly once. A prelude [(defn min [a $t b $t] $t ...)] would
be binary and would have to be nested at the call site, which is where
the double evaluation this arm exists to prevent would come back. The
generic half is already theirs — [ordered?] admits them inside any
body that declares it — so collapsing them would cost the arity and
the evaluation rule and buy nothing. *)
unconstrained ctx.env loc name ~needs:"ordered?" a.Tast.ty;
if not (Types.is_numeric a.Tast.ty || generic_ty a.Tast.ty) then
not_numeric name "numbers" a;
@ -7436,8 +7538,9 @@ and ordinary_call ctx ~want loc name args =
the fork the form fell down. *)
Loc.failk "check/unknown-function" loc
"unknown function %s. A capitalised name is a type, and a type \
given type arguments — (%s ...) — is generic code, which is \
milestone 5"
given type arguments — (%s ...) — is a generic type, which is \
not there yet. A generic *function* is: it is written with \
[$t] in its parameter vector and copied per call site"
name name
else Loc.failk "check/unknown-function" loc "unknown function %s" name
@ -7526,9 +7629,78 @@ and generic_call ctx ~want loc name vars pats pret args =
let subst = ref [] in
let targs =
map2_lr
(fun p a ->
let p = subst_ty !subst p in
let a = if generic_ty p then check ctx a else check ctx ~want:p a in
(fun pat a ->
let p = subst_ty !subst pat in
(* Which variable, if any, this parameter *is* — written as a bare
[$t] and already bound by an argument to the left. That is the one
shape implicit widening can reach, because [Types.widens_to] admits
only numeric scalars: a variable bound inside [[$t]] or
[(Fn [$t $t] bool)] leaves a parameter no widening applies to, so
the [sort-by] path below is untouched by construction. *)
let bound_scalar =
match pat with
| Types.Var v when (not (generic_ty p)) && Types.is_numeric p ->
Some v
| _ -> None
in
(* An untyped constant has no type of its own to keep, so it still
takes the variable's — [(clamp-to y 0 10)] with [y] an i64 means
three i64s and there is no conversion anywhere in it. Everything
else is checked on its own terms. *)
let untyped_literal =
match a.Ast.e with
| Ast.Int _ | Ast.Float _ | Ast.Byte _ -> true
| _ -> false
in
let a =
if generic_ty p then check ctx a
else if bound_scalar <> None && not untyped_literal then
(* On its own terms first. A form that has no type without a want
— [(zeroed)] is the one that matters — refuses here and is
checked against the parameter as it always was; the trial
leaves no trace of the attempt. *)
(match trial ctx (fun () -> check ctx a) with
| Ok r -> r
| Error _ -> check ctx ~want:p a)
else check ctx ~want:p a
in
(* **Implicit widening does not cross a generic binding.** A concrete
argument at a variable an earlier argument already bound has to be
the same type, not merely a type that widens into it.
This is a decision and not a consequence. Widening landed after
generics did, and left behind a rule that depended on argument
order: [(pair-eq? i64 i8)] was accepted, because [$t] bound to i64
first and the i8 widened into the want; [(pair-eq? i8 i64)] was
refused, because [$t] bound to i8 and i64 into i8 can lose. Same
two values, same function, two answers. Neither is unsound — a
widen cannot change a number — but which instantiation a program
gets should not depend on which argument was written first.
Refusing both is the direction that can be walked back. Allowing
the pair to join at the wider type is a coherent rule too, and it
is the one to reach for if the ergonomics turn out to want it; it
can be added later without invalidating a program that was written
under this rule, and the reverse is not true. FIX.org, "Generics
and implicit widening". *)
(* Only where the pair is one widening had an opinion about. A string
passed where $t was bound to i64 is an ordinary mismatch and gets
the ordinary refusal; the sentence below is about the conversion
that no longer happens, and it would read as a non-sequitur over a
pair that never had one available. *)
(match bound_scalar with
| Some v
when (not (Types.equal p a.Tast.ty))
&& Types.is_numeric a.Tast.ty ->
Loc.failk "check/tyvar-no-widening" a.Tast.loc
"%s's $%s was bound to %s by an earlier argument, and this one \
is %s. Implicit widening does not cross a generic binding: a \
written type is what a type variable takes, so the same \
variable is the same type at every argument. Write the \
conversion — (%s x) — or pass the arguments at one type"
name v (Types.to_string p) (Types.to_string a.Tast.ty)
(Types.to_string p)
| _ -> ());
if not (bind_ty subst p a.Tast.ty) then
fail a.Tast.loc "%s expects %s here, found %s" name
(Types.to_string p) (Types.to_string a.Tast.ty);
@ -7547,6 +7719,50 @@ and generic_call ctx ~want loc name vars pats pret args =
generic function is instantiated from its call site, and there is \
no syntax for naming the type" name v)
vars;
(* **A type variable is not instantiated at dyn.** Nothing stopped it before:
[dyn] is an ordinary case of [Types.t], so it substituted like any other
type and a copy was generated at it. The copy then reached whatever the
body did with the value, and the dyn answers are not all there — [(Option
dyn)] has no descriptor the collector can find, [as-slice] over a
[(Vec dyn)] refuses. So the refusal existed, it just arrived from inside
the generic's own source: [(or-else (Some d) e)] over two dyns is reported
against [<prelude>:385], a line the caller did not write and cannot act
on. Every one of those is this refusal arriving late and in the wrong
place.
Refusing at the binding is also the honest statement of the split. Two
models answer "one body, many types" here and they are not rivals: this
one instantiates at compile time and keeps the types, and [defgeneric] /
[defmulti] dispatch at run time on a value that carries its own. A dyn
argument is asking the second question of the first machinery. The
message says so and names the other spelling.
Bounded variables were already refused — [pred_holds] says no to dyn for
all four predicates — so this closes the unbounded half, which is exactly
the half that reached the prelude-source diagnostics. A variable that
*does* carry a clause is left to that refusal deliberately: it names the
predicate the signature actually wrote down, which is the more specific
answer of the two, and the generic cast's pin depends on it. *)
let clause_on v =
match Hashtbl.find_opt ctx.env.generics name with
| None -> false
| Some gfn ->
List.exists
(fun (p : Ast.pred) -> String.equal p.Ast.pvar v) gfn.Ast.fwhere
in
List.iter
(fun (v, t) ->
if reaches_dyn t && not (clause_on v) then
Loc.failk "check/tyvar-at-dyn" loc
"this call would instantiate %s at $%s = %s, and a type variable \
is not instantiated at dyn: a copy is made per *written* type, \
and dyn is the one type whose own type is not known until it \
runs. One value, two models — (defgeneric %s [...]) with a \
(defmethod ...) per class dispatches on what the value turns out \
to be, which is the question a dyn argument is asking. Write the \
type the value has, or reach for the dyn side"
name v (Types.to_string t) name)
!subst;
let cparams = List.map (subst_ty !subst) pats in
let cret = subst_ty !subst pret in
if List.exists generic_ty cparams || generic_ty cret then begin
@ -7760,8 +7976,18 @@ and trial ctx f =
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].
what else on [env] a trial may have touched.
The generic instantiation cache is the other table a trial reaches, and
it does not rewind either. [instantiate] rewinds a copy whose *body*
refused, which is a different event from a copy the caller abandoned —
and the abandoned one does not need rewinding. A generic call's
instantiation is read off its arguments and never off the ambient want:
an unbound variable is checked with no expectation at all, and a bound
one does not widen. So the trial and the live pass ask [instantiate] for
the same types, the second ask is a cache hit on the first, and exactly
one copy exists either way. Pinned in test_flan, "a generic inside an
abandoned trial".
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

59
lib/prelude.ml
View File

@ -467,6 +467,44 @@ let source = {flan|
(push v (at s i))))
v))
;; ── The sign questions, over every numeric type at once ───────────────
;;
;; The family the whole of generics was asked for. Three questions about a
;; number's sign, one body each, answering at i8 through u64 and at both
;; float widths — where without a type variable they would be three functions
;; per width, which is why they were never written at all.
;;
;; What makes them writable is not the type variable on its own: it is that a
;; written 0 may stand where $t stands. That needs the {:where (numeric? $t)}
;; clause and nothing weaker, because the bound is what promises the literal
;; has a meaning at every type the variable can become. An unconstrained
;; variable is refused, and so is [ordered?] — it admits an enum, which holds
;; no number.
;;
;; The comparison is the clause's too: [numeric?] entails [ordered?], so one
;; predicate on the line gives the body both the < it writes and the 0 it
;; writes it against.
;;
;; **The unsigned instantiations are not mistakes.** (neg? (u8 3)) is false at
;; every u8 and the copy is a constant, which a reader may find odd in the
;; emitted code and which is exactly right: a generic is copied per written
;; type, and the body says what it says at each of them. Refusing the copy
;; would mean a bound that spells "signed", and there is no such predicate.
(defn pos? [x $t] bool
{:where (numeric? $t)}
(> x 0))
(defn neg? [x $t] bool
{:where (numeric? $t)}
(< x 0))
;; Named zero? rather than =0 because it reads as the question it is. The
;; float instantiations answer true for both zeros, since -0.0 = 0.0 is what
;; IEEE says and this does not second-guess it.
(defn zero? [x $t] bool
{:where (numeric? $t)}
(= x 0))
;; ── The per-type layer that stays ─────────────────────────────────────
;;
;; sum is the one shape a type variable cannot express, and it is worth being
@ -947,9 +985,24 @@ let source = {flan|
(declare cbrt-f32 [x f32] f32 "cbrtf")
(declare cbrt-f64 [x f64] f64 "cbrt")
;; Integer magnitude, one per width because there are no generics over the
;; numeric types and min and max are builtins rather than functions, so a
;; single abs is not expressible today.
;; Integer magnitude, one per width, and the reason it stays that way changed
;; when generics landed. The old one — no generics over the numeric types —
;; is not true any more: (defn abs [x $t] $t {:where (numeric? $t)} (if (< x
;; 0) (- 0 x) x)) checks and runs at every integer width, and the literal 0
;; stands there because the clause admits it.
;;
;; **What stops it is the float half of its own bound.** numeric? is the only
;; predicate that admits a written 0, and it admits f32 and f64 too — so a
;; generic abs would be instantiated at them, and the body above is the wrong
;; abs for a float: (< -0.0 0) is false, so it hands back a negative zero
;; from a function named abs. The float pair below is libm's for exactly that
;; reason, a sign-bit clear rather than a negation, and a generic that shadows
;; it at f32 would be a quiet wrong answer rather than a tidier prelude.
;;
;; So the collapse waits on a bound that spells "an integer type" — an
;; integer? predicate, which is language surface and not this file's call.
;; FIX.org, "Generics and implicit widening", records it as the candidate.
;; Two functions is the honest price until then.
;;
;; The most negative value of each width has no positive counterpart, and this
;; does not special-case it: the subtraction is the same subtraction written

27
spec-memory.md
View File

@ -301,6 +301,33 @@ Type arguments are **inferred at call sites** from the argument types; there is
no explicit instantiation syntax in the first implementation. A type variable
that appears only in the return type is therefore an error.
Three further rules about what a call site may pass, all decided 2026-09-20 and
written up in FIX.org, "Milestone 5, and the sweep behind it":
**A written number may stand where a type variable stands, under `numeric?`.**
`(defn pos? [x $t] bool {:where (numeric? $t)} (> x 0))` is the family the
feature was asked for, and the bound is what makes the `0` 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. Nothing weaker admits it —
`ordered?` admits an enum, which holds no number. A *float* literal is refused
at a type variable even under `numeric?`, because `numeric?` covers the
integers too and a float literal is never usable where an integer is wanted.
The range check belongs to each copy, not to the definition.
**Implicit widening does not cross a generic binding.** A concrete argument at
a variable an earlier argument already bound has to be that type, not merely
one that widens into it — otherwise which copy a call gets depends on which
argument was written first. Letting the pair meet at the wider type stays
available as a later loosening; nothing written under this rule would stop
compiling. An untyped literal is unaffected: it has no type of its own to keep.
**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
carries its own. A dyn argument asks the second question of the first
machinery, and the refusal says so. Whether dyn should ever flow through a
generic is open.
## Function values
Three cases, split by whether the value escapes the frame that made it.

13
test/dune
View File

@ -60,6 +60,10 @@
; it defines a get of its own — shadow-builtin.flan, which is the pin that
; a shadow stops at the file that declared it.
(glob_files programs/pkgs/shadowed/*)
; The package whose exports are generic, which pkg-generic.flan and
; pkg-generic-reject.flan import: the body has to be present where the copy
; is made, so the directory comes whole like every other package.
(glob_files programs/pkgs/gen/*)
; The synthetic C header the importer's table reads. Committed rather than
; reached for on the machine: the raylib case needs raylib installed, at the
; right version, with a variable set, so it skips everywhere and covers
@ -221,7 +225,8 @@
(glob_files programs/pkgs/macring/*)
(glob_files programs/pkgs/macspin/*)
; And the package shadow-builtin.flan imports.
(glob_files programs/pkgs/shadowed/*))
(glob_files programs/pkgs/shadowed/*)
(glob_files programs/pkgs/gen/*))
(action (run ./test_valgrind.exe)))
; The corpus a fourth time, through the hand-written x86-64 backend, compared
@ -280,7 +285,8 @@
(glob_files programs/pkgs/macring/*)
(glob_files programs/pkgs/macspin/*)
; And the package shadow-builtin.flan imports.
(glob_files programs/pkgs/shadowed/*))
(glob_files programs/pkgs/shadowed/*)
(glob_files programs/pkgs/gen/*))
(action
(setenv SURVEY_STRICT 1
(setenv SURVEY_QUIET 1
@ -445,7 +451,8 @@
(glob_files programs/pkgs/macring/*)
(glob_files programs/pkgs/macspin/*)
; And the package shadow-builtin.flan imports.
(glob_files programs/pkgs/shadowed/*))
(glob_files programs/pkgs/shadowed/*)
(glob_files programs/pkgs/gen/*))
(action
(setenv SURVEY_STRICT 1
(setenv SURVEY_QUIET 1

53
test/programs/generics.flan
View File

@ -50,6 +50,37 @@
{:where (ordered? $t)}
(min (max x lo) hi))
;; An integer *literal* where the type variable is wanted, which is what the
;; sign 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.
;;
;; The -t? suffix is because the prelude now carries pos?/neg?/zero? itself.
;; These are the same three bodies written in an ordinary program, which is
;; what says the machinery belongs to the language and not to the prelude.
(defn pos-t? [x $t] bool {:where (numeric? $t)} (> x 0))
(defn neg-t? [x $t] bool {:where (numeric? $t)} (< x 0))
(defn zero-t? [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 +162,28 @@
(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-t? 3))
(println (neg-t? (i8 -3)))
(println (zero-t? (u8 0)))
(println (zero-t? 0.0))
(println (pos-t? (u16 1)))
(println (neg-t? (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))
;; And the prelude's own three, which are these bodies under their real
;; names. The -0.0 is the one worth asserting: IEEE says -0.0 = 0.0 and
;; zero? does not second-guess it.
(println (pos? (i64 3)))
(println (zero? -0.0))
(println (neg? (u8 3)))
(show 3)
(show 4.5)
(show "text")

12
test/programs/pkg-generic-reject.flan Normal file
View File

@ -0,0 +1,12 @@
;;;; The call-site half of a bound written in another file.
;;;;
;;;; gen/largest is {:where (ordered? $t)}, and a [string] is not ordered. The
;;;; refusal has to arrive here, against the call that asked for the copy, and
;;;; it has to quote the clause — a message pointing into pkgs/gen/gen.flan
;;;; would be naming a line the caller did not write and cannot change.
(import gen "pkgs/gen")
(defn main [] i32
(let [ss ["a" "b"]]
(println (gen/largest (slice ss 0 2))))
0)

35
test/programs/pkg-generic.flan Normal file
View File

@ -0,0 +1,35 @@
;;;; A generic defined in a package, instantiated by the program.
;;;;
;;;; The copies are made here, from a body written there. Three things are
;;;; being asserted and only the first is obvious: that the call works at all;
;;;; that instantiation is still transitive across the boundary, so gen/ends
;;;; asking for gen/last-of at its own variable generates that copy from this
;;;; file's call site; and that a {:where} clause written in the package is
;;;; what a caller here is judged against.
;;;;
;;;; And one thing in the other direction: a generic written *here* calling a
;;;; generic written *there* at its own variable, which is the shape that only
;;;; resolves once both bodies are in one namespace.
(import gen "pkgs/gen")
;;; Local generic over the imported one, at this file's variable.
(defn tail-twice [s [$t]] $t
{:where (numeric? $t)}
(+ (gen/ends s) (gen/ends s)))
(defn main [] i32
(let [ns [5 3 9 1]
fs [2.5 0.5 1.5]]
;; One package generic at two element types: two copies, one body.
(println (gen/last-of (slice ns 0 4)))
(println (gen/last-of (slice fs 0 3)))
;; The transitive one, also at two.
(println (gen/ends (slice ns 0 4)))
(println (gen/ends (slice fs 0 3)))
;; The bounded one.
(println (gen/largest (slice ns 0 4)))
;; And the local generic that calls across the boundary at its own $t.
(println (tail-twice (slice ns 0 4)))
(println (tail-twice (slice fs 0 3))))
0)

33
test/programs/pkgs/gen/gen.flan Normal file
View File

@ -0,0 +1,33 @@
;;;; A package whose exports are generic.
;;;;
;;;; The spike's "no plan" bucket named this one, and named what makes it
;;;; work: Load flattens every import into one namespace *before* the checker
;;;; runs, so the generic's body is present at the call site the way a C++
;;;; template's is because it sits in a header. Nothing here crosses a real
;;;; compilation-unit boundary, and the day a package becomes one, this is the
;;;; thing that has to change — a copy is made from a body, and a body that
;;;; did not cross cannot be copied.
;;;;
;;;; What this package is for: a generic called from the program at two types,
;;;; a bounded generic whose {:where} has to be readable from outside the
;;;; file that wrote it, and a generic that calls another generic in its own
;;;; package at its own variable, so the transitive copy is generated from a
;;;; call site two files away.
(defn last-of [s [$t]] $t
(at s (- (len s) 1)))
;;; Calls last-of at its own variable: the copy of last-of is generated when
;;; this is instantiated, and this is instantiated from the program.
(defn ends [s [$t]] $t
(last-of s))
;;; The bound travels with the signature. A caller that passes a type the
;;; clause refuses is refused at the call, against a requirement written in
;;; another file.
(defn largest [s [$t]] $t
{:where (ordered? $t)}
(let [m (at s 0)]
(dotimes [i (len s)]
(set m (max m (at s i))))
m))

51
test/test_acceptance.ml
View File

@ -2513,6 +2513,30 @@ let () =
raylib itself. Loading it twice would declare every binding twice. *)
outputs "a package reached along two routes" "programs/pkg-shared.flan"
"ok\n";
(* A generic defined in a package and instantiated by the program. The
spike's "no plan" bucket named this and named what makes it work: Load
flattens every import into one namespace before the checker runs, so
the generic's *body* is present where the copy is made, the way a C++
template's is because it sits in a header. It is also the thing that
has to change the day a package becomes a real compilation unit — a
copy is made from a body, and a body that did not cross cannot be
copied.
Three shapes, because only the first is obvious. gen/last-of at two
element types is one body and two copies. gen/ends calls gen/last-of at
its *own* variable, so that copy is generated from this file's call
site and instantiation is still transitive across the boundary. And
tail-twice is a generic written here calling one written there at its
own $t, which only resolves once both bodies are in the one namespace.
The numbers are: last-of at i32 and f64, ends at the same two, largest
at i32, and tail-twice at both. *)
outputs "a generic defined in a package" "programs/pkg-generic.flan"
"1\n1.5\n1\n1.5\n9\n2\n3\n";
outputs ~opt:"-O0" "a generic defined in a package, -O0"
"programs/pkg-generic.flan" "1\n1.5\n1\n1.5\n9\n2\n3\n";
(* The call-site half of a bound written in another file is pinned with
the other refusals, further down — see "a package generic's bound". *)
(* And the diamond with a type crossing it, which is the case the dedupe
exists for rather than a restatement of the one above. pkg-diamond
imports area and draw; both import shape; a shape/Box is built inside
@ -2598,9 +2622,22 @@ 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. The [true true false] after them is the
prelude's own pos?/zero?/neg? — the same three bodies under their real
names — and the middle one is zero? at -0.0, which IEEE says is zero
and which this does not second-guess. *)
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\
true\ntrue\nfalse\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"
@ -2661,6 +2698,18 @@ let () =
beneath it, naming rl/with-mode-2d at the call site rather than
pointing into the package — that half is rendering and is not asserted
here. *)
(* A {:where} clause travels with the signature across a package
boundary, and the refusal it produces lands at the call. Both halves
are asserted because only together are they the Elm-grade answer: the
type that failed and the clause it failed against, quoted here rather
than pointed at in pkgs/gen/gen.flan — a line the caller did not write
and cannot change. *)
refuses "a package generic's bound, refused at the call"
"programs/pkg-generic-reject.flan"
"string does not answer ordered?";
refuses "and the refusal quotes the clause the package wrote"
"programs/pkg-generic-reject.flan" "{:where (ordered? $t)}";
refuses "with-mode-2d written without a camera"
"programs/rl-with-reject.flan"
"with-mode-2d-takes-a-camera-and-a-body";

194
test/test_flan.ml
View File

@ -1161,12 +1161,15 @@ let () =
| Some { Tast.params = [ Types.Dyn; Types.Dyn ]; _ } -> ()
| _ -> check "an unannotated pair is two dyn parameters" false)
| exception _ -> check "an unannotated pair is two dyn parameters" false);
(* A bare lowercase name is still an unimplemented type variable everywhere a
type is the only thing a slot can hold. A defn's parameter vector stopped
being such a place — a slot there may be a parameter instead — so the rule
is exercised where it still decides, at a field. *)
(* A bare lowercase name where a type is the only thing a slot can hold. It
used to be reported as unimplemented generics; generics are implemented,
and a lowercase name is a type variable only where a defn signature
introduced one with the sigil — a struct field is not such a place and
never will be, since only a signature binds. So the sentence names the
sigil rather than a milestone. A defn's parameter vector stopped being a
type-only slot, which is why the rule is exercised at a field. *)
rejects_check "a real type variable" "(defstruct Holder [x elem])"
~needle:"milestone 5";
~needle:"write $elem in the parameter vector";
rejects_check "an unknown concrete type" "(defn f [x Widget] ())"
~needle:"unknown type Widget";
@ -2073,9 +2076,16 @@ let () =
(* [(Pair i32)] in a defvar falls down the value fork now that the third
element takes either reading, and the generics answer the type fork gave
it has to be reachable from here too. *)
rejects_check "a capitalised call with arguments is generics"
(* A capitalised head with arguments is a *type* given type arguments, and
that is the half of generics that is not built — Types.Named is a bare
string with no room for parameters. The sentence says which half, since
generic functions are here and pointing at them is the useful part. *)
rejects_check "a capitalised call with arguments is a generic type"
"(defvar x (Pair i32)) (defn f [] i32 0)"
~needle:"is generic code, which is milestone 5";
~needle:"is a generic type, which is not there yet";
accepts "and the generic function it points at is"
"(defn pair-fst [a $t b $u] $t (do b a))\n\
(defn main [] () (println (pair-fst 1 true)))";
rejects_check "defined twice" "(defn f [] ()) (defn f [] ())"
~needle:"defined twice";
accepts "main with no parameters and no return" "(defn main [] ())";
@ -2895,8 +2905,8 @@ let () =
defn's body that just answers one says nothing about them. *)
rejects_check "an fn with nothing to say what it takes"
"(defn f [] () (fn [x] x))" ~needle:"nothing here says what this fn";
rejects_check "type variables are milestone 5" "(defn f [] a 0)"
~needle:"milestone 5";
rejects_check "a lowercase return type no signature introduced"
"(defn f [] a 0)" ~needle:"write $a in the parameter vector";
(* The other half: a name in value position now *works*, and the arity is
checked against the function it names. *)
rejects_check "a function value at the wrong arity"
@ -4815,6 +4825,172 @@ let () =
accepts "and is accepted when it is"
"(defn outer [s [$t]] () {:where (ordered? $t)} (sort s))";
(* ── A generic call inside an abandoned widening trial ──────────────
The two features land days apart and meet here. A binary operator whose
operands disagree re-checks the right one at the left one's type inside a
[trial], and on a refusal reconsiders with the join — so a generic call
written on the right is checked twice, once in a pass that is thrown
away. What the discarded pass leaves behind in [env] is the question, and
[env] is the program's table, not the form's: an instantiation made
during it does not go back out, because [instantiate] rewinds only a copy
whose *body* refused.
It does not have to. The answer is that the two passes cannot disagree
about which copy to make, and that is a consequence of the rule above
rather than luck: a generic call's instantiation is read off its
arguments and never off the ambient want — an unbound variable is checked
with no expectation at all, and a bound one no longer widens — so the
trial and the live pass ask [instantiate] for the same types, and the
second ask is a cache hit on the first. One copy is emitted, at the type
the arguments chose, and the widening happens around the call.
(twoq 2 3) is i32 both times; the i8 on the left is what moves. *)
(let p =
checked
"(defn twoq [a $t b $t] $t {:where (numeric? $t)} (+ a b))\n\
(defn main [] () (let [small (i8 1)] \
(println (+ small (twoq 2 3)))))"
in
let copies =
List.filter
(fun (f : Tast.fn) ->
String.length f.Tast.name >= 5 && String.sub f.Tast.name 0 5 = "twoq-")
p.Tast.fns
in
match copies with
| [ { Tast.name = "twoq-i32"; _ } ] -> ()
| l ->
check
(Printf.sprintf
"a generic inside an abandoned trial is instantiated once: %s"
(String.concat " " (List.map (fun (f : Tast.fn) -> f.Tast.name) l)))
false);
(* ── A type variable is not instantiated at dyn ─────────────────────
Nothing stopped it before: dyn is an ordinary case of Types.t, so it
substituted like any other type and the copy was generated. What the copy
then ran into was the dyn answers that are not all there — (Option dyn)
has no descriptor the collector can find — and the refusal arrived from
inside the generic's own source. (or-else (Some d) e) over two dyns used
to be reported against <prelude>:385, a line the caller did not write.
The refusal is at the call site now, and it names the other model rather
than only saying no. *)
rejects_check "a type variable is not instantiated at dyn"
~needle:"is not instantiated at dyn"
"(defn idf [x $t] $t x)\n\
(defvar d dyn 5)\n\
(defn main [] () (println (idf d)))";
rejects_check "and the refusal names the dyn side rather than only saying no"
~needle:"defmethod"
"(defn idf [x $t] $t x)\n\
(defvar d dyn 5)\n\
(defn main [] () (println (idf d)))";
(* Nor at a type that merely *reaches* a dyn, which is the shape that used
to walk furthest before failing: (Option dyn) is the case the collector
has no descriptor for, and the refusal for it arrived from <prelude>:385.
It arrives here now, against the call that asked for the copy. *)
rejects_check "nor at a type that merely reaches a dyn"
~needle:"$t = (Option dyn)"
"(defn maybe [] (Option dyn) None)\n\
(defn idf [x $t] $t x)\n\
(defn main [] () (println (some? (idf (maybe)))))";
(* A variable that carries a clause keeps the clause's refusal, which names
the predicate the signature actually wrote down — the more specific of
the two answers, and the one the generic cast's pin above depends on. *)
rejects_check "a bounded variable is still refused by its bound"
~needle:"numeric?"
"(defn twice [x $t] $t {:where (numeric? $t)} (+ x x))\n\
(defvar d dyn 5)\n\
(defn main [] () (println (twice d)))";
(* ── Implicit widening does not cross a generic binding ─────────────
Widening landed after generics did, and the rule it left behind depended
on the order the arguments were written in: the i8-then-i64 call was
refused because i64 into i8 can lose, and the i64-then-i8 call was
*accepted*, because $t had already bound to i64 and the i8 widened into
the want. Same two values, same function, two answers.
Neither was unsound — a widen cannot change a number — but which copy a
program gets should not turn on which argument came first, so both are
refused now and both name the binding. Letting the pair join at the wider
type is the other coherent rule and it stays available: it can be added
without invalidating anything written under this one, which is why this
is the direction to be wrong in. FIX.org, "Generics and implicit
widening". *)
rejects_check "a narrower argument does not widen into a bound type variable"
~needle:"was bound to i64 by an earlier argument"
"(defn eq2? [a $t b $t] bool {:where (equal? $t)} (= a b))\n\
(defn main [] () (println (eq2? (i64 3) (i8 3))))";
rejects_check "and the other argument order refuses identically"
~needle:"was bound to i8 by an earlier argument"
"(defn eq2? [a $t b $t] bool {:where (equal? $t)} (= a b))\n\
(defn main [] () (println (eq2? (i8 3) (i64 3))))";
(* The written conversion is what the message asks for, and it is accepted:
the refusal is about the *implicit* step, not about reaching i64. *)
accepts "the written conversion is accepted"
"(defn eq2? [a $t b $t] bool {:where (equal? $t)} (= a b))\n\
(defn main [] () (println (eq2? (i64 3) (i64 (i8 3)))))";
(* An untyped constant has no type of its own to keep, so it still takes the
variable's. Nothing is converted here — three i64s were written. *)
accepts "an untyped literal still takes a bound type variable's type"
"(defn clamp3 [x $t lo $t hi $t] $t {:where (ordered? $t)} \
(min (max x lo) hi))\n\
(defn main [] () (println (clamp3 (i64 12) 0 10)))";
(* And the shapes widening cannot reach are untouched, which is the reason
the rule costs so little: [Types.widens_to] admits only numeric scalars,
so a variable bound inside a slice or a function type leaves a parameter
no widening applied to in the first place. *)
accepts "a variable bound inside a constructor is unaffected"
"(defn sort2 [s [$t] before? (Fn [$t $t] bool)] () \
(sort-by s before?))\n\
(defn main [] () (let [ns [5 3 9 1]] \
(sort2 (slice ns 0 4) (fn [a b] (< a b))) (println (at ns 0))))";
(* A form with no type of its own is still checked against the parameter:
the trial that asks for its natural type refuses, and the want it always
had is what it falls back to. *)
accepts "a form that needs a want still gets one at a bound type variable"
"(defn pick [a $t b $t] $t (do b a))\n\
(defn main [] () (println (pick (i64 3) (zeroed))))";
(* ── 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 above-zero? [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))";
(* And the prelude's own three, which are that body under its real name at
every numeric type from one definition. *)
accepts "the prelude's sign family answers at six numeric types"
"(defn main [] () (println (pos? 3) ) (println (neg? (i8 -1))) \
(println (zero? (u8 0))) (println (zero? 0.0)) \
(println (pos? (u64 1))) (println (neg? (f32 -0.5))))";
(* [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