diff --git a/compiler.lua b/compiler.lua
index fbdd06f..983af5c 100644
--- a/compiler.lua
+++ b/compiler.lua
@@ -548,10 +548,16 @@ end
 local CSE_MAX_LOCALS = 100
 local CCACHE = {}   -- chain key -> Lua local/slot name, block-scoped via __index
 local HOIST = nil   -- nil, or { out = {stmt strings}, pure = bool } at a flush site
-local FNL = { np = 0, npt = 0, pt = false, can_pt = false }  -- per-Lua-function
+-- nloc: every Lua local this function has declared so far (params, let
+-- locals, hoisted chain steps, fN callee refs), summed across branches, so it
+-- over-approximates the live count Lua checks against its 200 cap.
+local FNL = { np = 0, npt = 0, pt = false, can_pt = false, nloc = 0 }  -- per-Lua-function
 
-local function new_fnl(can_pt)
-  return { np = 0, npt = 0, pt = false, can_pt = can_pt }
+local WIDE = false  -- wide mode (see capture_plan)
+local WIDE_ARGS = 100
+
+local function new_fnl(can_pt, nparams)
+  return { np = 0, npt = 0, pt = false, can_pt = can_pt, nloc = nparams or 0 }
 end
 
 local function child_cache()
@@ -583,6 +589,7 @@ end
 local function chain_slot(expr)
   if FNL.np < CSE_MAX_LOCALS then
     FNL.np = FNL.np + 1
