\subsection{Capture Constraints}
%TODO: General Capture Constraint explanation

Capture Constraints are bound to a variable.
For example a let statement like \lstinline{let x = v in x.get()} will create the capture constraint
$\tv{x} \lessdotCC_x \exptype{List}{\wtv{a}}$.
This time we annotated the capture constraint with an $x$ to show its relation to the variable \texttt{x}.
Let's do the same with the constraints generated by the \texttt{concat} method invocation in listing \ref{lst:faultyConcat},
creating the constraints \ref{lst:sameConstraints}.

\begin{figure}
  \begin{minipage}[t]{0.49\textwidth}
    \begin{lstlisting}[caption=Faulty Method Call,label=lst:faultyConcat]{tamedfj}
  List<?> v = ...;
  
  let x = v in 
      let y = v in
        concat(x, y) // Error!
    \end{lstlisting}\end{minipage}
    \hfill
    \begin{minipage}[t]{0.49\textwidth}
  \begin{lstlisting}[caption=Annotated constraints,mathescape=true,style=constraints,label=lst:sameConstraints]
  $\tv{x} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \tv{x}$
  $\tv{y} \lessdotCC_\texttt{y} \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \tv{y}$
    \end{lstlisting}
    \end{minipage}
\end{figure}


During the \unify{} process it could happen that two syntactically equal capture constraints evolve,
but they are not the same because they are each linked to a different let introduced variable.
In this example this happens when we substitute $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ for $\tv{x}$ and $\tv{y}$
resulting in:
%For example by substituting $[\wctype{\rwildcard{X}}{List}{\rwildcard{X}}/\tv{x}]$ and $[\wctype{\rwildcard{X}}{List}{\rwildcard{X}}/\tv{y}]$:
\begin{displaymath}
  \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_x \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_y \exptype{List}{\wtv{a}}
\end{displaymath}
Thanks to the original annotations we can still see that those are different constraints.
After \unify{} uses the \rulename{Capture} rule on those constraints
it gets obvious that this constraint set is unsolvable:
\begin{displaymath}
  \exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}},
\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}
\end{displaymath}

%In this paper we do not annotate capture constraint with their source let statement.
The rest of this paper will not annotate capture constraints with variable names.
Instead we consider every capture constraint as distinct to other capture constraints even when syntactically the same,
because we know that each of them originates from a different let statement.
\textit{Hint:} An implementation of this algorithm has to consider that seemingly equal capture constraints are actually not the same
and has to allow doubles in the constraint set.

% %We see 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}$).
% This is necessary to solve challenge \ref{challenge:1}.
% A capture constraint is bound to a specific let statement.

\textit{Note:}
In the special case \lstinline{let x = v in concat(x,x)} the constraints would look like
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}},
\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}$
and we could actually delete one of them without loosing information.
But this case will never occur in our algorithm, because the let statements for our input programs are generated by a ANF transformation (see \ref{sec:anfTransformation}).



\section{Constraint generation}\label{chapter:constraintGeneration}
% Method names are not unique.
% It is possible to define the same method in multiple classes.
% The \TYPE{} algorithm accounts for that by generating Or-Constraints.
% This can lead to multiple possible solutions.

%\subsection{Well-Formedness}


% But it can be easily adapted to Featherweight Java or Java.
% We add T <. a for every return of an expression anyway. If anything returns a Generic like X it is not directly used in a method call like X <c T

\begin{description}
\item[input] \TamedFJ{} program in A-Normal form
\item[output] Constraints
\end{description}

The constraint generation works on the \TamedFJ{} language.
This step is mostly the same as in \cite{TIforFGJ} except for field access and method invocation.
We will focus on those two parts where also the new capture constraints and wildcard type placeholders are introduced.

%In \TamedFJ{} capture conversion is implicit.
%To emulate Java's behaviour we assume the input program not to contain any let statements.
%They will be added by an ANF transformation (see chapter \ref{sec:anfTransformation}).

Before generating constraints the input is transformed by an ANF transformation (see section \ref{sec:anfTransformation}).

%Constraints are generated on the basis of the program in A-Normal form.
%After adding the missing type annotations the resulting program is valid under the typing rules in \cite{WildFJ}.

%This is shown in chapter \ref{sec:soundness}

