unifyProof.tex

\subsection{Properties of \unify{}}
\label{sec:properties-unify}

First we give some definitions and results.

\begin{definition}[Unifier]
  Let $C$ be a set of constraints and $\Delta$ a type environment.
  A substitution $\sigma$  is a \emph{unifier} of $(C,\Delta)$ if
  \begin{itemize}
  \item for each $(\itype{T} \lessdot \itype{U}) \in C$ it holds that
    $\Delta \vdash \exp{\sigma}{T} \olsub \exp{\sigma}{U}$;
  \item  for each $(T \doteq U) \in C$ it holds that
    $\exp{\sigma}{T} = \exp{\sigma}{U}$; and
  \item for each or-constraint $\set{\set{\overline{\simpleCons_1}},
      \ldots, \set{\overline{\simpleCons_n}}} \in C$, there exists $1
    \le i \le n$ such that $\sigma$ is a unifier of
    $(\set{\overline{\simpleCons_i}}, \Delta)$. 
  \end{itemize}
\end{definition}

A set of general unifiers can provide any unifier as a substitution
instance of one of its members.
\begin{definition}[Set of general unifiers]
  Let $C$ be a set of constraints and $\Delta$ a type environment. 

  A set of unifiers $M$ for $(C, \Delta)$
  is called \emph{set of general unifiers} if for any unifier $\omega$
  for $(C, \Delta)$ there is some unifier $\sigma \in M$ and a substitution
  $\lambda$ such that $\omega = \lambda   \circ \sigma$.
\end{definition}

A unification problem is \emph{finitary} if there is a finite set of
general unifiers for each constraint set $C$ and type environment $\Delta$.

\begin{theorem}[Soundness]
  \label{theo:unifySoundness}
  % \replaced{If the \unify{} algorithm finds a solution it does not contradict any of the input constraints:
  % $\nexists (a \lessdot b) \in \consSet_{in}$ where $\sigma(a) \nless :
  % \sigma(b)$}{}
   If $\unify{}(\consSet, \Delta) = {(\sigma,  \ol{Y} \triangleleft
     \ol{P})}$, then $\sigma$ is a unifier of $(\consSet,\Delta \cup \set{\ol{Y} <: \ol{P}})$. 
\end{theorem}

\begin{proof}
We show theorem \ref{theo:unifySoundness} by going backwards over every step of the algorithm.
Let $\sigma = \set {a_1 \mapsto T_1, \ldots , a_n \mapsto T_n}$ and $\set{\ol{Y} <: \ol{P}}$ be the result of a $\unify{}(\consSet, \Delta)$ call.
We show for every constraint in the input set $(a \lessdot b) \in \consSet_{in}$ and $(c \doteq d) \in \consSet_{in}$:
$\Delta, \ol{Y} <: \ol{P} \vdash \sigma(a) \olsub \sigma(b)$ and $\sigma(c) = \sigma(d)$\\

We now consider each step of the \unify{} algorithm
which transforms the input set of constraints $C$ to a set $C'$
If $\sigma$ is an unifier of $C'$, then $\sigma$ is an unifier of $C$, too.

\begin{description}
\item[Step 6] The last step does not change the constraint set.
\item[Step 5]
A unifier which is correct for $a \doteq b$ is also correct for $a \lessdot b$.
The transformation $C' = [a/b]C$ does not change this.

\item[Step 4]
The constraint sets are not altered here.

\item[Step 3]
An unifier $\sigma$ that is correct for a constraint set
$[\itype{T}/a]C \cup \set{a \doteq \itype{T}}$ is also correct for
the set $C \cup \set{a \doteq \itype{T}}$.
From the constraint $(a \doteq \itype{T})$ it follows that $\sigma(a) = \itype{T}$.
This means that $\sigma(C) = \sigma([\itype{T}/a]C)$,
because every occurence of $a$ in $C$ will be replaced by $\itype{T}$ anyways when using the unifier $\sigma$.

\item[Step 2]
This step transforms constraints of the form $\exptype{C}{\ol{X}} \lessdot a$ and
$\set{a \lessdot \exptype{C}{\ol{X}}, a \lessdot^* b}$ jinto sets of or-constraints.
We can show that if there is a resulting set of constraints which has $\sigma$ as its correct unifier
then $\sigma$ also has to be a correct unifier for the constraints before this transformation.

