Ulf Norell's "insanely dependent" Pi: [x1 : A1, ..., xn : An] -> B, where every xi is in scope in every Ai, including its own. Must be fully applied. His prototype checker ties the knot lazily: types and terms are pointers to suspended closures, forced at the end. Source: https://github.com/UlfNorell/insane