%\section{\TamedFJ{}: Syntax and Typing}\label{sec:tifj}

% The syntax forces every expression to undergo a capture conversion before it can be used as a method argument.
% Even variables have to be catched by a let statement first.
% This behaviour emulates Java's implicit capture conversion.

\subsection{ANF transformation}\label{sec:anfTransformation}
\newcommand{\anf}[1]{\ensuremath{\tau}(#1)}
%https://en.wikipedia.org/wiki/A-normal_form)
Featherweight Java's syntax involves no \texttt{let} statement
and terms can be nested freely similar to Java's syntax.
Our calculus \TamedFJ{} uses let statements to explicitly apply capture conversion to wildcard types,
but we don't know which expressions will spawn wildcard types because there are no type annotations yet.
To emulate Java's behaviour we have to preemptively add capture conversion in every suitable place.
%To convert it to \TamedFJ{} additional let statements have to be added.
This is done by a \textit{A-Normal Form} \cite{aNormalForm} transformation shown in figure \ref{fig:anfTransformation}.
After this transformation every method invocation is preceded by let statements which perform capture conversion on every argument before passing them to the method.
See the example in listings \ref{lst:anfinput} and \ref{lst:anfoutput}.
\begin{figure}
\begin{minipage}{0.45\textwidth}
\begin{lstlisting}[style=fgj,caption=\TamedFJ{} example,label=lst:anfinput]
m(l, v){
    return l.add(v);
}
\end{lstlisting}
    \end{minipage}%
    \hfill
    \begin{minipage}{0.5\textwidth}
\begin{lstlisting}[style=tfgj,caption=A-Normal form,label=lst:anfoutput]
m(l, v) = 
    let x1 = l in
        let x2 = v in x1.add(x2)
\end{lstlisting}
\end{minipage}
\end{figure}

\begin{figure}
    \begin{center}
$\begin{array}{lrcl}
%\text{ANF}
& \anf{\expr{x}} & = & \expr{x} \\
& \anf{\texttt{new} \ \type{C}(\overline{t})} & = & \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}}) \\
& \anf{t.f} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \expr{x}.f \\
& \anf{t.\texttt{m}(\overline{t})} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \expr{x}.\texttt{m}(\overline{\expr{x}}) \\
& \anf{t_1 \elvis{} t_2} & = & \anf{t_1} \elvis{} \anf{t_2} \\
& \anf{\texttt{let}\ x = \expr{t}_1 \ \texttt{in}\ \expr{t}_2} & = & \texttt{let}\ x = \anf{\expr{t}_1} \ \texttt{in}\ \anf{\expr{t}_2} 
\end{array}$
\end{center}
\caption{ANF Transformation}\label{fig:anfTransformation}
\end{figure}

\begin{figure}
  \center
$
\begin{array}{lrcl}
%\hline
\text{Terms} & t & ::= & \expr{x} \\
& & \ \ | &  \texttt{let}\ \overline{\expr{x}_c} = \overline{t} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}_c}) \\
& & \ \ | & \texttt{let}\ \expr{x}_c = t \ \texttt{in}\ \expr{x}_c.f \\
& & \ \ | & \texttt{let}\ \expr{x}_c = t \ \texttt{in}\ \texttt{let}\ \overline{\expr{x}_c} = \overline{t} \ \texttt{in}\ \expr{x}_c.\texttt{m}(\overline{\expr{x}_c}) \\
& & \ \ | & t \elvis{} t \\
%\hline
\end{array}
$
\caption{Syntax of a \TamedFJ{} program in A-Normal Form}\label{fig:anf-syntax}
\end{figure}

\subsection{Constraint Generation Algorithm}
% Generally subtype constraints for an expression mirror the subtype relations in the premise of the respective type rule introduced in section \ref{sec:tifj}.
% Unknown types at the time of the constraint generation step are replaced with type placeholders.

% The constraint generation step cannot determine if a capture conversion is needed for a field access or a method call.
% Those statements produce $\lessdotCC$ constraints which signal the \unify{} algorithm that they qualify for a capture conversion.

