% 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}

%\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} \lessdotCC \type{T}, \type{T} \doteq \type{T} \ldots}$

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

%The transformation steps are not applied all at once but in a specific order:
\unify{} executes the following steps until a type solution is found:
\begin{description}
\item[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.

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

The second step is nondeterministic.
%\unify{} has to pick the right transformation for each constraint of the form $\type{N} \lessdot \tv{a}$.
%The rules in figure \ref{fig:step2-rules} offer three possibilities to deal with constraints $\type{N} \lessdot \tv{a}$.
For every $\type{T} \lessdot \tv{a}$ constraint \unify{} has to pick exactly one transformation from figure \ref{fig:step2-rules}.
The same principle goes for constraints of the form $\tv{a} \lessdot \type{N}, \tv{a} \lessdot \tv{b}$ and the two transformations in figure \ref{fig:step2-rules2}.
%They have to be applied until the constraint set holds no constraints of the form $\tv{a} \lessdot \type{N}, \tv{a} \lessdot \tv{b}$.
If atleast one transformation was applied in this step revert to step 1.
Otherwise proceed with step 3.
%This builds a search tree over multiple possible solutions.
%\unify{} has to try each branch and accumulate the resulting solutions into a solution set.

%$\type{T} \lessdot \ntv{a}$ constraints have three and $\type{T} \lessdot \wtv{a}$ constraints have five possible transformations.

\textit{Hint:}
When implementing this step via backtracking
the rules \rulename{General} and \rulename{Super} should be tried first.
% is the Same rule really necessary?
The \rulename{Settle} and \rulename{Raise} rules should only be used when none of the rules in figure \ref{fig:step2-rules} can be applied.


\item[Step 3:]
Apply the rules in figure \ref{fig:cleanup-rules} exhaustively.
\rulename{Ground} and \rulename{Flatten} deal with constraints containing free variables.
If a type placeholder is solely used as lower bound \rulename{Ground} can replace it with the bottom type.
Otherwise the \rulename{Flatten} rule has to remove the wildcards responsible for the free variable.
\text{Note:} Only one of those rules has to be applied per constraint.
If the constraint set has been changed by one of these rules the algorithm must return to step 1.
But if only the \rulename{SubElim} rule is applied or the constraint set is not changed at all,
the algorithm can proceed with step 4.

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.

\end{description}

\item[Step 4:] \textit{(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}

%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.

% \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}
\end{description}

\subsection{Transformation Rules (Step 1)}
Our \unify{} process uses a similar concept as the standard unification by Martelli and Montanari \cite{MM82},
consisting of terms, relations and variables.
Instead of terms we have types of the form $\exptype{C}{\ol{T}}$ and
the variables are called type placeholders.
The input consist out of subtype relations.
The goal is to find a solution (an unifier) which is a substitution for type placeholders
which satisfies all input subtype constraints.
Types are reduced until they %either reach a discrepancy like $\type{String} \doteq \type{Integer}$
reach a form like $\tv{a} \doteq \type{T}$.
Afterwards \unify{} substitutes type placeholder $\tv{a}$ with $\type{T}$.
This is done until a substitution for all type placeholders and therefore a valid solution is reached.
The reduction and substitutions are done in the first step of the algorithm.
The algorithms state consists out of a wildcard environment and a constraint set ($\wildcardEnv \vdash C$).
Initially they are set to the input environment $\Delta_{in}$ and the input constraints.

Each calculation step of the algorithm is expressed as a transformation rule consisting of three parts.
The input is shown above the line, the output below, and additional premises are displayed on the right side.
If the wildcard environment $\wildcardEnv$ and the constraint set $C$ match the pattern declared as the input
the transformation will reduce them into the specified output.
The \rulename{Subst} rule (figure \ref{fig:subst-rules}) for example takes a constraint set that has atleast one constraint of the form
$\ntv{a} \doteq \type{T}$ and replaces every occurence of $\ntv{a}$ by $\type{T}$
in the wildcard environment $\wildcardEnv{}$ aswell as the remaining constraint set $C$.

\begin{figure}
  \begin{center}
    \leavevmode
    \fbox{
    \begin{tabular}[t]{l@{~}l}
    \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}
    $
    \\\\
    \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}
    $
    \\\\
    \rulename{Bot}
    & $
    \begin{array}[c]{l}
    \wildcardEnv \vdash C \cup \set{ \bot \lessdot \type{T} } \\ 
    \hline
    \vspace*{-0.4cm}\\
    \wildcardEnv \vdash C 
    \end{array} 
    $
    \quad
    \rulename{Pit}
    $
    \begin{array}[c]{l}
    \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \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}

