From 54fb6f9f0fd476ff993a89a8d6cd3134a2b14b13 Mon Sep 17 00:00:00 2001
From: Andreas Stadelmeier <andi@paulus.haus>
Date: Tue, 30 Jan 2024 23:03:34 +0100
Subject: [PATCH] Fix Unify WF lemma

---
 soundness.tex | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/soundness.tex b/soundness.tex
index b658da0..803e864 100644
--- a/soundness.tex
+++ b/soundness.tex
@@ -155,10 +155,10 @@ Method calls generate multiple constraints that share the same wildcard placehol
 % %UNIFY fails when there are free variables on the right side of a a =. T constraint
 
 \begin{lemma}
-\unify{} generates well-formed type environments
+\unify{} generates well-formed types as long as well-formed types are supplied.
 \begin{description}
 \item[If] $(\Delta, \sigma) = \unify{}(\Delta', C)$ and $\sigma(\tv{a}) = \wcNtype{\ol{\wildcard{X}{\type{U}}{\type{L}}}}{N}$
-\item[and] $\forall \Delta_w \in C: \ \vdash \type{L} <: \type{U}$ 
+\item[and] $\forall \wcNtype{\Delta}{N} \in C: \ \Delta' \vdash \wcNtype{\Delta}{N} \ \ok$ 
 \item[then] $\Delta \vdash \ol{L <: U}$ and $\Delta \vdash \ol{U <: U'}$ % (with U' being upper limit by class definition)
 \end{description}
 \end{lemma}
@@ -166,6 +166,9 @@ Only the \rulename{General} rule generates fresh wildcards.
 By lemma \ref{lemma:unifySoundness} we get $\Delta \vdash $
 By S-Exists and S-Trans 
 
+% All types supplied to the Unify algorithm by TYPEs only contain ? extends or ? super wildcards. (X : [bot..T] or X : [T .. Object]).
+% Both are well formed!
+
 \begin{lemma}
     Well-formedness is hereditary
     \begin{description}