The parameter types given to a generic method also affect their return type.
During constraint generation the algorithm does not know the parameter types yet.
We generate $\lessdotCC$ constraints and let \unify{} do the capture conversion.
$\lessdotCC$ constraints are kept until they reach the form $\type{G} \lessdotCC \type{G}$ and a capture conversion is possible.
% TODO: Challenge examples!

At points where a well-formed type is needed we use a normal type placeholder.
Inside a method call expression sub expressions (receiver, parameter) wildcard placeholders are used.
Here captured variables can flow freely.
A normal type placeholder cannot hold types containing free variables.
Normal type placeholders are assigned types which are also expressible with Java syntax.
So no types like $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ or $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$.

It is possible to feed the \unify{} algorithm a set of free variables with predefined bounds.
This is used for class generics see figure \ref{fig:constraints-for-classes}.
The \fjtype{} function returns a set of constraints aswell as an initial environment $\Delta$
containing the generics declared by this class.
Those type variables count as regular types and can be held by normal type placeholders.

%Why do we need a constraint generation step?
%% The problem is NP-Hard
%% a method call, does not know which type it will produce
%% depending on its type the 

%NO equals constraints during the constraint generation step!
\begin{figure}[tp]
  \center
\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}
  \caption{Syntax of types and constraints used by \fjtype{} and \unify{}}
  \label{fig:syntax-constraints}
\end{figure}

\begin{figure}[tp]
  \begin{gather*}
    \begin{array}{@{}l@{}l}
      \fjtype & ({\mtypeEnvironment}, \mathtt{class } \ \exptype{C}{\overline{\type{X} \triangleleft \type{N}}} \ \mathtt{ extends } \ \mathtt{N \{ \overline{T} \ \overline{f}; \, \overline{M} \}}) =\\
              & \begin{array}{ll@{}l}
\textbf{let} & \ol{\methodAssumption} =
                \set{ \mv{m} : (\exptype{C}{\ol{X}}, \ol{\tv{a}} \to \tv{a}) \mid
                  \set{ \mv{m}(\ol{x}) = \expr{e} } \in \ol{M}, \, \tv{a}, \ol{\tv{a}}\ \text{fresh} } \\
              & \Delta = \set{ \overline{\wildcard{X}{\type{N}}{\bot}} } \\
              & C = \begin{array}[t]{l}
                \set{ \typeExpr(\mtypeEnvironment \cup \ol{\methodAssumption} \cup \set{\mv{this} :
              \exptype{C}{\ol{X}} , \, \ol{x} : \ol{\tv{a}} }, \texttt{e}, \tv{a})
               \\ \quad \quad \quad \quad \mid \set{ \mv{m}(\ol{x}) = \expr{e} }  \in \ol{M},\, \mv{m} : (\exptype{C}{\ol{X}}, \ol{\tv{a}} \to \tv{a}) \in \ol{\methodAssumption}}
                  \end{array} \\
              \textbf{in} 
                  & (\Delta, C)
                \end{array}
    \end{array}
  \end{gather*}
  \caption{Constraint generation for classes}
  \label{fig:constraints-for-classes}
\end{figure}

\begin{displaymath}
  \begin{array}{@{}l@{}l}
    \typeExpr{} &({\mtypeEnvironment} , \texttt{e}.\texttt{f}, \tv{a}) = \\
                & \begin{array}{ll}
                    \textbf{let} 
                    & \tv{r} \ \text{fresh} \\
                    & \consSet_R = \typeExpr({\mtypeEnvironment}, \texttt{e}, \tv{r})\\
                    & \constraint = \begin{array}[t]{@{}l@{}l}
                      \orCons\set{
                      \set{ &
                      \tv{r} \lessdotCC \exptype{C}{\ol{\wtv{a}}} ,
                      [\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a} ,
                      \ol{\wtv{a}} \lessdot [\overline{\wtv{a}}/\ol{X}]\ol{N}
                      } \\
                      & \quad \mid \mv{T}\ \mv{f} \in \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots}
                        , \, \overline{\wtv{a}} \text{ fresh}
                      }\end{array}\\
                    {\mathbf{in}} & {
                    \consSet_R \cup \set{\constraint}}
                  \end{array} 
  \end{array}
\end{displaymath}

