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

A thunk named for the order it was minted in is a different signature after a reorder

Browse Source 
Three from a review of the commit before this one, and the first is a dev
loop defect.  Naming the widening thunk thick/<count so far> put traversal
order into a symbol, and Session.compatible compares a reload's functions
against the running program's by name -- so swapping two calls in a body
renamed nothing the programmer can see and reported "thick/0 changes
signature, from [i32] i32 to [i64] i64.  Restart to change it."  The name is
the signature again, written by thick_enc: every type self-delimiting, an
atom as its length and then its spelling, so the boundaries mangle_ty loses
are in the string rather than inferred from the separators.  mangle_ty is
untouched -- it is load-bearing for the instantiation names a backtrace, a
Reach edge and a dev cell show -- and the memo stays keyed on the types.
fn-thunk-reload.flan is the pair of widenings and test_session reorders them.

The second was a silent miscompile.  bind_ty's Fn-pattern-against-CFn-argument
arm was structural, so it matched nested function positions too, and the
catch-up pass that builds the thunk compares the whole substituted parameter
list -- false when the mismatch is inside one, and the fallthrough handed the
argument over unchanged: one word where the instance declares two, 255 on
both backends with nothing said anywhere.  The widening is a value the caller
builds around the whole argument and there is nowhere inside one to build it,
so the arm is admitted at the top of an argument's type and nowhere else, and
the catch-up arm is total over the pair rather than guarded -- bind_ty's
fallthrough is Types.fits, which admits Never, so a binding can still succeed
over a pair the two words cannot bridge.  fn-generic-nested.flan is the
parameter position and fn-generic-nested-return.flan the return one.

And the third closes the hole the escaping inversion was for.  A match arm
binds the case's fields to slots and the store that fills them is inside the
branch, not in any form escape_check reads as a binding, so (match o (Some f)
f ...) handed back through a name what a case-field read cannot hand back at
all -- sound only because Some_ denies suspects.  An arm's slots of function
type are suspect now, for the same reason the read itself is.
This commit is contained in:
Joseph Ferano 2026-09-21 15:44:28 +07:00
parent a28aeda633
commit 0c711942f7
7 changed files with 231 additions and 36 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

154
lib/check.ml
View File

