Comments

introduction.tex

@@ -563,8 +563,6 @@ The constraints where this is possible are marked as capture constraints.
 Type information flows top down.
 Argument types of a method invocation impact its return type.
 But knowing the return type does not imply distinct argument types.
-The code in listing \ref{principalTypeExample} shows a nested method call
-\texttt{receive(copy(lSpecial))}.
 We know from the argument types of \texttt{receive} -which are given- that the \texttt{copy} method
 needs to return a type of the form $\exptype{Pair}{\type{X}, \type{Y}}$
 where \type{X} and \type{Y} can be any types as long as \type{Y} is a subtype of \type{X}.
@@ -573,6 +571,14 @@ Without wildcards this would leave us with a clue what the type should look like
 %TODO: simplify this example. lSpeial <. List<x> and List<x> <. id is sufficient
 % The unify algorithm needs to resolve l <c List<x?> to l <. X.List<X>, X.List<X> <c List<x?>
 
+% this is not complete:
+l <c Pair<x?, y?>
+l <. X,Y.Pair<X,Y>, X,Y.Pair<X,Y> <. Pair<x?, y?>
+
+% if a x =. y emerge:
+X =. Y, which will delete both wildcards
+
+
 \end{itemize}
 
 %TODO: Move this part. or move the third challenge some underneath.

unify.tex

@@ -415,6 +415,11 @@ which are used for the upper and lower bounds.
 % --------------
 % b =. X.C<X>
 % TODO: SameW rule can also be applied to normal type variables, because we have the contract rule now:
+
+% a <c List<x?>
+% --------------
+% a <. X.List<X>, X.List<X> <c List<x?>
+
 \begin{figure}
   \begin{center}
     \leavevmode