From c6571879b72eb446c4401de5b1ba2ca84005edf9 Mon Sep 17 00:00:00 2001
From: Andreas Stadelmeier <andi@paulus.haus>
Date: Wed, 3 Apr 2024 00:46:29 +0200
Subject: [PATCH] Comments to Completeness

---
 unify.tex | 37 +++++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)

diff --git a/unify.tex b/unify.tex
index 8405932..b8d0f15 100644
--- a/unify.tex
+++ b/unify.tex
@@ -1177,3 +1177,40 @@ 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}$.
+
+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 = ...
+cmp(make(l))
+\end{lstlisting}
+
+\begin{lstlisting}[style=tamedfj]
+let v = { let x = l in make(x) } in cmp(v)
+\end{lstlisting}
+$\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)
+
+% Example that does not work with our TI:
+Pair<Pair<X,X>> <. 
+a <. X.Pair<Pair<X,X>>