@ -1716,7 +1716,7 @@ let signature_tyvars (fn : Ast.fn) =
and with the same rule: a variable already bound must match what it is
bound to, so [(pair 1 2.0)] over [a $t b $t] is a refusal and not a
second instantiation. *)
let rec bind_ty subst (pat : Types.t) (arg : Types.t) =
let rec bind_ty ?(widen = false) subst (pat : Types.t) (arg : Types.t) =
match pat, arg with
| Types.Var v, a ->
(match List.assoc_opt v !subst with
@ -1729,24 +1729,36 @@ let rec bind_ty subst (pat : Types.t) (arg : Types.t) =
| Types.Array (n, p), Types.Array (m, a) -> Int64.equal n m && bind_ty subst p a
| Types.Map (k, v), Types.Map (k', v') ->
bind_ty subst k k' && bind_ty subst v v'
(* Both function types, and the widening between them.
(* Each function type against its own. *)
| Types.Fn (ps, r), Types.Fn (ps', r')
| Types.CFn (ps, r), Types.CFn (ps', r') ->
List.length ps = List.length ps'
&& List.for_all2 (bind_ty subst) ps ps' && bind_ty subst r r'
(* And the widening between them, which is admitted at the top of an
argument's type and nowhere inside it.
[(Fn [$t] $t)] against a [(CFn [i32] i32)] is the shape every caller of
a generic higher-order function now has, because a [defn]'s name carries
a generic higher-order function has, because a [defn]'s name carries
[CFn]: [(apply2 bump 1)]. It has to bind here, where the variables are
decided, and not only in [expect] — [generic_call] binds first and would
have reported the mismatch before [expect] was ever reached, which is
how this arrived as a regression against a program that used to compile.
have reported the mismatch before [expect] was ever reached.
The prelude hides it: its higher-order functions bind [$t] from an
The prelude hides that: its higher-order functions bind [$t] from an
earlier argument, so [subst_ty] has already made the parameter concrete
by the time this sees it and [(map-in-place s double)] never took this
path. That is why the corpus stayed green over a real break.
path.
[widen] is why it goes no deeper. The widening is a *value* the caller
builds — a thunk, minted at the call — and there is exactly one place to
build it, around the whole argument. A [(Fn [(Fn [$t] $t)] i32)]
parameter handed a [(CFn [(CFn [i32] i32)] i32)] would need one built
inside the argument's own parameter list, where no caller stands, so the
two types do not meet there and the pattern does not match. What reaches
the fallthrough below is an ordinary mismatch and is refused as one, the
same answer a call with no type variables in it gets.
One way, as everywhere else: a [CFn] pattern does not admit an [Fn]
argument. *)
| Types.Fn (ps, r), Types.Fn (ps', r')
| Types.CFn (ps, r), Types.CFn (ps', r')
| Types.Fn (ps, r), Types.CFn (ps', r') ->
| Types.Fn (ps, r), Types.CFn (ps', r') when widen ->
List.length ps = List.length ps'
&& List.for_all2 (bind_ty subst) ps ps' && bind_ty subst r r'
(* Nothing generic left on the pattern side: this is ordinary type
@ -2725,22 +2737,63 @@ let unbox_option ctx loc (t : Types.t) (got : Tast.expr) : Tast.expr =
for — the same arrangement [struct_key_pair] uses for a map's hash and
equality pair, and for the same reason.
**The memo is keyed on the types and the symbol is a counter**, and this
is not a matter of taste. [mangle_ty] flattens a whole signature into one
hyphen-joined string, which loses arity and every type boundary with it:
[(CFn [(Ptr i32)] i32)] and [(CFn [ptr i32] i32)] — the second over a
struct someone called [ptr] — both flatten to [cfn-ptr-i32-to-i32]. Keyed
on that string, the second widening silently reuses the first's thunk and
calls it with the wrong arity, which is a miscompile on both backends and
not a refusal anywhere. The types are the key, compared with
[Types.equal], and nothing is derived from a name.
**The memo is keyed on the types and the symbol spells them back**, and
both halves matter. [mangle_ty] cannot serve as the spelling: it flattens
a whole signature into one hyphen-joined string, which loses arity and
every type boundary with it, so [(CFn [(Ptr i32)] i32)] and
[(CFn [ptr i32] i32)] — the second over a struct someone called [ptr] —
both come out [cfn-ptr-i32-to-i32]. Keyed on that string, the second
widening silently reuses the first's thunk and calls it with the wrong
arity, which is a miscompile on both backends and not a refusal anywhere.
So the key is the types, compared with [Types.equal], and the name is
[thick_enc]'s encoding, which no two signatures share.
([mangle_ty]'s ambiguity is older than this and is still there for the
generic instantiation names it was written for. At one type's granularity
it is hard to reach; at a whole signature's it is a line of Flan away.)
**Why the name has to be the signature and not a counter.** A counter over
the thunks minted so far is unique within one compilation and says nothing
across two: reorder the definitions in the file and [thick/0] is a
different signature than it was. [Session.compatible] compares a reload's
functions against the running program's *by name*, so a thunk that changed
shape under a fixed name reads to it as a function whose signature was
edited, and the dev loop answers a form reorder with "Restart to change
it". Spelled from the types, the name moves with the shape and that
comparison is right again for the same reason it is right everywhere else.
[fparent] is [<thick>]: not a name anyone wrote, so [defs] hides it, and a
marker the redefinition modules match on to carry a copy of their own. *)
(* A signature written so that it can be read back: every type is
self-delimiting, so no two distinct signatures encode alike.
An atom is its length and then its spelling, which is what closes the gap
[mangle_ty] leaves — a name's boundaries are in the string rather than
inferred from the separators. A constructor is one letter, and the two
that hold a count write it before their children, so [(Fn [i32] i32)] and
[(Fn [] (Fn [i32] i32))] cannot read alike. [Named] and [Enum] carry
different letters because a struct and a C enum may share a spelling. *)
let rec thick_enc (t : Types.t) =
let atom s = Printf.sprintf "%d-%s" (String.length s) s in
let arrow tag ps r =
Printf.sprintf "%s%d-%s" tag (List.length ps)
(String.concat "-" (List.map thick_enc (ps @ [ r ])))
in
match t with
| Types.Named n -> "n" ^ atom n
| Types.Enum n -> "e" ^ atom n
| Types.Var v -> "y" ^ atom v
| Types.Slice e -> "s" ^ thick_enc e
| Types.Ptr e -> "p" ^ thick_enc e
| Types.Vec e -> "v" ^ thick_enc e
| Types.Option e -> "o" ^ thick_enc e
| Types.Array (n, e) -> Printf.sprintf "a%Ld-%s" n (thick_enc e)
| Types.Map (k, v) -> Printf.sprintf "m%s-%s" (thick_enc k) (thick_enc v)
| Types.Fn (ps, r) -> arrow "f" ps r
| Types.CFn (ps, r) -> arrow "c" ps r
| t -> atom (mangle_ty t)
let thick_thunk env loc ps r =
let same (f : Tast.fn) =
f.Tast.fparent = Some "<thick>"
@ -2755,16 +2808,7 @@ let thick_thunk env loc ps r =
let fty = Types.CFn (ps, r) in
let args = List.mapi (fun i t -> mk loc t (Tast.Local i)) ps in
let callee = mk loc fty (Tast.Local n) in
(* Counted over the thunks already minted, which is a fact about this
compilation and not about the signature — so no two of them can share
a name however the types are spelled. *)
let name =
Printf.sprintf "thick/%d"
(List.length
(List.filter
(fun (f : Tast.fn) -> f.Tast.fparent = Some "<thick>")
env.lifted))
in
let name = "thick/" ^ thick_enc fty in
env.lifted <-
{ Tast.name; params = ps;
slots = Array.of_list (ps @ [ fty ]);
@ -9102,7 +9146,9 @@ and generic_call ctx ~want loc name vars pats pret args =
true)
| _ -> false
in
if (not handled) && not (bind_ty subst p a.Tast.ty) then
(* [~widen]: this is the top of an argument's type, which is the one
place a widening thunk can be built around it. See [bind_ty]. *)
if (not handled) && not (bind_ty ~widen:true 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);
a)
@ -9161,13 +9207,27 @@ and generic_call ctx ~want loc name vars pats pret args =
is.
A *concrete* [Fn] parameter never reaches this: it was checked
with a want in the first pass and [expect] widened it there. *)
with a want in the first pass and [expect] widened it there.
The arm is total over the pair, and that is the point of writing
it as an [if] rather than as a guard. [bind_ty]'s fallthrough is
[Types.fits], which admits [Never] where the instance's signature
wants a type — so a binding can succeed over a pair these two
words cannot bridge, and a fallthrough of "hand the argument over
unchanged" would pass one word where the instance declares two.
Every [CFn] arriving at an [Fn] parameter either gets its thunk
here or gets the refusal, which is the answer [expect] gives a
call with no type variables in it. *)
| _ ->
(match subst_ty !subst pat, a.Tast.ty with
| Types.Fn (ps, r), Types.CFn (ps', r')
when Types.equal (Types.Fn (ps, r)) (Types.Fn (ps', r')) ->
mk a.Tast.loc (Types.Fn (ps, r))
(Tast.Thicken (thick_thunk ctx.env a.Tast.loc ps r, a))
| Types.Fn (ps, r), Types.CFn (ps', r') ->
if Types.equal (Types.Fn (ps, r)) (Types.Fn (ps', r')) then
mk a.Tast.loc (Types.Fn (ps, r))
(Tast.Thicken (thick_thunk ctx.env a.Tast.loc ps r, a))
else
fail a.Tast.loc "%s expects %s here, found %s" name
(Types.to_string (Types.Fn (ps, r)))
(Types.to_string a.Tast.ty)
| _ -> a))
pats targs
in
@ -11745,10 +11805,32 @@ let escape_check (fn : Tast.fn) =
let go (e : Tast.expr) =
(match e.Tast.e with
| Tast.Let (bs, _) ->
(* A binding is where a suspect spreads, and the only place it does. *)
(* A binding is where a suspect spreads, and one of the two places it
does. *)
List.iter
(fun (slot, v) -> if escaping suspects v then suspects := slot :: !suspects)
bs
(* And the other: an arm's pattern binds the case's fields to slots, and
the store that fills them is inside the branch rather than in a form
this walk reads as a binding. Reading the same field by hand is a
[CaseField] and suspect — a copy of a captured function value carries
whatever environment the original did — so the slot the pattern binds
it to is suspect too, or [(match o (Some f) f ...)] would hand back
through a name what [(case-field o ...)] cannot hand back at all.
Every arm's binds, not only an [Option]'s: a data type's field of
function type is written through [MakeCase], which denies suspects,
and read back through this. *)
| Tast.Match (_, arms) ->
List.iter
(fun (a : Tast.arm) ->
List.iter
(fun s ->
match fn.Tast.slots.(s) with
| Types.Fn _ -> suspects := s :: !suspects
| _ -> ())
a.Tast.binds)
arms
| Tast.Set (_, v) -> deny "a store" [ v ]
| Tast.Return (Some v) -> deny "a return" [ v ]
| Tast.Some_ v -> deny "an Option" [ v ]

16
test/programs/fn-escape-match.flan Normal file
View File

@ -0,0 +1,16 @@
;; A match arm's binding is a binding, and the escape check has to see it.
;;
;; Reading the payload by hand is a case-field read, which is suspect: a copy
;; of a function value carries whatever environment the original did. Binding
;; it to a name in an arm is the same read, and the store that fills the arm's
;; slot is inside the branch rather than in any form the walk reads as a
;; binding — so without the arm's slots being taken as suspect too, the Vec,
;; slice, struct and pointer spellings of this were all refused while the one
;; that goes through Option and a name was not.
(defn leak [o (Option (Fn [] i32))] (Fn [] i32)
(match o
(Some f) f
None (fn [] 0)))
(defn main [] i32 0)

15
test/programs/fn-generic-nested-return.flan Normal file
View File

@ -0,0 +1,15 @@
;; The same line drawn in return position, which is the half that is easy to
;; miss: a (Fn [] (Fn [] $t)) parameter handed a (CFn [] (CFn [] i32)) needs
;; the inner widening built by whatever calls the *argument*, and that is the
;; generic's own body, which was compiled against the parameter's type and not
;; against this caller's.
(defn inner [] i32 3)
(defn outer [] (CFn [] i32) inner)
(defn call-twice [g (Fn [] (Fn [] $t))] $t ((g)))
(defn main [] i32
(println (call-twice outer))
0)

19
test/programs/fn-generic-nested.flan Normal file
View File

@ -0,0 +1,19 @@
;; The widening between the two function types is a value the caller builds —
;; a thunk, minted at the call — so there is exactly one place to build it:
;; around the whole argument. Nested inside one, there is no caller standing
;; where the thunk would have to go.
;;
;; The parameter here is (Fn [(Fn [$t] $t)] i32) and taker's address carries
;; (CFn [(CFn [i32] i32)] i32). Admitting that structurally binds $t and then
;; hands one word where the instance declares two, in a position no later pass
;; can widen: the catch-up that builds the outer thunk compares the whole
;; substituted parameter list and this mismatch is inside it. A call with no
;; type variables in it is refused, so this one is too.
(defn taker [h (CFn [i32] i32)] i32 (h 1))
(defn hof [g (Fn [(Fn [$t] $t)] i32) k $t] i32 (g (fn [x] x)))
(defn main [] i32
(println (hof taker 0))
0)

24
test/programs/fn-thunk-reload.flan Normal file
View File

@ -0,0 +1,24 @@
;; Two widenings of different signatures in one program, so the dev loop has
;; two thunks to tell apart across a reload.
;;
;; A thunk is not a function anybody wrote, so nothing in the source names it
;; and nothing can be edited to rename it. But Session.compatible compares a
;; reload's functions against the running program's *by name*, and a name that
;; means whichever thunk was minted first means a different signature the
;; moment the forms are reordered — which reads to the session as a function
;; whose signature was edited, and answers an ordinary edit with "Restart to
;; change it". So the name is the signature, spelled so that it can be read
;; back, and reordering these two calls is an ordinary body change.
(defn a1 [x i32] i32 (+ x 1))
(defn b1 [x i64] i64 (+ x 1))
(defn use32 [f (Fn [i32] i32)] i32 (f 1))
(defn use64 [f (Fn [i64] i64)] i64 (f 1))
(defn both [] i32
(println (use32 a1))
(println (use64 b1))
0)
(defn main [] i32 (both))

15
test/test_acceptance.ml
View File

@ -3990,6 +3990,19 @@ level "1"
outputs ~opt:"-O0"
"a generic that binds its variable through a function type, -O0"
"programs/fn-generic.flan" fn_generic_out;
(* And where the same binding stops. The widening is a value the caller
builds around the whole argument, so a function type nested inside an
argument's own type has no caller standing where its thunk would go —
and the catch-up pass that builds the outer one compares the whole
substituted parameter list, so a mismatch inside it is not something
any later pass can repair. Both positions, because the return one is
the easier of the two to leave open. *)
refuses "a nested function type does not widen"
"programs/fn-generic-nested.flan"
"hof expects (Fn [(Fn [t] t)] i32) here";
refuses "and neither does one in return position"
"programs/fn-generic-nested-return.flan"
"call-twice expects (Fn [] (Fn [] t)) here";
outputs ~dev:true "an fn capturing by value, dev" "programs/fn-capture.flan"
fn_capture_out;
@ -4013,6 +4026,8 @@ level "1"
body's — so both are ways for a suspect to be a function's answer. *)
refuses "an index read is a read like any other"
"programs/fn-escape-at.flan" "may carry an environment";
refuses "a match arm's binding is a binding"
"programs/fn-escape-match.flan" "may carry an environment";
refuses "a captured function value cannot be handed back"
"programs/fn-escape-copy.flan" "a return would outlive the frame";
refuses "a handler-bind's value is a return too"

24
test/test_session.ml
View File

@ -1177,6 +1177,30 @@ let () =
| exception Loc.Error { Loc.dmsg = m; _ } ->
fail "an expression that instantiates a generic: %s" m);
(* ── The widening thunks, across a reorder ──────────────────────
A thunk is a function nobody wrote and nothing in the source names, so
the only way one can change is the program growing or losing a widening
— and reordering two calls is neither. But [compatible] compares by
name, so a thunk named for the order it was minted in means one
signature before the edit and another after, and the session answers a
body change with "Restart to change it" about a name the programmer
cannot find. The name spells the signature, so this reload is ordinary.
Both directions of the pair are here — the same two calls, swapped —
because a name that is a counter is wrong for exactly one of them and
the test has to be the one that is wrong. *)
(let t, _ = Session.create ~file:"programs/fn-thunk-reload.flan" () in
match
Session.eval t
"(defn both [] i32 (println (use64 b1)) (println (use32 a1)) 0)"
with
| c ->
if not (List.mem "both" c.Session.fns) then
fail "reordering two widenings installed %s"
(String.concat " " c.Session.fns)
| exception Loc.Error { Loc.dmsg = m; _ } ->
fail "reordering two widenings was refused: %s" m);
(* ── A class whose slots changed ────────────────────────────────
The dev loop's half of CLHS 4.3.6. Three things have to be true of the
session for the runtime's migration to ever be reached: a changed slot