Add Challenge 4. Wildcards are not allowed to leave their scope

introduction.tex

@@ -661,6 +661,72 @@ During the course of the \unify{} algorithm more and more types emerge.
 As soon as enough type information is given \unify{} can conduct a capture conversion if needed.
 The constraints where this is possible are marked as capture constraints.
 
+
+\item \textbf{Free Variables cannot leaver their scope}:
+
+\begin{example}
+Take the following Java program for example.
+It maps every element of a list
+$\expr{l} : \exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$
+to a polymorphic \texttt{id} method.
+We want to use our \unify{} algorithm to determine the correct type for the
+variable \expr{l2}.
+Although we do not specify constraint generation for language constructs like
+lambda expressions used in this example,
+we can imagine that the constraints have to look something like this:
+
+\begin{minipage}{0.45\textwidth}
+\begin{lstlisting}{java}
+<X> List<X> id(List<X> l){ ... }
+
+List<List<?>> ls;
+
+l2 = l.map(x -> id(x));
+\end{lstlisting}\end{minipage}
+\hfill
+\begin{minipage}{0.45\textwidth}
+\begin{constraintset}
+$
+\begin{array}{l}
+\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}}, \\
+\exptype{List}{\wtv{x}} \lessdot \tv{z}, \\
+\exptype{List}{\tv{z}} \lessdot \tv{l2}
+\end{array}
+$
+\end{constraintset}
+\end{minipage}
+
+The constraints
+$\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}},
+\exptype{List}{\wtv{x}} \lessdot \tv{z}$
+stem from the body of the lambda expression
+\texttt{shuffle(x)}.
+\textit{For clarification:} This method call would be represented as the following expression in \letfj{}:
+\texttt{let x1 :$\wctype{\rwildcard{A}}{List}{\rwildcard{A}}$ = x in id(x) :$\tv{z}$}
+
+The T-Let rule prevents us from using free variables created by the method call to \expr{id}
+to be used in the return type $\tv{z}$.
+But this has to be signaled to the \unify{} algorithm, which does not know about the origin and context of
+the constraints.
+If we naively substitute $\sigma(\tv{z}) = \exptype{List}{\rwildcard{A}}$
+the return type of the \texttt{map} function would be the type $\exptype{List}{\exptype{List}{\rwildcard{A}}}$.
+This type solution is unsound.
+The type of \expr{l2} is the same as the one of \expr{l}:
+$\exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$
+
+\textbf{Solution:}
+We solve this by distinguishing between wildcard placeholders and normal placeholders.
+$\ntv{z}$ is a normal placeholder and is not allowed to contain free variables.
+
+\end{example}
+
+\end{itemize}
+
+%TODO: Move this part. or move the third challenge some underneath.
+The \unify{} algorithm only sees the constraints with no information about the program they originated from.
+The main challenge was to find an algorithm which computes $\sigma(\wtv{a}) = \rwildcard{X}$ for example \ref{intro-example1} but not for example \ref{intro-example2}.
+
+
 \section{Discussion Pair Example}
 \begin{verbatim}
 <X> Pair<X,X> make(List<X> l){ ... }
@@ -740,13 +806,6 @@ $
 % t =. x.Triple<X,X,X>
 \end{constraintset}
 
-
-\end{itemize}
-
-%TODO: Move this part. or move the third challenge some underneath.
-The \unify{} algorithm only sees the constraints with no information about the program they originated from.
-The main challenge was to find an algorithm which computes $\sigma(\wtv{a}) = \rwildcard{X}$ for example \ref{intro-example1} but not for example \ref{intro-example2}.
-
 %TODO
 % The goal is to proof soundness in respect to the type rules introduced by \cite{aModelForJavaWithWildcards}
 % and \cite{WildcardsNeedWitnessProtection}.