ty_holds opens a datatype once with DUMMY for its value arguments (#1513)

[Lorenzobattistela]

Fixes #1513. Supersedes #1522 (its test is kept as gpu_reach_closure_instances).

The bug

ty_holds opens each datatype once per walk, keyed by name, using the arguments it first meets. For Duo{plain: Box<Num{}>, callable: Box<Fun{}>}, Box<Num{}> gets opened (its field is U32), and Box<Fun{}> is skipped. So ty_clo says "no closure", and the GPU build fails with "a function the device does not hold".

The fix

This follows @nicolas-abril's suggestion. A datatype is still opened once per walk, but with DUMMY in place of its value arguments, so what its fields say holds for every index it can be met with:

• Box<-t>{value: Pick(t)}: Pick(DUMMY) is stuck, so it may hold a closure (true).
• Expr<-t>, Vec<A, -n>, Fin, typed ASTs: the fields are U32, A, or the family again, so they hold no closure (false, same as main).

Type arguments are still looked into on every visit, as on main. There's no key, no rep flag and no depth cap. Which parameters are values is now memoized per datatype (FL.vals), so vs isn't recomputed on every visit.

DUMMY is used only when the predicate itself takes an unknown type as a hit (p(DUMMY)): that's ty_clo and ty_value. lay_of's re-entry check reads a stuck field as "doesn't re-enter", so with DUMMY it laid a cyclic family flat and overflowed the stack (family_cyclic_nested); it keeps main's first-met arguments.

Trade-off: a family whose computed field is closure-free in every branch (Box<-t>{value: Pick(t)} with Pick giving U32 or F32) now counts as may-hold, so its host closures are kept out of #if !DEVICE. Build size only, never a wrong answer; none of the tests or demos hit it.

comp.ts: +11/-5 lines, 63,511 tokens (main 63,391).

Checks (merged with main f846cb5)

• repo 54/54, test 1622/1622
• chain, instances and mutual fail on main and pass here. deep, grow, nested and wrap guard against the hangs and stack overflows the earlier versions had. family_cyclic_nested guards lay_of.
• The C output of all 766 test programs and 18 demos is byte-identical to main, except for the 3 ty_holds skips a closure in a later instance of the same datatype #1513 tests.
• Nico's Expr<-t: Ty> / ev!(e: Expr<TBool{}>) example: the C output is identical to main, and the host closures stay under #if !DEVICE. The previous head (0f6b929) moved them out.
• Gr<A, -n>{More{next: Gr<P<A, A>, (1n + n : Nat)>}}: compiles in 0.07 s, same as main.
• perf: 124/124 on a full run; two --gate runs gave 111/124 and 123/124, which look like noise.

Not run: CUDA, Linux, Windows (GPU checked on Metal only).

Please squash-merge.

[nicolas-abril]

This fixes #1513, but the repeat check also says "may hold a closure" for common value-indexed families that hold none, which turns on wide and pulls every host closure into the device build. Nothing breaks, but it costs size and build time. Details inline.

One more point, outside the diff: ty_value (line 904) and lay_of's re-entry check (line 951) still call ty_holds with the name-keyed skip that caused #1513. In a kind like Duo{a: K<X>, b: K<Y>} where only K<Y> computes to Type, the second K is skipped, ty_value says "value", and that argument gets keyed by syntax instead of walked as a type argument. That breaks the assumption the new comment rests on, that type arguments are "looked into apart".

[nicolas-abril]

incomprehensible comment

[nicolas-abril]

This answers true for any datatype whose recursion changes its value index, even when it holds no closure.

Example: type Expr<-t: Ty> is Data: Num{n: U32}; IsZero{a: Expr<TNum{}>} and ev!(e: Expr<TBool{}>). The walk meets Expr again with TNum instead of TBool, so ty_clo says true and dev takes in all of FL.clos. Compiling this moves main_c7, main_k8 and IO.print out of #if !DEVICE; on the merge base they stay host-only. The same happens for the typed Expr in demos/proof_typed_eval, the V.Con/Word.Con length-indexed vectors, Fin/Vec, and typed-AST shapes like App{f: Tm<Arr(a,b)>, x: Tm<a>}.

Suggestion: instead of a blanket true on a repeat, ask whether the datatype can hold a closure for any value of its value arguments. Open each datatype once with its value arguments replaced by DUMMY, memoized by name. It is about as cheap and still sound: for Box<-t>, Pick(DUMMY) is stuck and p returns true; for Expr<-t> or Vec<A,-n> the fields are U32/A/Expr<..> and the answer is no. That also removes the syntax-key problem below, without the per-instance blowup the earlier attempts hit.

[nicolas-abril]

The key is the raw syntax of each value argument (term_key(term_lower(x)), not normalized, Ann nodes kept), so equal indices written differently count as different. E.g. type Ch<-t: Tag> Link{next: Ch<(t : Tag)>} or next: Ch<Id(t)>, or a literal against its constructor-tree form after substitution, all give a spurious "may hold a closure". Plain recursion only stays "no" when the field writes the index exactly the same way.

Also a perf nit: with rep set, this runs term_lower + JSON.stringify on every datatype visit, even when there are no value arguments (the key is just empty strings joined). Computing it only when vs.some(Boolean) avoids that.

[nicolas-abril]

vs now runs ty_value (a full, unmemoized ty_holds walk of the kind) on every argument at every visit, including repeat visits that return right away. The old .some stopped at the first argument that held a closure. The kinds depend only on the declaration (ks from tele_unbind is already memoized), so memoizing ty_value per datatype and parameter index, or computing vs lazily, would remove this repeated work from every ty_clo, ty_value and lay_of walk.

[nicolas-abril]

Nit: the bare positional true (rep) is hard to read here without opening ty_holds, and any future caller that passes seen must also pass rep. A named options object, or a separate on-repeat callback, would keep the call site self-explanatory.