There were some previous threads suggesting that interactive unification wasn’t working properly with append lists:

I’ve done a bit more digging, and I think interactive unification has the following bug: if there is no possible type for a feature path, but that path does not exist in either of the two input feature structures, then interactive unification does not enforce all constraints (i.e. it produces an incorrect result, rather than reporting unification failure).

I wasn’t sure where to report this bug.

This is admittedly a rare situation (which is probably why it hasn’t been an issue until now). But it happens when recursive computation types lead to a unification failure. I’ve written the following small example to illustrate the problem, where the following code is the entire grammar. Note that there is no parsing involved here, just compilation of this file and interactive unification.

```
; The following types implement the natural numbers,
; using simplest kind of recursion (a single feature SUCC).
; A fully specified natural number is a chain of feature structures,
; with the last feature structure of type "zero",
; and all other feature structure of type "pos".
natnum := *top*.
zero := natnum.
pos := natnum &
[ SUCC natnum ].
; The following types implement an identity function on the natural numbers,
; in the sense that, for any feature structure compatible with "natnum",
; unifying that feature structure with "natnum-with-copy"
; will produce the original feature structure under RESULT.
natnum-with-copy := natnum &
[ RESULT natnum ].
zero-with-copy := zero & natnum-with-copy &
[ RESULT zero ].
pos-with-copy := pos & natnum-with-copy &
[ SUCC.RESULT #diagonal,
RESULT.SUCC #diagonal ].
; The following types implement a defective subtype of "natnum",
; in the sense that "defective-natnum" has no common subtype with "zero".
defective-natnum := natnum.
defective-pos := defective-natnum & pos.
; The following types extend the copying function to the defective type.
; However, note that defectiveness is shifted along the number by one:
; "defective-natnum-with-copy" has a RESULT that is just "natnum";
; "defective-pos-with-copy" enforces defectiveness on its RESULT.SUCC.
defective-natnum-with-copy := defective-natnum & natnum-with-copy.
defective-pos-with-copy := defective-natnum-with-copy & defective-pos & pos-with-copy &
[ RESULT.SUCC defective-natnum ].
; The following are wrapper types, holding a natural number under NATNUM.
; "natnum-with-copy-wrapper" holds the copy operation.
; "defective-one-wrapper" holds the number one (it has one SUCC),
; but where the "pos" is defective.
natnum-wrapper := *top* &
[ NATNUM natnum ].
natnum-with-copy-wrapper := natnum-wrapper &
[ NATNUM natnum-with-copy ].
defective-one-wrapper := natnum-wrapper &
[ NATNUM defective-pos & [ SUCC zero ]].
; The following type would apply the copy operation to the defective number one.
; This would cause a unification failure:
; NATNUM.RESULT.SUCC must be of type "defective-natnum";
; NATNUM.SUCC.RESULT must be of type "zero";
; the above two paths must be re-entrant;
; and there is no common subtype of "defective-natnum" and "zero".
; (Intuitively, the operation pushes the defectiveness along by one,
; but defectiveness is not allowed at the end of the number.)
; Note that neither of the above paths exist in the parent types
; "natnum-with-copy-wrapper" and "defective-one-wrapper".
;fail-wrapper := natnum-with-copy-wrapper & defective-one-wrapper.
; If the above type is uncommented, the LKB correctly throws an error when compiling.
; However, leaving the above type commented out,
; interactive unification of the values of NATNUM
; from "natnum-with-copy-wrapper" and "defective-one-wrapper"
; displays an incorrect result (it does not enforce all the constraints).
; When there is a well-defined result, interactive unification
; does not seem to have a problem with recursive type constraints.
; For example, we can fix the defective type by adding the following two types:
;defective-zero := defective-natnum & zero.
;defective-zero-with-copy := defective-natnum-with-copy & defective-zero & zero-with-copy.
; If these two types are uncommented, interactive unification produces the correct result.
; Similarly, if all three types ("fail-wrapper", "defective-zero", "defective-zero-with-copy")
; are uncommented, the LKB correctly compiles.
```

In more positive news, I can report that when there is no failure, the LKB and interactive unification are both robust to extremely recursive type constraints. I implemented the untyped lambda calculus as a type system, and I tested it using the Ackermann function as a lambda expression on Church numerals (the Ackermann function is non-primitive-recursive, so I thought this would be a good test case). With 10,570 re-entrancies (no that is not a typo), it correctly evaluated A(2,1)=5.