The \rulename{Upper} and \rulename{Lower} conversions (figure \ref{fig:wildcard-rules}) replace wildcards with their respective bounds when appearing in a subtype constraint.
\rulename{Lower} has to check if the wildcard is part of the input wildcards $\Delta_{in}$.
If that is the case the wildcard can be part of the type solution and stays in the constraint set.
\textit{Note:} The subtype constraints in these rules are annotated with numbers $\lessdot_1$.
All rule inputs containing subtype constraints $(\lessdot)$ are always meant for both kinds,
subtype ($\lessdot$) and capture constraints ($\lessdotCC$).
If multiple constraints are stated in the input format they will be annotated with numbers which map them to the constraints used in the output of the rule.
Constraints with the same number stay the same kind.
So if the input to \rulename{Upper} is $\rwildcard{A} \lessdotCC \type{G}$ the output will be something like $\type{U} \lessdotCC \type{G}$.
If the input is a normal subtype constraint the output has to be a normal subtype constraint too.
%TODO: Rephrase
%The reason being that capture constraints are treated like regular subtype constraints in these rules.
%All transformations for subtype constraints work for capture constraints aswell.
%For clarification Subtype constraints are marked with a number.
But the \rulename{Adopt} rule for example takes multiple subtype constraints and also adds a new one.
Here the numbered annotations are necessary.
\textit{Example:} 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}.
Note that 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.

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.
The \rulename{Erase} rule will remove redundant $\type{T} \doteq \type{T}$ constraints
\rulename{Equals} ensures equality of two types by ensuring they are mutual subtypes.
We define two types as equal if they are mutual subtypes of each other.
\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}

\begin{figure}
  \begin{center}
    \leavevmode
    \fbox{
    \begin{tabular}[t]{l@{~}l}
   \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}(\type{N'}) \subseteq \Delta_{in} \\
     \text{wtv}(\type{N'}) = \emptyset
     \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} } \\  
\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}
$
\end{tabular}}
\end{center}
  \caption{Dealing with wildcard types on the left side of a subtype constraint}
\end{figure}

