Fix WF-Class, WF-Var and Type for method call

constraints.tex

@@ -171,11 +171,11 @@ The ones to already typed methods and calls to untyped methods.
     & \begin{array}{@{}l@{}l}
       \constraint = \orCons\set{ & 
                 \begin{array}[t]{l}
-                  [\overline{\wtv{a}}/\ol{Y}] [\overline{\wtv{b}}/\ol{X}] \{ \tv{r} \lessdot \exptype{C}{\ol{X}},
+                  [\overline{\wtv{a}}/\ol{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdot \exptype{C}{\ol{X}},
                   \overline{\tv{r}} \lessdot \ol{T},
                   \type{T} \lessdot \tv{a}, 
-                  \overline{\wtv{a}} \lessdot \ol{N}, 
-                  \overline{\wtv{b}} \lessdot \ol{N'} \}
+                  \ol{X} \lessdot \ol{N}, 
+                  \ol{Y} \lessdot \ol{N'} \}
                 \end{array}\\
           & \ |\ 
           (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\texttt{m} : \generics{\ol{Y} \triangleleft \ol{N'}}\overline{\type{T}} \to \type{T}) \in 

soundness.tex

@@ -87,6 +87,12 @@ By structural induction over the expression $\texttt{e}$.
 
     So we do not have to proof S ok (but T)
 
+    % T_r <: C<T> (S is in T)
+    % Is C<T> ok?
+    % we could proof: \Delta' |- C<T> ok (\Delta' are all Wildcards used in Unify)
+    % if every type environment \Delta supplied to Unify is ok (L <: U), then \sigma(a) = \Delta'.N implies \Delta' conforms to (L <: U)
+    % this together with the X <. N constraints proofs T_r ok
+
     $\Delta \vdash \sigma(\tv{a}), \wcNtype{\Delta_c}{N} \ \ok$ %TODO
     %Easy, because unify only generates substitutions for normal type placeholders which are OK
 
@@ -159,12 +165,13 @@ Method calls generate multiple constraints that share the same wildcard placehol
 \textit{Proof:}
 
 \begin{lemma}
-    Well-formedness is hereditary
+    
     \begin{description}
-        \item[If] $\triangle \vdash \type{T} \ \ok$ and $\triangle \vdash \type{S} <: \type{T}$
-        \item[Then] $\triangle \vdash \type{S} \ \ok$
+        \item[If] $\Delta \vdash \wctype{\Delta'}{C}{\ol{T}} \ \ok$
+        \item[Then] $\Delta, \Delta' \vdash \ok{T} \ \ok$
     \end{description}
 \end{lemma}
+\textit{Proof:} by definition of WF-Class
 
 
 \begin{lemma} \label{lemma:tvsNoFV}

tRules.tex

@@ -94,6 +94,7 @@ $\begin{array}{l}
 \end{figure}
 
 \begin{figure}[tp]
+\begin{center}
 $\begin{array}{l}
     \typerule{WF-Bot}\\
     \begin{array}{@{}c}
@@ -113,6 +114,7 @@ $\begin{array}{l}
 $\begin{array}{l}
     \typerule{WF-Var}\\
     \begin{array}{@{}c}
+        \wildcard{W}{U}{L} \in \Delta \quad \quad 
         \Delta \vdash \ol{L}, \ol{U} \ \ok
         \\
         \hline
@@ -120,12 +122,14 @@ $\begin{array}{l}
         \Delta \vdash \wildcard{W}{U}{L} \ \ok
     \end{array}
 \end{array}$
+\\[1em]
 $\begin{array}{l}
     \typerule{WF-Class}\\
     \begin{array}{@{}c}
-        \Delta \vdash \ol{T}, \ol{L}, \ol{U} \ \ok \quad \quad
-        \Delta \vdash \ol{L} <: \ol{U} \\
-        \Delta \vdash \ol{T} <: [\ol{T}/\ol{X}] \ol{U'} \quad \quad 
+        \Delta' = \ol{\wildcard{W}{U}{L}} \quad \quad
+        \Delta, \Delta' \vdash \ol{T}, \ol{L}, \ol{U} \ \ok \quad \quad
+        \Delta, \Delta' \vdash \ol{L} <: \ol{U} \\
+        \Delta, \Delta' \vdash \ol{T} <: [\ol{T}/\ol{X}] \ol{U'} \quad \quad 
         \texttt{class}\ \exptype{C}{\ol{X \triangleleft U'}} \triangleleft \type{N} \ \{ \ldots \}
         \\
         \hline
@@ -133,6 +137,7 @@ $\begin{array}{l}
         \Delta \vdash \wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}} \ \ok
     \end{array}
 \end{array}$
+\end{center}
 \caption{Well-formedness}\label{fig:well-formedness}
 \end{figure}
 %TODO: Proof that well-formed (ok) implies that a type is witnessed