Motivation example

introduction.tex

@@ -42,6 +42,23 @@ void test(){
     <A> void receive(List<A> l, List<A> l2){}
 \end{verbatim}
 
+Error:
+\begin{verbatim}
+rrr(this.emptyBox().set(this.<Integer>emptyBox()).set(this.<String>emptyBox()));
+\end{verbatim}
+Correct:
+\begin{verbatim}
+rrr(this.<Box<?>>emptyBox().set(this.<Integer>emptyBox()).set(this.<String>emptyBox()));
+\end{verbatim}
+
+incorrect:
+\begin{verbatim}
+emptyList().add(emptyList()).head().head()
+\end{verbatim}
+
+In this example the return type of \texttt{emptyList} needs to consider that it should contain a list of a list.
+This is a limitation of local type inference as presented here \cite{javaTIisBroken}.
+
 The big difference to local type inference is the ability to have constraints where both sides contain type placeholders.
 As described in \cite{javaTIisBroken} local type inference is able to determine an unifier $\sigma$
 which satisfies $\set{\overline{A <: \sigma(F)}, \sigma(R) <: E }$.
@@ -52,7 +69,6 @@ $A$ are method arguments and $E$ is the expected return type.
 % with global type inference this is easy to produce
 % an example where this is the case for local type inference?
 %   - the val example
-%   - 
 
 \section{Type Inference for Java}
 %The goal is to find a correct typing for a given Java program.