Comments

tRules.tex

@@ -460,15 +460,18 @@ $\begin{array}{l}
 \end{array}$
 \\[1em]
 $\begin{array}{l}
+%TODO: why is dom(\Delta) subset of fv(N) a restriction. This excludes X,Y^X.Pair<X,Y>? 
+%TODO: we do not allow X.Pair<X,X> in the t-let (could we allow it? what about L and U being WTVs?)
     \typerule{T-Let}\\
     \begin{array}{@{}c}
         \Delta | \Gamma \vdash \expr{t}_1 : \type{T}_1 \quad \quad
-        \Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}
+        %\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}
+        \Delta \vdash \type{T}_1 <: \wctype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{C}{\ol{X}}
         \\
-        \Delta, \Delta' | \Gamma, \expr{x} : \wcNtype{}{N} \vdash \expr{t}_2 : \type{T}_2 \quad \quad
+        \Delta, \Delta' | \Gamma, \expr{x} : \wctype{}{C}{\ol{X}} \vdash \expr{t}_2 : \type{T}_2 \quad \quad
         \Delta, \Delta' \vdash  \type{T}_2 <: \type{T} \quad \quad
-        \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
+        % \text{dom}(\Delta') \subseteq \text{fv}(\type{N})  \quad \quad
-        \Delta \vdash \type{T}, \wcNtype{\Delta'}{N} \ \ok
+        \Delta \vdash \type{T}, \wctype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{C}{\ol{X}} \ \ok
         \\
         \hline
     \vspace*{-0.3cm}\\

unify.tex

@@ -1177,3 +1177,55 @@ C \cup \set{ \tv{a} \lessdot \wctype{\Delta'}{C}{[\ol{U}/\ol{X}]\ol{S}}}
 % a unifier of the form $\tv{a} \to \tv{b}$.
 % Otherwise the found solution is incorrect.
 % This only happens if the input constraints contain type variables with no upper bound constraint like $\tv{a} \lessdot \type{N}$.
+
+% FOLLOWING IS WRONG AND JUST COMMENTS:
+The motivating use case example for existential types in \cite{aModelForJavaWithWildcards} is not
+type correct in \TamedFJ{} unfortunately. %Unify can calculate it though!
+At least if we use the A-normal form transformation defined in chapter \cite{sec:anfTransformation}.
+\begin{lstlisting}[style=java]
+<X> boolean cmp(Pair<X,X> p)
+<X> Pair<X,X> make(List<X> l)
+
+X.List<X> l = ...
+m(l) {
+  return cmp(make(l));
+}
+\end{lstlisting}
+
+\begin{lstlisting}[style=tamedfj]
+let v = { let x = l in make(x) } in cmp(v)
+\end{lstlisting}
+x <. l, x <c List<a?>, Pair<a?,a?> <. v, v <c Pair<b?,b?>
+
+It will not infer a wildcard type. But a wildcard type can still be used to call m(l :: X.List<X>)
+
+is it complete? Our no free variable restriction is too restrictive for let statement.
+Not for method params. Only Java types are allowed. (no free variables)
+
+would it be complete if we allow free variables everywhere?
+Are there still supertypes that are not covered?
+Box<Pair<String,String>> <. a
+Box<Pair<Integer,Integer>> <. a
+a =. X.Box<Pair<X,X>>
+
+% TODO: find an example which is not inferred by our TI!
+
+$\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ is a correct type for \texttt{v}.
+But the T-Let rule does only allow a type in the form of $\wctype{\rwildcard{X},\rwildcard{Y}}{Pair}{\rwildcard{X},\rwildcard{Y}}$.
+%why is X,Y^X_X.Pair<X,Y> not a valid type?
+X,Y.Pair<X,Y> <. Pair<a,a>
+Y =. X
+l =. x
+u =. X
+
+
+
+let v : X,Y.Pair<X,Y> = { let x = l in make(x) } in cmp(v)
+
+Fix:
+let x : X.List<X> = l in cmp(make(x))
+% Does Unify calculate this solution?
+x <c List<a>, Pair<a,a> <c Pair<b,b>
+
+% which types are not allowed? the Same rule is the problem: here T <. a -> a =. T(without free variables)
+