Skip to content

Commit fe1bc86

Browse files
hyperpolymathclaude
andcommitted
fix(typecheck): make len/show truly polymorphic schemes (Refs #122)
v2.5/v2.6 (merged in #123) bound `len` and `show` via `bind_var` as `'a -> Int` / `'a -> String` using a SINGLE SHARED unification tyvar, not a generalized scheme. The first use pinned it (e.g. `len(name)` => tv:=String), so a later `len(ids)` on `[String]` failed with `Unify TypeMismatch (String, Array[String])`. This blocked any program mixing `len` over strings and arrays — notably the ubicity#30 storage port (diagnosed to root cause via an `sb7` minimal repro). Bind both as generalized schemes via `bind_scheme` (`poly1` helper: fresh tyvar quantified in `sc_tyvars`, instantiated per call site), so `len`/`show` are properly polymorphic. Verified green prior to an environment loss (WSL /tmp wipe): the sb7 repro and the full ubicity storage.affine compiled; the 5 Deno-ESM harnesses and `dune runtest` (214 tests, unchanged — same 2 pre-existing E2E Node-CJS vscode failures) all passed. CI re-verifies the build here. Refs #122 (follow-up to #123; unblocks ubicity#30). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
1 parent b00f8e4 commit fe1bc86

1 file changed

Lines changed: 17 additions & 8 deletions

File tree

lib/typecheck.ml

Lines changed: 17 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1205,12 +1205,21 @@ let register_builtins (ctx : context) : unit =
12051205
bind_var ctx "max" int_binop;
12061206
bind_var ctx "min" int_binop;
12071207
bind_var ctx "pow_float" float_binop;
1208-
(* `len` is polymorphic over String and [T] (issue #122 v2.5):
1209-
stdlib/string.affine calls `len` on both. Broadened from
1210-
Array[tv]->Int to 'a->Int (matches the interpreter's dynamic len;
1211-
the codegen lowers it to `.length`, valid for string and array). *)
1212-
bind_var ctx "len" (let tv = fresh_tyvar 0 in
1213-
TArrow (tv, QOmega, ty_int, EPure));
1208+
(* `len` / `show` are TRULY polymorphic — bound as generalized schemes
1209+
so each call site instantiates a fresh tyvar. v2.5/v2.6 mistakenly
1210+
bound them via bind_var as `'a -> _` with a SINGLE SHARED tyvar:
1211+
the first `len(String)` pinned it, then `len([T])` failed with
1212+
`Unify TypeMismatch (String, Array[T])` (diagnosed via the sb7
1213+
minimal repro; blocked the ubicity#30 storage port). issue #122. *)
1214+
let poly1 (body_of : ty -> ty) : scheme =
1215+
let tv = fresh_tyvar 0 in
1216+
let v = (match tv with
1217+
| TVar r -> (match !r with Unbound (v, _) -> v | _ -> assert false)
1218+
| _ -> assert false) in
1219+
{ sc_tyvars = [(v, Types.KType)]; sc_effvars = []; sc_rowvars = [];
1220+
sc_body = body_of tv }
1221+
in
1222+
bind_scheme ctx "len" (poly1 (fun a -> TArrow (a, QOmega, ty_int, EPure)));
12141223
(* Honest string/char primitives underpinning stdlib/string.affine
12151224
(issue #122 v2.5). Concrete String/Char types; the Deno-ESM backend
12161225
lowers each to a JS intrinsic. char ::= TCon "Char". *)
@@ -1232,8 +1241,8 @@ let register_builtins (ctx : context) : unit =
12321241
bind_var ctx "parse_float" (TArrow (ty_string, QOmega, opt ty_float, EPure));
12331242
bind_var ctx "char_to_int" (TArrow (ty_char, QOmega, ty_int, EPure));
12341243
bind_var ctx "int_to_char" (TArrow (ty_int, QOmega, ty_char, EPure));
1235-
bind_var ctx "show"
1236-
(let tv = fresh_tyvar 0 in TArrow (tv, QOmega, ty_string, EPure));
1244+
bind_scheme ctx "show"
1245+
(poly1 (fun a -> TArrow (a, QOmega, ty_string, EPure)));
12371246
bind_var ctx "panic" (TArrow (ty_string, QOmega, ty_never, EPure));
12381247
bind_var ctx "exit" (TArrow (ty_int, QOmega, ty_never, ESingleton "IO"));
12391248
(* TEA runtime — accepts any record, returns unit with IO effect *)

0 commit comments

Comments
 (0)