Suppose the signature is

`o : type.`

f : o -> o.

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.