A Note on "On Typability for Rank-2 Intersection Types with Polymorphic Recursion"
Tachio Terauchi
August 13th 2006
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.