An existential type can never be a subtype of a regular type:
$\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \nless: \exptype{C}{\rwildcard{X}}$.
This is a problem for constraints of the form $\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdot \type{N}$.
Take the constraint $\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdot \exptype{C}{\wtv{a}}$ for example.
After applying a reduction we get $\rwildcard{X} \doteq \wtv{a}$ which is not a valid solution.
The problem is that we loose the information of the left side being an existential type with the reduction step.
Therefore we have to assure beforehand that errors (like $\rwildcard{X} \doteq \wtv{a}$ in this example) cannot occur.
But we alsod don't want to exclude reductions for these kind of constraints in general.
The solution is to check if there are any free variables or wildcard placeholders on the right side of the constraint.
If that is the case one of the rules \rulename{Trim}, \rulename{Clear}, or \rulename{Exclude} have to be applied.
In our example this would be the \rulename{Exclude} rule replacing the wildcard placeholder with $\wtv{x}$ with a normal placeholder.
Afterwards \rulename{Prepare} can be used eventually leading to the erasure of the wildcard $\rwildcard{X}$ by equalizing its upper and lower bounds:
\begin{displaymath}
\prftree[r]{\rulename{Contract}}{
\prftree[r]{\rulename{Reduce}}{
\prftree[r]{\rulename{Equals}}{
\prftree[r]{\rulename{Reduce}}{
\prftree[r]{\rulename{Capture}}{
\prftree[r]{\rulename{Prepare}}{
  \wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\ntv{x}}}
}
{
  \wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\exptype{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\ntv{x}}}
}  
}
{
  \wildcard{X}{\tv{u}}{\tv{l}} \vdash \exptype{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\ntv{x}}}
}  
}
{
  \wildcard{X}{\tv{u}}{\tv{l}} \vdash \exptype{List}{\rwildcard{X}} \doteq \exptype{List}{\ntv{x}}
}}
{
  \wildcard{X}{\tv{u}}{\tv{l}} \vdash \exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\ntv{x}}, \exptype{List}{\ntv{x}} \lessdot \exptype{List}{\rwildcard{X}}
}
}
{
  \wildcard{X}{\tv{u}}{\tv{l}} \vdash \ntv{x} \doteq \rwildcard{X}
}}{
  \text{equalize upper and lower bound of }\rwildcard{X}: \quad
  \ntv{x} \doteq \tv{u}, \tv{u} \doteq \tv{l} 
}
\end{displaymath}
Note that the \rulename{Prepare} rule is always applied together with the \rulename{Capture} and the \rulename{Reduce} rule:
\rulename{Trim} removes unused wildcard declarations.
\rulename{Clear} and \rulename{Exclude} remove wildcard placeholders or wildcards to
allow the constraint to be processed by \rulename{Prepare}.

\unify{} keeps $\tv{a} \lessdot \type{T}$ constraints as long as possible.
The \rulename{Match} rule reduces two $\tv{a} \lessdot \type{T}$ constraints to one.
There has to be a common subtype $\type{C}$ of $\type{D}$ and $\type{D'}$ for this rule to work
expressed as premises $\type{C} \ll \type{D}$ and $\type{C} \ll \type{D'}$.
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}

For example the constraints $\tv{a} \lessdot \type{String}$ and $\tv{a} \lessdot \type{Integer}$
are unsolvable, because there exists no common subtype of $\type{String}$ and $\type{Integer}$.
Whereas the constraints $\tv{a} \lessdotCC \exptype{List}{\type{Integer}}$ and
$\tv{a} \lessdotCC \exptype{List}{\tv{b}}$ can be processed by \rulename{Match}:
\begin{displaymath}
\prftree[r]{\rulename{Tame}}{
\prftree[r]{\rulename{Reduce}}{
\prftree[r]{\rulename{Capture}}{
\prftree[r]{\rulename{Match}}{
\tv{a} \lessdotCC \exptype{List}{\type{Integer}}, \tv{a} \lessdotCC \exptype{List}{\tv{b}}
}{
\begin{array}{l}
\tv{a} \lessdot \wctype{\wildcard{A}{\tv{u}}{\tv{l}}}{List}{\rwildcard{A}}, \\
\wctype{\wildcard{A}{\tv{u}}{\tv{l}}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\type{Integer}}, \\
\wctype{\wildcard{A}{\tv{u}}{\tv{l}}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\tv{b}}
\end{array}
}}{
\wildcard{A}{\tv{u}}{\tv{l}} \vdash 
\begin{array}[t]{l}
\tv{a} \lessdot \wctype{\wildcard{A}{\tv{u}}{\tv{l}}}{List}{\rwildcard{A}}, \\
\exptype{List}{\rwildcard{A}} \lessdot \exptype{List}{\type{Integer}}, \\
\exptype{List}{\rwildcard{A}} \lessdot \exptype{List}{\tv{b}}
\end{array}
}}{
\wildcard{A}{\tv{u}}{\tv{l}} \vdash \tv{a} \lessdot \wctype{\wildcard{A}{\tv{u}}{\tv{l}}}{List}{\rwildcard{A}},
\rwildcard{A} \doteq \type{Integer}, \rwildcard{A} \doteq \tv{b}
}}{
\wildcard{A}{\tv{u}}{\tv{l}} \vdash \tv{a} \lessdot \wctype{\wildcard{A}{\tv{u}}{\tv{l}}}{List}{\rwildcard{A}},
\tv{u} \doteq \type{Integer}, \tv{l} \doteq \type{Integer}, \tv{u} \doteq \tv{b}
}
\end{displaymath}

After \rulename{Subst} and \rulename{Same} the remaining constraints are $\tv{b} \doteq \type{Integer}$ and
$\tv{a} \lessdot \wctype{\wildcard{A}{\type{Integer}}{\type{Integer}}}{List}{\rwildcard{A}}$
%which is equal to $\tv{a} \lessdot \exptype{List}{\type{Integer}}$ and additionally we have $\tv{b} \doteq \type{Integer}$.

\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}{[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}]\type{U}}{[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}]\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{Adopt} // is already covered by Raise and Settle
%         & $
%         \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}

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}}$.