\begin{displaymath}
  \begin{array}{@{}l@{}l}
    \typeExpr{} &({\mtypeEnvironment} , \texttt{let}\ \expr{x} = \expr{e}_1 \ \texttt{in} \ \expr{e}_2, \tv{a}) = \\
                & \begin{array}{ll}
                    \textbf{let} 
                    & \tv{e}_1, \tv{e}_2, \tv{x} \ \text{fresh} \\
                    & \consSet_1 = \typeExpr({\mtypeEnvironment}, \expr{e}_1, \tv{e}_1)\\
                    & \consSet_2 = \typeExpr({\mtypeEnvironment} \cup \set{\expr{x} : \tv{x}}, \expr{e}_2, \tv{e}_2)\\
                    & \constraint =
                      \set{
                      \tv{e}_1 \lessdot \tv{x}, \tv{e}_2 \lessdot \tv{a}
                      }\\
                    {\mathbf{in}} & {
                      \consSet_1 \cup \consSet_2 \cup \set{\constraint}}
                  \end{array} 
  \end{array}
\end{displaymath}

\begin{displaymath}
  \begin{array}{@{}l@{}l}
      \typeExpr{} & ({\mtypeEnvironment} , \expr{v}.\mathtt{m}(\overline{\expr{v}}), \tv{a}) = \\
      & \begin{array}{ll}
      \textbf{let}
      & \tv{r}, \ol{\tv{r}} \text{ fresh} \\
      & \constraint = [\overline{\wtv{b}}/\ol{Y}]\set{
                    \ol{S} \lessdotCC \ol{T}, \type{T} \lessdot \tv{a}, 
                    \ol{Y} \lessdot \ol{N} }\\
      \mathbf{in} & (\consSet_R \cup \overline{\consSet} \cup \constraint, \type{T}) \\
      & \mathbf{where}\ \begin{array}[t]{l}
        \expr{v}, \ol{v} : \ol{S} \in \localVarAssumption \\
        \texttt{m} : \generics{\ol{Y} \triangleleft \ol{N}}\overline{\type{T}} \to \type{T} \in {\mtypeEnvironment}
      \end{array}
                    
      \end{array}
      \end{array}
  \end{displaymath}
\\[1em]
\noindent
\textbf{Example:}
\begin{verbatim}
class Class1{
  <A> A head(List<X> l){ ... }
  List<? extends String> get() { ... }
}

class Class2{
  example(c1){
    return c1.head(c1.get());
  }
}
\end{verbatim}
%This example comes with predefined type annotations.
We assume the class \texttt{Class1} has already been processed by our type inference algorithm
leading to the following type annotations:
%Now we call the $\fjtype{}$ function with the class \texttt{Class2} and the method assumptions for the preceeding class:
\begin{displaymath}
\mtypeEnvironment =  \left\{\begin{array}{l}
    \texttt{m}: \generics{\type{A} \triangleleft \type{Object}} \ 
      (\type{Class1},\, \exptype{List}{\type{A}}) \to \type{X}, \\
     \texttt{get}: (\type{Class1}) \to \wctype{\wildcard{A}{\type{Object}}{\type{String}}}{List}{\rwildcard{A}}
\end{array} \right\} 
\end{displaymath}

At first we have to convert the example method to a syntactically correct \TamedFJ{} program.
Afterwards the the \fjtype{} algorithm is able to generate constraints.

\begin{minipage}{0.45\textwidth}
  \begin{lstlisting}[style=tamedfj]
class Class2 {
  example(c1) = let x = c1 in
    let xp = x.get() in x.m(xp);
}
\end{lstlisting}
      \end{minipage}%
      \hfill
      \begin{minipage}{0.5\textwidth}
\begin{constraintset}
$
    \begin{array}{l}
      \ntv{c1} \lessdot \ntv{x}, \ntv{x} \lessdotCC \type{Class1}, \\
    \ntv{c1} \lessdot \ntv{x}, \ntv{x} \lessdotCC \type{Class1}, \\
    \wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdot \tv{xp}, \\
    \tv{xp} \lessdotCC \exptype{List}{\wtv{a}}
    \end{array}
$
  \end{constraintset}
\end{minipage}

Following is a possible solution for the given constraint set:

\begin{minipage}{0.55\textwidth}
  \begin{lstlisting}[style=letfj]
