Three dyn-crossing gaps found beside the fold fix are recorded.

This commit is contained in:
Joseph Ferano 2026-09-26 16:28:15 +07:00
parent f4d79b0147
commit 3a2f3327f6

View File

@ -800,6 +800,14 @@ One spelling for one operation; != stays, and not= is refused with a suggestion
of !=. of !=.
* Checker * Checker
** TODO A u64 above the i64 maximum becomes -1 when it crosses into dyn
=(+ z u)= and =(max u 0 z)= with u = u64 max read u as -1, silently. It should trap at
the crossing, as a u64 field read through a view already does.
** TODO A dyn nil past the first pair of a fold is refused at compile time
=(+ 1 2 (the dyn nil))= says nil has no None at i32, while =(+ (the dyn nil) 1 2)= traps
at run time. Both should trap at run time.
** TODO A generic $t beside a dyn operand is refused
"does not cross into a written type yet"; rule 117 says typed beside dyn gives dyn.
** WAIT Checking a wide fold of let operands is slow ** WAIT Checking a wide fold of let operands is slow
Parked 2026-09-26: design first; remeasure on a quiet machine, it was timed under load 20. Parked 2026-09-26: design first; remeasure on a quiet machine, it was timed under load 20.
A 2000-operand (bit-and (let …) …) takes 32 s to check (37 s before the bit operators); A 2000-operand (bit-and (let …) …) takes 32 s to check (37 s before the bit operators);