The \unify{} algorithm applies a capture conversion by applying the \rulename{Capture} transformation when needed.
Capture conversion removes a types bounding environment $\Delta$ and adds the included wildcard definitions to the global environment $\wildcardEnv{}$.
Only the \rulename{Capture} transformation adds wildcards to the wildcard environment $\wildcardEnv{}$
and every added wildcard gets a fresh unique name.
This ensures the wildcard environment $\wildcardEnv{}$ never
gets the same wildcard twice.


\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{Subst} &
%                        $\begin{array}[c]{l}
%   \wildcardEnv \vdash C \cup \set{\cctv{a} \doteq \wctype{\Delta}{C}{\ol{X}}}\\
%                          \hline
%   [\exptype{C}{\ol{X}}/\cctv{a}]\wildcardEnv \vdash [\exptype{C}{\ol{X}}/\cctv{a}]
%   C \cup \set{\ntv{a} \doteq \type{T}}
%                        \end{array}
%                      \quad \begin{array}{c}
%                       \ntv{a} \notin \wctype{\Delta}{C}{\ol{X}} \\
%                       \text{fv}(\wctype{\Delta}{C}{\ol{X}}) \subseteq \Delta', \, \text{wtv}(\wctype{\Delta}{C}{\ol{X}}) = \emptyset
%                      \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}
$\\
\\
  \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{Contract} &
                 $\begin{array}[c]{l}
\wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}} \vdash C \cup \set{\ntv{a} \doteq \type{T}}\\
                   \hline
[\type{U}/\type{A}]\wildcardEnv \vdash [\type{U}/\type{A}]
C \cup [\type{U}/\type{A}]\set{\ntv{a} \doteq \type{T}, \type{L} \doteq \type{U}}
                 \end{array}
               \quad \begin{array}{c}
                \rwildcard{A} \in \text{fv}(\type{T})\\
               \end{array}$\\
\end{tabular}}
\end{center}
\caption{Substitution rules}\label{fig:subst-rules}
\end{figure}

\unify{} must not replace normal type placeholders with free variables
except variables initially passed by $\Delta_{in}$.
The \rulename{Subst} rule checks if a type $\type{T}$ contains any
free variables or wildcard placeholders before replacing a normal type placeholder with it.
%This ensures that free variables are never substituted for normal type placeholders.
This ensures that a normal type placeholder is never replaced by a type containing free variables.
A type solution for a normal type placeholder will never contain free variables.
This is needed to guarantee well-formed type solutions and also keep free variables inside their scope
(see challenge \ref{challenge3}).
\rulename{Subst-WC} does not need to do that and can freely replace wildcard placehodlers with types despite their free variables.
We do not keep replacements for wildcard placeholders and they will not show up in the final type solution.
If the \rulename{Subst} rule is not applicable then either the \rulename{Normalize}
or \rulename{Contract} transformation has to be used to remove wildcard placeholders and
wildcards.

\subsection{Branching Step (Step 2)}
\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.

\subsection{Generate Result (Step 4)}
The generation rules defined in figure \ref{fig:generation-rules} are similar to the other transformation rules but contain an additional part,
the result output consisting of a wildcard environment and a set of unifier $\sigma$.

