nix-effects

nix-effects embeds a Martin-Löf Type Theory proof checker in pure Nix. Dependent functions, dependent pairs, identity types with J, cumulative universes, verified extraction of plain Nix functions from proof terms. The whole system runs at nix eval time.

Nix has no loops and no tail-call optimization. builtins.genericClosure, the package dependency primitive, doubles as a general-purpose trampoline once you break the thunk chain.