From 3a2f3327f6e2a2dd59e8235bfbb917170e9e0bf1 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sat, 26 Sep 2026 16:28:15 +0700 Subject: [PATCH] Three dyn-crossing gaps found beside the fold fix are recorded. --- TODO.org | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/TODO.org b/TODO.org index c1ee43de..e23add54 100644 --- a/TODO.org +++ b/TODO.org @@ -800,6 +800,14 @@ One spelling for one operation; != stays, and not= is refused with a suggestion of !=. * 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 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);