\subsection{Adding Wildcards to the mix}
%\unify{} is able to create wildcard solutions even when the input set of constraints do not contain any wildcard variables.
%Input constraints originating from a completely untyped input program do not contain any existential types.
%Those are added during \unify{}.
Wildcard types are added preemptively and if necessary can be removed later down the line.
The parts where existential types are created are the \rulename{Match} and \rulename{General} transformations.
Everytime a constraint of the form $\type{T} \lessdot \tv{a}$ occurs, 
it could be possible that a wildcard type for $\tv{a}$ is needed.
For example the constraint $\exptype{List}{\type{String}} \lessdot \tv{a}$
results in $\tv{a} \doteq \wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}$.
The upper and lower bounds of the freshly generated wildcard $\rwildcard{X}$ are type placeholders.
If a second constraint like $\tv{a} \lessdot \exptype{List}{\type{String}}$
exists the wildcard $\rwildcard{X}$ has to be removed by setting both lower and upper bound to $\type{String}$.
\begin{displaymath}
\prftree[r]{\rulename{Reduce}}{
\prftree[r]{\rulename{Subst}}{
\prftree[r]{\rulename{Same}}{\exptype{List}{\type{Integer}} \lessdot \tv{r}}
{\exptype{List}{\type{Integer}} \lessdot \tv{r},
\tv{r} \doteq \wctype{\wildcard{X}{\ntv{u}}{\ntv{l}}}{List}{\rwildcard{X}}
}}
{\exptype{List}{\type{Integer}} \lessdot \wctype{\wildcard{X}{\ntv{u}}{\ntv{l}}}{List}{\rwildcard{X}}}
}
{\type{Integer} \lessdot \ntv{u}, \ntv{l} \lessdot \type{Integer}}
\end{displaymath}


%Wildcard creation. % TODO: Explain by the example from the Bad Honnef Talk
%Wildcards are bound to a type.
% and can therefore only be created at T <. a constraints
% After a reduce step the information to which Type the wildcard was bound is lost!
% \begin{lstlisting}
% <X> List<X> concat(List<X> l, List<X> r){ ... }

% someList(){
%   return new List("String") :? new List(42);
% }
% \end{lstlisting}

Let's have a look at the constraints generated by the introduction example in listing \ref{lst:intro-example-typeless}:
\begin{lstlisting}[style=constraints]
(*@$\exptype{List}{\ntv{x}} \lessdot {\ntv{r}}, \type{String} \lessdot {\ntv{x}}$@*),
(*@$\exptype{List}{\ntv{y}} \lessdot {\ntv{r}}, \type{Integer} \lessdot {\ntv{y}}$@*)
\end{lstlisting}

\unify{} executes the following steps to generate a solved constraint set:
\begin{displaymath}
\prftree[r]{\rulename{Subst}}
{
  \prftree[r]{\rulename{Same}}{\type{String} \lessdot \ntv{x}}
  {\type{String} \lessdot \ntv{x}, \ntv{x} \doteq \type{String}}
}
{
  \prftree[r]{\rulename{Same}}{\type{Integer} \lessdot \ntv{y}}
  {\type{Integer} \lessdot \ntv{y}, \ntv{y} \doteq \type{Integer}}
}
{
\prftree[r]{\rulename{Reduce}}{\type{String} \lessdot \type{String}, \type{Integer} \lessdot \type{Integer}, \ntv{x} \doteq \type{String}, \ntv{y} \doteq \type{Integer}}
{\ntv{x} \doteq \type{String},\ntv{y} \doteq \type{Integer}} 
}
\end{displaymath}
%After another substitution this leads to the constraints:
%$\exptype{List}{\type{String}} \lessdot {\ntv{r}}, \exptype{List}{\type{Integer}} \lessdot {\ntv{r}}$

