From 47259434488fad8c763f4540429b52fc3306acc8 Mon Sep 17 00:00:00 2001
From: Andreas Stadelmeier <stan@hb.dhhbw-stuttgart.de>
Date: Wed, 31 Jan 2024 18:05:42 +0100
Subject: [PATCH] Change = \emptyset to \subseteq Delta

---
 unify.tex | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/unify.tex b/unify.tex
index 7eaff5f..8b2c1e4 100644
--- a/unify.tex
+++ b/unify.tex
@@ -189,7 +189,7 @@ $
     \vspace*{-0.4cm}\\
     \wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}, \wildcard{B}{U'}{L'}} \vdash C \cup \, \set{ \type{L} \doteq \type{U} , \type{U'} \doteq \type{L'}, \type{U} \doteq \type{U'}  }
     \end{array} \quad
-    \text{fv}(\type{U}, \type{U'}, \type{L}, \type{L'}) = \emptyset
+    \text{fv}(\type{U}, \type{U'}, \type{L}, \type{L'}) \subseteq \Delta_in
     $
     \\\\
 \rulename{Tame}
@@ -199,7 +199,7 @@ $
     \hline
     \vspace*{-0.4cm}\\
     \wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}} \vdash C \cup \, \set{ \type{L} \doteq \type{T}, \type{U} \doteq \type{T} }
-    \end{array} \quad \text{fv}(\type{U}, \type{L}) = \emptyset
+    \end{array} \quad \text{fv}(\type{U}, \type{L}) \subseteq \Delta_in
     $
     \\\\
     % \rulename{Equals} %TODO
@@ -397,7 +397,7 @@ Their upper and lower bounds are fresh type variables.
       \end{array}
        %\quad \ol{Y} = \textit{fresh}(\ol{X})
        \quad \begin{array}[c]{l}
-        \text{fv}(\wctype{\Delta}{C}{\ol{S}}, \wctype{\Delta'}{C}{\ol{T}}) = \emptyset
+        \text{fv}(\wctype{\Delta}{C}{\ol{S}}, \wctype{\Delta'}{C}{\ol{T}}) \subseteq \Delta_in
         \end{array}
       \end{array}
       $
@@ -479,7 +479,7 @@ Starting with the \rulename{circle} rule. Afterwards the other rules in figure \
 
 If we find an illicit constraint assigning a type containing free variables to a type placeholder not flagged as a wildcard placeholder the algorithm fails. 
 
-$\set{\tv{a} \doteq \type{N}} \in C$ with $\text{fv}(\type{N}) \neq \emptyset$ $\implies$ fail! 
+$\set{\tv{a} \doteq \type{N}} \in C$ with $\text{fv}(\type{N}) \cap \Delta_in \neq \emptyset$ $\implies$ fail! 
 
 The first step of the algorithm is able to remove wildcards.
 Removing a wildcard works by setting its lower and upper bound to be equal.
@@ -736,7 +736,7 @@ If $C$ does not contain any wildcard variables the algorithm proceeds with step
       \tv{a} \ \text{fresh}
    \end{array}
     \end{array}
-$ 
+$
 \\\\
 \rulename{Remove-Cons} & $
     \begin{array}[c]{l}
@@ -967,7 +967,7 @@ For this step to succeed there should only be four kinds of constraints left.
 %\item\label{item:3} $\tv{a} \lessdot \tv{b}$ %, with $a$ and $b$ both isolated type variables
 \item $\tv{a} \doteq \tv{b}$
 %\item $\wtv{a} \doteq \type{G}$
-\item\label{item:1} $\tv{a} \lessdot \wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}$, with $\text{fv}(\wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}) = \emptyset$
+\item\label{item:1} $\tv{a} \lessdot \wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}$, with $\text{fv}(\wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}) \subseteq \Delta_in$
 \item\label{item:2} $\tv{a} \doteq \wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}$, with $\tv{a} \notin \ol{\type{T}}$ % and $\text{fv}(\wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}) = \emptyset$
 \item\label{item:3} $\tv{a} \doteq \rwildcard{X}$
 \end{enumerate}
@@ -1008,7 +1008,7 @@ Otherwise the generation rules \rulename{GenSigma} and \rulename{GenDelta} will
             \wildcardEnv \vdash [\type{B}/\tv{b}]C \implies \Delta \cup \set{\wildcard{B}{\type{N}}{\bot}}, \sigma \cup \set{\tv{b} \to \type{B}}
             } \quad
             \begin{array}{l}
-            \tph(\type{N}) = \emptyset, \text{fv}(\type{N}) \subseteq \Delta \\
+            \tph(\type{N}) = \emptyset, \text{fv}(\type{N}) \subseteq \Delta \cup \Delta_in \\
             \rwildcard{B} \ \text{fresh}, \tv{b} \notin \text{dom}(\sigma), \Delta \vdash \type{N} \ \ok
             \end{array}
           $
@@ -1041,7 +1041,7 @@ Otherwise the generation rules \rulename{GenSigma} and \rulename{GenDelta} will
       } \quad 
       \begin{array}{l}
       \tph(\type{T}) = \emptyset \\ %,\, \text{fv}(\type{T}) \subseteq \Delta \\ % T ok implies that
-      \tv{a} \notin \text{dom}(\sigma),\, \Delta \vdash \type{T} \ \ok
+      \tv{a} \notin \text{dom}(\sigma),\, \Delta, \Delta_in \vdash \type{T} \ \ok
       \end{array}
       $
     \\\\