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 ProcedureGiven 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 orvariable.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 hardto show that one of $s_p$, $t_p$, must be a variable and the other must be a leftparenthesis or a different variable. Further, $s_p$ can be shown to be the leftmostsymbol 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 onethat is first in the sequence given in Definition 2A1.) Then call the remainingmember 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 comparisonprocedure 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, withor without number-subscripts, and distinct letters denote distinct variables unlessotherwise stated.Arbitrary types are denoted by lower-case Greek letters except $\lambda$.Parentheses will often (but not always) be omitted from types, and the readershould 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.
Comparison Procedure in Robinson's Unification Algorithm
lambda calculus;type inference;unification
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.