The constraint $\type{String} \lessdot {\ntv{x}}$ is solved by applying
\rulename{Super} and afterwards substituting $\type{String}$ for $\ntv{x}$,
same for $\type{Integer} \lessdot \ntv{y}$,
resulting in the two constraints \linebreak[2]
$\exptype{List}{\type{Integer}} \lessdot {\ntv{r}}$ \linebreak[2] and \linebreak[2]
$\exptype{List}{\type{String}} \lessdot {\ntv{r}}$.
Now comes the part where \unify{} creates existential types by applying the \rulename{Same} transformation.
An existential type is created with fresh type placeholders as upper and lower bound.
After a substitution all $\tv{r}$ are replaced with this new existential type.
\unify{} can now determine type replacements for the freshly created bounds $\tv{u}$ and $\tv{l}$.
\begin{displaymath}
\prftree[r]{\rulename{Reduce}}{
\prftree[r]{\rulename{Subst}}{
\prftree[r]{\rulename{Same}}{\exptype{List}{\type{Integer}} \lessdot \tv{r},\exptype{List}{\type{Integer}} \lessdot \tv{r}}
{\exptype{List}{\type{String}} \lessdot \tv{r},
\exptype{List}{\type{Integer}} \lessdot \tv{r},
\tv{r} \doteq \wctype{\wildcard{X}{\ntv{u}}{\ntv{l}}}{List}{\rwildcard{X}}
}}
{\exptype{List}{\type{String}} \lessdot \wctype{\wildcard{X}{\ntv{u}}{\ntv{l}}}{List}{\rwildcard{X}},
\exptype{List}{\type{Integer}} \lessdot \wctype{\wildcard{X}{\ntv{u}}{\ntv{l}}}{List}{\rwildcard{X}}}
}
{\type{String} \lessdot \ntv{u}, \ntv{l} \lessdot \type{String},
\type{Integer} \lessdot \ntv{u}, \ntv{l} \lessdot \type{Integer}}
\end{displaymath}

In this example a correct solution is $\sigma(\tv{u}) = \type{Object}$ and $\sigma(\tv{l}) = \bot$.
Remember that the substitution for the type placeholder $\tv{r}$ is $\wctype{\wildcard{X}{\ntv{u}}{\ntv{l}}}{List}{\rwildcard{X}}$
leading to \texttt{List<?>} as a return type for the \texttt{someList} method after applying $\sigma$:

\begin{lstlisting}[style=tamedfj]
List<? extends Object> someList(){
  return new List("String") :? new List(42);
}
\end{lstlisting}

% \subsection{Wildcard Elimination Example}
% \begin{lstlisting}
%   <X> List<X> concat(List<X> l, List<X> l2){ ... }
%   someList(){
%     return new List("String") :? new List(42);
%   }

%   concat(someList(), someList());
% \end{lstlisting}

% Let's add an additional method call to the previous example.
% The \texttt{concat} method takes two lists of the same generic type.
% \texttt{concat} cannot be invoked with two existential lists.
% %TODO: Explain capture conversion


%\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 \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:}


%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'}$.


% \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}

% 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.

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

% \unify{} is able to remove wildcards by assigning their upper and lower bounds the same type
% (Def: $\type{Object} = \wildcard{A}{Object}{Object}$ by definition \ref{def:equal}).
% This is used by the \rulename{Tame} rule.

% \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]

% \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}


% if there are a <. List<x?> constraints remaining in the end, then this can be a sign of a irregular input constraint set.

% \begin{example}{Free variables must not leave the scope of the surrounding \texttt{let} statement}

% \noindent
% \begin{minipage}{0.40\textwidth}
% \begin{lstlisting}
% m(l) = let v = l in v.get()
% \end{lstlisting} 
% \end{minipage}%
% \hfill
% \begin{minipage}{0.59\textwidth}
% \begin{constraintset}
% $\tv{l} \lessdot \tv{v}, \tv{v} \lessdotCC \exptype{List}{\wtv{x}},
% \wtv{x} \lessdot \tv{r}$
% \end{constraintset}
% \end{minipage}
% Lets assume the variables \texttt{l} and \texttt{v}
% get the type $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$ assigned to them.
% After application of the \rulename{Capture} and \rulename{SubstWC} rules the constraint set looks like this:

