Function deepen_stack 

pub fn deepen_stack<R: Send>(
    term: &Term,
    f: impl FnOnce() -> R + Send,
) -> Option<R>

Run f on a stack sized for term — or report that this call is already on one.

Some(r): f ran, here or on a thread of the kernel’s own, and r is its answer. None: this call is NESTED inside one that already sized the stack, so the caller should carry straight on with its ordinary body.

It is one line at the top of a kernel entry point (infer_type opens with it), with no re-indentation of the body:

use logicaffeine_kernel::term_store::deepen_stack;
use logicaffeine_kernel::Term;

fn size(term: &Term) -> usize {
    if let Some(answer) = deepen_stack(term, || size(term)) {
        return answer;
    }
    match term {
        Term::App(f, x) => 1 + size(f) + size(x),
        _ => 1,
    }
}

let term = Term::App(Box::new(Term::Global("f".into())), Box::new(Term::Var("x".into())));
assert_eq!(size(&term), 3);
// A call already running on a sized stack is NESTED and answers `None`.
assert_eq!(deepen_stack(&term, || deepen_stack(&term, || ())), Some(None));

The recursive call inside the closure re-enters the entry point, sees the flag, gets None, and falls through to the real body — so the measurement is paid exactly ONCE per outermost kernel call, which is the same budget enter_kernel’s own depth_exceeds pass already has.

A panic inside f is re-raised on the calling thread with its payload intact, so #[should_panic] and catch_unwind behave exactly as they do without the switch.

The closure must be Send, which every kernel entry’s (&Context, &Term) capture is. reduction::normalize_at is the ONE exception: Transparency::Excluding holds a &dyn Fn(&str) -> bool with no Sync bound, so it is not Send. Adding + Sync to that trait object is the whole fix, and normalize/normalize_checked — which build their own Transparency::All — need nothing.