% TODO: unify changes
% delete wildcard tphs a? when needed
% aswell ass free variables:
% a <. T with fv(T) not empty and not in \Delta' must be removed by U = L
% also in T <. T constraints no free variables are allowed on both sides (why? this is wrong i think)
% the algorithm only removes wildcards, never adds them

\section{Unify}\label{sec:unify}

\subsection{Description}
The \unify{} algorithm tries to find a solution for a set of constraints like
$\set{\exptype{List}{String} \lessdot \tv{a}, \exptype{List}{Integer} \lessdot \tv{a}}$.
Those two constraints imply that we have to find a type replacement for type variable $\tv{a}$,
which is a supertype of $\exptype{List}{String}$ aswell as $\exptype{List}{Integer}$.

The input constraints are transformed until they reach a solved form which is then converted to a type solution.
A constraint set is in solved form if it only consists of constraints of the form 
$\tv{a} \doteq \type{T}$ and $\tv{a} \lessdot \type{T}$.
\unify{} is described as a nondeterministic algorithm.
Some constraints allow for multiple transformations from which
the algorithm has to pick the right one.
There are also cases where there is more than on correct transformation and
therefore more than one correct solution to the given input constraints.
For that case still only one correct solution is returned by this specification of the algorithm.
Our implementation of the algorithm considers this and tries every possible transformation option
and gathers all possible type solutions.
We skip the definition of this practice, because it is already described in \cite{TIforFGJ}
and only needed for a proof of completeness.

The \unify{} algorithm applies conversions according to the subtyping rules (depicted in figure \ref{fig:subtyping}).
At every step we try to find a reduction, which brings us closer to solved form without excluding any possible solution.
\textit{Examples:}
\begin{itemize}
\item A $\bot \lessdot \type{T}$ constraint is always satisfied and can be ignored. It will be removed by the \rulename{Bot} rule.
For the type placeholder $\tv{a}$ in the constraint $\tv{a} \lessdot \bot$ only the $\bot$ type is a possible substitution,
which is set by the \rulename{Pit} rule.
\item The \rulename{Reduce} rule represents the S-Exists type rule.
This rule uses wildcard placeholders ($\ol{\wtv{a}}$) to find a possible substitution for the wildcards on the right side.
The constraint $\type{N} \lessdot \wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N'}$ is satisfied if
there is a substitution $[\ol{T}/\ol{X}]\type{N} = \type{N'}$ with $\ol{T}$ inside the bounds $\ol{U}$ and $\ol{L}$.

For example the constraint
$\exptype{List}{\tv{a}} \lessdot \wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$ 
is converted to 
$\set{\tv{a} \doteq \wtv{x}, \wtv{x} \lessdot \type{Object}, \bot \lessdot \wtv{x} }$.
After applying \rulename{Swap} and \rulename{Subst-WC} on $\tv{a} \doteq \wtv{x}$ we get
$\set{\tv{a} \lessdot \type{Object}, \bot \lessdot \tv{a}}$ and can now apply the \rulename{Bot} rule.
This leaves us with $\set{\tv{a} \lessdot \type{Object}}$.
\item The \rulename{Erase} rule will remove redundant $\type{T} \doteq \type{T}$ constraints
\item \rulename{Equals} ensures equality of two types by ensuring they are mutual subtypes.
Constraints like $\wctype{\wildcard{X}{\tv{a}}{\tv{b}}}{List}{\rwildcard{X}} \doteq \wctype{\wildcard{Y}{\type{Object}}{\tv{String}}}{List}{\rwildcard{Y}}$
are transformed to
$\wctype{\wildcard{X}{\tv{a}}{\tv{b}}}{List}{\rwildcard{X}} \lessdot \wctype{\wildcard{Y}{\type{Object}}{\tv{String}}}{List}{\rwildcard{Y}}$
and $\wctype{\wildcard{Y}{\type{Object}}{\tv{String}}}{List}{\rwildcard{Y}} \lessdot \wctype{\wildcard{X}{\tv{a}}{\tv{b}}}{List}{\rwildcard{X}}$.
% The types $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ and $\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}$
% are equal.
\end{itemize}

We define two types as equal if they are mutual subtypes of each other.
%This relation is symmetric, reflexive and transitive by the definition of subtyping.
%This definition is sufficient for proofing soundness.
\begin{definition}{Type Equality:}\label{def:equal}
  $\Delta \vdash \type{S} = \type{T}$ if $\Delta \vdash \type{T} <: \type{S}$ and $\Delta \vdash \type{T} <: \type{S}$