% $\begin{array}[c]{l}
% \wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}, \wtv{x} \lessdot \ntv{r}
%   \\
% \hline
% \vspace*{-0.4cm}\\
% \wildcard{X}{\type{Object}}{\type{String}} \vdash \wtv{x} \doteq \rwildcard{X}, \rwildcard{X} \lessdot \ntv{r}
% \end{array}
% $

% Replacing $\tv{r}$ with $\rwildcard{X}$ would solve the constraint set but lead to the method type

% \texttt{X m(List<? super String> l)} which makes no sense.
% The normal type placeholder $\ntv{r}$ has to be replaced by a type without free type variables
% ($\ntv{r} \doteq \type{Object}$) leading to

% \texttt{Object m(List<? super String> l)}.
% \end{example}

% % TODO: 
% a <c C<X> 
% -------------
% a <. X.C<X>, X.C<X> <c C<X>

% a <. C<X>
% ---------
% a <. C<U>, U = L

%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} %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}
    \quad
    \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}


\begin{figure}
\begin{mathpar}
\inferrule[Capture]{
        \wildcardEnv \vdash 
        C \cup \, \set{ \wctype{\overline{\wildcard{B}{\type{U}}{\type{L}}}}{C}{\ol{S}} \lessdotCC \type{T} } \\ 
}{
      \wildcardEnv \cup \overline{\wildcard{C}{[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}]\type{U}}{[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}]\type{L}}}
        \vdash C \cup \, \set{  
        [\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}} \lessdot \type{T} }
} 
      \quad \ol{\rwildcard{C}} \ \text{fresh}
\and
\inferrule[Reduce]{
    \wildcardEnv \vdash 
            C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot
            \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}} }
}{
\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}} }
}
\quad \text{wtv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset
\and
\inferrule[Reduce-Empty]{
    \wildcardEnv \vdash 
            C \cup \, \set{ \exptype{C}{\ol{S}} \lessdot
            \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}} }
}{
\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}} }
}
\and
\inferrule[Exclude]{
\wildcardEnv \vdash 
C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T} }
}{
\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} } \\  
}\quad \Delta \neq \emptyset,
\wtv{a} \in \text{fv}(\type{T}), \tv{a} \ \text{fresh}
\end{mathpar}
\end{figure}

\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}
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}

\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{Same}
            & $
            \begin{array}[c]{l}
              \wildcardEnv \vdash
              C \cup \type{G} \lessdot \tv{a}\\
              \hline
              \wildcardEnv \vdash
              C \cup \set{
                \tv{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}
          $
      \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}

      \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-rules2}
  \end{figure}

Figure \ref{fig:step2-rules} are special transformations aimed at free variables defined in the input environment $\Delta_{in}$.
Usually \rulename{Upper} takes care of $\rwildcard{X} \lessdot \tv{a}$ constraints,
but if $\rwildcard{X}$ is an element of $\Delta_{in}$ we can also treat it as a regular type.
This leaves us with the two possibilities \rulename{Subst-X} and \rulename{Gen-X} which is the same as \rulename{Upper}.

\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} % why does this rule need a X \notin C premise? a \notin C is needed because there could be a constraint b <. List<a> (a is only allowed to be used as lower bound)
& $\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}}{\tv{a}}}} \vdash
C \cup \set{ \overline{\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, \,  \tv{a} \notin \overline{T}, \, \tv{a} \notin \wildcardEnv % , \, \rwildcard{X} \notin C\\
%\text{length}( \overline{\tv{a} \lessdot \type{T}} ) > 1
\end{array}
\end{array}$
\\\\
\rulename{Flatten} 
& $\begin{array}[c]{l}
  \wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash C \cup \set{\tv{a} \lessdot \type{T}}\\
  \hline
  [\type{U}/\rwildcard{X}]\wildcardEnv \vdash [\type{U}/\rwildcard{X}]C \cup [\type{U}/\rwildcard{X}]\set{\tv{a} \lessdot \type{T}, \type{U} \doteq \type{L}}
\end{array} \quad \rwildcard{X} \in \text{fv}(\type{T})
$
  \end{tabular}}
\end{center}
\caption{Cleanup rules}\label{fig:cleanup-rules}
\end{figure}

\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{Examples}

% \textit{Example} of the type reduction rules in figure \ref{fig:reductionRules} with the input 
% $\wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}$
% The first step is the \rulename{Capture} rule.
% %The right side of the constraint does not contain any free variables.
% $\begin{array}{c}
% \wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}\\
% \hline %Capture
% \wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdotCC \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}
% \end{array}$

