The description of the unification test (Section 6) is underspecified and actually quite misleading.
The paragraph following Lemma 6.1 appears to suggest that the unification test checks the finite satisfiability of C \cup {\tau^s = \tau} for each single character s. This is a misunderstanding. The unification test actually checks the satisfiability of C' \cup {\tau^s = \tau} where C' is the subset of C that consists of all constraints that _do not_ involve superscripted type variables except \tau^s. (It is pretty obvious that there was something wrong because if we had a way to check the finite satisfiability of C \cup {\tau^s = \tau}, we just solved what we claimed as an undecidable problem.) Note that because C' is finite, this satisfiability is obviously a finite one.
Therefore, in Lemma 6.1, although true, it is not important that C \cup {\tau^s = \tau} is _finitary_ satisfiable to show that the unification test and the extension of it are insufficient. A plain, i.e., possibliy infinite, satisfiability is enough for that purpose. (On the other hand, the premise that C is finitely satisfiable as opposed to being just satisfiable is important. E.g., C such that (C,\alpha) = fix x.x x is infinitely satisfiable but fails the unification test.)
A related error is in the definition of the set A in Corollary 6.2. Here, a plain satisfiability should be used instead of finite satisfiability. Indeed, it is easy to decide the problem for A defined in the proceeding version, i.e., just accept everything in A.
The online version corrects the error in Corollary 6.2. I plan to revise the misleading paragraph sometime in the future.