From 5371824a55b77f4231ffbac2208cbc57223b643c Mon Sep 17 00:00:00 2001
From: Andreas Stadelmeier <andi@paulus.haus>
Date: Wed, 3 Apr 2024 00:50:59 +0200
Subject: [PATCH] Comments

---
 unify.tex | 23 +++++++++++++++++++----
 1 file changed, 19 insertions(+), 4 deletions(-)

diff --git a/unify.tex b/unify.tex
index b8d0f15..f3d3aa1 100644
--- a/unify.tex
+++ b/unify.tex
@@ -1178,6 +1178,7 @@ C \cup \set{ \tv{a} \lessdot \wctype{\Delta'}{C}{[\ol{U}/\ol{X}]\ol{S}}}
 % 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}.
@@ -1186,12 +1187,29 @@ At least if we use the A-normal form transformation defined in chapter \cite{sec
 <X> Pair<X,X> make(List<X> l)
 
 X.List<X> l = ...
-cmp(make(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?
@@ -1211,6 +1229,3 @@ 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)
 
-% Example that does not work with our TI:
-Pair<Pair<X,X>> <. 
-a <. X.Pair<Pair<X,X>>