+    FNL.nloc = FNL.nloc + 1
     local ln = gen("p")
     HOIST.out[#HOIST.out+1] = "local " .. ln .. " = " .. expr .. "; "
     return ln
@@ -780,8 +787,13 @@ local function try_flatten_call_chain(form, env)
       call_str = ar and ("APP(" .. symlit(hname) .. ", " .. arg_list .. ")")
                  or unknown_call(hname, arg_list, #prev_strs + 1)
     end
-    stmts[#stmts+1] = "local " .. next_name .. " = " .. call_str .. ";"
-    inner_name = next_name
+    if WIDE then
+      -- one local for the whole chain: each step reads only the previous one
+      stmts[#stmts+1] = inner_name .. " = " .. call_str .. ";"
+    else
+      stmts[#stmts+1] = "local " .. next_name .. " = " .. call_str .. ";"
+      inner_name = next_name
+    end
   end
   -- outermost: emit as return statement
   local frame = frames[1]
@@ -867,6 +879,10 @@ local function ccall(form, env)
   local cargs = {}
   for i=1,#args do cargs[i] = cexpr(args[i], env) end
   local argstr = table.concat(cargs, ", ")
+  if WIDE and #cargs > WIDE_ARGS then
+    -- each argument would hold a register until the call
+    argstr = "UNPACK({" .. argstr .. "}, 1, " .. #cargs .. ")"
+  end
   -- Chain-hoist purity: this application runs after its args; anything the
   -- statement evaluates after it may no longer be hoisted ahead of it unless
   -- the head is known effect-free and non-raising.
@@ -1534,6 +1550,7 @@ local function snapshot_env(eform, env)
     local ln = env[kname]
     if type(ln) == "string" and params[ln] then
       local cap = gen("c")
+      FNL.nloc = FNL.nloc + 1
       stmts[#stmts + 1] = "local " .. cap .. " = " .. ln .. ";"
       newenv[kname] = cap
     end
@@ -1577,7 +1594,7 @@ local function try_lower_freeze_let(var, val, body, env)
     CONT[#CONT] = nil
     return (snap ~= "" and (snap .. " ") or "") .. s
   end
-  if nontail > 0 or not HAS_GOTO then return nil end
+  if nontail > 0 or not HAS_GOTO or WIDE then return nil end
   local rec = {
     name = var.name, kind = "goto", expr = eform, env = freeze_env,
     label = gen("fail"),
@@ -1602,6 +1619,143 @@ local function push_inline_cont()
   return saved
 end
 
+-- Wide mode (C.compile_top(form, true)): the code shape for a defun whose
+-- ordinary Lua exceeded a Lua limit (200 locals, 60 upvalues, 250 registers).
+-- prims.lua recompiles only such defuns this way, so everything that loads
+-- today keeps its exact code. In wide mode:
+--   * a hoisted body (KC function) with more than WIDE_CAPS captures takes
+--     ONE table T and reads T[i]; narrower ones whose captures are not plain
+--     names (T[i] from an enclosing wide body) get fresh parameter names;
+--   * a lambda closing over more than WIDE_UPVALS outer names is hoisted the
+--     same way and built by LAMW(KC[i], {captures});
+--   * let chains split at WIDE_SPLIT_LOCALS, passing a wide live set as T;
+--   * multi-thaw failure continuations stay BIND/THAW closures instead of a
+--     goto label, so no label pins a let chain to one function.
+-- Captured values are immutable KL bindings, so copying them into T at the
+-- use site observes exactly what the parameter form did.
+local WIDE_CAPS = 24
+local WIDE_UPVALS = 40
+local WIDE_SPLIT_LOCALS = 80
+
+-- see the lambda case of cexpr; deeper than any curried chain in the kernel
+local CURRY_DEPTH = 32
+
+local function is_ident(s)
+  return type(s) == "string" and s:match("^[%a_][%w_]*$") ~= nil
+end
+
+-- How a hoisted body receives `lnames` (sorted Lua expressions): returns the
+-- body's parameter list, the call-site argument list, an expr -> expr remap
+-- for the body's env (nil = identity), and the number of parameter slots.
+local function capture_plan(lnames)
+  local joined = table.concat(lnames, ", ")
+  if not WIDE then return joined, joined, nil, #lnames end
+  local remap = {}
+  if #lnames > WIDE_CAPS then
+    local t = gen("T")
+    for i, ln in ipairs(lnames) do remap[ln] = t .. "[" .. i .. "]" end
+    return t, "{" .. joined .. "}", remap, 1
+  end
+  local plain = true
+  for _, ln in ipairs(lnames) do
+    if not is_ident(ln) then plain = false; break end
+  end
+  if plain then return joined, joined, nil, #lnames end
+  local ps = {}
+  for i, ln in ipairs(lnames) do ps[i] = gen("q"); remap[ln] = ps[i] end
+  return table.concat(ps, ", "), joined, remap, #lnames
+end
+
+local function remap_env(env, remap)
+  if not remap then return env end
+  local e = {}
+  for k, v in pairs(env) do e[k] = remap[v] or v end
+  return e
+end
+
+-- after push_inline_cont: inline records expand inside the hoisted body, so
+-- their envs must see the body's names too
+local function remap_cont(remap)
+  if not remap then return end
+  for i = 1, #CONT do
+    local r = CONT[i]
+    CONT[i] = { name = r.name, kind = r.kind, expr = r.expr, env = remap_env(r.env, remap) }
+  end
+end
+
+-- Lua names a hoisted KC body must take as parameters. Beyond the form's own
+-- free variables, an inline freeze-let thawed inside the form is expanded
+-- there with ITS env, so the freeze body's free variables must be passed in
+-- too (they are locals of the enclosing function, not visible from KC).
+local function kc_lnames(form, env)
+  local set = {}
+  local fv = {}
+  collect_free(form, env, {}, fv)
+  for k in pairs(fv) do set[env[k]] = true end
+  local pending, seen = { form }, {}
+  while #pending > 0 do
+    local f = table.remove(pending)
+    for i = 1, #CONT do
+      local rec = CONT[i]
+      if rec.kind == "inline" and not seen[rec] and mentions_name(f, rec.name, {}) then
+        seen[rec] = true
+        local rfv = {}
+        collect_free(rec.expr, rec.env, {}, rfv)
+        for k in pairs(rfv) do set[rec.env[k]] = true end
+        pending[#pending + 1] = rec.expr
+      end
+    end
+  end
+  local lnames = {}
+  for ln in pairs(set) do lnames[#lnames + 1] = ln end
+  table.sort(lnames)
+  return lnames
+end
+
+-- Compile `form` (tail-compiled) as a constant chunk-scope KC function taking
+-- its free variables as parameters; returns the `KC[i](params)` call. The
+-- body is a SEPARATE Lua function: no `goto tco` (SELF cleared), no goto-kind
+-- failure continuations, no impl-local fN refs, and its own local budget.
+local function hoist_kc(form, env, lnames)
+  lnames = lnames or kc_lnames(form, env)
+  local params, args, remap, nslots = capture_plan(lnames)
+  local saved_self = SELF
+  local saved_h, saved_cc, saved_fnl = HOIST, CCACHE, FNL
+  local saved_cont = push_inline_cont()
+  remap_cont(remap)
+  local saved_impl = IN_IMPL
+  SELF = nil; HOIST = nil; CCACHE = {}; FNL = new_fnl(true, nslots); IN_IMPL = false
+  local body_stmts = ctail(form, remap_env(env, remap))
+  if FNL.pt then body_stmts = "local PT = {}; " .. body_stmts end
+  SELF = saved_self; HOIST = saved_h; CCACHE = saved_cc; FNL = saved_fnl
+  CONT = saved_cont; IN_IMPL = saved_impl
+  local idx = #CTX.cbodies + 1
+  CTX.cbodies[idx] = "function(" .. params .. ") " .. body_stmts .. " end"
+  return "KC[" .. idx .. "](" .. args .. ")"
+end
+
+-- A long let chain in one Lua function (the kernel's pattern-matching KL for
+-- a sequent rule with ~30 premises spends ~6 lets per premise) would exceed
+-- Lua's 200-locals-per-function cap. Past this budget the rest of the chain
+-- continues in a fresh KC function via a proper tail call. The margin covers
+-- locals the budget does not see ahead of time (call-chain flattening).
+local LET_SPLIT_LOCALS = 120
+
+local function try_split_let(form, env)
+  if not CTX or FNL.nosplit then return nil end
+  local used = FNL.nloc + (IN_IMPL and #FREF_LIST or 0)
+  if used < (WIDE and WIDE_SPLIT_LOCALS or LET_SPLIT_LOCALS) then return nil end
+  -- a goto-kind failure continuation's label lives in this function
+  for i = 1, #CONT do
+    if CONT[i].kind == "goto" then return nil end
+  end
+  -- a body that needs this many parameters would split again on its first
+  -- let (wide mode passes them as one table instead)
+  local lnames = kc_lnames(form, env)
+  if not WIDE and #lnames >= LET_SPLIT_LOCALS then FNL.nosplit = true; return nil end
+  return "return " .. hoist_kc(form, env, lnames)
+end
+
 -- ------------------------------------------------------------------
 -- cexpr : value position (returns a Lua expression string)
 -- ------------------------------------------------------------------
@@ -1661,12 +1815,6 @@ function cexpr(form, env)
       -- the body FIRST so any nested freezes/control-forms claim lower KB
       -- indices before we take ours.
       if CTX then
-        local fv = {}
-        collect_free(form, env, {}, fv)
-        local lnames = {}
-        for kname in pairs(fv) do lnames[#lnames+1] = env[kname] end
-        table.sort(lnames)
-        local params = table.concat(lnames, ", ")
         -- Compile the body FIRST so nested freezes/control-forms claim their KC
         -- indices before we take ours. The body references only its param free
         -- vars, globals, and KC (a load-time upvalue) -- never an impl local --
@@ -1676,21 +1824,11 @@ function cexpr(form, env)
         -- would illegally cross the function boundary. Likewise reset the
         -- chain-hoist state: KC[i] has its own local budget, and locals cached
         -- in the enclosing function are not in scope here.
-        local saved_self = SELF
-        local saved_h, saved_cc, saved_fnl = HOIST, CCACHE, FNL
-        local saved_cont = push_inline_cont()
-        local saved_impl = IN_IMPL
-        SELF = nil; HOIST = nil; CCACHE = {}; FNL = new_fnl(true); IN_IMPL = false
-        local body_stmts = ctail(form, env)
-        if FNL.pt then body_stmts = "local PT = {}; " .. body_stmts end
-        SELF = saved_self; HOIST = saved_h; CCACHE = saved_cc; FNL = saved_fnl
-        CONT = saved_cont; IN_IMPL = saved_impl
-        local idx = #CTX.cbodies + 1
-        CTX.cbodies[idx] = "function(" .. params .. ") " .. body_stmts .. " end"
+        local call = hoist_kc(form, env)
         -- The KC call itself may raise or side-effect: later siblings in the
         -- enclosing statement must not hoist chains ahead of it.
         if HOIST then HOIST.pure = false end
-        return "KC[" .. idx .. "](" .. params .. ")"
+        return call
       end
       -- No per-defun context (top-level eval chunk): fall back to the IIFE.
       -- (Clear SELF here too: the IIFE is a separate function.)
@@ -1713,7 +1851,54 @@ function cexpr(form, env)
     if op == "lambda" then
       local v = car(cdr(form))
       local body = car(cdr(cdr(form)))
+      -- A curried chain this deep (the kernel's lambda entry for an
+      -- N+6-ary consume helper) nests one Lua function per lambda, past
+      -- LuaJIT's 200 syntax levels. CURRY(n, f) builds the same curried
+      -- closures at runtime and calls f with the n arguments as one table.
+      local depth, inner, vars = 0, form, {}
+      while is_cons(inner) and car(inner) == form[1] and is_symbol(car(cdr(inner)))
+            and not is_cons(cdr(cdr(cdr(inner)))) do
+        depth = depth + 1
+        vars[depth] = car(cdr(inner))
+        inner = car(cdr(cdr(inner)))
+      end
+      if depth > CURRY_DEPTH then
+        local t = gen("T")
+        local e2 = env
+        for i = 1, depth do e2 = extend(e2, vars[i].name, t .. "[" .. i .. "]") end
+        local saved_h, saved_impl = HOIST, IN_IMPL
+        HOIST = nil; IN_IMPL = false
+        local bodyc = cexpr(inner, e2)
+        HOIST = saved_h; IN_IMPL = saved_impl
+        return "CURRY(" .. depth .. ", function(" .. t .. ") return " .. bodyc .. " end)"
+      end
       local ln = gen("v")
+      if WIDE and CTX then
+        -- each distinct outer name the closure reads is one upvalue
+        local fv = {}
+        collect_free(form, env, {}, fv)
+        local lnames, roots, nroots = {}, {}, 0
+        for kname in pairs(fv) do
+          local e = env[kname]
+          lnames[#lnames + 1] = e
+          local r = type(e) == "string" and e:match("^[%a_][%w_]*") or e
+          if not roots[r] then roots[r] = true; nroots = nroots + 1 end
+        end
+        if nroots > WIDE_UPVALS then
+          table.sort(lnames)
+          local t = gen("T")
+          local remap = {}
+          for i, e in ipairs(lnames) do remap[e] = t .. "[" .. i .. "]" end
+          local saved_h, saved_impl, saved_cont = HOIST, IN_IMPL, CONT
+          push_inline_cont(); remap_cont(remap)
+          HOIST = nil; IN_IMPL = false
+          local bodyc = cexpr(body, extend(remap_env(env, remap), v.name, ln))
+          HOIST = saved_h; IN_IMPL = saved_impl; CONT = saved_cont
+          local idx = #CTX.cbodies + 1
+          CTX.cbodies[idx] = "function(" .. ln .. ", " .. t .. ") return " .. bodyc .. " end"
+          return "LAMW(KC[" .. idx .. "], {" .. table.concat(lnames, ", ") .. "})"
+        end
+      end
       local e2 = extend(env, v.name, ln)
       -- Deferred body: nothing inside may be hoisted to the creation site.
       -- Not impl-scope: `fN` locals live in impl, not this nested function.
@@ -1736,15 +1921,18 @@ function cexpr(form, env)
         local lnames = {}
         for kname in pairs(fv) do lnames[#lnames+1] = env[kname] end
         table.sort(lnames)  -- stable order for caller / body
+        local params, args, remap = capture_plan(lnames)
         -- Deferred body: nothing inside may be hoisted to the creation site.
         local saved_h, saved_impl = HOIST, IN_IMPL
+        local saved_cont = CONT
+        if remap then push_inline_cont(); remap_cont(remap) end
         HOIST = nil; IN_IMPL = false
-        local body_str = cexpr(body, env)
-        HOIST = saved_h; IN_IMPL = saved_impl
+        local body_str = cexpr(body, remap_env(env, remap))
+        HOIST = saved_h; IN_IMPL = saved_impl; CONT = saved_cont
         local idx = #CTX.cbodies + 1
-        CTX.cbodies[idx] = "function(" .. table.concat(lnames, ", ") .. ") return "
+        CTX.cbodies[idx] = "function(" .. params .. ") return "
                            .. body_str .. " end"
-        local call_args = (#lnames == 0) and "" or (", " .. table.concat(lnames, ", "))
+        local call_args = (#lnames == 0) and "" or (", " .. args)
         return "BIND(KC[" .. idx .. "]" .. call_args .. ")"
       end
       local saved_h, saved_impl = HOIST, IN_IMPL
@@ -1888,8 +2076,11 @@ function ctail(form, env)
       local v   = car(cdr(form))
       local val = car(cdr(cdr(form)))
       local body= car(cdr(cdr(cdr(form))))
+      local split = try_split_let(form, env)
+      if split then return split end
       local lowered = try_lower_freeze_let(v, val, body, env)
       if lowered then return lowered end
+      FNL.nloc = FNL.nloc + 1
       local ln = gen("v")
       local pre, valc = cstmt_expr(val, env)
       local e2 = extend(env, v.name, ln)
@@ -2004,7 +2195,7 @@ local function cdefun(form)
   CTX = new_ctx()
   -- fresh chain-hoist state for the impl function (see CSE block above ccall)
   local saved_fnl, saved_cc = FNL, CCACHE
-  FNL = new_fnl(true)
+  FNL = new_fnl(true, #params)
   CCACHE = {}
   -- Self-tail-call -> loop lowering. Eligible unless:
   --   * the function is not PURELY tail-recursive -- some self-reference is a
@@ -2125,7 +2316,17 @@ local function cdefun(form)
   end
   return src
 end
-C.cdefun = cdefun
+-- wide: compile in wide mode (see WIDE above)
+local function cdefun_mode(form, wide)
+  if not wide then return cdefun(form) end
+  local saved = WIDE
+  WIDE = true
+  local ok, res = pcall(cdefun, form)
+  WIDE = saved
+  if not ok then error(res, 0) end
+  return res
+end
+C.cdefun = cdefun_mode
 
 -- Pre-scan a list of forms to register arities of all defuns (so mutual /
 -- forward references compile as direct exact-arity calls).
@@ -2147,9 +2348,9 @@ function C.compile_expr_chunk(form)
 end
 
 -- compile any top-level form to a Lua statement string
-function C.compile_top(form)
+function C.compile_top(form, wide)
   if is_cons(form) and is_symbol(car(form)) and car(form).name == "defun" then
-    return cdefun(form)
+    return cdefun_mode(form, wide)
   else
     -- a top-level expression: evaluate for side effects. Wrapped in do..end
     -- so a whole kernel file can be concatenated into ONE chunk (boot.lua's
diff --git a/prims.lua b/prims.lua
index 110f40f..7010663 100644
--- a/prims.lua
+++ b/prims.lua
@@ -2233,6 +2233,26 @@ local ENV = {
     end
     return setmetatable({ fn, ... }, Thunk)
   end,
+  -- A wide-mode lambda (compiler.lua, WIDE): its body is the constant
+  -- function fn(x, T) with the captures in the table T.
+  UNPACK = unpack,
+  LAMW = function(fn, t)
+    return MKFUN(1, function(x) return fn(x, t) end)
+  end,
+  -- A curried lambda chain n deep (compiler.lua, CURRY_DEPTH): each
+  -- application returns a fresh closure over its own copy of the arguments
+  -- so far, exactly like the nested closures; the last calls fn(args).
+  CURRY = function(n, fn)
+    local function step(args, i)
+      return MKFUN(1, function(x)
+        local a = { unpack(args, 1, i - 1) }
+        a[i] = x
+        if i == n then return fn(a) end
+        return step(a, i + 1)
+      end)
+    end
+    return step({}, 1)
+  end,
   -- MKTREE consumes a flat blueprint produced by the compiler for deep
   -- cons-trees. See compile_cons_tree in compiler.lua. ops is a sequence of
   -- 'v' followed by a leaf value (push), or 'c' (pop two, push cons).
@@ -2513,8 +2533,30 @@ end
 -- WHILE one of those chunks executes (nested eval-kl, e.g. compile-prolog
 -- inside process-datatype) are not recorded — replaying the outer chunk
 -- regenerates them naturally.
-local function compile_and_load(luasrc, chunkname)
-  local fn = load_chunk(luasrc, chunkname)
+-- Lua limits the wide code shape avoids (compiler.lua, WIDE)
+local function is_width_error(msg)
+  msg = tostring(msg)
+  return msg:find("has more than %d+ local variables") ~= nil
+      or msg:find("has more than %d+ upvalues") ~= nil
+      or msg:find("function or expression too complex", 1, true) ~= nil
+end
+
+-- defun_form: when the ordinary code for this defun exceeds a Lua limit,
+-- recompile it in wide mode (loads that succeed never pay for this)
+local function compile_and_load(luasrc, chunkname, defun_form)
+  local fn
+  if defun_form then
+    local ok, res = pcall(load_chunk, luasrc, chunkname)
+    if ok then
+      fn = res
+    elseif is_width_error(res) then
+      fn = load_chunk(require("compiler").compile_top(defun_form, true), chunkname)
+    else
+      error(res, 0)
+    end
+  else
+    fn = load_chunk(luasrc, chunkname)
+  end
   local rec = P.FASL_REC
   if rec and not rec.in_chunk then
     rec.n = rec.n + 1
@@ -2568,7 +2610,7 @@ function P.eval(form)
     -- error positions and debug.traceback frames identify the Shen function
     -- (the REPL's Shen-level backtrace filters on this prefix; repl.lua).
     local nm = is_cons(form[2]) and is_symbol(form[2][1]) and form[2][1].name or "defun"
-    compile_and_load(C.compile_top(form), "shen:" .. nm)
+    compile_and_load(C.compile_top(form), "shen:" .. nm, form)
     return form[2][1]   -- the function NAME symbol (car of cdr), as shen-c returns
   end
   return compile_and_load(C.compile_expr_chunk(form), "eval")
diff --git a/prolog_compile.lua b/prolog_compile.lua
index eaf5e1b..0a7c918 100644
--- a/prolog_compile.lua
+++ b/prolog_compile.lua
@@ -145,15 +145,74 @@ local function refuse(ctx, why)
   error(ctx.fail, 0)
 end
 
+-- ctx.fnloc counts the locals (params included) declared so far in the Lua
+-- function being emitted, across all branches: an upper bound on what Lua
+-- checks against its 200-locals-per-function cap.
 local function newlocal(ctx, pfx)
   ctx.nlocal = ctx.nlocal + 1
+  ctx.fnloc = ctx.fnloc + 1
   return (pfx or "v") .. ctx.nlocal
 end
 
+-- On the split retry (see translate_core), past this many locals a let chain
+-- continues in a lifted static. The margin covers locals a single let can
+-- add after the check (if-chains, fork, guard imports).
+local LET_SPLIT_LOCALS = 120
+
+-- The wide retry (see translate_core) is for predicates that still pass a
+-- Lua limit after splitting: a 40+ premise consume helper hands ~2N
+-- captures to one constructor call (250 registers), its lifted functions
+-- outgrow the chunk's locals, and one function can reference more than 60
+-- of them as upvalues. In wide mode:
+--   * a static with more than WIDE_CAPS parameters takes its free vars as
+--     one table T (read as T[i]), and splitting never refuses;
+--   * a continuation with more than WIDE_CAPS captures reads CAPREF(base, i)
+--     at each use instead of copying every capture into a local;
+--   * a handle with more than WIDE_NEWCONT captures is built by
+--     NEWCONTT(fn, {...}): same capbuf layout, no wide argument list;
+--   * lifted functions are fields of one chunk table LT;
+--   * a cons chain longer than WIDE_CONS is built by CONSL({...}, tail).
+local WIDE_SPLIT_LOCALS = 60
+local WIDE_CAPS = 24
+local WIDE_NEWCONT = 48
+local WIDE_CONS = 16
+
 local function indent(d) return string.rep("  ", d) end
 
+-- A let extends env with a child table that __index-chains to its parent.
+-- LuaJIT gives up on __index chains of 100 tables ("loop in gettable"), and
+-- a wide sequent rule's consume helper nests that many lets. Every
+-- ENV_FLATTEN levels the chain is collapsed into one table (inner bindings
+-- win) whose __index is the chain's root lookup (nil, or a lift_static /
+-- lift_cont penv function), so lookups see exactly the same bindings.
+-- Parents are never written after a child is created, so the copy is safe.
+local ENV_FLATTEN = 32
+
+local function extend_env(env)
+  local mt = getmetatable(env)
+  local depth = (mt and mt.depth or 0) + 1
+  if depth < ENV_FLATTEN then
+    return setmetatable({}, { __index = env, depth = depth })
+  end
+  local flat, t, root = {}, env, nil
+  while t do
+    for k, v in pairs(t) do
+      if flat[k] == nil then flat[k] = v end
+    end
+    local tmt = getmetatable(t)
+    local idx = tmt and tmt.__index
+    if type(idx) == "table" then
+      t = idx
+    else
+      root = idx; t = nil
+    end
+  end
+  return setmetatable({}, { __index = setmetatable(flat, { __index = root, depth = 1 }), depth = 2 })
+end
+
 local compile_value  -- fwd: control/result position
 local compile_term   -- fwd: term-construction position
+local static_fvs     -- fwd: free vars of a static about to be lifted
 
 -- atom constant: interned at translate time, inlined as a number literal
 local function atomconst(x)
@@ -260,6 +319,20 @@ compile_term = function(ctx, e, env, out, d)
   if is_cons(e) then
     local h = e[1]
     if h == SYM["cons"] and is_cons(e[2]) and is_cons(e[2][2]) then
+      if ctx.wide then
+        -- every pending CONS argument holds a register
+        local elems, t = {}, e
+        while is_cons(t) and t[1] == SYM["cons"] and is_cons(t[2]) and is_cons(t[2][2]) do
+          elems[#elems + 1] = t[2][1]
+          t = t[2][2][1]
+        end
+        if #elems > WIDE_CONS then
+          local parts = {}
+          for i, x in ipairs(elems) do parts[i] = compile_term(ctx, x, env, out, d) end
+          return "CONSL({" .. table.concat(parts, ", ") .. "}, "
+                 .. compile_term(ctx, t, env, out, d) .. ")"
+        end
+      end
       local a = compile_term(ctx, e[2][1], env, out, d)
       local b = compile_term(ctx, e[2][2][1], env, out, d)
       return "CONS(" .. a .. ", " .. b .. ")"
@@ -338,6 +411,15 @@ compile_value = function(ctx, e, env, out, d)
   -- (let V Expr Body) — including the kernel's multi-binding form
   -- (let V1 E1 V2 E2 ... Body), which the Shen macro pipeline would desugar
   if h == SYM["let"] and is_cons(args) and is_cons(args[2]) then
+    if ctx.split and ctx.fnloc >= (ctx.wide and WIDE_SPLIT_LOCALS or LET_SPLIT_LOCALS) then
+      -- a static this wide would split again on its first let (a wide
+      -- static takes them as one table)
+      local fvs, implicit = static_fvs({}, e, env)
+      if ctx.wide or #fvs < LET_SPLIT_LOCALS then
+        local st = ctx:lift_static(nil, {}, e, env, fvs, implicit)
+        return ctx:callstatic(st, {}, env, out, d)
+      end
+    end
     local v, ex = args[1], args[2][1]
     local rest = args[2][2]
     local body
@@ -347,7 +429,7 @@ compile_value = function(ctx, e, env, out, d)
       -- more bindings follow: re-wrap as a nested let
       body = R.cons(SYM["let"], rest)
     end
-    local nenv = setmetatable({}, { __index = env })
+    local nenv = extend_env(env)
     if is_cons(ex) and (ex[1] == SYM["freeze"] or ex[1] == SYM["lambda"]) then
       -- closure-convert: a let-bound freeze/lambda-chain becomes a static
       -- chunk-level function with its free vars as trailing parameters
@@ -650,10 +732,31 @@ end
 local CtxMT = {}
 CtxMT.__index = CtxMT
 
+-- Handle constructor for k captures. NEWCONT0..16 and the varargs NEWCONTV
+-- share one layout (k contiguous capbuf slots at contBase[h]). Generated
+-- fixed-width constructors past 16 win in isolation but measured ~25% slower
+-- on einsteins-riddle, whose wide continuations take NEWCONTV.
+local function newcont_ctor(k)
+  if k <= 16 then return "NEWCONT" .. k end
+  return "NEWCONTV"
+end
+
+-- the handle construction for continuation function `fname` over the Lua
+-- expressions `caps`
+local function newcont_call(ctx, fname, caps)
+  if ctx.wide and #caps > WIDE_NEWCONT then
+    return "NEWCONTT(" .. fname .. ", {" .. table.concat(caps, ", ") .. "})"
+  end
+  local parts = { fname }
+  for _, c in ipairs(caps) do parts[#parts + 1] = c end
+  return newcont_ctor(#caps) .. "(" .. table.concat(parts, ", ") .. ")"
+end
+
 local function liftname(ctx, pfx)
   ctx.nlift = ctx.nlift + 1
   local fname = pfx .. ctx.nlift
   ctx.liftnames[#ctx.liftnames + 1] = fname
+  if ctx.wide then return "LT." .. fname end
   return fname
 end
 
@@ -661,11 +764,10 @@ end
 -- A static referencing another static is fine (both are chunk-level fns):
 -- the inner static's free vars are folded into THIS static's free vars so
 -- they are in scope at the inner call sites.
-function CtxMT.lift_static(ctx, name, params, body, env)
-  local fname = liftname(ctx, "LF")
+static_fvs = function(params, body, env)
   local bound = {}
   for _, p in ipairs(params) do bound[p.name] = true end
-  local fvs, fvseen = {}, {}
+  local fvs, fvseen, implicit = {}, {}, {}
   local function addfv(vn)
     if bound[vn] or fvseen[vn] then return end
     fvseen[vn] = true
@@ -675,30 +777,51 @@ function CtxMT.lift_static(ctx, name, params, body, env)
       for _, f in ipairs(outer.fvs) do addfv(f) end
     elseif outer.kind == "vec" or outer.kind == "lock" then
       -- engine-implicit, dropped at use sites
+      implicit[vn] = outer
     else
       fvs[#fvs + 1] = vn
     end
   end
   for _, vn in ipairs(freevars(body)) do addfv(vn) end
+  return fvs, implicit
+end
+
+function CtxMT.lift_static(ctx, name, params, body, env, fvs, implicit)
+  if not fvs then fvs, implicit = static_fvs(params, body, env) end
+  local fname = liftname(ctx, "LF")
   local st = { kind = "static", fn = fname, params = params, fvs = fvs,
                body = body, env = env }
-  -- emit the lifted definition; statics resolve through to chunk scope
+  -- emit the lifted definition; statics resolve through to chunk scope.
+  -- The vec/lock params keep their kinds so a misuse refuses exactly as it
+  -- would have in the enclosing env.
   local penv = setmetatable({}, { __index = function(_, k)
     local b = env[k]
     if b and b.kind == "static" then return b end
     return nil
   end })
+  for vn, b in pairs(implicit) do penv[vn] = b end
   local sig = {}
   for i, p in ipairs(params) do
     sig[#sig + 1] = "p" .. i
     penv[p.name] = { lua = "p" .. i, kind = "term" }
   end
-  for i, vn in ipairs(fvs) do
-    sig[#sig + 1] = "fv" .. i
-    penv[vn] = { lua = "fv" .. i, kind = env[vn].kind }
+  if ctx.wide and #params + #fvs > WIDE_CAPS then
+    st.wide = true
+    sig[#sig + 1] = "T"
+    for i, vn in ipairs(fvs) do
+      penv[vn] = { lua = "T[" .. i .. "]", kind = env[vn].kind }
+    end
+  else
+    for i, vn in ipairs(fvs) do
+      sig[#sig + 1] = "fv" .. i
+      penv[vn] = { lua = "fv" .. i, kind = env[vn].kind }
+    end
   end
   local fbuf = {}
+  local saved_loc = ctx.fnloc
+  ctx.fnloc = #sig
   local fval = compile_value(ctx, body, penv, fbuf, 1)
+  ctx.fnloc = saved_loc
   local def = { fname .. " = function(" .. table.concat(sig, ", ") .. ")" }
   for _, l in ipairs(fbuf) do def[#def + 1] = l end
   def[#def + 1] = "  return " .. fval
@@ -709,12 +832,17 @@ end
 
 -- direct invocation of a static (thaw GoTo / (GoTo a b))
 function CtxMT.callstatic(ctx, st, call_args, env, out, d)
-  local parts = {}
+  local parts, fvp = {}, {}
   for _, a in ipairs(call_args) do parts[#parts + 1] = a end
   for _, vn in ipairs(st.fvs) do
     local b = env[vn]
     if not b then refuse(ctx, "static fv out of scope: " .. vn) end
-    parts[#parts + 1] = b.lua
+    fvp[#fvp + 1] = b.lua
+  end
+  if st.wide then
+    parts[#parts + 1] = "{" .. table.concat(fvp, ", ") .. "}"
+  else
+    for _, l in ipairs(fvp) do parts[#parts + 1] = l end
   end
   return st.fn .. "(" .. table.concat(parts, ", ") .. ")"
 end
@@ -729,7 +857,7 @@ function CtxMT.lift_cont(ctx, body, env, out, d)
   end
   -- statics referenced from the cont body are chunk-level fns whose OWN free
   -- vars must also be captured
-  local capture, statics, seen = {}, {}, {}
+  local capture, statics, seen, implicit = {}, {}, {}, {}
   local function addcap(vn)
     if seen[vn] then return end
     seen[vn] = true
@@ -740,6 +868,7 @@ function CtxMT.lift_cont(ctx, body, env, out, d)
     elseif b.kind == "vec" or b.kind == "lock" then
       -- the prolog vector / lock vector are engine-implicit: dropped at
       -- every use site, so never captured
+      implicit[vn] = b
     else
       capture[#capture + 1] = vn
     end
@@ -752,14 +881,23 @@ function CtxMT.lift_cont(ctx, body, env, out, d)
     if b and b.kind == "static" then return b end
     return nil
   end })
+  for vn, b in pairs(implicit) do penv[vn] = b end
   local fbuf = {}
   local decls = {}
+  local wide = ctx.wide and #capture > WIDE_CAPS
   for i, vn in ipairs(capture) do
-    local lv = "c" .. i
-    decls[#decls + 1] = "local " .. lv .. " = CAPREF(base, " .. (i - 1) .. ")"
-    penv[vn] = { lua = lv, kind = env[vn].kind }
+    if wide then
+      penv[vn] = { lua = "CAPREF(base, " .. (i - 1) .. ")", kind = env[vn].kind }
+    else
+      local lv = "c" .. i
+      decls[#decls + 1] = "local " .. lv .. " = CAPREF(base, " .. (i - 1) .. ")"
+      penv[vn] = { lua = lv, kind = env[vn].kind }
+    end
   end
+  local saved_loc = ctx.fnloc
+  ctx.fnloc = (wide and 0 or #capture) + 2
   local fval = compile_value(ctx, body, penv, fbuf, 1)
+  ctx.fnloc = saved_loc
   local def = { fname .. " = function(base, h)" }
   for _, l in ipairs(decls) do def[#def + 1] = "  " .. l end
   for _, l in ipairs(fbuf) do def[#def + 1] = l end
@@ -767,31 +905,38 @@ function CtxMT.lift_cont(ctx, body, env, out, d)
   def[#def + 1] = "end"
   ctx.buf[#ctx.buf + 1] = table.concat(def, "\n")
 
-  local parts = { fname }
-  for _, vn in ipairs(capture) do parts[#parts + 1] = env[vn].lua end
-  local mk = (#capture <= 16) and ("NEWCONT" .. #capture) or "NEWCONTV"
-  return mk .. "(" .. table.concat(parts, ", ") .. ")"
+  local caps = {}
+  for _, vn in ipairs(capture) do caps[#caps + 1] = env[vn].lua end
+  return newcont_call(ctx, fname, caps)
 end
 
 -- a zero-param static used as a continuation value: wrap into a handle
 function CtxMT.mkhandle(ctx, st, out, d)
-  -- captures = the static's free vars (numbers)
-  if #st.fvs > 16 then refuse(ctx, "handle captures > 16") end
+  -- captures = the static's free vars (numbers). A consume helper for a
+  -- sequent premise closes over two locals per premise variable plus the
+  -- assumption and the engine temps (2*N+5), so six premises already need
+  -- 17. The width must not be capped: refusing leaves NativePred[name]
+  -- unset while the already-translated caller still calls it.
   local fname = liftname(ctx, "LH")
-  local decls, parts = {}, { fname }
-  local penv = setmetatable({}, { __index = st.env })
+  local decls, caps = {}, {}
   local args = {}
   for i, vn in ipairs(st.fvs) do
-    decls[#decls + 1] = "  local c" .. i .. " = CAPREF(base, " .. (i - 1) .. ")"
-    args[#args + 1] = "c" .. i
-    parts[#parts + 1] = st.env[vn].lua
+    if st.wide then
+      args[#args + 1] = "CAPREF(base, " .. (i - 1) .. ")"
+    else
+      decls[#decls + 1] = "  local c" .. i .. " = CAPREF(base, " .. (i - 1) .. ")"
+      args[#args + 1] = "c" .. i
+    end
+    caps[#caps + 1] = st.env[vn].lua
   end
+  local call_args = table.concat(args, ", ")
+  if st.wide then call_args = "{" .. call_args .. "}" end
   local def = { fname .. " = function(base, h)" }
   for _, l in ipairs(decls) do def[#def + 1] = l end
-  def[#def + 1] = "  return " .. st.fn .. "(" .. table.concat(args, ", ") .. ")"
+  def[#def + 1] = "  return " .. st.fn .. "(" .. call_args .. ")"
   def[#def + 1] = "end"
   ctx.buf[#ctx.buf + 1] = table.concat(def, "\n")
-  return "NEWCONT" .. #st.fvs .. "(" .. table.concat(parts, ", ") .. ")"
+  return newcont_call(ctx, fname, caps)
 end
 
 -- ---------------------------------------------------------------------------
@@ -821,7 +966,8 @@ local VAR_BASE, CONS_BASE = E.VAR_BASE, E.CONS_BASE
 -- translate_core: shared by defprolog define-forms and the t-star driver
 -- defuns. `allparams` is the full parameter list whose LAST FOUR entries are
 -- the Vec / Lock / Count / Cont gensyms (the uniform CPS goal ABI).
-local function translate_core(name, allparams, body)
+-- mode: false, "split" (LET_SPLIT_LOCALS), or "wide" (see WIDE_CAPS)
+local function translate_once(name, allparams, body, mode)
   local np = #allparams
   assert(np >= 4, "prolog fn must have at least the B L K C params")
   local nparams = np - 4
@@ -830,6 +976,7 @@ local function translate_core(name, allparams, body)
 
   local ctx = setmetatable({
     buf = {}, nlift = 0, nlocal = 0, fail = {}, liftnames = {},
+    fnloc = nparams + 2, split = mode and true or false, wide = mode == "wide",
   }, CtxMT)
 
   local env = {}
@@ -855,12 +1002,17 @@ local function translate_core(name, allparams, body)
     return nil, tostring(val)
   end
 
-  if #ctx.liftnames > 150 then
-    return nil, "too many lifted functions (" .. #ctx.liftnames .. ")"
-  end
   local src = { CHUNK_PREAMBLE }
-  if #ctx.liftnames > 0 then
-    src[#src + 1] = "local " .. table.concat(ctx.liftnames, ", ")
+  if ctx.wide then
+    src[#src + 1] = "local NEWCONTT, CONSL = E.newcontT, E.cons_list\nlocal LT = {}"
+  else
+    if #ctx.liftnames > 150 then
+      return nil, "too many lifted functions (" .. #ctx.liftnames .. ")", nil,
+             "too many lifted functions"
+    end
+    if #ctx.liftnames > 0 then
+      src[#src + 1] = "local " .. table.concat(ctx.liftnames, ", ")
+    end
   end
   for _, def in ipairs(ctx.buf) do src[#src + 1] = def end
   src[#src + 1] = "return function(" .. table.concat(sig, ", ") .. ")"
@@ -871,11 +1023,35 @@ local function translate_core(name, allparams, body)
 
   local chunk, err = loadstring(source, "@prolog:" .. name)
   if not chunk then
-    return nil, "luagen: " .. tostring(err) .. "\n" .. source
+    return nil, "luagen: " .. tostring(err) .. "\n" .. source, nil, err
   end
   local fn = chunk(E, NP, F, E.materialize, E.import_cached)
   return fn, nil, source
 end
+
+-- Let-chain splitting (see compile_value) costs a call per split point, so
+-- it is only used when the unsplit chunk exceeds Lua's local-variable cap.
+-- The wide shape (see WIDE_CAPS) is the last resort, for what splitting
+-- alone cannot fit.
+local function width_error(lerr)
+  if not lerr then return false end
+  lerr = tostring(lerr)
+  return lerr:find("local variables", 1, true) ~= nil
+      or lerr:find("upvalues", 1, true) ~= nil
+      or lerr:find("too complex", 1, true) ~= nil
+      or lerr:find("too many lifted functions", 1, true) ~= nil
+end
+
+local function translate_core(name, allparams, body)
+  local fn, err, src, lerr = translate_once(name, allparams, body, false)
+  if lerr and tostring(lerr):find("local variables", 1, true) then
+    fn, err, src, lerr = translate_once(name, allparams, body, "split")
+  end
+  if width_error(lerr) then
+    fn, err, src = translate_once(name, allparams, body, "wide")
+  end
+  return fn, err, src
+end
 M.translate_core = translate_core
 
 -- translate a (define Name P1..Pk B L K C -> Body) form (defprolog output)
diff --git a/prolog_engine.lua b/prolog_engine.lua
index 40a8eb2..819bd80 100644
--- a/prolog_engine.lua
+++ b/prolog_engine.lua
@@ -186,6 +186,12 @@ local function mkcons(carv, cdrv)
 end
 M.cons = mkcons
 
+-- t[1] . t[2] . ... . tail, allocated innermost first like nested CONS calls
+function M.cons_list(t, tail)
+  for i = #t, 1, -1 do tail = mkcons(t[i], tail) end
+  return tail
+end
+
 function M.car(v) return cells[v - CONS_BASE] end
 function M.cdr(v) return cells[v - CONS_BASE + 1] end
 function M.is_cons(v) return v >= CONS_BASE end
@@ -344,6 +350,20 @@ function M.newcontV(fn, ...)
   return h
 end
 
+-- the captures arrive as one array: the wide translation of a continuation
+-- whose argument list alone would pass LuaJIT's 250-register frame limit.
+-- Same capbuf layout as newcontV; the table is not kept.
+function M.newcontT(fn, t)
+  local k = #t
+  ckroom(k)
+  local b = cap_top
+  for i = 1, k do capbuf[b + i - 1] = t[i] end
+  cap_top = b + k
+  local h = ch_top + 1; ch_top = h
+  contFn[h] = fn; contBase[h] = b
+  return h
+end
+
 -- handle with a spill table for non-int32 captures (cold path)
 function M.newcont_spill(fn, tbl)
   local h = ch_top + 1; ch_top = h
diff --git a/scripts/run-tests.lua b/scripts/run-tests.lua
index 29a9dcd..6b3fc68 100644
--- a/scripts/run-tests.lua
+++ b/scripts/run-tests.lua
@@ -32,6 +32,7 @@ local specs = {
   "test/boot_cache_spec.lua",
   "test/cli_spec.lua",
   "test/checked_integer_spec.lua",
+  "test/datatype_consume_spec.lua",
   "test/engine_spec.lua",
   "test/error_robustness_spec.lua",
   "test/eval_order_spec.lua",
@@ -52,6 +53,7 @@ local specs = {
   "test/typecheck_api_spec.lua",
   "test/typecheck_lazy_spec.lua",
   "test/utf8_strings_spec.lua",
+  "test/wide_compile_spec.lua",
 }
 
 local function sh_quote(s) return "'" .. tostring(s):gsub("'", "'\\''") .. "'" end
diff --git a/test/datatype_consume_spec.lua b/test/datatype_consume_spec.lua
new file mode 100644
index 0000000..370f365
--- /dev/null
+++ b/test/datatype_consume_spec.lua
@@ -0,0 +1,214 @@
+-- datatype_consume_spec.lua — sequent rules with many premises.
+--
+--   luajit test/datatype_consume_spec.lua
+--
+-- A datatype rule whose conclusion context has six or more premises over
+-- another user type used to die, once that rule was entered, with
+-- "shen.consume<N> is undefined". Five premises worked.
+--
+-- shen.specialise-consume gensyms a helper per premise. The native Prolog
+-- translator closure-converts that helper's continuation, and the capture
+-- count is two locals per premise variable plus the assumption and engine
+-- temps (2*N+5). Five premises capture 15 values and fit NEWCONT0..16.
+-- Six premises capture 17. mkhandle refused past 16, so NativePred[name]
+-- stayed nil and the already-translated caller invoked a missing field.
+--
+-- Entering the rule does not require the query to use it: after the datatype
+-- is loaded, any typecheck that walks *datatypes* and reaches the predicate
+-- (here, "2 : piece", which fails the earlier piece rule) calls it. A
+-- matching hypothesis must still succeed, and a miss must still fail.
+
+local shen = require("shen")
+shen.boot{ quiet = true }
+local R = require("runtime")
+local P = shen.prims
+local E = require("prolog_engine")
+local PC = require("prolog_compile")
+
+local pass, fail = 0, 0
+local function check(desc, got, want)
+  if got == want then
+    pass = pass + 1
+  else
+    fail = fail + 1
+    print(string.format("FAIL %s: got %s want %s", desc, tostring(got), tostring(want)))
+  end
+end
+
+local function errmsg(err)
+  if type(err) == "string" then return P.translate_error(err) end
+  if type(err) ~= "table" then return P.translate_error(tostring(err)) end
+  local parts = {}
+  for k, v in pairs(err) do
+    parts[#parts + 1] = tostring(k) .. "=" .. tostring(v)
+  end
+  return table.concat(parts, " | ")
+end
+
+-- Kernel shen.typecheck, not the embedding helper: the helper turns every
+-- error into false, which would hide "shen.consumeN is undefined".
+local function typecheck(expr, ty)
+  P.GLOBALS["shen.*infs*"] = 0
+  local forms = P.F["read-from-string"](expr .. " : " .. ty)
+  local ok, res = pcall(P.F["shen.typecheck"], forms[1], forms[2][2][1])
+  if not ok then return nil, errmsg(res) end
+  return res
+end
+
+local CONS = R.intern("cons")
+local COLON = R.intern(":")
+local PIECE = R.intern("piece")
+
+local function cons_form(a, b)
+  return R.cons(CONS, R.cons(a, R.cons(b, R.NIL)))
+end
+
+local function list_form(xs)
+  local t = R.NIL
+  for i = #xs, 1, -1 do t = cons_form(xs[i], t) end
+  return t
+end
+
+local function judgement(term, ty)
+  return R.cons(term, R.cons(COLON, R.cons(ty, R.NIL)))
+end
+
+-- Run the datatype predicate the way search-user-datatypes does.
+local function run_rule(name, goal, assum)
+  local fn = E.NativePred[name .. "#type"]
+  if fn == nil then return nil, "no native predicate " .. name end
+  local q = E.query_begin()
+  local done = E.newcont0(function() return true end)
+  local ok, res = pcall(fn, E.import_cached(goal), E.import_cached(assum), 0, done)
+  E.query_end(q)
+  if not ok then return nil, errmsg(res) end
+  return res
+end
+
+-- The same predicate on the legacy engine: the KL defun, called the way
+-- shen.typecheck starts a proof. Wide rules run wide-mode code here
+-- (compiler.lua, WIDE).
+local function run_legacy(name, goal, assum)
+  local fn = P.F[name .. "#type"]
+  local lock = P.F["@v"](true, P.F["@v"](0, P.F["vector"](0)))
+  local ok, res = pcall(fn, goal, assum, P.F["shen.prolog-vector"](), lock, 0,
+                        function() return true end)
+  if not ok then return nil, errmsg(res) end
+  return res
+end
+
+local function varname(i) return "V" .. i end
+
+local function define_row(n)
+  local vars, jud = {}, {}
+  for i = 1, n do
+    vars[i] = varname(i)
+    jud[i] = vars[i] .. " : piece"
+  end
+  local name = "row" .. n
+  shen.eval(string.format([[
+(datatype %s
+  %s >> P;
+  %s
+  [%s] : %s >> P;)
+]], name, table.concat(jud, ", "), string.rep("_", 16),
+     table.concat(vars, " "), name))
+  return name
+end
+
+shen.eval([[
+(datatype piece
+  if (element? X [0 1])
+  _____________________
+  X : piece;)
+]])
+
+-- Five is the last width that fit the old 16-capture helper. Six is the
+-- first that used to be missing. From sixteen the native consume helper
+-- nested past LuaJIT's 100-table __index chain ("loop in gettable") and then
+-- past Lua's 200 locals per function; from about thirty the legacy KL defun
+-- did too, and the datatype failed to load at all. From thirty-eight the
+-- legacy continuations passed ~3N values (250 registers per frame), which
+-- needed wide mode on both compilers, as did 40+ in the native translator.
+-- Sixty-four is past the 60-upvalue and 200-syntax-level limits, 100 and
+-- 128 past the native 150 lifted functions. See the note at the end.
+local WIDTHS = { 5, 6, 8, 12, 15, 16, 20, 24, 30, 32, 37, 38, 40, 64, 100, 128 }
+
+local function check_width(n)
+  local before = {}
+  for k in pairs(PC.registry) do before[k] = true end
+  local loaded, name = pcall(define_row, n)
+  check(n .. " premises: datatype loads", loaded or errmsg(name), true)
+  if not loaded then return end
+  local helpers, native = 0, 0
+  for k in pairs(PC.registry) do
+    if not before[k] and k:match("^shen%.consume") then
+      helpers = helpers + 1
+      if E.NativePred[k] ~= nil then native = native + 1 end
+    end
+  end
+  check(n .. " premises: every consume helper translates natively",
+        helpers > 0 and native == helpers, true)
+  check(n .. " premises: rule predicate translates natively",
+        E.NativePred[name .. "#type"] ~= nil, true)
+  local ty, err = typecheck("0", "piece")
+  check(n .. " premises: 0 : piece still holds",
+        err or R.to_str(ty), "piece")
+  local ty2, err2 = typecheck("2", "piece")
+  check(n .. " premises: walking the rule does not raise", err2, nil)
+  check(n .. " premises: 2 : piece is not a piece",
+        ty2 == false, true)
+
+  local elems = {}
+  for i = 1, n do elems[i] = (i % 2 == 0) and 1 or 0 end
+  local row = list_form(elems)
+  local hyp = R.cons(judgement(row, R.intern(name)), R.NIL)
+  local goal = judgement(0, PIECE)
+  local hit, herr = run_rule(name, goal, hyp)
+  check(n .. " premises: matching hypothesis fires the rule",
+        herr or hit, true)
+  local miss, merr = run_rule(name, goal, R.NIL)
+  check(n .. " premises: empty context misses", merr or miss, false)
+
+  local short = {}
+  for i = 1, n - 1 do short[i] = 0 end
+  local bad = R.cons(judgement(list_form(short), R.intern(name)), R.NIL)
+  local wrong, werr = run_rule(name, goal, bad)
+  check(n .. " premises: short hypothesis misses", werr or wrong, false)
+
+  -- the LAST premise is still unpacked: on wide rules it runs in code that
+  -- a let-chain split moved into a separate function. Only the assumption
+  -- 7 : piece taken from the last element proves 7 : piece.
+  local tail = {}
+  for i = 1, n do tail[i] = elems[i] end
+  tail[n] = 7
+  local tailhyp = R.cons(judgement(list_form(tail), R.intern(name)), R.NIL)
+  local seven = judgement(7, PIECE)
+  local thit, therr = run_rule(name, seven, tailhyp)
+  check(n .. " premises: last element is unpacked", therr or thit, true)
+  local tmiss, tmerr = run_rule(name, seven, hyp)
+  check(n .. " premises: 7 : piece needs the last element", tmerr or tmiss, false)
+
+  local nope = judgement(2, PIECE)
+  local no, nerr = run_rule(name, nope, hyp)
+  check(n .. " premises: unpacked rule does not prove 2 : piece",
+        nerr or no, false)
+
+  local lt, lterr = run_legacy(name, seven, tailhyp)
+  check(n .. " premises: legacy: last element is unpacked", lterr or lt, true)
+  local lm, lmerr = run_legacy(name, seven, hyp)
+  check(n .. " premises: legacy: 7 : piece needs the last element", lmerr or lm, false)
+  local ls, lserr = run_legacy(name, goal, bad)
+  check(n .. " premises: legacy: short hypothesis misses", lserr or ls, false)
+  local le, leerr = run_legacy(name, goal, R.NIL)
+  check(n .. " premises: legacy: empty context misses", leerr or le, false)
+end
+
+for _, n in ipairs(WIDTHS) do check_width(n) end
+
+-- 194 premises is the widest that loads (checked by hand, ~15 s, so not in
+-- WIDTHS). At 195 the consume helper's own signature has N+6 = 201
+-- parameters, past Lua's 200 locals per function in either compiler.
+
+print(string.format("datatype_consume_spec: %d pass, %d fail", pass, fail))
+os.exit(fail == 0 and 0 or 1)
diff --git a/test/engine_spec.lua b/test/engine_spec.lua
index 0f0d0dd..d432e80 100644
--- a/test/engine_spec.lua
+++ b/test/engine_spec.lua
@@ -161,6 +161,45 @@ do
     return E.spill(hh)[1] == sym
   end, { sym })
   check(E.thawH(hs) == true, "spill captures")
+
+  -- wide handles (the translator emits newcontV past 16 captures): same
+  -- capbuf layout as newcont16, and reclaimed by undo
+  local function readback(k, mk)
+    local vals = {}
+    for i = 1, k do vals[i] = i * 3 + k end
+    local seen
+    local kfn = function(b)
+      seen = {}
+      for i = 1, k do seen[i] = E.capref(b, i - 1) end
+      return true
+    end
+    local tm2, vm2, hm2, bm2, cm2 = E.marks()
+    local hh = mk(kfn, unpack(vals))
+    local _, _, _, top = E.tops()
+    E.thawH(hh)
+    local ok = #seen == k and top == bm2 + k
+    for i = 1, k do ok = ok and seen[i] == vals[i] end
+    E.undo(tm2, vm2, hm2, bm2, cm2)
+    local _, _, _, top2, ch2 = E.tops()
+    return ok and top2 == bm2 and ch2 == hm2
+  end
+  check(readback(16, E.newcont16) and readback(16, E.newcontV),
+        "newcontV matches newcont16 layout")
+  for _, k in ipairs({ 17, 41, 100 }) do
+    check(readback(k, E.newcontV), "newcontV " .. k .. " captures read back and reclaim")
+  end
+  -- the wide translation's table-fed constructor
+  local function newcontT(fn, ...) return E.newcontT(fn, { ... }) end
+  for _, k in ipairs({ 1, 16, 49, 261 }) do
+    check(readback(k, newcontT), "newcontT " .. k .. " captures read back and reclaim")
+  end
+
+  -- cons_list builds the same term as nested cons
+  local a, b, c = E.newvar(), E.newvar(), E.newvar()
+  local flat = E.cons_list({ a, b, c }, 0)
+  check(E.car(flat) == a and E.car(E.cdr(flat)) == b
+        and E.car(E.cdr(E.cdr(flat))) == c and E.cdr(E.cdr(E.cdr(flat))) == 0,
+        "cons_list matches nested cons")
 end
 
 -- ---------------------------------------------------------------------------
diff --git a/test/eval_order_spec.lua b/test/eval_order_spec.lua
index 799bfe6..56a27a6 100644
--- a/test/eval_order_spec.lua
+++ b/test/eval_order_spec.lua
@@ -167,6 +167,51 @@ do
         "pure chain codegen allocates no scratch table")
 end
 
+-- ---------------------------------------------------------------------------
+-- long let chains: past a local budget the rest of the chain continues in a
+-- separate KC function (Lua caps a function at 200 locals). Order, value and
+-- tail calls must be unaffected. Each binding feeds the next, as in the
+-- kernel's pattern-matching code, so few are live across a split point.
+-- ---------------------------------------------------------------------------
+do
+  -- past Lua's 200-local cap; kept shallow otherwise, since the Shen reader
+  -- recurses several frames per nesting level
+  local n = 210
+  -- L1 = Z + log(1), Li = L(i-1) + log(i); every binding is a local
+  local function chain(step, final)
+    local src = final
+    for i = n, 2, -1 do
+      src = "(let L" .. i .. " (+ L" .. (i - 1) .. " " .. step(i) .. ") " .. src .. ")"
+    end
+    return "(let L1 (+ Z " .. step(1) .. ") " .. src .. ")"
+  end
+  local logged = function(i) return "(eo-log " .. i .. ")" end
+  local Ln = "L" .. n
+  local total = n * (n + 1) / 2
+
+  local kl = R.read_all("(defun eo-lets-kl (Z) " .. chain(logged, Ln) .. ")")[1]
+  check((loadstring or load)(C.cdefun(kl)) ~= nil, "210-let KL defun compiles to loadable Lua")
+
+  shen.eval("(define eo-lets Z -> " .. chain(logged, Ln) .. ")")
+  eq(trace("(eo-lets 0)"), upto(n), "210-let chain evaluates in source order")
+  eq(shen.eval("(eo-lets 0)"), total, "210-let chain value")
+  -- a binding from before the split, read after it
+  shen.eval("(define eo-lets-early Z -> " .. chain(logged, "(+ L1 " .. Ln .. ")") .. ")")
+  eq(shen.eval("(eo-lets-early 5)"), 5 + 1 + 5 + total, "binding from before a let split is visible after it")
+
+  -- the same chain in value position (hoisted as a control form first)
+  shen.eval("(define eo-lets-val Z -> (+ 1 " .. chain(logged, Ln) .. "))")
+  eq(shen.eval("(eo-lets-val 0)"), total + 1, "210-let chain in value position")
+
+  -- a self-tail call that ends up in the split-off part stays a tail call
+  local plain = function(i) return tostring(i) end
+  shen.eval("(define eo-lets-rec 0 Acc -> Acc N Acc -> "
+            .. chain(plain, "(eo-lets-rec (- N 1) (+ Acc " .. Ln .. "))")
+            :gsub("%(%+ Z ", "(+ 0 ") .. ")")
+  eq(shen.eval("(eo-lets-rec 20000 0)"), 20000 * total,
+     "self tail call past a let split does not grow the stack")
+end
+
 -- ---------------------------------------------------------------------------
 -- collateral: constructs whose order must NOT have changed.
 -- ---------------------------------------------------------------------------
diff --git a/test/freeze_cont_spec.lua b/test/freeze_cont_spec.lua
index 62b7ce5..a683029 100644
--- a/test/freeze_cont_spec.lua
+++ b/test/freeze_cont_spec.lua
@@ -129,5 +129,21 @@ ev([[(defun fc-cap (X)
           (if false 1 (thaw G)))))]])
 check(ev("(fc-cap 8)") == 8, "freeze captures outer X, not inner let")
 
+-- an inline thaw inside a value-position control form: that form is hoisted
+-- into a KC function, which must receive the freeze body's free variables
+-- (here Z, which the hoisted `if` never mentions itself)
+ev([[(defun fc-kc (X Z)
+      (let G (freeze Z)
+        (let Y (if (= X 0) (thaw G) 5)
+          Y)))]])
+check(ev("(fc-kc 0 42)") == 42, "inline thaw in hoisted control form sees freeze captures")
+check(ev("(fc-kc 1 42)") == 5, "inline thaw in hoisted control form: other branch")
+ev([[(defun fc-kc2 (X Z W)
+      (let G1 (freeze W)
+        (let G2 (freeze (+ Z (thaw G1)))
+          (let Y (if (= X 0) (thaw G2) 5)
+            Y))))]])
+check(ev("(fc-kc2 0 40 2)") == 42, "nested inline thaws in hoisted control form")
+
 io.write(string.format("freeze_cont_spec: %d pass, %d fail\n", npass, nfail))
 os.exit(nfail == 0 and 0 or 1)
diff --git a/test/wide_compile_spec.lua b/test/wide_compile_spec.lua
new file mode 100644
index 0000000..d519b9c
--- /dev/null
+++ b/test/wide_compile_spec.lua
@@ -0,0 +1,167 @@
+-- test/wide_compile_spec.lua — KL functions too wide for ordinary Lua.
+--
+--   luajit test/wide_compile_spec.lua
+--
+-- Each case is a defun whose ordinary Lua exceeds a Lua limit (200 locals,
+-- 60 upvalues). prims.lua's P.eval then recompiles just that defun in wide
+-- mode (compiler.lua, WIDE). Every case checks the ordinary code really is
+-- rejected, so the case keeps exercising the wide path, and that the wide
+-- code computes the same values with the same evaluation behaviour.
+
+package.path = (arg[0]:gsub("test/[^/]*$", "")) .. "?.lua;" .. package.path
+
+local shen = require("shen")
+shen.boot{ quiet = true }
+local R = require("runtime")
+local C = require("compiler")
+local P = shen.prims
+local F = P.F
+local loadstr = loadstring or load
+
+local npass, nfail = 0, 0
+local function check(cond, name)
+  if cond then npass = npass + 1
+  else
+    nfail = nfail + 1
+    io.write("FAIL: ", name, "\n")
+  end
+end
+local function eq(got, want, name)
+  if got == want then npass = npass + 1
+  else
+    nfail = nfail + 1
+    io.write("FAIL: ", name, "\n  want: ", tostring(want),
+             "\n  got:  ", tostring(got), "\n")
+  end
+end
+
+local function show(x)
+  local t = {}
+  while R.is_cons(x) do t[#t + 1] = tostring(x[1]); x = x[2] end
+  return table.concat(t, " ")
+end
+
+local function nums(from, to, step)
+  local t = {}
+  for i = from, to, step or 1 do t[#t + 1] = tostring(i) end
+  return table.concat(t, " ")
+end
+
+local function kl_list(xs)
+  local s = "()"
+  for i = #xs, 1, -1 do s = "(cons " .. xs[i] .. " " .. s .. ")" end
+  return s
+end
+
+-- (let N1 E1 (let N2 E2 ... BODY)) from parallel name / expr lists
+local function let_chain(names, exprs, body)
+  local s = body
+  for i = #names, 1, -1 do s = "(let " .. names[i] .. " " .. exprs[i] .. " " .. s .. ")" end
+  return s
+end
+
+local function read1(src) return R.read_all(src)[1] end
+
+-- the ordinary code is rejected with `why`; the wide code loads; P.eval
+-- (the path every defun takes) installs a working function
+local function define_wide(src, why, name)
+  local form = read1(src)
+  local _, err = loadstr(C.compile_top(form))
+  check(err ~= nil and tostring(err):find(why, 1, true) ~= nil,
+        name .. ": ordinary code exceeds " .. why .. " (" .. tostring(err) .. ")")
+  local wide = C.compile_top(form, true)
+  check(loadstr(wide) ~= nil, name .. ": wide code loads")
+  P.eval(form)
+  return form, wide
+end
+
+local N = 210
+
+-- 1) more than 120 bindings live at once: the let split hands the whole live
+--    set to the continuation as one table
+do
+  local names, exprs, refs = {}, {}, {}
+  for i = 1, N do
+    names[i] = "L" .. i
+    exprs[i] = "(+ X " .. i .. ")"
+    refs[i] = names[i]
+  end
+  local _, wide = define_wide("(defun wc-live (X) " .. let_chain(names, exprs, kl_list(refs)) .. ")",
+                              "local variables", "all-live let chain")
+  check(wide:find("return KC%[%d+%]%({") ~= nil, "all-live let chain: split passes a table")
+  eq(show(F["wc-live"](10)), nums(11, 10 + N), "all-live let chain: every binding survives the split")
+
+  -- the same live set captured by a freeze: BIND(KC[i], {...})
+  define_wide("(defun wc-frz (X) " .. let_chain(names, exprs, "(freeze " .. kl_list(refs) .. ")") .. ")",
+              "local variables", "wide freeze")
+  local th = F["wc-frz"](0)
+  eq(show(F["thaw"](th)), nums(1, N), "wide freeze: thaw sees every capture")
+  eq(show(F["thaw"](th)), nums(1, N), "wide freeze: thawing twice gives the same value")
+end
+
+-- 2) a long let chain under a goto-kind failure continuation: the ordinary
+--    code keeps the failure label in one function, which then cannot split.
+--    In wide mode the failure path is a freeze/thaw closure instead.
+do
+  local names, exprs = {}, {}
+  for i = 1, N do
+    names[i] = "G" .. i
+    exprs[i] = (i == 1) and "(+ X 1)" or ("(+ G" .. (i - 1) .. " 1)")
+  end
+  local body = "(if (= X 0) (thaw K) (if (= X 1) (thaw K) (cons G" .. N .. " (cons G1 ()))))"
+  local src = "(defun wc-goto (X) (let K (freeze (do (set wc-fails (+ 1 (value wc-fails))) "
+              .. "(cons fail (cons X ())))) " .. let_chain(names, exprs, body) .. "))"
+  check(C.compile_top(read1(src)):find("goto fail", 1, true) ~= nil,
+        "goto failure path: ordinary code uses a goto failure label")
+  local _, wide = define_wide(src, "local variables", "goto failure path")
+  check(wide:find("goto fail", 1, true) == nil, "goto failure path: wide code has no failure label")
+  shen.eval("(set wc-fails 0)")
+  eq(show(F["wc-goto"](5)), (5 + N) .. " 6", "goto failure path: success path value")
+  eq(shen.eval("(value wc-fails)"), 0, "goto failure path: failure body not run on success")
+  eq(show(F["wc-goto"](0)), "fail 0", "goto failure path: first failure exit")
+  eq(show(F["wc-goto"](1)), "fail 1", "goto failure path: second failure exit")
+  eq(shen.eval("(value wc-fails)"), 2, "goto failure path: failure body runs once per exit")
+end
+
+-- 3) a lambda closing over more than 60 bindings: LAMW(KC[i], {...})
+do
+  local names, exprs, refs = {}, {}, { "Y" }
+  for i = 1, 70 do
+    names[i] = "A" .. i
+    exprs[i] = "(+ X " .. i .. ")"
+    refs[#refs + 1] = names[i]
+  end
+  local _, wide = define_wide("(defun wc-lam (X) " .. let_chain(names, exprs, "(lambda Y " .. kl_list(refs) .. ")") .. ")",
+                              "upvalues", "wide lambda")
+  check(wide:find("LAMW(", 1, true) ~= nil, "wide lambda: built by LAMW")
+  local f = F["wc-lam"](0)
+  eq(show(P.APP(f, 99)), "99 " .. nums(1, 70), "wide lambda: applies with every capture")
+  eq(show(P.APP(f, 7)), "7 " .. nums(1, 70), "wide lambda: reusable")
+end
+
+-- 4) a curried lambda chain deeper than CURRY_DEPTH (the kernel's lambda
+--    entry for a many-argument function) compiles to CURRY in ordinary code
+do
+  local depth = 40
+  local s = "(cons Y1 (cons Y2 (cons Y" .. depth .. " ())))"
+  for i = depth, 1, -1 do s = "(lambda Y" .. i .. " " .. s .. ")" end
+  local form = read1("(defun wc-curry () " .. s .. ")")
+  local src = C.compile_top(form)
+  check(src:find("CURRY(", 1, true) ~= nil and loadstr(src) ~= nil,
+        "curried chain: compiles to CURRY and loads")
+  P.eval(form)
+  local f1 = P.APP(F["wc-curry"](), "a")
+  local fa, fb = P.APP(f1, "b"), P.APP(f1, "c")
+  for i = 3, depth - 1 do fa = P.APP(fa, i); fb = P.APP(fb, i) end
+  eq(show(P.APP(fa, "z")), "a b z", "curried chain: one branch")
+  eq(show(P.APP(fb, "z")), "a c z", "curried chain: a sibling partial application is independent")
+  eq(show(P.APP(fa, "y")), "a b y", "curried chain: a partial application is reusable")
+
+  local shallow = "(cons Y1 ())"
+  for i = 8, 1, -1 do shallow = "(lambda Y" .. i .. " " .. shallow .. ")" end
+  check(C.compile_top(read1("(defun wc-shallow () " .. shallow .. ")")):find("CURRY", 1, true) == nil,
+        "curried chain: a shallow chain keeps nested closures")
+end
+
+print(string.format("wide_compile_spec: %d pass, %d fail", npass, nfail))
+os.exit(nfail == 0 and 0 or 1)