\end{definition}
%This definition makes sense
% The symmetric subtyping allows this type to be substit
% We define types to be equal if they are symmetric subtypes.
% This allows the substitution of these types with eachother.
% If $\Delta \vdash \type{S} = \type{S'}$ and $\Delta \vdash \type{T} <: \type{T'}$,
% then $\Delta \vdash [\type{S}/\type{S'}]\type{T} <: \type{T'}$.


The equality relation on Capture constraints is not reflexive.
A capture constraint is never equal to another capture constraint even when structurally the same
($\type{T} \lessdotCC \type{S} \neq \type{T} \lessdotCC \type{S}$).
An implementation of the algorithm has to take this into account.
All constraints are stored in a set and there are no dublicates of subtype constraints in a constraint set.
Capture constraints however have to be stored as a list or have an unique number assigned
so that duplicates don't get automatically discarded.

% \subsection{Capture Conversion}
% % TODO: Describe Capture conversion
% Capture conversion is done during the \unify{} algorithm.
% \unify{} has to make two promises to ensure soundness of our type inference algorithm.
% Capture conversion can only be applied at capture constraints.
% Free variables are not allowed to leave their scope.
% This is ensured by type variables which are not allowed to be assigned type holding free variables.

\subsection{Algorithm}

\newcommand{\gtype}[1]{\type{#1}}
%\newcommand{\tw}[1]{\tv{#1}_?}
\begin{description}
  \item[Input:] An environment $\Delta'$
and a set of constraints $C = \set{ \type{T} \lessdot \type{T}, \type{T} \doteq \type{T} \ldots}$
and a list of constraints $C' = \set{ \type{T} \lessdotCC \type{T}}$.
The input constraints must be of the following format:

\begin{tabular}{lcll}
    $c $ &$::=$ & $\type{T} \lessdot \type{T}, \type{T} \lessdotCC \type{T}$ & Constraint \\
    $\type{T}, \type{U}, \type{L} $ & $::=$ & $\ntv{a} \mid \wtv{a} \mid \ntype{N}$ & Type variable or Wildcard Variable or Type \\
    $\ntype{N}, \ntype{S}$ & $::=$ & $\wctype{\overline{\wildcard{X}{U}{L}}}{C}{\ol{T}} $ & Class Type \\
\end{tabular}\\[0.5em]

\item[Output:]
Set of unifiers $Uni = \set{\sigma_1, \ldots, \sigma_n}$ and an environment $\Delta$
\end{description}

The \unify{} algorithm internally uses the following data types:

\begin{tabular}{lcll}
    $C $ &$::=$ &$\overline{c}$ & Constraint set \\
    $c $ &$::=$ & $\type{T} \lessdot \type{T} \mid \type{T} \lessdotCC \type{T} \mid \type{T} \doteq \type{T}$ & Constraint \\
    $\type{T}, \type{U}, \type{L} $ & $::=$ & $\tv{a} \mid \gtype{G}$ & Type placeholder or Type \\
    $\tv{a}$ & $::=$ & $\ntv{a} \mid \wtv{a}$ & Normal and wildcard type placeholder \\
    $\gtype{G}$ & $::=$ & $\type{X} \mid \ntype{N}$ & Wildcard, or Class Type \\
    $\ntype{N}, \ntype{S}$ & $::=$ & $\wctype{\triangle}{C}{\ol{T}} $ & Class Type \\
    $\triangle$ & $::=$ & $\overline{\wtype{W}}$ & Wildcard Environment \\
    $\wtype{W}$ & $::=$ & $\wildcard{X}{U}{L}$ & Wildcard \\
\end{tabular}

The $\wtv{a}$ type variables are flagged as wildcard type variables.
These type variables can be substituted by a wildcard or a type with free wildcard variables.
As long as a type variable is flagged as $\wtv{a}$ it can be used by the \rulename{Subst-WC} rule in step 1.

With \texttt{C} being class names and \texttt{A} being wildcard names.
The wildcard type $\wildcard{X}{U}{L}$ consist of an upper bound $\type{U}$, a lower bound $\type{L}$
and a name $\mathtt{X}$.

The \rulename{Tame} rule eliminates wildcards. %TODO
This is done by setting the upper and lower bound to the same value.

\unify{} applies a capture conversion everywhere it is possible (see \rulename{Capture} rule).
Capture conversion removes a types bounding environment $\Delta$.
Type variables used in its type parameters are now bound to a global scope and not locally anymore.

\begin{figure}
  \begin{center}
    \leavevmode
    \fbox{
    \begin{tabular}[t]{l@{~}l}
      \rulename{Subst} &
                       $\begin{array}[c]{l}
  \wildcardEnv \vdash C \cup \set{\ntv{a} \doteq \type{T}}\\
                         \hline
  [\type{T}/\tv{a}]\wildcardEnv \vdash [\type{T}/\tv{a}]
  C \cup \set{\ntv{a} \doteq \type{T}}
                       \end{array}
                     \quad \begin{array}{c}
                      \ntv{a} \notin \type{T} \\
                      \text{fv}(\type{T}) \subseteq \Delta', \, \text{wtv}(\type{T}) = \emptyset
                     \end{array}$\\
  \\
  \rulename{Normalize} &
                   $\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{\ntv{a} \doteq \type{T}}\\
                     \hline
[\ntv{b}/\wtv{b}]\wildcardEnv \vdash [\ntv{b}/\wtv{b}]
C \cup \set{\ntv{a} \doteq [\ntv{b}/\wtv{b}]\type{T}}
                   \end{array}
                 \quad \begin{array}{c}
                  \wtv{b} \in \text{wtv}(\type{T})\\
                  \ntv{b} \ \text{fresh}
                 \end{array}$\\
\\
\rulename{Subst-WC} &$
                 \begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{\wtv{a} \doteq \rwildcard{T}}\\
                   \hline
[\type{T}/\wtv{a}]\wildcardEnv \vdash [\type{T}/\wtv{a}]C 
                 \end{array} \quad \wtv{a} \notin \type{T}
$
\end{tabular}}
\end{center}
\caption{Substitution rules}\label{fig:subst-rules}
\end{figure}


%The capture constraints are preserved when applying the \rulename{Upper} rule.
% This is legal: a T <c S constraint indicates a let-statement can be inserted. Therefore there must exist a type T' with T <. T' <c S

\begin{figure}
  \begin{center}
    \leavevmode
    \fbox{
    \begin{tabular}[t]{l@{~}l}
    % \rulename{normalize}
    % & $
    % \begin{array}[c]{l}
    % \wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}, \wildcard{B}{U'}{L'}} \vdash C \cup \, \set{ \rwildcard{A} \doteq \rwildcard{B}  } \\ 
    % \hline
    % \vspace*{-0.4cm}\\
    % \wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}, \wildcard{B}{U'}{L'}} \vdash C \cup \, \set{ \type{L} \doteq \type{U} , \type{U} \doteq \type{U'}, \type{L} \doteq \type{L'}   }
    % \end{array}
    % $
    % \\\\
    \rulename{Upper}
    & $
    \begin{array}[c]{l}
    \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdot_1 \type{G} } \\ 
    \hline
    \vspace*{-0.4cm}\\
    \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdot_1 \type{G}   }
    \end{array}
    $
    % \quad \quad
    % \begin{array}[c]{l} %TODO: can the second part be removed by adding a X.C<X> <. C<a?> constraint at method invocation?
    % \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdotCC \type{G} } \\ 
    % \hline
    % \vspace*{-0.4cm}\\
    % \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdotCC \type{G}   }
    % \end{array}
    % $
    \\\\
    \rulename{Lower}
    & $
    \begin{array}[c]{l}
    \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \type{G} \lessdot_1 \type{A} } \\ 
    \hline
    \vspace*{-0.4cm}\\
    \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup  \set{ \type{G} \lessdot_1 \type{L} }
    \end{array}
    $
    \\\\
    \rulename{Lower}
    & $
    \begin{array}[c]{l}
    \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \ntv{a} \lessdot_1 \type{A} } \\ 
    \hline
    \vspace*{-0.4cm}\\
    \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup  \set{ \ntv{a} \lessdot_1 \type{L} }
    \end{array} \quad \type{A} \notin \Delta_{in}
    $ %TODO: a <. X with X in Delta_in => a =. X 
    % other possibliity: is it allowed to see X extends List<X> as class X extends List<X> {}
    % other way round: every class declaration comes in Delta_in
    \\\\
    \rulename{Bot}
    & $
    \begin{array}[c]{l}
    \wildcardEnv \vdash C \cup \set{ \bot \lessdot_1 \type{T} } \\ 
    \hline
    \vspace*{-0.4cm}\\
    \wildcardEnv \vdash C 
    \end{array}
    $
    \\\\
    \rulename{Pit}
    & $
    \begin{array}[c]{l}
    \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot_1 \bot } \\ 
    \hline
    \vspace*{-0.4cm}\\
    \wildcardEnv \vdash C \cup \set{ \tv{a} \doteq \bot }
    \end{array}
    $
    \\\\
\end{tabular}}
\end{center}
\caption{Wildcard reduce rules}\label{fig:wildcard-rules}
\end{figure}

\begin{figure}
  \begin{center}
    \leavevmode
    \fbox{
    \begin{tabular}[t]{l@{~}l}
% \rulename{normalize} %obsolete because of Tame
%     & $
%     \begin{array}[c]{l}
%     \wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}, \wildcard{B}{U'}{L'}} \vdash C \cup \, \set{ \rwildcard{A} \doteq \rwildcard{B}  } \\ 
%     \hline
%     \vspace*{-0.4cm}\\
%     \wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}, \wildcard{B}{U'}{L'}} \vdash C \cup \, \set{ \type{L} \doteq \type{U} , \type{U'} \doteq \type{L'}, \type{U} \doteq \type{U'}  }
%     \end{array}
%     % \quad \text{fv}(\type{U}, \type{U'}, \type{L}, \type{L'}) \subseteq \Delta_in
%     $
%     \\\\
\rulename{Tame}
    & $
    \begin{array}[c]{l}
    \wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}} \vdash C \cup \, \set{ \rwildcard{A} \doteq \type{T}  } \\ 
    \hline
    \vspace*{-0.4cm}\\
    \wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}} \vdash C \cup \, \set{ \type{L} \doteq \type{T}, \type{U} \doteq \type{T} }
    \end{array} %\quad \text{fv}(\type{U}, \type{L}) \subseteq \Delta_in
      \quad \type{T} \ \text{is no wildcard placeholder}
    $
    \\\\