% \begin{NiceTabular}{l}
%   $\ \wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}$ \\
%   $\nextdeduction{
%     \wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdotCC \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}
%   } $\\
%   $\nextdeduction{
%     \rwildcard{X} \vdash \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}
%   } $\\
%   $\nextdeduction{
%     \rwildcard{X} \vdash \wctype{\rwildcard{Y}}{List}{\rwildcard{Y}} \doteq \wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X} \doteq \wtv{a}
%   } $\\
%   $\nextdeduction{
%       \wildcard{X}{Object}{\type{String}} \vdash
%       \type{String} \lessdot \mathcolorbox{addition}{\type{String}}, \tv{a} \doteq \rwildcard{X}
%   } $\\
%   $\nextdeduction{
%       \wildcard{X}{Object}{\type{String}} \vdash
%       \cancel{\type{String} \lessdot \rwildcard{X}}, \tv{a} \doteq \rwildcard{X}
%   } $\\
%       \CodeAfter
%       \begin{tikzpicture}
%           \node [right] at (2-|last) { \colorbox{white}{\rulename{Prepare}} } ; 
%           \node [right] at (3-|last) { \colorbox{white}{\rulename{Capture}} } ; 
%           \node [right] at (4-|last) { \colorbox{white}{\rulename{Reduce}} } ; 
%           \node [right] at (5-|last) { \colorbox{white}{\rulename{Equals}} } ; 
%           \node [right] at (6-|last) { \colorbox{white}{\rulename{Erase}} } ; 
%       \end{tikzpicture}
%   \end{NiceTabular}

% \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.

% 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}\label{sec: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.

% \letfj{} is not able to represent all Java programs. %TODO: this makes ist impossible for our algorithm to be complete on Java

% %Loss of completeness:
% % a <. b, b <c List<x>

% % Example
% \begin{lstlisting}
% m(l){
%   return let x = l in x.add(1);
% }
% \end{lstlisting}
% Here generality is lost.
% Constraints: $\ntv{l} \lessdot \ntv{x}, \ntv{x} \lessdotCC \exptype{List}{\wtv{x}}$

% Correct solution would be:
% \begin{lstlisting}
% m(List<? super Int> l){
%   return let x = l in x.add(1);
% }
% \end{lstlisting}

% Our solution:
% \begin{lstlisting}
% <X extends List<Integer> m(X l){
%   return let x = l in x.add(1);
% }
% m(List<? super Integer>)
% \end{lstlisting}
% $\tv{a} \lessdotCC \type{T}$ constraints allow for existential types on the left side,
% because there will be a capture conversion.
% We do not cover this and only apply capture conversion when the left side is known.
% So $\tv{a}$ will not be assigned a existential type, which explains our less general solution.

% If all of the program is given this may be not much of an issue.
% The $\tv{a} \lessdotCC \type{T}$ constraint is kept until the end and if the method
% is called and $\tv{a}$ gets a type, then this type can be an existential type aswell.

% Problem: There are infinite subtypes to a type Pair<x,y> when capture conversion is allowed 

% a <. b, b <c List<X>
% b <. X.List<X>, X.List<X> <c List<x> (is this sound? -> yes)
% ( is this complete? X,Y.Pair<X,Y> <c X.Pair<X,X>)


% \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.


% \textbf{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}}$.

% \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}


% 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}$.
