@@ -866,16 +866,16 @@ left-hand side of negated arrows.

\begin{definition}[Rank-0 negation]

A derivation of $\Gamma\vdash e:t$ is \emph{rank-0 negated} if \Rule{Abs--} never occurs in the derivation of a left premise of a \Rule{PAppL} rule.

\end{definition}

The use of this terminology is borrowed from the ranking of higher-order

\noindentThe use of this terminology is borrowed from the ranking of higher-order

types, since, intuitively, it corresponds to typing a language in

which in the types used in dynamic tests, a negated arrow never occurs on the

left-hand side of another negated arrow.

\begin{theorem}[Partial Completeness]

For every $\Gamma$, $e$, $t$, if $\Gamma\vdash e:t$ is derivable by a rank-0 negated derivation, then there exists $n_o$ such that ${\tyof e \Gamma}\leq t$.

\end{theorem}

The use of type schemes and of possibly non convergencing iterations

\noindentThe use of type schemes and of possibly diverging iterations

yield a system that may seem overly complicated. But it is important

to stress that this systems is defined only to study the declarative

to stress that this systems is defined only to study the

type inference system of Section~\ref{sec:static} and in particular to prod

how close we can get to a complete algorithm for it. But for the

practical application type schemes are not needed, since they are