Ecoop2024_TIforWildFJ/soundness.tex

\section{Soundness}

The differenciation of wildcard placeholders and normal type placeholders is vital for the soundness proof.
During a let statement the environment $\Delta$ is extended by capture converted wildcards,
but only for the scope of the body of the let statement.
The capture converted wildcards must not be used outside of the let statement.
This is ensured by two things:
The first is lemma \ref{lemma:freeVariablesOnlyTravelOneHop} which ensures that free variables only
travel one hop at the time through a constraint set.
And the second one is the fact that normal type placeholders never contain free variables.

\unify{} calculates solutions for all normal type placeholders.
Those are used for all untyped method's argument and return type.
A correct typing for method calls can be deducted from those type informations.

\begin{lemma}{Soundness:}\label{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}) = (\Delta', C)$
    \item[then] $\Delta|\Gamma  \vdash \texttt{e} : \sigma(\tv{a})$ where $\Delta = \Delta_u \cup \Delta'$
    \end{description}
\end{lemma}
\textit{Proof:}
By structural induction over the expression $\texttt{e}$. 
\begin{description}
    \item[$\texttt{let}\ \texttt{x} = \texttt{t}_1 \ \texttt{in}\ \expr{t}_2$]
    $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ by lemma \ref{lemma:wildcardWellFormedness}.
    $\Delta \vdash \type{T}, \wcNtype{\Delta'}{N} \ \ok$ by lemma \ref{lemma:unifyWellFormedness}.
        $\Delta|\Gamma \vdash \expr{t}_1: \sigma(\tv{e}_1)$ by assumption.
        $\Delta \vdash \sigma(\tv{e}_1) <: \wcNtype{\Delta'}{N}$ by constraint $\tv{e}_1 \lessdot \tv{x}$ and lemma \ref{lemma:unifySoundness}.
        The body of the let statement will only use the free variables provided by $\Delta$ and $\Delta'$.
        We can prove this by lemma \ref{lemma:tvsNoFV} and the fact that the wildcard placeholders used generated the body of the let statement are not used outside of it.
        Therefore we can say $\Delta,\Delta' | \Gamma, \expr{x}:\type{N} \vdash \expr{t}_2 : \sigma(\tv{e}_2)$ by assumption
        and $\Delta, \Delta' \vdash  \sigma(\tv{e}_2) <: \sigma(\tv{a})$ by lemma \ref{lemma:unifySoundness}
        given the constraint $\tv{e}_2 \lessdot \tv{a}$.
    \item[$\texttt{let}\ \texttt{x} = \texttt{t}_1 \ \texttt{in}\ \expr{x}.\texttt{f}$]
The let statement in the input is untyped and we have to create a let statement
$\texttt{let}\ \texttt{x} : \wcNtype{\Delta'}{N} = \texttt{t}_1 \ \texttt{in}\ \expr{x}.\texttt{f}$
that suffices the T-Let and T-Field type rules.
The case where no capture conversion is needed, because $\Delta' = \emptyset$, is trivial. Here the Let statement can be skipped entirely.
We investigate the case $\sigma(\tv{x}) = \wcNtype{\Delta}{N}$.
%Constraints t1 <. x, x <. C<a>, T <. t2
Let $\type{T}_1 = \wcNtype{\Delta'}{N} = \sigma(\tv{x})$, $\sigma(\tv{t_1}) = \type{T}_1$,
$\sigma(\tv{a}) = \type{T}_2$ then
\begin{itemize}
\item $\Delta | \Gamma \vdash t_1 : \type{T}_1$ by assumption
\item $\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$ by constraint $\tv{t_1} \lessdot \tv{x}$ and lemma \ref{lemma:unifySoundness}
\item $\Delta, \Delta' | \Gamma, x : \type{N} \vdash \expr{x}.f_1 : \type{T}_2$
First we can say $\Delta | \Gamma \vdash \expr{x} : \type{N}$ by T-Var.
%$\Delta, \Delta', \overline{\Delta} \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$ by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$
%and lemma \ref{lemma:unifySoundness}.
%The environment $\overline{\Delta}$ is not needed, because of lemma \ref{lemma:freeVariablesOnlyTravelOneHop}:
%$\Delta, \Delta' \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$
%by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$
%and lemmas \ref{lemma:unifySoundness} and \ref{lemma:freeVariablesOnlyTravelOneHop}.
By lemma \ref{lemma:unifyWellFormedness} and WF-Var we can deduct
$\text{fv}(\wcNtype{\Delta'}{N}) \subseteq \Delta$ 
and by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$
and lemmas \ref{lemma:unifySoundness} and \ref{lemma:freeVariablesOnlyTravelOneHop}
we can finally say 
$\Delta, \Delta' \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$.
With the constraint $\tv{a} \doteq [\ol{\wtv{a}}/\ol{X}]\type{T}$
and $\sigma([\ol{\wtv{a}}/\ol{X}]\type{T}) \in \text{fields}(\sigma(\exptype{C}{\ol{\wtv{a}}}))$ by F-Class
we proof $\Delta, \Delta' | \Gamma, x : \type{N} \vdash \expr{x}.f_1 : \type{T}_2$.
\item $\Delta, \Delta' \vdash \type{T}_2 <: \type{T}$ by constraint %TODO: Rename constraints
\end{itemize}

%generated constraints: t1 <. x, x <. N, T <. t2
        We are allowed to use capture conversion for $\expr{v}$ here.
        $\Delta \vdash \expr{v} : \sigma(\tv{a})$ by assumption.
        $\Delta \vdash \sigma(\tv{a}) <: \sigma(\exptype{C}{\ol{\wtv{a}}})$ and
        $\Delta \vdash \type{U}_i <: \sigma(\tv{a})$,
    because of the constraints $[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a}$, $\tv{r} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$ and lemma \ref{lemma:unifySoundness}.
    $\textit{fields}(\sigma(\exptype{C}{\overline{\wtv{a}}})) = \sigma([\overline{\wtv{a}}/\ol{X}]\type{T})$.

\item[$\text{let}\ \expr{x} = \expr{e} \ \text{in}\ 
\text{let}\ \overline{\expr{x} = \expr{e}} \ \text{in}\ \texttt{x}.\texttt{m}(\ol{x})$]
generates constraints $\tv{e} \lessdot \tv{x}, \overline{\tv{e} \lessdot \tv{x}},
\tv{r} \lessdot \tv{a}, \ol{\tv{x}} \lessdotCC \ol{T}, \type{T} \lessdot \tv{r}, \ol{\wtv{b}} \lessdot \ol{N}$.
%We need to proof $\text{let}\ \expr{x} : \wcNtype{\Delta'}{N} = \expr{e}, \,
%\overline{\expr{x} : \wcNtype{\Delta'}{N} = \expr{e}} \ \text{in}\ \texttt{x}.\texttt{m}(\ol{x}) : \type{T}_2$
%where $\sigma(\tv{x}) = \wcNtype{\Delta'}{N}$, $\sigma(\ol{\tv{x}}) = \ol{\wcNtype{\Delta'}{N}}$,  $\sigma(\tv{a}) = \type{T}_2$.
We omit the case where a capture conversion is not needed and
assume $\sigma(\tv{x}) = \wcNtype{\Delta'}{N}$, $\sigma(\ol{\tv{x}}) = \ol{\wcNtype{\Delta'}{N}}$.
We have to show T-Let and T-Call which leaves us with:
\begin{itemize}
    \item $\Delta | \Gamma \vdash \expr{e} : \sigma(\tv{e})$ and $\Delta | \Gamma \vdash \overline{\expr{e} : \sigma(\tv{e})}$ by assumption
    \item $\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$ and $\Delta \vdash \overline{\type{T}_1 <: \wcNtype{\Delta'}{N}}$ by constraints $\tv{e} \lessdot \tv{x}$, $\overline{\tv{e} \lessdot \tv{x}}$ and lemma \ref{lemma:unifySoundness}
    \item $\Delta, \Delta', \overline{\Delta'} | \Gamma, \expr{x} : \type{N}, \overline{\expr{x} : \type{N}} \vdash \expr{x}.\texttt{m}(\ol{x}) : \sigma(\tv{r})$ by T-Call and lemma \ref{lemma:freeVariableScope}, because the following promises are satisfied.
    Note: The lemma \ref{lemma:freeVariableScope} and the fact that the wildcard placeholders $\overline{\wtv{b}}$ are
    solely used here guarantees that no other than the variables declared in $\Delta, \Delta', \overline{\Delta}$ appear in $\sigma'(\overline{\wtv{b}})$.
    \begin{itemize}
        \item $\generics{\ol{X} \triangleleft \ol{U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m})$ is given, otherwise the program fails at the constraint generation step.
        \item $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}$ by constraints $\ol{\wtv{b}} \lessdot [\ol{\wtv{b}}/\ol{X}]\ol{N}$ and lemma \ref{lemma:unifySoundness}
        there must be some $\ol{S}$ satisfying this premise.
        
        % what about we apply Unify again. With the known types. TODO: proof that unify can be applied again, with the capture converted versions of the constraints
        %TODO: does not work because left side is a wildcard variable (maybe just change lemma soundness a bit)
        \item 
    \end{itemize}
\end{itemize}
    \item[$\texttt{v}.\texttt{m}(\ol{v})$]
    Proof is analog to field access, except the $\Delta \vdash \ol{S}\ \ok$ premise.
    We know that $\unify{}(\Delta, [\overline{\wtv{b}}/\ol{Y}]\set{
        \ol{\tv{e}} \lessdotCC \ol{T}, \type{T} \lessdot \tv{a}, 
        \ol{Y} \lessdot \ol{N} } \cup C) = (\Delta', \sigma)$
        and if we assume $\sigma(\ol{\tv{e}}) = \ol{\wcNtype{\Delta}{N'}}$
        then the call to $\unify{}(\Delta \cup \overline{\Delta}, [\overline{\ntv{b}}/\ol{Y}]\set{
            \ol{N'} \lessdot \ol{T}, \type{T} \lessdot \tv{a}, 
            \ol{Y} \lessdot \ol{N} } \cup C)$ succeeds with $\overline{\ntv{b}}$ being normal placeholders this time,
            which proofs $\Delta \vdash \ol{S}\ \ok$ via lemma \ref{lemma:unifyWellFormedness}.
            %TODO: why does this call succeed?
% 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}


During the unification process free variables can only move one hop at a time.
Free variables originate from capture constraints.
By applying the capture rule to a constraint of the form $\wcNtype{\Delta}{N} \lessdotCC \type{T}$ the variables declared in $\Delta$
are now free in the constraint $\type{N} \lessdot \type{T}$.
The other way of free variables traveling into a constraint is by substitution.
This is only possible if a constraint contains wildcard placeholders.
And only free variables which reside in the same constraint as a wildcard placeholders have the possibility of being set in.

This effect is transitive. Free variables travel from constraint to constraint.
If there is no connection of constraints containing wildcard type placeholders between a free variable and a constraint,
then free variables cannot travel there.

\begin{lemma}
    Free variables travel only 
\end{lemma}

\begin{lemma}{Free variables}\label{lemma:freeVariableScope}
    Free variables never leave their scope.
    If a set of constraints does not share a single wildcard type placeholder with the rest of the constraint set,
    then it will never contain free variables used outside of it.
$(\Delta, \sigma) = \unify{}(\Delta_{in}, C \cup C')$

and $\text{wtv}(C') \cap \text{wtv}(C) = \emptyset$
and $\overline{\sigma(\tv{x}) = \wcNtype{\Delta}{N}}$

then $\Delta, \Delta', \overline{\Delta}$ are all the variables used in $C'$.
\end{lemma}
\textit{Proof:} This is due to free variables only travel inbetween constraints and themselves via substitution.

If $\type{S} \lessdotCC \type{T}$ spawns free variables, they will be contained within the reach of the wildcard type placeholders
used for the method call.
No other free variables can move into that scope.
With this lemma we can further proof that during a method call only the generated free variables are used.

% \begin{lemma}
%     Free variables never leave their scope.
%     $C' = \set{
%         \overline{\tv{e} \lessdot \tv{x}}, \overline{\tv{x} \lessdotCC \tv{x}},
%         \overline{\tv{r} \lessdot \tv{a}}
%     }$
% $(\Delta, \sigma) = \unify{}(\Delta_{in}, C \cup C')$

% and $\text{wtv}(C') \cap \text{wtv}(C) = \emptyset$
% and $\overline{\sigma(\tv{x}) = \wcNtype{\Delta}{N}}$

% then $\Delta, \Delta', \overline{\Delta}$ are all the variables used in $C'$.
% %if a wildcard type placeholder does not appear anywhere else, then only the free variables of its scope can be used for him
% \end{lemma}

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


\begin{lemma}\label{lemma:wildcardWellFormedness}
\unify{} generates well-formed existential types
\begin{description}
\item[If] $(\Delta, \sigma) = \unify{}(\Delta', C)$
\item[and] $\forall \wcNtype{\Delta''}{N} \in C: \text{dom}(\Delta') \subseteq \text{fv}(\type{N})$
\item[and] $\sigma(\tv{a}) = \wcNtype{\Delta'}{N}$
%\item[then] $\Delta \vdash \ol{L <: U}$ and $\Delta \vdash \ol{U <: U'}$ % (with U' being upper limit by class definition)
\item[then] $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$
\end{description}
\end{lemma}
\textit{Proof} is straightforward induction over the transformation rules of \unify{}
under the assumption that all supplied existential types are satisfying the premise.
All parts of \unify{} that generate wildcard types always spawn types $\wcNtype{\Delta'}{N}$
with $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$.
Only the \rulename{Adapt} rule is able to produce types neglecting the premise,
but is immediately corrected by the \rulename{Trim} rule.

% 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} by induction on subtyping rules in figure \ref{fig:subtyping}

% \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:wildcardsStayInScope}
% Free variables can only hop to another constraint if they share the same wildcard placeholder.
% \begin{description}
%     \item[If] $(\sigma, \Delta) = \unify{} (\Delta', C \cup \set{\wcNtype{\Delta'}{N} \lessdot \tv{a}})$
%     \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}



%TODO: use this to proof soundness. Wildcard placeholders are not shared with other constraints and therefore only the wildcards generated by capture conversion are used in a let statement.

% \begin{lemma} \label{lemma:unifyWeakening}
% Removing constraints does not render \unify{} impossible as long as the removed constraints do not share wildcard placeholders.
% 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')$% and $\text{wtv}(C) \cap \text{wtv}(C') = \emptyset$
%     \item[then] $ (\sigma', \Delta') = \unify{}( C')$
% \end{description}

% \end{lemma}
%\textit{Proof:}
%TODO
% does this really work. We have to show that the algorithm never gets stuck as long as there is a solution
% maybe there are substitutions with types containing free variables that make additional solutions possible. Check!
\begin{lemma}{\unify{} Soundness:}\label{lemma:unifySoundness}
\unify{}'s type solutions are correct respective to the subtyping rules defined in figure \ref{fig:subtyping}.
\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[Then] there exists a substitution $\sigma'$ with:
\begin{itemize}
\item $\sigma \subseteq \sigma'$
\item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$
\item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S'}) <: \wcNtype{\Delta}{N}}$
\item $\Delta, \Delta', \overline{\Delta} \vdash \overline{\type{N} <: \sigma'(\type{T'})}$
\end{itemize}
\end{description}
\end{lemma}

\begin{lemma}{\unify{} Soundness:}%\label{lemma:unifySoundness}
\unify{}'s type solutions are correct respective to the subtyping rules defined in figure \ref{fig:subtyping}.
\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'} })$
with $\text{wtv}(\ol{S}) = \emptyset$ and $\text{wtv}(\ol{T}) = \emptyset$
\item[Then] $\Delta, \Delta' \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$
\item[and] either $\Delta, \Delta' \vdash \overline{\sigma(\type{S'}) <: \sigma(\type{T'})}$
or $\Delta, \Delta', \overline{\Delta} \vdash \overline{\sigma'(\type{S'}) <: \sigma(\type{T'})}$
with the capture converted substitution $\sigma' = \set{ \tv{a} \mapsto \type{N} \mid \tv{a} \mapsto \wcNtype{\Delta}{N} \in \sigma}$
and $\overline{\Delta} = \set{\Delta \mid \tv{a} \mapsto \wcNtype{\Delta}{N} \in \sigma }$

% there exists a substitution $\sigma'$ and a set of types $\overline{\wcNtype{\Delta}{N}}$ with:
% \begin{itemize}
% \item $\sigma \subseteq \sigma'$
% \item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$
% \item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S'}) <: \wcNtype{\Delta}{N}}$ 
% \item $\Delta, \Delta', \overline{\Delta} \vdash \overline{\type{N} <: \sigma'(\type{T'})}$
% \end{itemize}
\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[GenDelta'] same as GenDelta by setting $\sigma'(\wtv{b}) = \rwildcard{B}$
\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[Same] by S-Exists
\item[SameW] %TODO
\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]
To proof $\wctype{\Delta}{C}{\ol{S}} <: \wctype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{C}{\ol{T}}$
we have to show S-Exists for some $\Delta''$ and $\ol{T} = \sigma(\overline{\wtv{a}})$:
\begin{itemize}
\item $\Delta'' \vdash \subst{\ol{T}}{\ol{X}}\ol{L} <: \ol{T}$ by assumption and $\subst{\ol{\wtv{a}}}{\ol{X}}\ol{L} \lessdot \ol{\wtv{a}}$
\item $\Delta'' \vdash \ol{T} <: \subst{\ol{T}}{\ol{X}}\ol{U}$ by assumption and $\ol{\wtv{a}} \lessdot \subst{\ol{\wtv{a}}}{\ol{X}}\ol{L}$
\item $\text{fv}(\ol{T}) \subseteq \text{dom}(\Delta'', \Delta')$ by setting $\Delta''$ accordingly
\end{itemize}

%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 \text{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 \ref{def:equal}
%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}

\begin{lemma}
\label{lemma:freeVariablesOnlyTravelOneHop}
A constraint $\tv{a} \lessdotCC \type{T}$ or $\tv{a} \lessdot \type{T}$ implies that
$\text{fv}(\sigma(\type{T})) \subseteq \text{fv}(\sigma(\tv{a}))$.
Only free variables, which are part of the left side are used on the right side.
\end{lemma}

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