From 0c51692936331fe629677b3ffd6d26e32f94c7f0 Mon Sep 17 00:00:00 2001
From: JanUlrich <andi@michlaustderaffe.de>
Date: Wed, 17 Apr 2024 16:45:24 +0200
Subject: [PATCH] Intro

---
 introduction.tex | 24 +++++++++++++++++++++++-
 1 file changed, 23 insertions(+), 1 deletion(-)

diff --git a/introduction.tex b/introduction.tex
index 0d5c4ab..9125e87 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -17,13 +17,35 @@ List<String> ls = emptyList();
 
 Local type inference \cite{javaTIisBroken} is able to find a type substitution $\sigma$ satisfying
 $\overline{\type{A} <: \sigma(\type{F}) }, \sigma(\type{R}) <: \type{E}$.
+It is important that $\overline{\type{A}}$ and $\type{E}$ are given types and do not contain
+type placeholders already used in $\overline{\type{F}}$.
 
 The type parameters are not allowed on the left side of $A <: F$
 We can generate method calls where this is the case. The second call to \texttt{get}.
 
+Local type inference is based on matching and not unification.
+When calling the \texttt{emptyList} method without context its return value will be set to a \texttt{List<Object>}.
+The following Java code snippet is incorrect, because \texttt{emptyList()} returns
+a \texttt{List<Object>} instead of the required \texttt{List<String>}.
 \begin{verbatim}
-emptyList().get(0).get(0);
+emptyList().add(new List<String>())
+    .get(0)
+    .get(0);
 \end{verbatim}
+%List<String> <. A
+%List<A> <: List<B>, B <: List<C> 
+% B = A and therefore A on the left and right side of constraints.
+% this makes matching impossible
+
+\begin{verbatim}
+this.<List<String>>emptyList().add(new List<String>())
+    .get(0)
+    .get(0);
+\end{verbatim}
+
+Local type inference cannot deal with type inference during the algorithm.
+If the left side contains unknown type parameters.
+
 
 \begin{verbatim}
 import java.util.ArrayList;