Add Example infinite types

introduction.tex

@@ -244,16 +244,38 @@ $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}} \lessdotCC \exptype
 why do we need a lessdotCC constraint
 \dbox{Eine dashbox!}
 input is e.m(e);
+
+\begin{verbatim}
+<X> List<X> concat(List<X> a, X b){}
+\end{verbatim}
+
 \begin{recap}\textbf{TI for FGJ without Wildcards:}
-The type inference algorithm for Featherweight Generic Java \cite{TIforFGJ} (called \TFGJ{}) is complete and sound.
+The type inference algorithm for Featherweight Generic Java \cite{TIforFGJ} (called \TFGJ{}) is complete and sound:
 It is able to find a type solution for a Featherweight Generic Java program, which has no type annotations at all,
 if there is any.
 It's only restriction is that no polymorphic recursion is allowed.
 \TFGJ{} generates subtype constraints $(\type{T} \lessdot \type{T})$ consisting of named types and type placeholders.
-- usually the type of e must be subtypes of the method parameters
+For example the method invocation \texttt{concat(new List(), new Object())} generates the constraints
-- in case of a polymorphic method: type placeholders resemble type parameters
+$\exptype{List}{\tv{l}} \lessdot \exptype{List}{\tv{a}}, \type{Object} \lessdot \tv{a}$.
+Subtyping without the use of wildcards is invariant \cite{FJ}:
+Therefore the only possible solution for the type placeholders $\tv{l}$ and $\tv{a}$ is $\tv{l} \doteq \type{Object}$ and $\tv{a} \doteq \type{Object}$. % in Java and Featherweight Java.
+Solution: \texttt{concat(new List<Object>(), new Object())}
+%- usually the type of e must be subtypes of the method parameters
+%- in case of a polymorphic method: type placeholders resemble type parameters
 \end{recap}
-Most 
+In \letfj{} the \texttt{concat} method has infinitely many possibilities of argument types.
+It can be called with a $\exptype{List}{\type{String}}$ or $\wctype{\wildcard{X}{\type{String}}{\type{Object}}}{List}{\rwildcard{X}}$
+or $\wctype{\rwildcard{X}, \wildcard{Y}{\bot}{\rwildcard{X}}}{List}{\rwildcard{X}}$
+\begin{lstlisting}
+class List2<A,B extends A> extends List<B>{
+  void addAll(List<B> l){ ... }
+}
+
+
+\end{lstlisting}
+
+% TODO: Change example: Assuming String is a final type.
+
 involving wildcards:
 - depending on the type of e a capture conversion must be applied first
 - the captured type N must be a subtype of the method parameters