\rulename{Equals} %TODO
    & $
    \begin{array}[c]{l}
        \wildcardEnv \vdash C \cup \, \set{ \wcNtype{\Delta}{N} \doteq \wcNtype{\Delta'}{N'} } \\ 
        \hline
        \vspace*{-0.4cm}\\
        \wildcardEnv \vdash C \cup \, 
        \set{
          \wcNtype{\Delta}{N} \lessdot \wcNtype{\Delta'}{N'}, \wcNtype{\Delta'}{N'} \lessdot \wcNtype{\Delta}{N}
        }
    \end{array} %\quad |\Delta| = |\Delta'|
    % \quad \text{fv}(\type{N}) = \text{fv}(\type{N'}) = \emptyset 
    $
     \\\\
%  \rulename{Equals} %TODO
% & $
% \begin{array}[c]{l}
%     \wildcardEnv \vdash C \cup \, \set{ \wctype{\Delta}{C}{\ol{T}} \doteq \wctype{\Delta}{C}{\ol{T'}} } \\ 
%     \hline
%     \vspace*{-0.4cm}\\
%     \wildcardEnv \vdash C \cup \, 
%     \set{
%       \pi(\ol{T}) \doteq  \pi(\ol{T'} )
%       %\ol{T} \doteq \ol{T'}
%     }
% \end{array}
% \quad \begin{array}{l}
% \text{given a permutation}\ \pi\ \text{with:}\\
% \pi(\Delta) = \pi(\Delta')
% \end{array}
%    $
%    \\\\
    \rulename{Erase}
    & $
    \begin{array}[c]{l}
        \wildcardEnv \vdash C \cup \, \set{ \type{T} \doteq \type{T} } \\ 
        \hline
        \vspace*{-0.4cm}\\
        \wildcardEnv \vdash C
    \end{array}
    $
    \\\\
    \rulename{Erase}
    & $
    \begin{array}[c]{l}
        \wildcardEnv \vdash C \cup \, \set{ \type{T} \lessdot \type{T} } \\ 
        \hline
        \vspace*{-0.4cm}\\
        \wildcardEnv \vdash C 
    \end{array}
    $
    \\\\ 
    \rulename{Swap} & $
        \begin{array}[c]{l}
        \wildcardEnv \vdash C \cup \set{\type{G} \doteq \tv{a}}\\
        \hline
        \wildcardEnv \vdash C \cup \set{\tv{a} \doteq \type{G}}
        \end{array}
 \quad
        \begin{array}[c]{l}
        \wildcardEnv \vdash C \cup \set{\type{T} \doteq \wtv{a}}\\
        \hline
        \wildcardEnv \vdash C \cup \set{\wtv{a} \doteq \type{T}}
        \end{array} \quad
        \begin{array}[c]{l}
        \wildcardEnv \vdash C \cup \set{\type{N} \doteq \rwildcard{A}}\\
        \hline
        \wildcardEnv \vdash C \cup \set{\rwildcard{A} \doteq \type{N}}
        \end{array} \quad
        \begin{array}[c]{l}
        \wildcardEnv \vdash C \cup \set{\ntv{a} \doteq \rwildcard{A}}\\
        \hline
        \wildcardEnv \vdash C \cup \set{\rwildcard{A} \doteq \ntv{a}}
        \end{array}$
\end{tabular}}
\end{center}
\caption{Constraint normalize rules}\label{fig:normalizing-rules}
\end{figure}

The \rulename{match} rule generates fresh wildcards $\overline{\wildcard{A}{\tv{u}}{\tv{l}}}$.
Their upper and lower bounds are fresh type variables.


\begin{figure}
  \begin{center}
      \leavevmode
      \fbox{
      \begin{tabular}[t]{l@{~}l}
        \rulename{Circle} & $
        \begin{array}[c]{l}
          \wildcardEnv \vdash C \cup \, \set{\tv{a}_1 \lessdot
          \tv{a}_2, \tv{a}_2 \lessdot \tv{a}_3, \dots, \tv{a}_n \lessdot \tv{a}_1}\\
          \hline
          \wildcardEnv \vdash C \cup \, \set{\tv{a}_1 \doteq \tv{a}_2, \tv{a}_2 \doteq \tv{a}_3, \dots , \tv{a}_n \doteq \tv{a}_1} 
        \end{array} \quad n>0
              $
      \end{tabular}}
  \end{center}
    \caption{Rules for normal placeholders}\label{fig:reduce-rules}
\end{figure}

\begin{figure}
    \begin{center}
        \leavevmode
        \fbox{
        \begin{tabular}[t]{l@{~}l}
          \rulename{Match} 
          & $
          \begin{array}[c]{@{}ll}
          \begin{array}[c]{l}
             \wildcardEnv \vdash C \cup \, \set{
                \tv{a} \lessdot_1 \wctype{\Delta}{D}{\ol{T}}, \tv{a} \lessdot_2 \wctype{\Delta'}{D'}{\ol{T'}} }\\ 
            \hline
            \vspace*{-0.4cm}\\
\wildcardEnv \vdash C \cup \, \left\{ \begin{array}[c]{l}
                \tv{a} \lessdot \wctype{\overline{\wildcard{A}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{A}}},
              \ol{\tv{l}} \lessdot \ol{\tv{u}}, \\
            \wctype{\overline{\wildcard{A}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{A}}}
                     \lessdot_1 \wctype{\Delta}{D}{\ol{T}}, \\
            \wctype{\overline{\wildcard{A}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{A}}}
                     \lessdot_2 \wctype{\Delta'}{D'}{\ol{T'}}
\end{array}
\right\}
          \end{array}
          &\begin{array}[c]{l}
            \text{fresh}\ \overline{\wildcard{A}{\tv{u}}{\tv{l}}} \\
            \type{C} \ll \type{D}\\
            \type{C} \ll \type{D'} % TODO: THe match rule has to pick the most general type for C
         \end{array}
          \end{array}
          $
        \\\\ 
        \ruleReduceWC{}
        & 
        $
        \begin{array}[c]{@{}ll}
        \begin{array}[c]{l}
            \wildcardEnv \vdash 
            C \cup \, \set{ \exptype{C}{\ol{S}} \lessdot
            \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}} } \\ 
          \hline
          \vspace*{-0.4cm}\\
          \wildcardEnv
           \vdash C \cup \, \set{ 
           \ol{\type{S}} \doteq [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{\type{T}},
          \ol{\wtv{a}} \lessdot [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{U}, [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{L} \lessdot \ol{\wtv{a}} }
        \end{array}
         %\quad \ol{Y} = \textit{fresh}(\ol{X})
         \quad \begin{array}[c]{l}
          \ol{\wtv{a}} \ \text{fresh}\\
          %\text{fv}(\exptype{C}{\ol{S}}) \subseteq \text{dom}(\overline{\wildcard{B}{\type{U'}}{\type{L'}}})
          %\text{dom}(\overline{\wildcard{A}{\type{U}}{\type{L}}}) \subseteq \text{fv}(\exptype{C}{\ol{T}}) \\
          %\text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset
          \end{array}
        \end{array}
        $
      \\\\
      \rulename{Capture}
      & 
      $
      \begin{array}[c]{@{}ll}
      \begin{array}[c]{l}
          \wildcardEnv \vdash 
          C \cup \, \set{ \wctype{\overline{\wildcard{B}{\type{U}}{\type{L}}}}{C}{\ol{S}} \lessdotCC \type{T} } \\ 
        \hline
        \vspace*{-0.4cm}\\
        \wildcardEnv \cup \overline{\wildcard{C}{\type{U}}{\type{L}}}
         \vdash C \cup \, \set{  
          [\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}} \lessdot \type{T} }
      \end{array}
       %\quad \ol{Y} = \textit{fresh}(\ol{X})
       \quad \begin{array}[c]{l}
        \ol{\rwildcard{C}} \ \text{fresh}\\
        %\text{fv}(\type{T}) \neq \emptyset
        \end{array}
      \end{array}
      $
    \\\\
      \rulename{Prepare} %The lessdotCC constraint only ensures that the left side looses its wildcardEnvironment.
      %It does not ensure that the left side doesn't contain free variables. If you want to ensure that you have to give the left side a normal placeholder
      & 
      $
      \begin{array}[c]{@{}ll}
      \begin{array}[c]{l}
          \wildcardEnv \vdash 
          C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \wctype{\Delta'}{C}{\ol{T}} } \\ 
        \hline
        \vspace*{-0.4cm}\\
          \wildcardEnv \vdash 
          C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdotCC \wctype{\Delta'}{C}{\ol{T}} } \\ 
      \end{array}
       %\quad \ol{Y} = \textit{fresh}(\ol{X})
       \quad \begin{array}[c]{l}
        \text{fv}(\wctype{\Delta'}{C}{\ol{T}}) \subseteq \Delta_{in}
        \end{array}
      \end{array}
      $
    \\\\
    \rulename{Trim}
    & 
    $
    \begin{array}[c]{@{}ll}
    \begin{array}[c]{l}
        \wildcardEnv \vdash 
        C \cup \, \set{ \wctype{\Delta,\Delta'}{C}{\ol{S}} \lessdot \type{T} } \\ 
      \hline
      \vspace*{-0.4cm}\\
        \wildcardEnv \vdash 
        C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T} } \\  
    \end{array}
     %\quad \ol{Y} = \textit{fresh}(\ol{X})
     \quad \begin{array}[c]{l}
      \text{fv}(\ol{S}) \cap \Delta' = \emptyset
      \end{array}
    \end{array}
    $
  \\\\
  \rulename{Clear}
  & 
  $
  \begin{array}[c]{@{}ll}
  \begin{array}[c]{l}
      \wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}} \vdash 
      C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T} } \\ 
    \hline
    \vspace*{-0.4cm}\\
    \subst{\type{U}}{\rwildcard{A}}\wildcardEnv \vdash 
      [\type{U}/\rwildcard{A}]C \cup \, [\type{U}/\rwildcard{A}]\set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T}, \type{U} \doteq \type{L} } \\  
  \end{array}
   %\quad \ol{Y} = \textit{fresh}(\ol{X})
   \quad \begin{array}[c]{l}
    \Delta \neq \emptyset\\
    \rwildcard{A} \in \text{fv}(\type{T})
    \end{array}
  \end{array}
  $
\\\\
\rulename{Exclude}
& 
$
\begin{array}[c]{@{}ll}
\begin{array}[c]{l}
    \wildcardEnv \vdash 
    C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T} } \\ 
  \hline
  \vspace*{-0.4cm}\\
  \subst{\tv{a}}{\wtv{a}}\wildcardEnv \vdash 
    [\tv{a}/\wtv{a}]C \cup \, [\tv{a}/\wtv{a}]\set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T}, \type{U} \doteq \type{L} } \\  
\end{array}
 %\quad \ol{Y} = \textit{fresh}(\ol{X})
 \quad \begin{array}[c]{l}
  \Delta \neq \emptyset\\
  \wtv{a} \in \text{fv}(\type{T}), \tv{a} \ \text{fresh}
  \end{array}
\end{array}
$
\\\\
        \rulename{Adopt}
        & $
        \begin{array}[c]{@{}ll}
        \begin{array}[c]{l}
          \wildcardEnv \vdash C \cup \, \set{
           \tv{b} \lessdot_1 \tv{a},
\tv{a} \lessdot_2 \type{N}, \tv{b} \lessdot_3 \type{N'}} \\ 
          \hline
          \vspace*{-0.4cm}\\
          \wildcardEnv \vdash C \cup \, \set{
 \tv{b} \lessdot \type{N},
           \tv{b} \lessdot_1 \tv{a},
\tv{a} \lessdot_2 \type{N} , \tv{b} \lessdot_3 \type{N'}
           }
        \end{array}
        \end{array}
        $
      \\\\
  \rulename{Adapt}
  & 
  $
  \begin{array}[c]{@{}ll}
  \begin{array}[c]{l}
    \wildcardEnv \vdash C \cup \, \set{ \wctype{\Delta}{C}{\ol{T}} \lessdot
       \wctype{\Delta'}{D'}{\ol{T'}} } \\ 
  \hline
  \vspace*{-0.4cm}\\
  \wildcardEnv \vdash C \cup \, \set{ \wctype{\Delta}{D}{[\ol{\type{T}}/\ol{X}]\ol{S}} \lessdot \wctype{\Delta'}{D'}{\ol{T'}} }
  
  \end{array}
  & \begin{array}[c]{l}
  \type{C} \ll \type{D'} \\
   \texttt{class} \ \exptype{C}{\ol{X} \triangleleft \ol{N}} \triangleleft \exptype{D}{\ol{S}} 
  \end{array}
  \end{array}
  $
    \end{tabular}}
  \end{center}
\caption{Constraint reduce rules}\label{fig:reduce-rules}
\end{figure}

Capture constraints are treated like regular subtype constraints.
All transformations for subtype constraints work for capture constraints aswell.
For clarification Subtype constraints are marked with a number.
Subtype constraints holding the same number keep their respective type.
Newly created subtype constraints are always regular subtype constrains unless stated otherwise.
The \rulename{Adopt} rule for example takes multiple subtype constraints and adds a new one.
Having the constraints
$\ntv{a} \lessdotCC \wtv{b}, \ntv{a} \lessdot \type{String}, \wtv{b} \lessdot \type{Object}$
would lead to
$\wtv{b} \lessdot \type{String}, \ntv{a} \lessdotCC \wtv{b}, \ntv{a} \lessdot \type{String}, \wtv{b} \lessdotCC \type{Object}$
after applying \rulename{Adopt}.
The new generated constraint $\wtv{b} \lessdot \type{String}$ is a normal subtype constraint.
The type placeholders which are annotated as wildcard placeholders also stay wildcard placeholders.
The only rule that replaces wildcard type placeholders with regular placeholders is the \rulename{Normalize} rule.

The algorithm holds two sets.
The input constraints and a wildcard environment $\wildcardEnv{}$ keeping free variables.
The algorithm starts with an empty wildcard environment $\wildcardEnv{}$.
Only the \rulename{Capture} rule adds wildcards to that environment.
And every added wildcard gets a fresh unique name.
This ensures the wildcard environment $\wildcardEnv{}$ never
gets the same wildcard twice.


\textbf{Step 1:}
Apply the rules depicted in the figures \ref{fig:normalizing-rules}, \ref{fig:reduce-rules} and \ref{fig:wildcard-rules} exhaustively.
Starting with the \rulename{circle} rule. Afterwards the other rules in figure \ref{fig:normalizing-rules}.

\begin{figure}
If we find an illicit constraint assigning a type containing free variables to a type placeholder not flagged as a wildcard placeholder the algorithm fails. 

$\set{\tv{a} \doteq \type{N}} \in C$ with $\text{fv}(\type{N}) \cap \Delta_{in} \neq \emptyset$ $\implies$ fail! 

% if T <. S with not T << S
% T <. S with fv(T) cup fv(S) not empty (free variables in a non capture conversion constraint)

\caption{Fail conditions}
\end{figure}

The first step of the algorithm is able to remove wildcards.
Removing a wildcard works by setting its lower and upper bound to be equal.
(Def: $\type{Object} = \wildcard{A}{Object}{Object}$).
The \rulename{Equals} rule is responsible for this.

The subtype constraints are a subset of the capture constraints $(\type{T} \lessdot \type{S}) \implies (\type{T} \lessdotCC \type{S})$.
Every transformation on a subtype constraint can also be applied to a capture constraint, but the capture constraints need to be preserved.
We indicate this by numbering the constraints in each transformation.
Constraints with the same number stay the same type.

\textbf{Example:}
\begin{displaymath}
  \begin{array}[c]{@{}ll}
    \begin{array}[c]{l}
        \wildcardEnv \cup \set{ \wildcard{X}{\tv{u}}{\tv{l}} } \vdash
        C \cup \, \set{ \type{Object} \doteq \type{X}, \tv{l} \lessdot \tv{u} } \\ 
        \hline
        \vspace*{-0.4cm}\\
        \wildcardEnv \cup \set{ \wildcard{X}{\tv{u}}{\tv{l}} } \vdash C \cup \, 
        \set{\type{Object} \lessdot \type{X}, \type{X} \lessdot \type{Object}, \tv{l} \lessdot \tv{u}
        }\\ 
        \hline
        \vspace*{-0.4cm}\\
        \wildcardEnv \cup \set{ \wildcard{X}{\tv{u}}{\tv{l}} } \vdash C \cup \, 
        \set{\type{Object} \lessdot \tv{l}, \tv{u} \lessdot \type{Object}, \tv{l} \lessdot \tv{u}
        }\\ 
        \hline
        \vspace*{-0.4cm}\\
        \ldots\\ 
        \hline
        \vspace*{-0.4cm}\\
        \wildcardEnv \cup \set{ \wildcard{X}{\type{Object}}{\type{Object}} } \vdash C \\ 
    \end{array} 
    \end{array}
\end{displaymath}

\textbf{Helper functions:}
\begin{description}
\item[$\tph{}$] returns all type placeholders inside a given type.

\textit{Example:} $\tph(\wctype{\wildcard{X}{\tv{a}}{\bot}}{Pair}{\wtv{b},\rwildcard{X}}) = \set{\tv{a}, \wtv{b}}$
\item [$\ll$ relation:]
The $\ll$ relation is the reflexive and transitive closure of the \texttt{extends} relations:
\begin{displaymath}
  \begin{array}[c]{c}
\exptype{C}{\ol{X} \triangleleft \ol{N}} \triangleleft \exptype{D}{\ol{N}} \\ 
\hline
\vspace*{-0.4cm}\\
\texttt{C} \ll \texttt{D}
\end{array}
\quad
\begin{array}[c]{l}
  \\
\hline
\vspace*{-0.4cm}\\
\texttt{C} \ll \texttt{C}
\end{array}
\quad
\begin{array}[c]{l}
\texttt{C} \ll \texttt{D}, \texttt{D} \ll \texttt{E} \\ 
\hline
\vspace*{-0.4cm}\\
\texttt{C} \ll \texttt{E}
\end{array}
\end{displaymath}
The algorithm uses it to determine if two types are possible subtypes of one another.
This is needed in the \rulename{adapt} and \rulename{match} rules.

%\textbf{Wildcard renaming}\\
\item[Wildcard renaming:]
The \rulename{reduce} rule separates wildcards from their environment.
At this point each wildcard gets a new and unique name.
To only rename the respective wildcards the reduce rule renames wildcards up to alpha conversion:
($[\ol{C}/\ol{B}]$ in the \rulename{reduce} rule)
\begin{align*}
  [\type{A}/\type{B}]\type{B} &= \type{A} \\
  [\type{A}/\type{B}]\type{C} &= \type{C} & \text{if}\ \type{B} \neq \type{C}\\
  [\type{A}/\type{B}]\wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N} &= \wcNtype{\overline{\wildcard{X}{[\type{A}/\type{B}]\type{U}}{[\type{A}/\type{B}]\type{L}}}}{[\type{A}/\type{B}]N} & \text{if}\ \type{B} \notin \overline{\rwildcard{X}} \\
  [\type{A}/\type{B}]\wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N} &= \wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N} & \text{if}\ \type{B} \in \overline{\rwildcard{X}} \\
\end{align*}
\item[Free Variables:]
The $\text{fv}$ function assumes every wildcard type variable to be a free variable aswell.

%\textbf{Fresh Wildcards}\\
\item[Fresh Wildcards:]
$\text{fresh}\ \overline{\wildcard{A}{\tv{u}}{\tv{l}}}$ generates fresh wildcards.
The new names $\ol{A}$ are fresh, aswell as the type variables $\ol{\tv{u}}$ and $\ol{\tv{l}}$,
which are used for the upper and lower bounds.
\end{description}
% \noindent
% \textbf{Example: (reduce-rule)}
% %The \ruleReduceWC{} resembles the \texttt{S-Exists} subtyping rule.
% %It converts wildcard types to fresh type variables.
% %For example take the input constraint $\exptype{Pair}{\ntype{Object},\tv{b}} \lessdot \wctype{\wildcard{A}{\tv{c}}{\tv{d}}}{Pair}{\wildcard{A}{\tv{c}}{\tv{d}},\wildcard{A}{\tv{c}}{\tv{d}}}$.
% %First we apply the \ruleReduceWC{} rule, which replaces $\wildcard{A}{\tv{c}}{\tv{d}}$ with a fresh type variable $\tv{a}$:
% We assume the input constraints $C = \exptype{Pair}{\ntype{Object},\tv{b}} \lessdot \wctype{\wildcard{A}{\tv{c}}{\tv{d}}}{Pair}{\wildcard{A}{\tv{c}}{\tv{d}},\wildcard{A}{\tv{c}}{\tv{d}}}$.
% The type on the right side $\wctype{\wildcard{A}{\tv{c}}{\tv{d}}}{Pair}{\wildcard{A}{\tv{c}}{\tv{d}},\wildcard{A}{\tv{c}}{\tv{d}}}$
% \begin{align*}
%   \ddfrac{
%       \exptype{Pair}{\ntype{Object},\tv{b}} \lessdot \wctype{\wildcard{A}{\tv{c}}{\tv{d}}}{Pair}{\wildcard{A}{\tv{c}}{\tv{d}},\wildcard{A}{\tv{c}}{\tv{d}}}
%   }{
%       \ntype{Object} \doteq \tv{a}, \tv{b} \doteq \tv{a}, \tv{a} \lessdot \tv{c}, \tv{d} \lessdot \tv{a}
%   } \ruleReduceWC{}
% \end{align*}

% By substition we get the result: % $\tv{a} \doteq \type{Object}$, $\tv{a} \doteq \type{Object}$, $\ldots$.

% \begin{align*}
%   \ddfrac{
%       \ntype{Object} \doteq \tv{a}, \tv{b} \doteq \tv{a}, \tv{a} \lessdot \tv{c}, \tv{d} \lessdot \tv{a}
%   }{
%         \tv{a} \doteq \ntype{Object} , \tv{b} \doteq \ntype{Object}, \ntype{Object} \lessdot \tv{c}, \tv{d} \lessdot \ntype{Object}
%   } \rulename{Subst}
% \end{align*}
% \\[1em]

\noindent
\textbf{Step 2:}
%If there are no $(\type{T} \lessdot \tv{a})$ constraints remaining in the constraint set $C$
%resume with step 4.

The rules in figure \ref{fig:step2-rules} offer multiple possibilities to deal with constraints of the form $\type{N} \lessdot \tv{a}$.
This builds a search tree over multiple possible solutions.
\unify{} has to try each branch and accumulate the resulting solutions into a solution set.
\def\boxit#1#2{%
    \smash{\color{red}\fboxrule=1pt\relax\fboxsep=2pt\relax%
    \llap{\rlap{\fbox{\phantom{\rule{#1}{#2}}}}~}}\ignorespaces
}
\begin{figure}
  \begin{center}
          \fbox{
          \begin{tabular}[t]{l@{~}l}
            \rulename{SameW}
            & $
            \begin{array}[c]{l}
              \wildcardEnv \vdash
              C \cup \type{G} \lessdot \wtv{a}\\
              \hline
              \wildcardEnv \vdash
              C \cup \set{
                \wtv{a} \doteq \type{G}
            }
            \end{array}
              $
          \\\\
          \cdashline{1-2} \\
          \rulename{Same}
          & $
          \begin{array}[c]{l}
            \wildcardEnv \cup \set{\overline{\wildcard{A}{\type{U}}{\type{L}}}} \vdash
            C \cup \wctype{\Delta'}{C}{\ol{X}} \lessdot \ntv{a}\\
            \hline
            \wildcardEnv \cup \set{\overline{\wildcard{A}{\type{U}}{\type{L}}}} \vdash
            C \cup \set{
              \ntv{a} \doteq \wctype{\Delta',\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{X}}
          }
          \end{array} \quad \begin{array}[c]{l}
            \text{fv}(\wctype{\Delta'}{C}{\ol{X}}) / \Delta_{in} = \overline{\rwildcard{A}}
          \end{array}
            $
        \\\\
        \cdashline{1-2} \\
            \rulename{\generalizeRule}
            & $
            \begin{array}[c]{l}
              \wildcardEnv \vdash C \cup \wctype{\Delta}{C}{\ol{T}} \lessdot \ntv{a}\\
              \hline
              \wildcardEnv \vdash C \cup \set{\wctype{\Delta}{C}{\ol{T}} \lessdot \ntv{a},
            \ntv{a} \doteq \wctype{\overline{\wildcard{X}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{X}}},
            %\overline{\tv{l} \lessdot \tv{u}}, % not needed, due to subst and reduce rule which are used afterwards
            \overline{\tv{u} \lessdot \type{S}}
            }
            \end{array} \quad \begin{array}[c]{l}
              \texttt{class} \ \exptype{C}{\ol{X \triangleleft \type{S}}} \triangleleft \exptype{D}{\ol{N}} \\
              \text{fresh}\ \overline{\wildcard{X}{\tv{u}}{\tv{l}}}
            \end{array}
              $ 
              \\\\
              \cdashline{1-2} \\
          \rulename{Super}
          & $
          \begin{array}[c]{l}
            \wildcardEnv \vdash C \cup \wctype{\Delta}{C}{\ol{T}} \lessdot \tv{a}\\
            \hline
            \wildcardEnv \vdash C \cup \set{ \wctype{\Delta'}{D}{[\ol{T}/\ol{X}]\ol{N}} \lessdot \tv{a}   }
          %\set{\wctype{\ol{\wtype{W}}}{D}{[\ol{X}/\ol{Y}]\ol{Z}} \lessdot \tv{a}}
          \end{array} \quad
          \begin{array}{l}
            \texttt{class} \ \exptype{C}{\ol{X}} \triangleleft \exptype{D}{\ol{N}} \\
            \ol{X} \notin \wildcardEnv \cup \Delta,\, \Delta' = \Delta \cap \text{fv}([\ol{T}/\ol{X}]\ol{N})
          \end{array}
          $
              % \\\\
              % \hline \\
              % \rulename{SameW}
              % & $
              % \begin{array}[c]{l}
              %   \wildcardEnv \vdash
              %   C \cup \type{G} \lessdot \wtv{a}\\
              %   \hline
              %   \wildcardEnv \vdash
              %   C \cup \set{
              %     \wtv{a} \doteq \type{G}
              % }
              % \end{array}
              %   $
            \\\\
            \cdashline{1-2} \\
                \rulename{\generalizeRule{}W}
                & $
                \begin{array}[c]{l}
                  \wildcardEnv \vdash C \cup \wctype{\Delta}{C}{\ol{T}} \lessdot \wtv{a}\\
                  \hline
                  \wildcardEnv \vdash C \cup \set{\wctype{\Delta}{C}{\ol{T}} \lessdot \wtv{a},
                \wtv{a} \doteq \wctype{\overline{\wildcard{X}{\wtv{u}}{\wtv{l}}}}{C}{\overline{\rwildcard{X}}},
                %\overline{\tv{l} \lessdot \tv{u}}, % not needed, due to subst and reduce rule which are used afterwards
                \overline{\wtv{u} \lessdot \type{S}}
                }
                \end{array} \quad \begin{array}[c]{l}
                  \texttt{class} \ \exptype{C}{\ol{X \triangleleft \type{S}}} \triangleleft \exptype{D}{\ol{N}} \\
                  \text{fresh}\ \overline{\wildcard{X}{\wtv{u}}{\wtv{l}}}
                \end{array}
                  $
      \end{tabular}
      }
          \end{center}
        \caption{Step 2 branching: Multiple rules can be applied to the same constraint}
        \label{fig:step2-rules}
        \end{figure}

        \begin{figure}
          \begin{center}
\fbox{
      \begin{tabular}[t]{l@{~}l}
        \rulename{Subst-X}
        & $
        \begin{array}[c]{l}
          \wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash
          C \cup \rwildcard{X} \lessdot \tv{a}\\
          \hline
          \wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash
          C \cup \set{
            \tv{a} \doteq \rwildcard{X}
        }
        \end{array} \quad \begin{array}[c]{l}
          \rwildcard{X} \in \Delta_{in}
        \end{array}
          $
          \\\\
          \cdashline{1-2} \\
      \rulename{Gen-X}
      & $
      \begin{array}[c]{l}
        \wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash
        C \cup \rwildcard{X} \lessdot \tv{a}\\
        \hline
        \wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash
        C \cup \set{
          \type{U} \lessdot \tv{a}
      }
      \end{array}
        $
    \end{tabular}
    }
        \end{center}
      \caption{Step 2 branching: Multiple rules can be applied to the same constraint}
      \label{fig:step2-rules}
      \end{figure}

      $\type{T} \lessdot \ntv{a}$ constraints have three and $\type{T} \lessdot \wtv{a}$ constraints have five possible transformations.
      
      \begin{figure}
        \begin{center}
\fbox{
      \begin{tabular}[t]{l@{~}l}
        \rulename{Settle}
        & $
        \begin{array}[c]{l}
          \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N},
          \tv{a} \lessdot_1 \tv{b}}
          \\
          \hline
          \wildcardEnv \vdash C \cup \set{  \tv{a} \lessdot_1 \tv{b}, \tv{b} \lessdot \type{N}  }
        \end{array}
        $
        \\\\
        \cdashline{1-2} \\
      \rulename{Raise}
      & $
      \begin{array}[c]{l}
        \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot_1 \type{N},
        \tv{a} \lessdot \tv{b}}
        \\
        \hline
        \wildcardEnv \vdash C \cup \set{\tv{a} \lessdot_1 \type{N}, \type{N} \lessdot \tv{b}  }
      \end{array}
      $
    \end{tabular}
}
    \end{center}
  \caption{Step 2 branching: Multiple rules can be applied to the same constraint}
  \label{fig:step2-rules}
  \end{figure}

\unify{} generates wildcard types for constraints of the form $\type{N} \lessdot \tv{a}$ with the \rulename{\generalizeRule} rule.
Otherwise only the wildcards already defined in the input constraints will be included in the result.
\rulename{\generalizeRule} attempts to give $\tv{a}$ a more general type by replacing only the type parameters with fresh wildcards.
The second variation sets $\tv{a}$ to the direct supertype of type \texttt{C}.
For the constraint $\texttt{Object} \lessdot \tv{a}$ the algorithm can only apply $\tv{a} \doteq \texttt{Object}$,
because \texttt{Object} has no other supertype than itself.

Constraints of the form $\set{ \tv{a} \lessdot \type{N}, \tv{a} \lessdot^* \tv{b}}$
need to be handled in a similiar fashion.
The type variable $\tv{b}$ could either be a sub or a supertype of the type $\type{N}$.
We have to consider both possibilities.
\\[1em]

\noindent
\textbf{Step 3:}
We apply the rules in figure \ref{fig:cleanup-rules} exhaustively and proceed with step 4.

\begin{figure}
  \begin{center}
      \leavevmode
      \fbox{
      \begin{tabular}[t]{l@{~}l}
\rulename{SubElim} 
& $\begin{array}[c]{l}
  \wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \tv{b}}\\
  \hline
  [\tv{a}/\tv{b}]\wildcardEnv \vdash [\tv{a}/\tv{b}]C \cup \set{ \tv{b} \doteq \tv{a} }
\end{array}
$
\\\\
\rulename{Ground}
& $\begin{array}[c]{@{}ll}
\begin{array}[c]{l}
 \wildcardEnv \cup \overline{\set{\wildcard{X}{\type{U}}{\tv{a}}}} \vdash C \cup \, \set{
    \overline{\tv{a} \lessdot \type{T}} } \\ 
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \cup \overline{\set{\wildcard{X}{\type{U}}{\bot}}} \vdash
C \cup \set{ \tv{a} \doteq \bot }
\end{array}
&\begin{array}[c]{l}
%\forall \wctype{\Delta}{C}{\ol{T}} \in C: \tv{a} \notin \ol{T} \\
\tv{a} \notin C, \, \rwildcard{X} \notin C, \, \tv{a} \notin \overline{T} %\\
%\text{length}( \overline{\tv{a} \lessdot \type{T}} ) > 1
\end{array}
\end{array}$
  \end{tabular}}
\end{center}
\caption{Cleanup rules}\label{fig:cleanup-rules}
\end{figure}

The cleanup step prepares the constraint set for the last step by applying the following concepts:
%Two transformations are done which also help to remove unnecessary types from the solution set.
\begin{description}
\item[Bottom type]
The bottom type $\bot$ is used to generate \texttt{? extends} wildcard definitions.
This is the only possible solution when dealing with multiple upper bounds:
$\tv{a} \lessdot \type{T}, \tv{a} \lessdot \type{S}$ is usually not a correct solution (given $\type{S}$ and $\type{T}$ are no subtypes of eachother).
But if $\tv{a}$ is a lower bound of a wildcard it can be set to $\bot$.
Those constraints only stay in the constraint set after the first step if $\type{S}$ and $\type{T}$ do not have a common subtype.
The \rulename{Ground} rule uses this concept to generate \texttt{extends} Wildcards.

\item[Eliminating Wildcards]
Wildcards that have the same upper and lower bounds can be removed.
This is done by the \rulename{Crunch} rule.

\textit{Example:} The type $\wctype{\wildcard{X}{\type{String}}{\type{String}}}{List}{\rwildcard{X}}$
becomes $\exptype{List}{\type{String}}$.


%TODO: The a =. T (with T containing free variables) could be removed here.
% Not needed for the soundness of the algorithm, but handy for the implementation (check this when implementing the algorithm)
\end{description}

\noindent
\textbf{Step 6 (Generating Result):}
Apply the rules in figure \ref{fig:generation-rules} until $\wildcardEnv = \emptyset$ and $C = \emptyset$.
The resulting $\Delta, \sigma$ is a correct solution.

For this step to succeed there should only be four kinds of constraints left.
\begin{enumerate}
%\item\label{item:3} $\tv{a} \lessdot \tv{b}$ %, with $a$ and $b$ both isolated type variables
\item $\tv{a} \doteq \tv{b}$
%\item $\wtv{a} \doteq \type{G}$
\item\label{item:1} $\tv{a} \lessdot \wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}$, with $\text{fv}(\wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}) \subseteq \Delta_in$
\item\label{item:2} $\tv{a} \doteq \wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}$, with $\tv{a} \notin \ol{\type{T}}$ % and $\text{fv}(\wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}) = \emptyset$
\item\label{item:3} $\tv{a} \doteq \rwildcard{X}$
\end{enumerate}
% Constraints of the form $\tv{a} \doteq \rwildcard{X}$ are also possible.
% should we add those to the \Delta environment?
% How about removing them completely from the result set? Check with soundness condition

%Each type placeholder $\tv{a}$ must solely appear on the left side of a constraint.
\unify{} fails if there is any $\tv{a} \doteq \type{T}$ such that $\tv{a}$ occurs in $\type{T}$.
For the cases \ref{item:1}, \ref{item:2}, and \ref{item:3} the placeholder $\tv{a}$
cannot appear anywhere else in the constraint set.
Otherwise the generation rules \rulename{GenSigma} and \rulename{GenDelta} will not be able to process every constraint.

% After applying the GenDelta and GenSigma rules unifiers $\sigma$ do not contain
% a unifier of the form $\tv{a} \to \tv{b}$.
% Otherwise the found solution is incorrect.
% This only happens if the input constraints contain type variables with no upper bound constraint like $\tv{a} \lessdot \type{N}$.

% \begin{displaymath}
% \deduction{
% \wildcardEnv \cup \set{\wildcard{B}{\type{G}}{\type{G'}}} \vdash C \implies \Delta, \sigma
% }{
% \wildcardEnv \vdash C \implies \Delta \cup \set{\wildcard{B}{\type{G}}{\type{G'}}}, \sigma
% }\quad \text{tph}(\type{G}) = \emptyset, \text{tph}(\type{G'}) = \emptyset,
% \rwildcard{B} \notin \text{dom}(\Delta)
% \quad \rulename{AddDelta}
% \end{displaymath}

\dashbox{The \text{tph} function returns all type placeholders inside a given type.}

\begin{figure}
\begin{center}
        \fbox{
        \begin{tabular}[t]{l@{~}l}
          \rulename{GenDelta}
          & $
          \deduction{
            \wildcardEnv \vdash C \cup \set{\ntv{b} \lessdot \type{T} } \implies \Delta, \sigma
            }{
            \wildcardEnv \vdash [\type{B}/\ntv{b}]C \implies \Delta \cup \set{\wildcard{B}{\type{T}}{\bot}}, \sigma \cup \set{\ntv{b} \to \type{B}}
            } \quad
            \begin{array}{l}
            \tph(\type{T}) = \emptyset, \text{fv}(\type{T}) \subseteq \Delta \cup \Delta_{in} \\
            \rwildcard{B} \ \text{fresh}, \ntv{b} \notin \text{dom}(\sigma), \Delta, \Delta_{in} \vdash \type{T} \ \ok
            \end{array}
          $
        \\\\ 
        \rulename{GenDelta'}
        & $
        \deduction{
          \wildcardEnv \vdash C \cup \set{\wtv{b} \lessdot \type{T} } \implies \Delta, \sigma
          }{
          \wildcardEnv \vdash [\type{B}/\ntv{b}]C \implies \Delta \cup \set{\wildcard{B}{\type{T}}{\bot}}, \sigma
          } \quad
          \begin{array}{l}
          \tph(\type{T}) = \emptyset, \text{fv}(\type{T}) \subseteq \Delta \cup \Delta_{in} \\
          \rwildcard{B} \ \text{fresh}, \Delta, \Delta_{in} \vdash \type{T} \ \ok
          \end{array}
        $
      \\\\ 
      \rulename{GenSigma}
      & $
      \deduction{
      \wildcardEnv \vdash C \cup
      \set{\ntv{a} \doteq \type{T} }  \implies \Delta, \sigma
      }{
      \wildcardEnv \vdash C   \implies \Delta,  \sigma \cup
      \set{\ntv{a} \to \type{T} }
      } \quad 
      \begin{array}{l}
      \tph(\type{T}) = \emptyset \\ %,\, \text{fv}(\type{T}) \subseteq \Delta \\ % T ok implies that
      \ntv{a} \notin \text{dom}(\sigma),\, \Delta, \Delta_{in} \vdash \type{T} \ \ok % TODO: Is it possible to imply well-formedness as long as input is well-formed?
      \end{array}
      $
    \\\\ 
    \end{tabular}}
  \end{center}
\caption{Generate result}
\label{fig:generation-rules}
\end{figure}

\subsection{Capture Conversion during Unification}
The \unify{} algorithm applies a capture conversion when needed.
A constraint of the form $\wcNtype{\Delta'}{N} \lessdot \type{T}$,
where $\text{fv}(\type{T}) \neq \emptyset$ is not solvable without capture conversion.
\unify{} converts those constraints to $\type{N} \lessdot \type{T}$.
This is only possible for subtype constraints which originated from a method call.

Capture conversion only works with constraints containing free variables.
It also introduces fresh free variables into the constraint set.
Both have to be regulated.
It is not allowed to substitute free type variables freely.
The algorithm introduces a new type of variables: $\wtv{a}$.
\unify{} treats those as free type variables.
This makes it possible to replace a $\wtv{a}$ with a captured wildcard variable
without having to worry about introducing free type variables at unwanted places.

The challenge for a type inference algorithm is to apply capture conversion during type inference.
Given a program 
\begin{verbatim}
class TypeInferenceExample{
	m(l){
		return swap(make(l));
	}
}
\end{verbatim}

During the time of the type inference algorithm the type of the parameter \texttt{l} is not known.
Due to the call to the method \texttt{make} it is clear that it has to be a subtype of
\texttt{List}.
These subtype relations are expressed with constraints.
$\tv{l} \lessdot \exptype{List}{\tv{a}}$ in this case.
$\tv{l}$ and $\tv{a}$ are type placeholders.
$\tv{l}$ is a type placeholder for the method parameter \texttt{l}.

One correct solution for this constraint is the substitution $\tv{l} \doteq \exptype{List}{\type{Object}}$,
which leads to the program:
\begin{verbatim}
	class TypeInferenceExample{
		Pair<Object, Object> m(List<Object> l){
			return swap(make(l));
		}
	}	
\end{verbatim}

But $\tv{l} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ is also a possible solution.
Eventhough the constraint $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\tv{a}}$
is not solvable.
But when we apply capture conversion to create $\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\tv{a}}$
we can substitute $\tv{a} \doteq \rwildcard{Y}$.

The \unify{} algorithm has to apply capture conversions during the unification of type constraints.

But this renders additional problems:
\begin{itemize}
	\item Capture conversion is not allowed for every constraint.
	\item Capture Converted variables are not allowed to leave their scope
	\item \unify{} generates type substitution which cannot be translated to Java types.
\end{itemize}


\subsection{Completeness}
It is not possible to create all super types of a type.
The General rule only creates the ones expressable by Java syntax, which still are infinitly many in some cases \cite{TamingWildcards}.
%thats not true. it can spawn X^T_T2.List<X> where T and T2 are types and we need to choose one inbetween them
Otherwise the algorithm could generate more solutions, but they have to be filterd out afterwards, because they cannot be translated into Java.


\subsection{Implementation}
%List this under implementation details
Every constraint that is not in solved form and is not able to be processed by any of the rules accounts as a error constraint and renders the constraint set unsolvable

The new constraint generated by the adopt rule may be eliminated by the match rule.
The adopt rule still needs to be applied only once per constraint.

Two additional rules can be added to remove clutter in the output.
Wildcards with same upper and lower bounds can be replaced with their upper bound.

\begin{tabular}[t]{l@{~}l}
\\\\ 
\rulename{Crunch}
& $\begin{array}[c]{@{}ll}
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \, \set{ \tv{a} \doteq \wctype{\Delta', \set{\overline{\wildcard{X}{\type{U}}{\type{L}}}}}{C}{\ol{S}} } \\ 
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \vdash
C \cup \set{ \tv{a} \doteq \wctype{\Delta'}{C}{[\ol{U}/\ol{X}]\ol{S}}} 
\end{array}
&\begin{array}[c]{l}
  \ol{U} = \ol{L}
\end{array}
\end{array}$
\\\\ 
\rulename{Crunch}
& $\begin{array}[c]{@{}ll}
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \, \set{ \tv{a} \lessdot \wctype{\Delta', \set{\overline{\wildcard{X}{\type{U}}{\type{L}}}}}{C}{\ol{S}} } \\ 
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \vdash
C \cup \set{ \tv{a} \lessdot \wctype{\Delta'}{C}{[\ol{U}/\ol{X}]\ol{S}}} 
\end{array}
&\begin{array}[c]{l}
  \ol{U} = \ol{L}
\end{array}
\end{array}$
\end{tabular}