From 93c0b76b9c69b6df0b05c0d8e5de1dc441db05d3 Mon Sep 17 00:00:00 2001
From: Andreas Stadelmeier <stan@hb.dhhbw-stuttgart.de>
Date: Tue, 9 Jan 2024 16:28:19 +0100
Subject: [PATCH] Add <:_? constraint (work in progress)

---
 soundness.tex | 27 ++++++++++++++++++++++++---
 unify.tex     |  4 ++--
 2 files changed, 26 insertions(+), 5 deletions(-)

diff --git a/soundness.tex b/soundness.tex
index 2754d93..433c919 100644
--- a/soundness.tex
+++ b/soundness.tex
@@ -153,12 +153,20 @@ $\text{fv}(\type{T}) \subseteq \text{dom}(\Delta)$.
 % \end{lemma}
 
 \begin{lemma} \label{lemma:unifyCC}
+Free variables do not leave their scope.
 \begin{description}
-    \item[If] $(\sigma, \Delta) = \unify{}( C \cup \set{ \overline{\wcNtype{\Delta}{N} \lessdot \type{T} } } )$
-    \item[and] $\text{fv}(\ol{T}) \notin C$, $\text{fv}(\ol{\wcNtype{\Delta}{N}}) \notin C$
-    \item[Then] $\Delta, \overline{\Delta} \vdash \overline{ \sigma(\type{N}) <: \sigma(\type{T}) }$
+    \item[If] $(\sigma, \Delta) = \unify{}( C \cup \set{ \type{T} \lessdot \type{S} } \cup \set{ \overline{\type{T} \lessdot \type{S} } } )$
+    \item[and] $\text{fv}(\type{T}, \type{S}) \subseteq \text{fv}(\ol{T}, \ol{S})$, 
+        $\sigma(\ol{T}) = \ol{\wcNtype{\Delta}{N}}$ and $\sigma(\type{T}) = \wcNtype{\Delta'}{N'}$
+    \item[then] $ \Delta, \overline{\Delta}, \Delta' \vdash \sigma(\type{T}) <: \sigma(\type{S}) $
+
+    % \item[If] $(\sigma, \Delta) = \unify{}( C \cup \set{ \overline{\wcNtype{\Delta}{N} \lessdot \type{T} } } )$
+    % \item[and] $\text{fv}(\ol{T}) \notin C$, $\text{fv}(\ol{\wcNtype{\Delta}{N}}) \notin C$
+    % \item[Then] $\Delta, \overline{\Delta} \vdash \overline{ \sigma(\type{N}) <: \sigma(\type{T}) }$
 \end{description}
 
+Their scope is the set of constraints, which contain the same free variable placeholders.
+
     % Wildcard place holders only use free variables occuring in the same constraint as them.
     % \begin{description}
     %     \item[If] $(\sigma, \Delta) = \unify{}( C )$
@@ -167,6 +175,19 @@ $\text{fv}(\type{T}) \subseteq \text{dom}(\Delta)$.
 \end{lemma}
 \textit{Proof:}
 %TODO: is it true even?
+The input set does not contain free variables, only free variable placeholders.
+The only time \unify{} add a wildcard to the $\wildcardEnv$ is the \rulename{Capture} rule.
+This rule is only applied for the outer wildcard environments for each type.
+
+%where to get a Box<Box<a?>> ?
+
+% Box<Box<a?>> <. Box<? super Box<?>>
+
+% %What is with wildcards in the lower bounds of type
+% Box<Box<a?>> <. X_Y.Box<Y>.Box<X>
+% Y.Box<Y> <. Box<a?>
+% Y =. a?
+
 
 \begin{lemma}
 The \unify{} algorithm only produces correct output for constraints not containing free variables.
diff --git a/unify.tex b/unify.tex
index 0c2908e..68b1c02 100644
--- a/unify.tex
+++ b/unify.tex
@@ -44,7 +44,7 @@ The \unify{} algorithm internally uses the following data types:
 
 \begin{tabular}{lcll}
     $C $ &$::=$ &$\overline{c}$ & Constraint set \\
-    $c $ &$::=$ & $\type{T} \lessdot \type{T} \mid \type{T} \doteq \type{T}$ & Constraint \\
+    $c $ &$::=$ & $\type{T} \lessdot \type{T} \mid \type{T} \lessdotCC \type{T} \mid \type{T} \doteq \type{T}$ & Constraint \\
     $\type{T}, \type{U}, \type{L} $ & $::=$ & $\tv{a} \mid \wtv{a} \mid \gtype{G}$ & Type variable or Type \\
     $\gtype{G}$ & $::=$ & $\type{X} \mid \ntype{N}$ & Wildcard, or Class Type \\
     $\ntype{N}, \ntype{S}$ & $::=$ & $\wctype{\triangle}{C}{\ol{T}} $ & Class Type \\
@@ -359,7 +359,7 @@ Their upper and lower bounds are fresh type variables.
       \begin{array}[c]{@{}ll}
       \begin{array}[c]{l}
           \wildcardEnv \vdash 
-          C \cup \, \set{ \wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}} \lessdot \wctype{\Delta}{C}{\ol{T}} } \\ 
+          C \cup \, \set{ \wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}} \lessdotCC \wctype{\Delta}{C}{\ol{T}} } \\ 
         \hline
         \vspace*{-0.4cm}\\
         \wildcardEnv \cup \overline{\wildcard{C}{\type{U'}}{\type{L'}}}