class Class2 {
  example(c1) = let x : Class1 = c1 in
    let xp : (*@$\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$@*) = x.get()
      in x.m(xp);
}
\end{lstlisting}
      \end{minipage}%
      \hfill
      \begin{minipage}{0.4\textwidth}
\begin{constraintset}
$
    \begin{array}{l}
    \sigma(\ntv{x}) = \type{Class1} \\
    %\tv{xp} \lessdot \exptype{List}{\wtv{x}}, \\
    %\exptype{List}{\type{String}} \lessdot \tv{p1}, \\
    \sigma(\tv{xp}) = \wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \\
    \end{array}
$
  \end{constraintset}
\end{minipage}

For $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$ to be a correct solution for $\tv{xp}$
the constraint $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{a}}$
must be satisfied.
This is possible, because we deal with a capture constraint.
The $\lessdotCC$ constraint allows the left side to undergo a capture conversion
which leads to $\exptype{List}{\rwildcard{A}} \lessdot \exptype{List}{\wtv{a}}$.
Now a substitution of the wildcard placeholder $\wtv{a}$ with $\rwildcard{A}$ leads to a satisfied constraint set.

The wildcard placeholders are not used as parameter or return types of methods.
Or as types for variables introduced by let statements.
They are only used for generic method parameters during a method invocation.
Type placeholders which are not flagged as wildcard placeholders ($\wtv{a}$) can never hold a free variable or a type containing free variables.
This practice hinders free variables to leave their scope.
The free variable $\rwildcard{A}$ generated by the capture conversion on the type $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$
cannot be used anywhere else then inside the constraints generated by the method call \texttt{x.m(xp)}.

\begin{displaymath}
  \begin{array}{@{}l@{}l}
    \typeExpr{} &({\mtypeEnvironment} , e_1 \elvis{} e_2, \tv{a}) = \\
                & \begin{array}{ll}
                    \textbf{let} 
                    & \tv{r}_1, \tv{r}_2 \ \text{fresh} \\
                    & \consSet_1 = \typeExpr({\mtypeEnvironment}, e_1, \tv{r}_2)\\
                    & \consSet_2 = \typeExpr({\mtypeEnvironment}, e_2, \tv{r}_2)\\
                    {\mathbf{in}} & {
                    \consSet_1 \cup \consSet_2 \cup
                        \set{\tv{r}_1 \lessdot \tv{a}, \tv{r}_2 \lessdot \tv{a}}}
                  \end{array} 
  \end{array}
\end{displaymath}

%We could skip wfresh here:
\begin{displaymath}
  \begin{array}{@{}l@{}l}
    \typeExpr{} &({\mtypeEnvironment} , x, \tv{a}) = 
    \mtypeEnvironment(x)
  \end{array}
\end{displaymath}

\begin{displaymath}
  \begin{array}{@{}l@{}l}
    \typeExpr{} &({\mtypeEnvironment} , \texttt{new}\ \type{C}(\overline{e}), \tv{a}) = \\
                & \begin{array}{ll}
                    \textbf{let} 
                    & \ol{\ntv{r}}, \ol{\ntv{a}} \ \text{fresh} \\
                    & \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \overline{e}, \ol{\ntv{r}}) \\
                    & C = \set{\ol{\ntv{r}} \lessdot [\ol{\ntv{a}}/\ol{X}]\ol{T}, \ol{\ntv{a}} \lessdot \ol{N} \mid \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots}} \\
                    {\mathbf{in}} & {
                    \overline{\consSet} \cup
                        \set{\tv{a} \doteq \exptype{C}{\ol{\ntv{a}}}}}
                  \end{array} 
  \end{array}
\end{displaymath}

% Problem:
% <X, A extends List<X>> void t2(List<A> l){}

% void test(List<List<?>> l){
%    t2(l);
% }
% Problem:
% List<Y.List<Y>> <. List<a>, a <. List<x>
% Y.List<Y> =. a
% Z.List<Z> <. List<x>

% These constraints should fail!

% \section{Result Generation}
% If \unify{} returns atleast one type solution $(\Delta, \sigma)$
% the last step of the type inference algorithm is to generate a typed class.

