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 reflShowing 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.