We look at each transformation done in step 2:
\begin{description}
\item[$\set{\exptype{C}{\ol{T}} \lessdot a} \in C \to \set{a \doteq [\ol{T}/\ol{X}]N} \in C'$:]
If $\exptype{C}{\ol{X}} <: N$ and $\sigma$ is correct for $(a \doteq [\ol{T}/\ol{X}]N)$
then $\sigma$ is also correct for $(\exptype{C}{\ol{T}} \lessdot a))$.
When substituting $a$ for $[\ol{T}/\ol{X}]N$ we get 
$(\exptype{C}{\ol{T}} \lessdot [\ol{T}/\ol{X}]N)$
, which is correct because $\exptype{C}{\ol{X}} <: \exptype{C}{\ol{Y}}$
(see \texttt{S-CLASS} rule).
\item[$\set{a \lessdot \exptype{C}{\overline{T}},\ a \lessdot^* b} \in C \to \set{T \lessdot b, a \lessdot \exptype{C}{\overline{T}},\ a \lessdot^* b} \in C'$]
obviously.
\item[$\set{a \lessdot \exptype{C}{\overline{T}},\ a \lessdot^* b} \in C \to \set{a \doteq [\ol{T}/\ol{X}]N, a \lessdot \exptype{C}{\overline{T}},\ a \lessdot^* b} \in C'$]
This is the same as in the first transformation.
Here we can also show correctness via the \texttt{S-CLASS} rule.

\end{description}

\item[Step 1]
\begin{description}
\item[erase-rules] remove correct constraints from the constraint set.
A unifier $\sigma$ that is correct for the constraint set $C$
is also correct for $C \cup \set{\theta \doteq \theta}$
and $C \cup \set{\theta \lessdot \theta'}$, when $\theta \leq \theta'$.
\item[swap-rule] does not change the unifier for the constraint set.
$\doteq$ is a symmetric operator and parameters can be swapped freely.
\item[match] The subtype relation is transitive, so if there is a correct solution for
$a \lessdot \exptype{C}{\ol{X}}, \exptype{C}{\ol{X}} \lessdot \exptype{D}{\ol{Y}}$
then this solution would also apply for $a \lessdot \exptype{C}{\ol{X}} \lessdot \exptype{D}{\ol{Y}}$
or $a \lessdot \exptype{D}{\ol{Y}}$.
\item[adopt] An unifier which is correct for $C \cup \set{a \lessdot \exptype{C}{\ol{X}}, b \lessdot^* a, b \lessdot \exptype{D}{\ol{Y}}, b \lessdot \exptype{C}{\ol{X}}}$
is also correct for $C \cup \set{a \lessdot \exptype{C}{\ol{X}}, b \lessdot^* a, b \lessdot \exptype{D}{\ol{Y}}}$.
\item[adapt] If there is a $\sigma$ which is a correct unifier for a set
$C \cup \set{ \exptype{C}{[\ol{A}/\ol{X}]\ol{Y}} \doteq \exptype{C}{\ol{B}}}$ then it is also
a correct unifier for the set $C \cup \set{ \exptype{D}{\ol{A}} \lessdot \exptype{C}{\ol{B}}}$,
if there is a subtype relation $\exptype{D}{\ol{X}} \leq^* \exptype{C}{\ol{Y}}$.
To make the set $C \cup \set{ [\ol{A}/\ol{X}]\exptype{C}{\ol{Y}} \doteq \exptype{C}{\ol{B}}}$ the unifier 
$\sigma$ must satisfy the condition $\sigma([\ol{A}/\ol{X}]\ol{Y}) = \sigma(\ol{B})$.
By substitution we get $C \cup \set{ \exptype{D}{\ol{A}} \lessdot \exptype{C}{[\ol{A}/\ol{X}]\ol{Y}}}$
which is correct under the \texttt{S-CLASS} rule.
\item[reduce] The \texttt{reduce} rule is obviously correct under the FJ typing rules.
\end{description}

\item[OrConstraints]
If $\sigma$ is a correct unifier for one of the constraint sets in $C_{set}$
then it is also a correct unifier for the input set $\consSet_{in}$.
When building the cartesian product of the \textbf{OrConstraints} every possible
combination for $\consSet_{in}$ is build.
No constraint is altered, deleted or modified during this step.
\end{description}
\end{proof}

\hfill $\square$


\begin{theorem}[Completeness]\label{theo:unifyCompleteness}
  $\unify{} (\consSet, \Delta)$ calculates {the set} of general
  unifiers for $(\consSet, \Delta)$. 
\end{theorem}
% A unifier $\sigma$ is a general unifier for $\consSet_{in}$ if it unifies $\consSet_{in}$
% and for every other unifier $\omega$ there is a substitution $\lambda$ so
% that $\omega(x) = \lambda(\sigma(x))$.

\begin{proof}

Let $\sigma = \set {a_1 \mapsto T_1, \ldots , a_n \mapsto T_n}$ be a general unifier.
  
%The \unify{} calculates multiple solutions.

%Our proof goes as follows:
We look at every step of the algorithm, which alters the set of constraints $C$.
We show that if $\sigma$ is general unifer for the input then $\sigma$ is a
general unifer for the altered set of constraints. This means that no solution
is excluded.


%Assume there is a unifier and the Unify algorithm finds it.
%Then no rule makes this unifier impossible / removes this unifier.

\begin{description}
\item[Step 1:]
The first step applies the seven rules from figure
\ref{fig:fgjreduce-rules} and \ref{fig:fgjerase-rules}.

\textbf{erase-rule:} The constraint $\tv{a} \doteq \tv{a}$ is true for every unifier and can be removed.

\textbf{swap-rule:} $\doteq$ is a symmetric operator and parameters can be swapped freely.
This operation does not change the meaning of the constraint set.

\textbf{match-rule:}
If there is a solution for $a \lessdot \exptype{C}{\ol{\itype{T}}}, a \lessdot \exptype{D}{\ol{\itype{U}}}$,
this is also a solution for $a \lessdot \exptype{C}{\ol{\itype{T}}}, \exptype{C}{\ol{\itype{T}}} \lessdot \exptype{D}{\ol{\itype{U}}}$.
A correct unifier $\sigma$ has to find a type for $a$, which complies with $a \lessdot \exptype{C}{\ol{\itype{T}}}$ and $a \lessdot \exptype{D}{\ol{\itype{U}}}$.
Due to the subtyping relation being transitive this means that $\sigma(a) \lessdot \exptype{C}{\ol{\itype{T}}} \lessdot \exptype{D}{\ol{\itype{U}}}$.

\textbf{adopt-rule:} Subtyping in FJ is transitive,
which allows us to apply the adopt rule without excluding any possible unifier.

\textbf{adapt-rule:} Every solution which is correct for the constraints
$Eq \cup \set{ \exptype{C}{[\ol{\itype{A}}/\ol{X}]\ol{\itype{T}}} \doteq \exptype{C}{\ol{\itype{U}}}}$ is also
a correct solution for the set $Eq \cup \set{ \exptype{D}{\ol{\itype{A}}} \lessdot \exptype{C}{\ol{\itype{U}}}}$.
According to the FGJ \texttt{S-CLASS} rule there can only be a possible solution for 
$\exptype{C}{[\ol{\itype{A}}/\ol{X}]\ol{\itype{T}}} \doteq \exptype{C}{\ol{\itype{U}}}$
if $\ol{\itype{U}} = [\ol{\itype{A}}/\ol{X}]\ol{\itype{T}}$.
Therefore this transformation does not remove any possible solution from the constraint set.

\textbf{reduce-rule:}
%The constraint is not altered

If $\sigma$ is a unifier of $\exptype{D}{\ol{\itype{T}}} \lessdot
\exptype{D}{\ol{\itype{U}}}$
then $\sigma$ is a unifier of $\ol{\itype{T}} = \ol{\itype{U}}$.
Therefore this step does not remove a possible solution.

\textbf{equals-rule:}
This rule removes a circle in the constraints.
This does not remove a solution.

\item[Step 2:]
%The second step builds multiple constraint sets of all possible type combinations for the $\lessdot$-constraints.
The second step of the algorithm eliminates $\lessdot$-constraints
by replacing them with $\doteq$-constraints.
For each $(\exptype{C}{\ol{\itype{T}}} \lessdot b), (b \lessdot \exptype{C}{\ol{\itype{U}}})$ constraint the algorithm builds a set with every
possible supertype of $\exptype{C}{\ol{\itype{T}}}$.
So if there is a correct unifier $\sigma$ for the constraints before this conversion there will be at least one set of
constraints for which $\sigma$ is a correct unifier.

Additionally this step resolves constraints of the form $\tv{a} \lessdot \exptype{C}{\ol{\itype{T}}}, \tv{a} \lessdot^* \tv{b}$.
We generate an or-constraint with every possible combination for $\tv{b}$.
This includes every possible solution for $\tv{b}$ and therefore does not remove a possible solution.
This is due to the fact that \TFGJ does not allow lower bounds for generic variables.
%Every type variable left of a $\lessdot$-constraint will get a type assigned by \

\item[Step 3:]
In the third step the \textbf{substitution}-rule is applied.
If there is a constraint $\tv{a} \doteq \type{N}$ then there is no other way to fulfill the constraint set
than replacing $\tv{a}$ with $\type{N}$.
This does not remove a possible solution.

\item[Step 4:]
None of the constraints get modified.

\if0
\erased{
Step 5 a):\\
The removed sets do not have a possible unifier, therefore no possible solution is
omitted in this step.
%\textbf{Proof}:
In step 5.a all constraint sets that have a unifier are in solved form.
All other possibilities are eliminated in steps 1-4.
There are 8 different variations of constraints:\\
$(\tv{a} \doteq \tv{a}), (\tv{a} \doteq C), (C \doteq \tv{a}), (C \doteq C), (\tv{a} \lessdot \tv{a}), (\tv{a} \lessdot C), (C \lessdot \tv{a}), (C \lessdot C)$
After step 1 there are no $(C \doteq C)$, $(C \lessdot C)$ and $(C \doteq \tv{a})$ constraints anymore,
as long as the constraint set has a correct unifier.
Because a constraint set that has a correct unifier cannot contain constraints of the form $N_1 \doteq N_2$ with $N_1 \neq N_2$ and
$(N_1 \lessdot N_2)$ with $(N_1 \nless: N_2)$.
By removing $(N \doteq N)$ and $(C \lessdot D)$ with $(C <: D)$ constraints
no constraints of the form $(C \doteq C)$ and $(C \lessdot D)$
remain in a constraint set that has a correct unifier after step 1.
After step 2 there are no more $(C \lessdot a)$ constraints.
%After step 3 there are no $(a \doteq C)$ anymore.
We only reach step 5 if the constraint set is not changed by the substitution (step 3).
%If at this point a set $Eq_i$ is not in solved form it has no correct unifier.
If the constraint set has a correct unifier only $(a \lessdot a)$, $(a \doteq a)$, $a \lessdot C$ and $(a \doteq C)$ constraints are left at this point.
The type variables in the $(a \lessdot a)$ and $(a \doteq a)$ constraints have to be independent type variables.
If a type variable $c$ is inside a $(c \doteq C)$ constraint it is not an independent type variable.
But this variable $c$ cannot be inside a $(a \doteq a)$ or $(a \lessdot a)$ constraint, because otherwise step 3 would have replaced it in there.
So this step only excludes constraint sets which do not have a correct unifier.
}
\fi
\item[Step 5:]
If the algorithm advances to this step we further only work on constraint sets in solved form.
This means there are only four kinds of constraints left:
($a \doteq \itype{T}$), ($a \lessdot \itype{T}$), ($a \doteq b$) and ($a \lessdot b$) with $a$ and $b$ as type variables.

%We can set all TVs equal, because we allow only same TVs when having circles in a method call.
%This still will lead to the principal type.

The FGJ language does not allow subtype constraints for generic types.
A constraint like $(a \lessdot b)$ in a solution could be inserted as the typing shown in the example below.
But this is not allowed by the syntax of FGJ.
That is why we can treat this constraint as $(a \doteq b)$.

%TODO: This does not alter the outcome because the solution set is not modified anymore. All other TVs alread have a type like A =. Typ

\textit{Example:}
This would be a valid Java program but is not allowed in FGJ:
\begin{lstlisting}
class Example {
  <A extends Object, B extends A> A id(B a){
    return a;
  }
}
\end{lstlisting}

By replacing all ($a \lessdot b$) constraints with ($a \doteq b$) we
  do not remove the general unifier $\sigma$ as $a$ and $b$ are not substituted
  in $\sigma$. 

\item[Step 6:]
In the last step all the constraint sets, which are in solved form, are converted to unifiers.

We see that only a constraint set which has no unifier does not reach solved form.
We showed that in none of the steps of the \unify{} algorithm we exclude a possible unifier.
Also we showed that after we reach step 5 only constraint sets with a correct unifier are in solved form.
By removing all constraint sets which are not in solved form the algorithm does not
remove a possible correct unifier.

If we assume that there is a possible general unifier $\sigma$ for the input set $\consSet_{in}$
and the \unify{} algorithm does not exclude any of the possible unifiers,
then the result \unify{} contains the general unifier.
\hfill $\square$
\end{description}
\end{proof}

\begin{theorem}[Termination]\label{theo:unifyTermination}
  The \unify{} algorithm terminates on every finite input set.
\end{theorem}
The \unify{} algorithm gets called with a set of input constraints.
After resolving the \textbf{OrConstraints} we end up with multiple $Eq$ sets.
Afterwards the algorithm iterates over each of those sets (see Chapter \ref{sec:unify}).
We will show that \unify{} terminates on each of those sets by showing,
that each step of the algorithm removes at least one type variable
until the finishing state is reached.
The finishing state for a constraint set is reached when step 3 is not able to substitute a type variable.
This is checked by step 4 of the algorithm.
Then the $Eq$ set is either in solved form or determined to be unsolvable.

\textit{Proof:}
The \unify{} algorithm reduces the amount of type variables with every iteration.
No step adds a new type variable to the constraint set.
Additionally we have to show that the first step of the algorithm also terminates on every finite input set.

\begin{description}
\item[Step 1] 
Step 1 of the algorithm always terminates. \textit{Proof:}
Every rule either removes a $\lessdot$ constraint or reduces a $\exptype{C}{\ol{X}}$ to $\ol{X}$ inside a constraint.
None of the rules add a new $\lessdot$ constraint or a $\exptype{C}{\ol{X}}$ type to the constraint set.
Step 1 has to come to a stop once there are no more $\lessdot$ constraints or $\exptype{C}{\ol{X}}$ types to reduce.

The rule \textbf{match} seems to generate a new $\exptype{C}{\ol{X}}$ constraint,
but the $\exptype{C}{\ol{X}} \lessdot \exptype{D}{\ol{Y}}$ constraint added by \texttt{match}
will be changed immidiatly into a $\doteq$ constraint by the \texttt{adapt} rule.
Afterwards the \texttt{reduce1} rule will remove this freshly added $\exptype{C}{\ol{X}}$ type.
So effectively a $\doteq$ constraint is removed by this rule in combination with \texttt{adapt} and \texttt{reduce1}.

The \textbf{adopt} rule seems to generate a new $\lessdot$ constraint.
But the \texttt{adopt} rule triggers two other rules. The \texttt{match} and the \texttt{adapt} rule.
\begin{enumerate}
  \item We start with the \texttt{adopt} rule: \\
   $
  \begin{array}[c]{ll}
      \begin{array}[c]{l}
          Eq \cup \, \set{a \lessdot
          \exptype{C}{\ol{X}},
          b \lessdot^* a, b \lessdot \exptype{D}{\ol{Y}}} \\ 
          \hline
          \vspace*{-0.4cm}\\
          Eq \cup \set{
          a \lessdot
          \exptype{C}{\ol{X}},
          b \lessdot^*
          a
          , b \lessdot \exptype{C}{\ol{X}}
          , b \lessdot \exptype{D}{\ol{Y}}
          }
      %Eq \cup \set{\theta_1 \doteq \lambda'_1 \ldo \theta_n \doteq \lambda'_n}
      \end{array}
      \end{array}
      $
  \item We can now apply the \texttt{match} rule to the two resulting $(b \lessdot \ldots)$-constraints.
  If this is not possible due to type \texttt{C} not being a subtype of \texttt{D} or vice versa,
  then the $Eq$ set has no possible solution and \unify{} would terminate as fail $Uni = \emptyset$: \\
  $
  \begin{array}[c]{ll}
  \begin{array}[c]{l}
      Eq \cup \, \set{b \lessdot
      \exptype{C}{\ol{X}},
      b \lessdot
      \exptype{D}{\ol{Y}}} \\ 
      \hline
      \vspace*{-0.4cm}\\
      Eq \cup \set{b \lessdot \exptype{C}{\ol{X}}
      , \exptype{C}{\ol{X}} \lessdot \exptype{D}{\ol{Y}}}
  %Eq \cup \set{\theta_1 \doteq \lambda'_1 \ldo \theta_n \doteq \lambda'_n}
  \end{array}
  & \exptype{C}{\ol{Z}} <: \exptype{D}{\ol{N}} 
  \end{array}
      $\\
  \item The constraint added by the \texttt{match} rule fits the \texttt{adapt} rule, which we apply in the next step: $
  \begin{array}[c]{ll}
  \begin{array}[c]{l}
     Eq \cup \, \set{\exptype{C}{\ol{X}} \lessdot
      \exptype{D}{\ol{Y}}} \\ 
    \hline
    \vspace*{-0.4cm}\\
    Eq \cup \set{\exptype{D}{[ \ol{X} / \ol{Z} ]\ol{N}}
    \doteq \exptype{D}{\ol{Y}}}
  %Eq \cup \set{\theta_1 \doteq \lambda'_1 \ldo \theta_n \doteq \lambda'_n}
  \end{array}
  & \exptype{C}{\ol{Z}} <:\ \exptype{D}{\ol{N}}
  \end{array}
  $
  \end{enumerate}
In the end we have the conversion:\\
\begin{align*}\ddfrac{
  Eq \cup \, \set{a \lessdot
  \exptype{C}{\ol{X}},
  b \lessdot^* a, b \lessdot \exptype{D}{\ol{Y}}}
}{
  Eq \cup \set{a \lessdot
  \exptype{C}{\ol{X}},
  b \lessdot^* a, b \lessdot \exptype{D}{\ol{Y}}, \exptype{D}{[ \ol{X} / \ol{Z} ]\ol{N}}
  \doteq \exptype{D}{\ol{Y}}}
}\end{align*}

We can see now, that only a $\doteq$ constraint is added.
The \texttt{adopt} alone adds a $\lessdot$ constraint,
but due to the fact that it is always used together with \texttt{match} and \texttt{adapt} it effectively just adds a $\doteq$ constraint.

\item[Step 2] This step does not add new type variables to the constraint set.
\item[Step 3] The third step of the \unify{} algorithm removes at least one type variable
from the constraint set or otherwise does not alter $Eq$ at all.
If $Eq$ is not altered the algorithm terminates in the next step.
The type variable is not completely removed but stays inside $Eq$ only in one $a \doteq N$ constraint.
All other occurences are replaced by $N$.
The \texttt{subst} step can therefore only be executed once per type variable.
\end{description}

We see that with each iteration over the steps 1-3 at least one type variable is removed from the constraint set.
Due to the fact that there is never added a fresh type variable during the \unify{} algorithm,
the algorithm will terminate for any given finite set of constraints. \hfill $\square$

%The function $\textbf{TVs}$ returns a set of every type variable used as a singleton in the left or right side of a constraint in the given constraint set.
\if0
\begin{lemma}[Exhaustiveness]\label{lemma:unify-exhaustive}
  %Every type variable used in the input constraints will get an unifier assigned by \unify{}.
  %Given a $\mv{\Pi}$ and $\texttt{L}$ with $\fjtype{}(\mv{\Pi}, \texttt{L}) = (\mtypeEnvironment, \consSet)$
  Given $\unify{}(\consSet) = (\sigma, \unifyGenerics{})$ with $\sigma \neq \emptyset$,
  then the following statement holds:
  $\tv{a} \lessdot \itype{T} \in \consSet \implies \tv{a} \in \textit{dom}(\sigma)$.
  %and $\tv{a} \doteq \itype{T} \in \consSet \implies \tv{a} \in \textit{dom}(\sigma)$.
  Here $\textit{dom}(\sigma)$ is the domain of $\sigma$.
\end{lemma} %TODO:
\textbf{Proof:}
There is no step that removes a type variable on the left side of a $\tv{a} \lessdot \itype{T}$ constraint.
The exception is the \texttt{subst} step, which could replace a $\tv{a}$ in any constraint.
%but here atleast one constraint with the type variable on the left side is kept.
But the \texttt{subst} rule generates a $\tv{a} \doteq \itype{T}$ constraint, which will lead to a type unifier for $\tv{a}$.
If the \unify{} algorithm is successful, then the constraint set is in solved form in step 5.
Every type variable on the left side of a constraint set in solved form will get a substitution in $\sigma$.
\hfill $\square$
\fi

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "TIforGFJ"
%%% End: