The foreign boundary walks two questions, and they are not the same question:
one counts a dyn reachable only through a further pointer, the other counts
any dyn at all. They shared a [seen] set across the crossing between them, so
a type name marked visited on the way down was pruned from the walk below the
pointer — and the shape that hits it is a struct with a pointer to its own
name. [(defstruct Node [next (Ptr Node) x dyn])] at a [(Ptr Node)] parameter
was accepted, while exactly the same thing unrolled into two types was
refused, which is the tell. A cycle of two, [A {b (Ptr B), x dyn}] and
[B {a (Ptr A)}], went the same way.
C hung a malloc'd node off [next], put a dyn in it, and Flan allocated a
hundred thousand times: heap-use-after-free in flan_dyn_tag out of c_peek,
freed by gc_sweep out of flan_gc_collect. The checker accepted it and the
collector freed a live value, which is the one failure this boundary exists to
prevent.
The set does not travel across the crossing now. It still terminates — each
walk's own set guards its own recursion over names, and a crossing starts a
separate finite walk — and it does not start refusing a recursive shape with
no dyn under it, which has rows of its own here because that is the way a fix
like this goes wrong.
Neither recursive shape had a row. That gap is why it took four passes over
this code to surface, so both are pinned now, alongside the two acceptances
that say termination held. And the three return rows stop sharing one needle:
each names its own type, because three rows against the common half of one
sentence would all pass on a message that named the wrong shape.
dune test --force: green, 0 failures.
Joseph Ferano
70f87d90b2