Comparison Procedure in Robinson's Unification Algorithm

Question

I'm studying the Principal Type (PT) Algorithm in Basic Simple Type Theory by J. Roger Hindley. One step to find the PT of a term is the Unification of types. The Robinson's Unification Algorithm uses a comparison procedure like as follow:

Comparison Procedure

Given a pair $(u, v)$ of types, write $u$ and $v$ as symbol-strings, say

$u \equiv s_1 ... s_m$ and $v \equiv t_1 ... t_n$ $(m, n >1)$

where each o f $s_1,... , s_m$, $t_1, ... , t_n$ is an occurrence of a parenthesis, arrow or variable.

If $u \equiv v$, state that $u \equiv v$ and stop.

If $u \not \equiv v$, choose the least $p < \min(m, n)$ such that $s_p \not \equiv t_p$; it is not hard to show that one of $s_p$, $t_p$, must be a variable and the other must be a left parenthesis or a different variable. Further, $s_p$ can be shown to be the leftmost symbol of a unique subtype $u^*$ of $u$. (If $s_p$ is a variable, $u^* \equiv s_p$.) Similarly $t_p$ is the leftmost symbol of a unique subtype $v^*$ of $v$. Choose one of $u^*, v^*$ that is a variable and call it $a$. (If both are variables, choose the one that is first in the sequence given in Definition 2A1.) Then call the remaining member of $(u^*, v^*)$ $\alpha$; the pair $(a, \alpha)$ is called the disagreement pair for $(u, v)$.

My issue is with the Note bellow:

3D5.1 Note To prove that $p$ exists in the case that $u \not \equiv v$ in the comparison procedure we must show that it is not possible to have

$t_1 ... t_n \equiv s_1....s_m t_{m + 1} ... t_n$

with $n > m$. This is left as a (rather dull) exercise for the reader.

I disagree with this note. I can image, say, $u \equiv a \rightarrow b$ and $v \equiv a \rightarrow b \rightarrow c$, where no $p$ is possible.

Maybe I'm missing something! How $p$ is always possible?

---

As asked, the definition of types is given as follow:

2A1 Definition (Types) An infinite sequence of type-variables is assumed to be given, distinct from the term-variables. Types are linguistic expressions defined thus:

i. each type-variable is a type (called an atom);

ii. if $\delta$ and $\rho$ are types then $(\delta \rightarrow \rho)$ is a type (called composite type).

2A1.1 Notation Type-variables are denoted by "a", "b", "c", "d", "e", "f", "g", with or without number-subscripts, and distinct letters denote distinct variables unless otherwise stated.

Arbitrary types are denoted by lower-case Greek letters except $\lambda$.

Parentheses will often (but not always) be omitted from types, and the reader should restore omitted ones in such a way that, for example,

$\rho \rightarrow \sigma \rightarrow \tau \equiv (\rho \rightarrow (\sigma \rightarrow \tau))$

This restoration rule is called association to the right.

Answer 1

It looks like the answer is that, to be syntactically valid, composite types must be fully parenthesized.

In particular, $a \to b \to c$ is not a syntactically valid type (per definition 2A1). 2A1.1 introduces "syntactic shorthand": when they write something like $a \to b \to c$, it should be understand that they actually mean $(a \to (b \to c))$.

The Note appears to be valid when we restrict to syntactically valid types. Thus, your example is not actually a counterexample.