From cdda829835ae048a957b3ea8812195be84370339 Mon Sep 17 00:00:00 2001
From: Joseph Ferano
Date: Sun, 20 Sep 2026 21:48:39 +0700
Subject: [PATCH] The direction a container-fixed binding admits, pinned
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
A narrower scalar at a $t a slice already fixed widens into the fixed
type — the same cast a monomorphic parameter applies — where the old
rule refused both directions. One accepts pin, one runtime line in
int-generic.flan, and the web page's predicate table catches up: five
predicates, integer? at the head, and the entailment chain grown one
link.
---
test/programs/int-generic.flan | 10 +++++++++-
test/test_acceptance.ml | 6 ++++--
test/test_flan.ml | 8 ++++++++
web/index.html | 12 ++++++++----
4 files changed, 29 insertions(+), 7 deletions(-)
diff --git a/test/programs/int-generic.flan b/test/programs/int-generic.flan
index 63e1ed0..03ceb3d 100644
--- a/test/programs/int-generic.flan
+++ b/test/programs/int-generic.flan
@@ -101,4 +101,12 @@
;; A literal beside a wider variable joins too: 4 arrives as an i32 and the
;; copy is i64's.
(let [w (i64 38)]
- (println (tri w 3 1))))
+ (println (tri w 3 1)))
+ ;; And the one direction a container-bound variable does admit: the slice
+ ;; fixed $t at i32 exactly, and a narrower scalar widens *into* that — the
+ ;; same conversion a monomorphic i32 parameter would apply. (The reverse,
+ ;; an i64 scalar against this slice, stays refused; the checker pins it.)
+ (let [ns [5 3 9 1]]
+ (match (index-of (slice ns 0 4) (i16 9))
+ (Some i) (println i)
+ _ (println -1))))
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index fbab847..b31b649 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -2652,12 +2652,14 @@ let () =
spells. Then the integer?-only operations at several widths, and last
the join family: [true true], [6 6] and [42] are mixed widths at one
$t answering identically in both argument orders, from one copy at
- the wider type (FIX.org 2026-09-20). *)
+ the wider type (FIX.org 2026-09-20). The closing [2] is an i16 scalar
+ widening into the i32 a slice fixed index-of's $t at — the one
+ direction a container-bound variable admits. *)
let int_generic_out =
"7\n7\n7\n7\n7\n7\n-2147483648\n-9223372036854775808\n\
0\n0\n1.5\n2.5\n\
7\n15\n31\ntrue\nfalse\ntrue\n240\n9\n5\n-2\n301\n301\n\
- true\ntrue\n6\n6\n42\n"
+ true\ntrue\n6\n6\n42\n2\n"
in
outputs "integer? and the collapsed abs" "programs/int-generic.flan"
int_generic_out;
diff --git a/test/test_flan.ml b/test/test_flan.ml
index fd138cc..1cd7c15 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -5030,6 +5030,14 @@ let () =
"(defn main [] () (let [ns [5 3 9 1]] \
(match (index-of (slice ns 0 4) (i64 9)) \
(Some i) (println i) _ (println -1))))";
+ (* The one direction a container-fixed binding does admit, and it is new
+ with the join: a *narrower* scalar widens into the type the container
+ fixed, through the same cast a monomorphic i32 parameter applies. This
+ used to refuse with the same both-ways sentence as everything else. *)
+ accepts "a narrower scalar widens into a container-fixed binding"
+ "(defn main [] () (let [ns [5 3 9 1]] \
+ (match (index-of (slice ns 0 4) (i16 9)) \
+ (Some i) (println i) _ (println -1))))";
(* The written conversion is what the message asks for, and it is accepted:
the refusal is about the *implicit* step, not about reaching i64. *)
accepts "the written conversion is accepted"
diff --git a/web/index.html b/web/index.html
index 16f5cd2..45b8673 100644
--- a/web/index.html
+++ b/web/index.html
@@ -927,11 +927,12 @@ $t)} at the head of the body, or take the operation as a parameter — a
What makes that liveable is a where clause, written as a Clojure-style
map at the head of the body — {:where (ordered? $t)}, or a vector when
there is more than one: {:where [(ordered? $t) (hashable? $u)]}. There
-are four predicates, and each gates builtins the compiler already has:
+are five predicates, and each gates builtins the compiler already has: