\section{Soundness}

\newcommand{\CC}{\text{CC}}

\begin{theorem}\label{testenv-theorem}
Type inference produces a correctly typed program.
\begin{description}
    \item[If] $\fjtypeinference(\mv{\Pi}, \texttt{class}\ \exptype{C}{\ol{X}
    \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \}) = \mtypeEnvironment{}'$
    \item[Then] $\texttt{class}\ \exptype{C}{\ol{X}
    \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \} \text{ok}$,
    with $\ol{M} = $
\end{description}
\end{theorem}

\begin{lemma}{Well-formedness:}
TODO: 
\end{lemma}

\begin{lemma}{Soundness:}
    \unify{}'s type solutions for a constraint set generated by $\typeExpr{}$ are correct.
    \begin{description}
    \item[if] $\typeExpr{}(\mtypeEnvironment{}, \texttt{e}, \tv{a}) = C$
    and $(\Delta_u, \sigma) = \unify{}(\Delta', C)$ and let $\Delta = \Delta_u \cup \Delta'$
%    , with $C = \set{ \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } }$
%    and $\vdash \ol{L} : \mtypeEnvironment{}$
%    and $\Gamma \subseteq \mtypeEnvironment{}$
%    \item[given] a $(\Delta, \sigma)$ with $\Delta \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$
%    and there exists a $\Delta'$ with $\Delta, \Delta' \vdash \overline{\CC{}(\sigma(\type{S'})) <: \sigma(\type{T'})}$
    \item[then] there is a completion $|\texttt{e}|$ with $\Delta|\Gamma  \vdash |\texttt{e}| : \sigma(\tv{a})$
    \end{description}
\end{lemma}
Regular type placeholders represent type annotations.
These are the only types a \wildFJ{} program needs to be correctly typed.
The type placeholders flagged as wildcard placeholders are intermediate types
used in let statements and as type parameters for generic method calls.

%Unify needs to return S aswell and guarantee that the \Delta' environment are the wildcards
% only used inside the constraint the wildcard variable occurs
% should Unify also return the \Delta' environment? Otherwise the bounds of free wildcard variables are lost

% Or is it possible to deduct the right \ol{S} directly from the types in the normal TPHs?

\textit{Proof:}
By structural induction over the expression $\texttt{e}$. 
\begin{description}
    \item[$\texttt{e}.\texttt{f}$] Let $\sigma(\tv{r}) = \wcNtype{\Delta_c}{N}$,
    then $\Delta|\Gamma  \vdash \texttt{e} : \wcNtype{\Delta_c}{N}$ by assumption.
    $\Delta', \Delta, \Delta_c \vdash \type{N} <: \sigma(\exptype{C}{\overline{\wtv{a}}})$ by premise.
    %Let $\sigma(\tv{r}) = \wcNtype{\Delta'}{N}$.
    %Let $\sigma([\ol{\wtv{a}}/\ol{X}]\type{T}) = \wcNtype{\Delta_t}{N_t}$.
    
    The completion of $|\texttt{e}.\texttt{f}|$ is $\texttt{let}\ \texttt{x} = \texttt{e} : \wcNtype{\Delta_c}{N}\ \texttt{in} \ \texttt{x}.\texttt{f}$
    
    We now show
    $\Delta|\Gamma \vdash \texttt{let}\ \texttt{x} = \texttt{e} : \wcNtype{\Delta_c}{N}\ \texttt{in} \ \texttt{x}.\texttt{f} : \sigma(a)$
    by the T-Field rule.
    $\Delta \vdash \wcNtype{\Delta_c}{N} <: \wcNtype{\Delta_c}{N}$ by S-Refl.
    $\Delta, \Delta_c \vdash \type{U}_i <: \sigma(\tv{a})$,
    because of the constraint $[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a}$ and lemma \ref{lemma:unifySoundness}.
    $\textit{fields}(\sigma(\exptype{C}{\overline{\wtv{a}}})) = \sigma([\overline{\wtv{a}}/\ol{X}]\type{T})$
    and $\text{fv}(\type{U}_i) \subseteq \text{fv}(\type{N})$ by definition of $\textit{fields}$.

    $\text{dom}(\Delta_c) \subseteq \text{fv}{\type{N}}$ by lemma \ref{lemma:tvsNoFV}.

    % X.List<X> <. List<a?>
    % $\sigma(\ol{\tv{r}}) = \overline{\wcNtype{\Delta}{N}}$,
    % $\ol{N} <: [\ol{S}/\ol{X}]\ol{U}$,
    % TODO: S ok? We could proof $\Delta, \Delta' \overline{\Delta} \vdash \ol{S} \ \ok$
    % by proofing every substitution in Unify is ok aslong as every type in the inputs is ok
    % S ok when all variables are in the environment and every L <: U and U <: Class-bound
    % This can be given by the constraints generated. We can proof if T ok and S <: T and T <: S' then S ok and S' ok

    % If S ok and T <. S , then Unify generates a T ok
    S typeinference:
    T <: [S/Y]U
    We apply the following lemma
    Lemma
    if T ok and T <: S then S ok

    until
    T = [S/Y]U

    and then we can say by 
    Lemma:
    If [S/Y]U ok then S ok (TODO: proof!)

    So we do not have to proof S ok (but T)

    % T_r <: C<T> (S is in T)
    % Is C<T> ok?
    % if every type environment \Delta supplied to Unify is ok (L <: U), then \sigma(a) = \Delta'.N implies \Delta' conforms to (L <: U)
    % this together with the X <. N constraints proofs T_r ok

    $\Delta \vdash \sigma(\tv{a}), \wcNtype{\Delta_c}{N} \ \ok$ %TODO
    %Easy, because unify only generates substitutions for normal type placeholders which are OK

    \item[$\texttt{e}.\texttt{m}(\ol{e})$]
Lets have a look at the case where the receiver and parameter types are all named types.
So $\sigma(\ol{\tv{r}}) = \ol{T} = \ol{\wcNtype{\Delta_u}{N}}$ and $\sigma(\tv{r}) = \type{T}_r = \wcNtype{\Delta_u}{N}$
and a $\Delta'$, $\overline{\Delta}$ where $\Delta' \subseteq \Delta_u$, $\overline{\Delta \subseteq \Delta_u}$
and $\text{dom}(\Delta') = (\text{fv}(\type{N})/\Delta)$, $\overline{\text{dom}(\Delta) = (\text{fv}(\type{N})/\Delta)}$  in

$\texttt{let}\ \texttt{x} : \wcNtype{\Delta'}{N} = \texttt{e} \ \texttt{in}\ 
\texttt{let}\ \ol{x} : \overline{\wcNtype{\Delta'}{N}} = \ol{e} \ \texttt{in}\ \texttt{x}.\texttt{m}(\ol{x})$

%TODO: show that this type exists \wcNtype{\Delta'}{N} (a \Delta' which only contains free variables of the type N)
% and which is a supertype of T_r (so no free variables in T_r)
% Solution: Make this a lemma and guarantee that Unify does only create types Delta.T with \Delta subset fv(T)
% This is possible because free variables (except those in \Delta_in) are never used in wildcard environments

By lemma \ref{lemma:unifyWeakening} we know that 
$\unify{}(\Delta, [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}/\ol{Y}]\set{ \overline{\wcNtype{\Delta}{N}} \lessdotCC \ol{T}, \wcNtype{\Delta'}{N} \lessdotCC \exptype{C}{\ol{X}}})$
has a solution.
Also $\overline{\wcNtype{\Delta}{N}} \lessdot \ol{T}$ and $\wcNtype{\Delta'}{N} \lessdotCC \exptype{C}{\ol{X}}$ will be converted to 
$\ol{N} \lessdot \ol{T}$ and $\type{N} \lessdot \exptype{C}{\ol{X}}$ by the \rulename{Capture} rule.
Which then results in the same as calling $\unify{}((\Delta, \Delta', \overline{\Delta}), [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}/\ol{Y}]\set{\ol{N} \lessdot \ol{T}, \type{N} \lessdot \exptype{C}{\ol{X}}})$,
which shows $\Delta, \Delta', \overline{\Delta} \vdash \overline{N} <: [\ol{S}/\ol{X}]\overline{U}$.

    This implies $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ and $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$
    $\Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T}$,
    $\Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U}$,
    and $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}$
    are guaranteed by the generated constraints and lemma \ref{lemma:unifySoundness} and \ref{lemma:unifyCC}.
    $\Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}$ due to $\ol{T} = \ol{\wcNtype{\Delta}{N}}$ and S-Refl. $\Delta, \Delta' \vdash \type{T}_r <: \wcNtype{\Delta'}{N}$ accordingly.
    $\Delta|\Gamma \vdash \texttt{t}_r : \type{T}_r$ and $\Delta|\Gamma \vdash \ol{t} : \ol{T}_r$ by assumption.
    $\Delta, \Delta' \vdash \ol{\wcNtype{\Delta}{N}} \ \ok$ by lemma \ref{lemma:unifyWellFormedness},
    therefore $\Delta, \Delta', \overline{\Delta} \vdash \ol{N} \ \ok$, which implies $\Delta, \Delta', \overline{\Delta} \vdash \ol{U} \ \ok$
    by lemma \ref{lemma:wfHereditary} and $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok $ by premise of WF-Class.
    The same goes for $\wcNtype{\Delta'}{N}$.

    % \begin{gather}
%         \label{sp:0}
%         \Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T} \\
%         \label{sp:1}
%         \Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U} \\
%         \label{sp:2}
%         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'} \\
%         \label{sp:3}
%         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \\
%         \label{sp:4}
%         \Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}
%     \end{gather}

Method calls generate multiple constraints that share the same wildcard placeholders ($\ol{\wtv{a}}$, $\ol{\wtv{b}}$).

\end{description}

% \begin{lemma} Unify does add free variables to types not containing free variables (or wildcard placeholders)
% \begin{description}
%     \item[If] $(\sigma, \Delta) = \unify{}( \Delta', C )$
%     \item[Then] $\forall x \in \set{\type{S} \mid \type{S} \in C, \text{fv}(\type{S}) = \emptyset }: \text{fv}(\sigma(\type{S})) \subseteq \text{dom}(\Delta)$
% \end{description}
% \end{lemma}
% \textit{Proof:} by induction over the \unify{} algorithm.
% A unifier $\sigma(\tv{a}) = \type{T}$, where the type variable $\tv{a}$ is not flagged as a wildcard will always hold
% $\text{fv}(\type{T}) \subseteq \text{dom}(\Delta)$.
% %UNIFY fails when there are free variables on the right side of a a =. T constraint

\begin{lemma}\label{lemma:unifyNoExcessWildcards}
\begin{description}
    \item[If] $(\Delta, \sigma) = \unify{}(\Delta', C)$ 
    \item[Then] $\sigma(\tv{a}) = \wcNtype{\Delta''}{N} \implies \text{dom}(\Delta'') \subseteq \text{fv}(\type{N})$
\end{description}
\end{lemma}
\textit{Proof:} Easy - 
All types given in the input to the \unify{} algorithm already comply with this requirement
and none of the rules change.
Note: the \rulename{Super} rule removes unnecessary wildcards.

\begin{lemma}\label{lemma:unifyWellFormedness}
\unify{} generates well-formed types as long as well-formed types are supplied.
\begin{description}
\item[If] $(\Delta, \sigma) = \unify{}(\Delta', C)$ %and $\sigma(\tv{a}) = \wcNtype{\ol{\wildcard{X}{\type{U}}{\type{L}}}}{N}$
\item[and] $\wcNtype{\Delta}{N} \in C \implies \Delta' \vdash \wcNtype{\Delta}{N} \ \ok$ 
%\item[then] $\Delta \vdash \ol{L <: U}$ and $\Delta \vdash \ol{U <: U'}$ % (with U' being upper limit by class definition)
\item[then] $\Delta \vdash \sigma(\tv{a}) \ \ok$
\end{description}
\end{lemma}
%Only the \rulename{General} rule generates fresh wildcards.
%By lemma \ref{lemma:unifySoundness} we get $\Delta \vdash \sigma(\type{T}) <: \sigma(\tv{a})$ with $\sigma(\tv{a}) = \wctype{\ol{\wildcard{X}{\sigma(U)}{\sigma(L)}}}{C}{\ol{X}}$
%By S-Exists and S-Trans we can say $\Delta \vdash \sigma(\type{L}) <: \sigma(\type{U})$
\textit{Proof:}
by induction over every step of the \unify{} algorithm.
Hint: a type placeholder $\tv{a}$ will never be replaced by a free variable or a type containing free variables.
This fact together with the presumption that every supplied type is well-formed we can easily show that this lemma is true.

\textit{Proof: (Variant 2)}
The GenSigma and GenDelta rules check for well-formedness.

% All types supplied to the Unify algorithm by TYPEs only contain ? extends or ? super wildcards. (X : [bot..T] or X : [T .. Object]).
% Both are well formed!

\begin{lemma}\label{lemma:wfHereditary}
    Well-formedness is hereditary
    \begin{description}
        \item[If] $\triangle \vdash \exptype{C}{\ol{X}} \ \ok$ and $\triangle \vdash \exptype{C}{\ol{X}} <: \type{S}$
        \item[Then] $\triangle \vdash \type{S} \ \ok$
    \end{description}
\end{lemma}
\textit{Proof:}

\begin{lemma}
    
    \begin{description}
        \item[If] $\Delta \vdash \wctype{\Delta'}{C}{\ol{T}} \ \ok$
        \item[Then] $\Delta, \Delta' \vdash \ok{T} \ \ok$
    \end{description}
\end{lemma}
\textit{Proof:} by definition of WF-Class


\begin{lemma} \label{lemma:tvsNoFV}
    \unify{} does not add free variables to types not containing free variables.
    \begin{description}
        \item[If] $(\sigma, \Delta) = \unify{} (\Delta', C)$
        \item[and] $\tv{a}$ being a type placeholders used in $C$
        \item[then] $\text{fv}(\sigma(\tv{a})) \subseteq \Delta, \Delta'$
    \end{description}
\end{lemma}
\textit{Proof:}
Trivial. \unify{} fails when a constraint $\tv{a} \doteq \rwildcard{X}$ arises.

% do we even have to proof that?
% \begin{lemma}
% C = Delta.N <c T
% is the same for Unify as:
% Delta |-  N <. T
% \end{lemma}

\begin{lemma} \label{lemma:unifyWeakening}
Removing constraints does not render \unify{} impossible.
If there is a solution for a constraint set $C$, then there is also a solution for a subset of that constraint set.
\begin{description}
    \item[If] $(\sigma, \Delta) = \unify{}( C \cup C')$
    \item[then] $ (\sigma', \Delta') = \unify{}( C')$
\end{description}
\textit{Proof:}
%TODO

\end{lemma}
\textit{Proof:}
%TODO: is it true even?
The input set does not contain free variables, only free variable placeholders.
The only time \unify{} add a wildcard to the $\wildcardEnv$ is the \rulename{Capture} rule.
This rule is only applied for the outer wildcard environments for each type.

\begin{lemma}\label{lemma:unifySoundness}
The \unify{} algorithm only produces correct output.
\begin{description}
\item[If] $(\sigma, \Delta) = \unify{}( \Delta', \, \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } )$ %\cup \overline{ \type{S} \doteq \type{S'} })$
%\item[and] $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$
\item[Then] there exists a $\sigma'$ with:
$\sigma \subseteq \sigma'$ and
$\Delta, \Delta' \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$
and $\Delta, \Delta', \overline{\Delta} \vdash \overline{\type{N} <: \sigma'(\type{T'})}$ where $\overline{\sigma(\type{S'}) = \wcNtype{\Delta}{N}}$,
otherwise $\Delta, \Delta' \vdash \overline{\sigma'(\type{S'}) <: \sigma'(\type{T'})}$
% and $\sigma(\type{T'}) = \sigma(\type{T'})$.

\end{description}
\end{lemma}

% \begin{lemma} % a lemma where we distinguis between free variable on the left or the right side of a constraint (not needed anymore)
%     The \unify{} algorithm only produces correct output for constraints not containing free variables.    
% \begin{description}
% \item[If] $(\sigma, \Delta) = \unify{}( \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \wcNtype{\Delta'}{N} \lessdot \type{T'} } \cup \overline{ \type{S'} \lessdot \wcNtype{\Delta'}{N'} })$ 
% \item[and] $fv(\overline{ \type{S} }) = \emptyset, fv(\overline{ \type{T} }) = \emptyset, fv(\overline{ \type{T'} }) = \emptyset, fv(\overline{ \type{S'} }) = \emptyset$
% \item[Then] $\Delta \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$
% and $\Delta, \Delta' \vdash \overline{\sigma(\type{N}) <: \sigma(\type{T'})}, \overline{\sigma(\type{S'}) <: \sigma(\type{N'})}$
% %TODO: Rephrase (\Delta' is used three times!)
% %The function $\CC{}$ is given as $\CC{}(\wcNtype{\Delta}{N}) = \type{N}$
% \end{description}
% \end{lemma}
\textit{Proof:}
%(we are going backwards over the algorithm)
%first we have to determine the \Delta'' -> it's only the wildcards which are free in N
% during this proof we can use Delta'' as we like

For every step in the \unify{} algorithm:
Assuming the unifier $\sigma$ is correct for a constraint set $C'$, the unifier is also correct for the
constraint set $C$ before the transformation.
% \begin{description}
% \item[Assumption:] $\unify{}(C) = (\Delta, \sigma)$, with $\Delta \vdash \sigma(C)$
% \item[Induction step:] For every case $C'$ which can be transformed to $C$ we have to show $\Delta \vdash \sigma(C')$   
% \end{description}

\unify{} terminates with $C = \emptyset$ for which the preposition holds:
$\Delta \vdash \sigma(\emptyset)$

We now show that for every transformation of a constraint set $C$ to a constraint set $C'$
the preposition holds for $C$ using the assumption that it holds for $C'$ :
$\Delta \vdash  \sigma(C') \implies \Delta \vdash \sigma(C)$

\begin{description}
\item[AddDelta] $C$ is not changed
\item[GenDelta] by definition, S-Var-Left, and S-Trans %The generated type variable is unique due to the solved form property. %and the solved form property (no $\tv{a}$ in $C$)
\item[GenSigma] by definition and S-Refl.
% holds for $\set{\tv{a} \doteq \type{G}}$ by definition.
% Holds for $C$ by assumption and because $\tv{a} \notin C$ by solved form definition ($[\type{G}/\tv{a}]C = C$).
\item[Ground] Assumption and S-Bot
\item[Sub-Elim] Assumption and S-Refl
\item[Force] by assumption and $\rwildcard{X} = \type{U}$ %TODO: step 5 should remove all X^T_T with T (make wildcards with same upper and lower bounds to normal types)
\item[Raise] Assumption, S-Trans
\item[Settle] Assumption, S-Trans
\item[Super] S-Extends ($\vdash \wctype{\Delta}{C}{\ol{T}} <: \wctype{\Delta}{D}{[\ol{T}/\ol{X}]\ol{N}}$), S-Trans
\item[\generalizeRule{}] by Assumption, because $C \subset C'$
\item[Adapt] Assumption, S-Extends, S-Trans
\item[Adopt] Assumption, because $C \subset C'$
%\item[Capture, Reduce] are always applied together. We have to destinct between two cases:
\item[Prepare]
Given a $\wctype{\Delta_c}{C}{\ol{S}} \lessdot \wcNtype{\Delta''}{N}$
we get $\Delta, \Delta', \overline{\Delta} \vdash \exptype{C}{\ol{S}} <: \wcNtype{\Delta''}{N}$ with $\Delta_c \subseteq \overline{\Delta}$.

$\text{fv}(\sigma'(\wctype{\Delta_c}{C}{\ol{S}})) = \emptyset$ implies $\text{fv}(\ol{S})\subseteq \text{dom}(\Delta, \Delta_c)$
and $\text{fv}(\sigma'(\wcNtype{\Delta''}{N})) = \emptyset$ implies $\text{dom}(\Delta_c) \cap \text{fv}(\sigma'(\wcNtype{\Delta''}{N})) = \emptyset$.

No free variables on both sides also mean we do not need $\overline{\Delta}$.
Therefore we can say $\Delta, \Delta' \vdash \wctype{\Delta_c}{C}{\ol{S}} <: \wcNtype{\Delta''}{N}$.

\item[Capture]
Everytime the \rulename{Capture} rule is invoked we add the freshly generated free variables to the global environment $\wildcardEnv$.
We get a $\sigma'$ %and a $\Delta'$
with $\Delta, \Delta' \vdash \sigma'([\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}}) <: \sigma'(\wctype{\Delta}{C}{\ol{T}})$
where $\sigma'(\ol{\wildcard{C}{U}{L}}) \subseteq \Delta'$ by assumption.
\unify{} performs a capture conversion only on $\lessdotCC$ constraints.
Therefore we can say that $\Delta, \Delta', \overline{\Delta} \vdash \sigma'(\exptype{C}{\ol{S}})
<: \sigma'(\wctype{\Delta}{C}{\ol{T}})$ with $\overline{\Delta}$ being all the fresh wildcards generated by \rulename{Capture}.

\item[Reduce]

%Assumption and S-Exists.
% Three different cases of the constraint $\exptype{C}{\ol{S}} \lessdot \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}$:
% \begin{description} 
%     \item[$\text{fv}(\exptype{C}{\ol{S}}) = \emptyset, \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$:]
%     the preposition holds by Assumption and S-Exists.
%     \item[$\text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset$:]
%     then $\text{fv}(\exptype{C}{\ol{S}}) \subseteq \Delta'$ with $\Delta' = \overline{\wildcard{A}{\type{U}}{\type{L}}}$ 
%     \item[$\text{fv}(\exptype{C}{\ol{S}}) = \emptyset$] $\Delta' = \emptyset$
% \end{description}
% List<X> <. Y.List<Y>, free variables are either in 
If $\text{fv}(\exptype{C}{\ol{S}}) = \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset$ the preposition holds by Assumption and S-Exists.
Otherwise 
$\Delta' \vdash \CC{}(\sigma(\exptype{C}{\ol{S}})) <: \sigma(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$
holds with any $\Delta'$ so that $(\text{fv}(\exptype{C}{\ol{S}}) \cup \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) ) \subseteq \text{dom}(\Delta') $.
\item[Match] Assumption, S-Trans
\item[Trim] Assumption and S-Exists
\item[Remove] $C$ is not changed
\item[Circle] S-Refl
\item[Swap] by definition
\item[Erase] S-Refl
\item[Equals] %by definition
%TODO
% Unify does never contain wildcard environments with unused wildcards. Therefore after N <: N' and N' <: N, both types have the same wildcard environment


% \item[Reduce]
% The renaming from $\rwildcard{C}$ to $\rwildcard{B}$ is not a problem. It's allowed to rename wildcards inside a type.
% Removing $\rwildcard{C}$ from the environment does not change anything because it was freshly generated and is used nowhere.

% The rest follows directly from S-Exists.
% We can say: $\text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset$,
% because the input to the \unify{} algorithm has no free type variables and we never substitute a type with free type variables
% and none of the other steps of the algorithm generates a $\lessdot$ constraint containing free type variables on the right side. %TODO: proof

% $\text{fv}(\ol{T}) \subseteq \text{dom}(\wildcardEnv \cup \overline{\wildcard{B}{\type{U'}}{\type{L'}}})$
% TODO: The capture conversion has to be when substituting a $\wtv{a}$ variable. Then we have to rename!
% %Lets first try it without the capture conversion. And involve the wtvs in the second step
% % The algorithm works by never substituting wildcards



% \unify{} cannot guarantee the premise $\text{dom}(\Delta, \Delta') \cap \text{fv}(\wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N}) = \emptyset$.
% We loosen the soundness requirements and allow a arbitrary environment $\Delta''$ to be added to the right side of the subtype relation.
% This is still sufficient to proof soundness for the whole algorithm.
% We show that the need for the additional environment $\Delta''$ can be satisfied by a let statement.

% \begin{itemize}
% \item $\Delta, \Delta' \vdash [\ol{T}/\ol{X}]\ol{L} <: \ol{T}$: S-Exists 
% \item $\Delta, \Delta' \vdash \ol{T} <: [\ol{T}/\ol{X}]\ol{U}$: S-Exists
% \item $\textit{fv}(\ol{T}) \subseteq \text{dom}{\Delta, \Delta'}$: $\wildcardEnv$ holds all variables %TODO: Proof
% \end{itemize}
\item[Normalize] Assumption and lemma 5 \emph{substitution preserves subtyping}.%\ref{lemma:wildcardReplacement}. (Or Lemma 5 from the wildcard paper. \emph{substitution preserves subtyping})
% The GenSigma step replaces both sides of $\rwildcard{A} \doteq \rwildcard{B}$ with the upper bound $\type{U}$.
% This works for every constraint, whether it contains free variables or not.
% It does not add to free variables of constraints because the upper bound does not contain any.
The GenSigma and Gen Delta steps remove Wildcards which have the same upper and lower bound.
$\rwildcard{A},\rwildcard{B} \notin \sigma(C)$

% sigma(T) = sigma(U) we have to show that T = U means \Delta \vdash [T/U]C \implies \Delta \vdash [U/T]C 
% the constraints L <. U, U <. L lead to L =. U
%If L is List<X> with X being free wildcard
%then U <. L will fail if U is type variable




% this is because bounds never contain free variables (is that true?)

%This type contains free variables when A is replaced by an CC wildcard

%This must fail:
\begin{verbatim}
<A> A m(List<? extends List<A>> l, A)

m(List<List<? super String>> l, "hi") 
\end{verbatim}
%This fails because of Equals rule (TODO: proof)

\item[Tame] same reasoning as Normalize
\item[Bot] S-Bot
\item[Pit] S-Bot
\item[Upper] S-Trans and S-VarLeft
\item[Lower] S-Trans and S-VerRight
\item[Subst-WC] by S-Refl
\item[Subst]
$\sigma(C \cup \set{\tv{a} \doteq \type{T}}) = \sigma([\type{T}/\tv{a}]C \cup \set{\tv{a} \doteq \type{T}})$
and
$\sigma(\wildcardEnv) = \sigma([\type{T}/\tv{a}]\wildcardEnv)$
\item[Subst-WC]
%Proof by Lemma 5 \emph{Type substitution preserves subtyping} from \cite{WildcardsNeedWitnessProtection}.
Same as Subst
\end{description}


\subsection{Converting to Wild FJ}
Wildcards are existential types which have to be \textit{unpacked} before they can be used.
In Java this is done implicitly by a process called capture conversion \cite{JavaLanguageSpecification}.
The type system in \cite{WildcardsNeedWitnessProtection} makes this process explicit by using \texttt{let} statements.
Our type inference algorithm will accept an input program without let statements and add them where necessary.

%Type inference adds \texttt{let} statements in a fashion similar to the Java capture conversion \cite{WildFJ}.
%We wrap every parameter of a method invocation in \texttt{let} statement unknowing if a capture conversion is necessary.

Figure \ref{fig:tletexpr} shows type rules for fields and method calls.
They have been merged with let statements and simplified.

The let statements and the type $\wcNtype{\Delta'}{N}$, which the type inference algorithm can freely choose,
are necessary for the soundness proof.

%TODO: Show that well-formed implies witnessed!
We change the type rules to require the well-formedness instead of the witnessed property.
See figure \ref{fig:well-formedness}.

Our well-formedness criteria is more restrictive than the ones used for \wildFJ{}.
\cite{WildcardsNeedWitnessProtection} works with the two different judgements $\ok$ and \texttt{witnessed}.
With \texttt{witnessed} being the stronger one.
We rephrased the $\ok$ judgement to include \texttt{witnessed} aswell.
$\type{T} \ \ok$ in this paper means $\type{T} \ \ok$ and $\type{T} \ \texttt{witnessed}$ in the sense of the \wildFJ{} type rules.
Java's type system is complex enough as it is. Simplification, when possible, is always appreciated.
Our $\ok$ rule may not be able to express every corner of the Java type system, but is sufficient to show soundness regarding type inference for a Java core calculus.

The \rulename{WF-Class} rule requires upper and lower bounds to be direct subtypes of each other $\type{L} <: \type{U}$.
The type rules from \cite{WildcardsNeedWitnessProtection} use a witness type instead.
Stating that a type is well formed (\texttt{witnessed}) if there exists atleast one simple type $\type{N}$ as a possible subtype:
$\Delta \vdash \type{N} <: \wctype{\Delta'}{C}{\ol{T}}$.

A witness type is easy to find by replacing every wildcard $\ol{W}$ in $\wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}}$ by its upper bound:
$\Delta \vdash \exptype{C}{[\ol{U}/\ol{W}]\ol{T}} <: \wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}}$.
$\Delta \vdash \exptype{C}{[\ol{U}/\ol{W}]\ol{T}} \ \texttt{witnessed}$ is given due to $\Delta \vdash \ol{T}, \ol{L}, \ol{U} \ \ok$
and $\Delta \vdash \wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}} \ \ok$.

\begin{figure}[tp]
$\begin{array}{l}
    \typerule{T-Var}\\
    \begin{array}{@{}c}
        x : \type{T} \in \Gamma
        \\
        \hline
    \vspace*{-0.3cm}\\
        \Delta | \Gamma \vdash x : \type{T}
    \end{array}
\end{array}$
\\[1em]
$\begin{array}{l}
    \typerule{T-New}\\
    \begin{array}{@{}c}
        \Delta, \overline{\Delta} \vdash  \exptype{C}{\ol{T}} \ \ok \quad \quad
        \text{fields}(\exptype{C}{\ol{T}}) = \overline{\type{U}\ f} \quad \quad
        \Delta | \Gamma \vdash \overline{t : \type{S}} \quad \quad
        \Delta \vdash  \overline{\type{S}} <: \overline{\wcNtype{\Delta}{N}} \\
        \Delta, \overline{\Delta} \vdash  \overline{\type{N}} <: \overline{\type{U}} \quad \quad
        \Delta, \overline{\Delta} \vdash \exptype{C}{\ol{T}} <: \type{T} \quad \quad
        \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})} \quad \quad
        \Delta \vdash \type{T},  \overline{\wcNtype{\Delta}{N}} \ \ok
        \\
        \hline
    \vspace*{-0.3cm}\\
    \Delta | \Gamma \vdash \letstmt{\ol{x} : \ol{\wcNtype{\Delta}{N}} = \ol{t}}{\texttt{new} \ \exptype{C}{\ol{T}}(\overline{t})} : \type{T}
    \end{array}
\end{array}$
\\[1em]
$\begin{array}{l}
    \typerule{T-Field}\\
    \begin{array}{@{}c}
        \Delta | \Gamma \vdash \texttt{t} : \type{T} \quad \quad 
        \Delta \vdash \type{T} <: \wcNtype{\Delta'}{N} \quad \quad
        \textit{fields}(\type{N}) = \ol{U\ f} \\
\Delta, \Delta' \vdash \type{U}_i <: \type{S} \quad \quad
\text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
\Delta \vdash \type{S}, \wcNtype{\Delta'}{N} \ \ok
        \\
        \hline
    \vspace*{-0.3cm}\\
        \Delta | \Gamma \vdash \texttt{let}\ x : \wcNtype{\Delta'}{N} = \texttt{t} \ \texttt{in}\ x.\texttt{f}_i : \type{S}
    \end{array}
\end{array}$
\\[1em]
$\begin{array}{l}
    \typerule{T-Call}\\
    \begin{array}{@{}c}
        \Delta, \Delta', \overline{\Delta} \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
        \textit{mtype}(\texttt{m}, \type{N}) = \generics{\ol{X \triangleleft U'}} \ol{U} \to \type{U} \quad \quad
        \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
        \\
        \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \quad \quad
        \Delta | \Gamma \vdash \texttt{t}_r : \type{T}_r \quad \quad
        \Delta | \Gamma \vdash \ol{t} : \ol{T} \quad \quad
        \Delta \vdash \type{T}_r <: \wcNtype{\Delta'}{N} \quad \quad
        \Delta \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}
        \\
        \Delta \vdash \type{T}, \wcNtype{\Delta'}{N}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad
        \Delta, \Delta', \Delta'' \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T} \quad \quad
        \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
        \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
        \\
        \hline
    \vspace*{-0.3cm}\\
        \Delta | \Gamma \vdash \letstmt{x : \wcNtype{\Delta'}{N} = t_r, \ol{x} : \ol{\wcNtype{\Delta}{N}} = \ol{t}}
        {\texttt{x}.\generics{\ol{S}}\texttt{m}(\ol{x})} : \type{T}
    \end{array}
\end{array}$
\\[1em]
$\begin{array}{l}
    \typerule{T-Elvis}\\
    \begin{array}{@{}c}
        \Delta | \Gamma \vdash t_1 : \type{T}_1 \quad \quad 
        \Delta | \Gamma \vdash t_2 : \type{T}_2 \quad \quad
        \Delta \vdash \type{T}_1 <: \type{T} \quad \quad
        \Delta \vdash \type{T}_2 <: \type{T}
        \\
        \hline
    \vspace*{-0.3cm}\\
        \Delta | \Gamma \vdash t_1 \elvis{} t_2 : \type{T}
    \end{array}
\end{array}$
\\[1em]
$\begin{array}{l}
        \typerule{T-Method}\\
    \begin{array}{@{}c}
        \text{dom}(\Delta)=\ol{X} \quad \quad
        \Delta' = \overline{\type{Y} : \bot .. \type{U}} \quad \quad
        \Delta, \Delta' \vdash \ol{U}, \type{T}, \ol{T}\ \ok \quad \quad
        \texttt{class}\ \exptype{C}{\ol{X \triangleleft \_ }} \triangleleft \type{N} \set{\ldots} \\
        \Delta, \Delta' | \overline{x:\type{T}}, \texttt{this} : \exptype{C}{\ol{X}} \vdash t:\type{S} \quad \quad
        \Delta, \Delta' \vdash \type{S} <: \type{T} \quad \quad 
        \text{override}(\texttt{m}, \type{N}, \generics{\ol{Y \triangleleft U}}\ol{T} \to \type{T})
        \\
        \hline
    \vspace*{-0.3cm}\\
        \Delta \vdash \generics{\ol{Y \triangleleft U}} \type{T} \ \texttt{m}(\overline{\type{T} \ x}) = t \ \ok \ \texttt{in C}
    \end{array}
\end{array}$
\\[1em]
$\begin{array}{l}
        \typerule{T-Class}\\
    \begin{array}{@{}c}
        \Delta = \overline{\type{X} : \bot .. \type{U}} \quad \quad 
        \Delta \vdash \ol{U}, \ol{T} \ \ok \quad \quad
        \Delta \vdash \type{N} \ \ok \quad \quad
        \Delta \vdash \ol{M} \ \ok \texttt{ in C}
        \\
        \hline
    \vspace*{-0.3cm}\\
        \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M} } \ \ok
    \end{array}
\end{array}$
\caption{T-Call and T-Field} \label{fig:tletexpr}
\end{figure}