Suppose the signature is
o : type.
f : o -> o.
Imagine everything lives in a (deBruijn-indexed) context that consists of two variables of type o.
Consider the unification equations
(X[1] = f (Y[Z[2]])) ∧ (Y[1] = X[Z[2]])
where all the existential variables X, Y, Z are variables in contextual-modal-type-theory style, of type (o ⊦ o).
Say the algorithm looks at the first equation. It can't push the inverse of [1] all the way through Y[Z[2]] (since it knows only that at least one of Y or Z must project out its argument, but it doesn't know which one(s) will) so it tries to make progress by at least using the information that X starts with an application of f. It makes up a new variable X', instantiates
X := f (X'[id])
and adds the constraint
X'[1] = Y[Z[2]]
After eliminating the equation with X on the left, carrying out the substitution and conjoining the new constraint onto the right, we get
(Y[1] = f (X'[Z[2]])) ∧ (X'[1] = Y[Z[2]])
which is just an alpha-rewrite (X ↦ Y, Y ↦ X') of the original set of equations, so we haven't made any progress.
Below is some twelf code that illustrates the problem, with a %query not terminating, despite a %terminates check. I feel like I should be able to twist this into a simple type-checking problem, but my brain hasn't coughed it up yet.
o : type. k : o. f : o -> o. eq : o -> o -> o -> type. eq/refl : eq DUMMY M M. test : o -> type. test/ : {X : o -> o} {Y : o -> o} {Z : o -> o} test DUMMY <- ({a} {b} eq DUMMY (X a) (Y (Z b))) <- ({a} {b} eq DUMMY (Y a) (f (X (Z b)))). %mode eq +DUMMY *A *B. %terminates DUMMY (eq DUMMY A B). %mode test +DUMMY. %terminates DUMMY (test DUMMY). %query 1 1 D : test k.
Another update: Frank's reply to my twelf-bearing email contains the word "Oops", so I guess I have found a real bug in the implementation and am not discovering known problems. I've mixed feelings: finding bugs is good, but bugs being there to be found is bad.