I finally found a nice simple example of the oft-mentioned Twelf unification/type-reconstruction bug that happens because of circularity in types of unification variables. o : type. a : o -> type. b : o -> o -> type. eq : b M M -> type. x-c : {w : o} {u : a w -> o} {v : a w} b (u v) w. %abbrev c = x-c W U V. test : eq c. Its symptom, like the last bug I mentioned , is non-termination. The unification problem that comes up is this: find w : o u : a w -> o v : a w such that w = u v Should be simple because the left-hand side is (trivially) a pattern substitution, right? But if you make the substitution w := u v then you're left with the problem of finding u : a (u v) -> o v : a (u v) such that, well, top holds. Twelf stops and proclaims success at this point and runs the abstraction phase, which tries to turn these remaining free unification variables into a sequence of Pi quantifiers — but it can't order them by dependency since there's a cycle, and so loops forever trying. Supposing your signature has k : o, though, the unification problem that has the additional equation that u = lambda x . k is completely solvable. You just get that v is a free variable of type a k. You can see this explicitly happening on the example o : type. k : o. a : o -> type. eq : o -> o -> type. eqo : (a Z -> o) -> (a Z -> o) -> type. refl : eq M M. reflo : eqo M M. x-c : {W : o} {U : a W -> o} {V : a W} eqo U ([x] k) -> eq W (U V) -> type. %abbrev c = x-c W U V. test : c reflo refl. where the typing of test comes back test : {X1:a k} x-c k ([x:a k] k) X1 reflo refl Showing that w must be k, and u must be ([x : a k] k) , and v is left free as X1 : a k . I am beginning to be of the opinion that even the successful inversion of a pattern substitution should be postponed as if it weren't a pattern, if the resulting variable instantiation leads to circularity.