Unify example

tRules.tex

@@ -51,7 +51,7 @@ $
 \text{Lower bounds} & \type{K}, \type{L} & ::= & \type{T} \mid \bot \\
 \text{Type variable contexts} &  \Delta & ::= & \overline{\wildcard{X}{T}{L}} \\
 \text{Class declarations} &  D & ::= & \texttt{class}\ \exptype{C}{\ol{X \triangleleft T}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M}} \\
-\text{Method declarations} &  \texttt{M} & ::= & \texttt{m}(\overline{\expr{x}}) = t \\
+\text{Method declarations} &  \texttt{M} & ::= & \texttt{m}(\overline{\expr{x}}) \set{ \texttt{return}\ t;} \\
 \text{Terms} & t & ::= & \expr{x} \\
 & & \ \ | &  \texttt{let}\ \overline{\expr{x}_c} = \overline{t} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}_c}) \\
 & & \ \ | & \texttt{let}\ \expr{x}_c = t \ \texttt{in}\ \expr{x}_c.f \\

unify.tex

@@ -20,6 +20,17 @@ someList(){
 }
 \end{lstlisting}
 
+Constraints for the untyped \texttt{someList} method:
+\begin{constraintset}
+$\begin{array}{l}
+\exptype{List}{\tv{x}} \lessdot {\tv{r}}, \type{String} \lessdot {\tv{x}},
+\exptype{List}{\tv{y}} \lessdot {\tv{r}}, \type{Integer} \lessdot {\tv{y}}
+\end{array}$
+\end{constraintset}
+
+The constraint $\type{String} \lessdot {\ntv{x}}$ is solved by applying
+\rulename{Super} and substituting $\type{String}$ for $\ntv{x}$.
+
 \subsection{Description}
 The \unify{} algorithm tries to find a solution for a set of constraints like
 $\set{\exptype{List}{String} \lessdot \tv{a}, \exptype{List}{Integer} \lessdot \tv{a}}$.