Function deepen_stack_all_with_depth 

pub fn deepen_stack_all_with_depth<R: Send>(
    terms: &[&Term],
    extra_depth: usize,
    f: impl FnOnce() -> R + Send,
) -> Option<R>

deepen_stack_all told about depth the TERMS DO NOT SHOW — and it is not a refinement, it is a hole in the door that this is the only way to close.

THE DEFECT, measured rather than argued. The depth door and the sized stack both measure the term they were HANDED. infer_type’s Var arm does not walk the term — it returns ctx.get(name).cloned(), and Term’s Clone is derived, so it recurses over the BINDING’S type. A term of depth 1 under a context that binds one variable at a type of depth 5000 therefore walks 5000 rungs that neither the door nor deepen_stack ever saw: W_perf_extra::a_shallow_term_under_a_deep_binding_walks_a_depth_nobody_measured runs it in a child process. Every other arm inherits it — an App’s domain check normalises the function’s type, a Global’s type is cloned out of the environment — so the input term’s depth is a LOWER BOUND on what a kernel call descends, never the bound itself.

A caller that knows the depth its walk reaches passes it as extra_depth: the second kernel’s open entry points pass their local plan’s deepest binding. extra_depth of 0 is exactly deepen_stack_all.

use logicaffeine_kernel::term_store::deepen_stack_all_with_depth;
use logicaffeine_kernel::Term;

let shallow = Term::Var("x".into());
// One node, but the walk will descend a binding 5000 levels deep: the stack is sized for that.
assert_eq!(deepen_stack_all_with_depth(&[&shallow], 5000, || "answered"), Some("answered"));