% This section presents our type inference algorithm.
% The algorithm is given method assumptions $\mv\Pi$ and applied to a
% single class $\mv L$ at a time:
% \begin{gather*}
% \fjtypeinference(\mtypeEnvironment, \texttt{class}\ \exptype{C}{\ol{X}
% \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \}) = \\
% \quad \quad \begin{array}[t]{rll}
%   \textbf{let}\ 
%   (\overline{\methodAssumption}, \consSet) &= \fjtype{}(\mv{\Pi}, \texttt{class}\ \exptype{C}{\ol{X}
%   \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \ldots \}) &
%                                                                      \text{// constraint generation}\\
%               {(\Delta, \sigma)} &= \unify{}(\consSet,\, \ol{X} <: \ol{N}) & \text{// constraint solving}\\
%               \generics{\ol{Y} \triangleleft \ol{S}} &= \set{ \type{Y} \triangleleft \type{S} \mid \wildcard{Y}{\type{P}}{\bot} \in \Delta} \\
%   \ol{M'} &= \set{ \generics{\ol{Y} \triangleleft \ol{S}}\ \sigma(\tv{a}) \ \texttt{m}(\ol{\sigma(\tv{a})\ x}) = \texttt{e} \mid (\mathtt{m}(\ol{x})\ = \mv e) \in \ol{M}, (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\mv{m} : \ol{\tv{a}} \to \tv{a}) \in \overline{\methodAssumption}}
%   %TODO: Describe whole algorithm (Insert types, try out every unify solution by backtracking (describe it as Non Deterministic algorithm))
% \end{array}\\
% \textbf{in}\ \texttt{class}\ \exptype{C}{\ol{X}
% \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M'} \} \\
% \textbf{in}\ \mtypeEnvironment \cup
% \set{(\exptype{C}{\ol{X} \triangleleft \ol{N}}.\mv{m} : \generics{\ol{Y} \triangleleft \ol{S}}\ \ol{\sigma(\tv{a})} \to \sigma(\tv{a})) \ |\ (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\mv{m} : \ol{\tv{a}} \to \tv{a}) \in \overline{\methodAssumption}}
% % \fjtypeInsert(\overline{\methodAssumption}, (\sigma, \unifyGenerics{}) )
% \end{gather*}

% The overall algorithm is nondeterministic. The function $\unify{}$ may
% return finitely many times as there may be multiple solutions for a constraint
% set.  A local solution for class $\mv C$ may not
% be compatible with the constraints generated for a subsequent class. In this case, we have to backtrack to $\mv C$ and proceed to the next
% local solution; if thats fail we have to backtrack further to an earlier class.

% \begin{gather*}
%   \textbf{ApplyTypes}(\mtypeEnvironment, \texttt{class}\ \exptype{C}{\ol{X}
%   \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \}) = \\
%   \quad \quad \begin{array}[t]{rl}
%     \textbf{let}\ 
%     \ol{M'} &= \set{ \generics{\ol{Y} \triangleleft \ol{S}}\ \sigma(\tv{a}) \ \texttt{m}(\ol{\sigma(\tv{a})\ x}) = \texttt{e} \mid (\mathtt{m}(\ol{x})\ = \mv e) \in \ol{M}, (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\mv{m} : \ol{\tv{a}} \to \tv{a}) \in \overline{\methodAssumption}}
%   \end{array}\\
%   \textbf{in}\ \texttt{class}\ \exptype{C}{\ol{X}
%   \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M'} \} \\
% \end{gather*}

% %TODO: Rules to create let statements
% % Input is type solution and untyped program.
% % Output is typed program
% % describe conversion for each expression

% Given a result $(\Delta, \sigma)$ and the type placeholders generated by $\TYPE{}$
% we can construct a \wildFJ{} program.

% %TODO: show soundness by comparing constraints and type rules
% % untyped expression | constraints | typed expression (making use of constraints and sigma)
% $\begin{array}{l|c|r}
% m(x) = e & r m(p x) = e & \Delta \sigma(r) m(\sigma(p) x) = |e| \\
% e \elvis{} e' \\
% e.m(\ol{e}) & (e:a).m(\ol{e:p}) & a <. T, p <. T & let x : sigma(a) = e in e.m(x); %TODO
% \end{array}$
% \begin{displaymath}
% \begin{array}[c]{l}
%    \\ 
% \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}
% \end{displaymath}