stan/Ecoop2024_TIforWildFJ
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Fix Related Work. Adapt Soundness proof

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-05-31 11:49:44 +02:00
parent c86dc891f3
commit 0e157cf427
2 changed files with 106 additions and 86 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
relatedwork.tex
View File

@ -63,14 +63,14 @@ indeed the transitiv closure of $\QMextends{\theta} \sub \theta'$ and $\theta' \
algorithm for this type system, which he proved as sound and complete. algorithm for this type system, which he proved as sound and complete.
The problem of his type system is in the lossing reflexivity as shown in The problem of his type system is in the lossing reflexivity as shown in
example \ref{intro-example1}. First approaches to solve this problem he gave in example \ref{lst:intro-example-typeless}. First approaches to solve this problem he gave in
\cite{plue24_1}, where he fixes that no pairwise different nodes in the \cite{plue24_1}, where he fixes that no pairwise different nodes in the
abstract syntax gets the same type variable and that no pairwise different type abstract syntax gets the same type variable and that no pairwise different type
variables are equalized. In \cite{PH23} he showed how his type inference variables are equalized. In \cite{PH23} he showed how his type inference
algorithm suffices theese properties. algorithm suffices theese properties.
In Pl\"umicke's work there is indeed a formal definition of the subtying % In Pl\"umicke's work there is indeed a formal definition of the subtying
ordering and a correctness proof of the type unification algorithms but no % ordering and a correctness proof of the type unification algorithms but no
soundness proof of the type system, itself. Therefore we choose for our type % soundness proof of the type system, itself. Therefore we choose for our type
inference algorithms with wildcars the approach of ??????? % inference algorithms with wildcars the approach of ???????

182
soundness.tex
View File

@ -95,21 +95,21 @@
\unify{}'s type solutions for a constraint set generated by $\typeExpr{}$ are correct. \unify{}'s type solutions for a constraint set generated by $\typeExpr{}$ are correct.
\begin{description} \begin{description}
\item[if] $\typeExpr{}(\mtypeEnvironment{}, \texttt{e}, \tv{a}) = (\Delta', C)$ \item[if] $\typeExpr{}(\mtypeEnvironment{}, \texttt{e}, \tv{a}) = (\Delta', C)$
and $(\Delta_u, \sigma) = \unify{}(\Delta', C)$ and let $\Delta= \Delta_u \cup \Delta'$ and $(\Delta_u, \sigma) = \unify{}(\Delta', C)$ % and let $\Delta= \Delta_u \cup \Delta'$
$\Delta, \Delta' \vdash $ % $\Delta, \Delta' \vdash $
% , with $C = \set{ \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } }$ % , with $C = \set{ \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } }$
% and $\vdash \ol{L} : \mtypeEnvironment{}$ % and $\vdash \ol{L} : \mtypeEnvironment{}$
% and $\Gamma \subseteq \mtypeEnvironment{}$ % and $\Gamma \subseteq \mtypeEnvironment{}$
% \item[given] a $(\Delta, \sigma)$ with $\Delta \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$ % \item[given] a $(\Delta, \sigma)$ with $\Delta \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$
% and there exists a $\Delta'$ with $\Delta, \Delta' \vdash \overline{\CC{}(\sigma(\type{S'})) <: \sigma(\type{T'})}$ % and there exists a $\Delta'$ with $\Delta, \Delta' \vdash \overline{\CC{}(\sigma(\type{S'})) <: \sigma(\type{T'})}$
%\item[then] there is a completion $|\texttt{e}|$ with $\Delta|\Gamma \vdash |\texttt{e}| : \sigma(\tv{a})$ %\item[then] there is a completion $|\texttt{e}|$ with $\Delta|\Gamma \vdash |\texttt{e}| : \sigma(\tv{a})$
\item[then] $\Delta|\Gamma \vdash \texttt{e} : \sigma(\tv{a})$ \item[then] $\Delta,\Delta'|\Gamma \vdash \texttt{e} : \sigma(\tv{a})$
\end{description} \end{description}
\end{lemma} \end{lemma}
Regular type placeholders represent type annotations. % Regular type placeholders represent type annotations.
These are the only types a \wildFJ{} program needs to be correctly typed. % These are the only types a \wildFJ{} program needs to be correctly typed.
The type placeholders flagged as wildcard placeholders are intermediate types % The type placeholders flagged as wildcard placeholders are intermediate types
used in let statements and as type parameters for generic method calls. % used in let statements and as type parameters for generic method calls.
%Unify needs to return S aswell and guarantee that the \Delta' environment are the wildcards %Unify needs to return S aswell and guarantee that the \Delta' environment are the wildcards
% only used inside the constraint the wildcard variable occurs % only used inside the constraint the wildcard variable occurs
@ -121,33 +121,44 @@ used in let statements and as type parameters for generic method calls.
By structural induction over the expression $\texttt{e}$. By structural induction over the expression $\texttt{e}$.
\begin{description} \begin{description}
\item[$\texttt{let}\ \texttt{x} = \texttt{t}_1 \ \texttt{in}\ \expr{t}_2$] \item[$\texttt{let}\ \texttt{x} = \texttt{t}_1 \ \texttt{in}\ \expr{t}_2$]
$\Delta|\Gamma \vdash \expr{t}_1: \type{T}_1$ by assumption. $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ by lemma \ref{lemma:wildcardWellFormedness}.
The body of the let statement will only use the free variables provided by $\Delta$ and $\Delta'$ (see lemma \ref{lemma:wildcardsStayInScope}). $\Delta \vdash \type{T}, \wcNtype{\Delta'}{N} \ \ok$ by lemma \ref{lemma:unifyWellFormedness}.
$\Delta|\Gamma \vdash \expr{t}_1: \sigma(\tv{e}_1)$ by assumption.
$\Delta \vdash \sigma(\tv{e}_1) <: \wcNtype{\Delta'}{N}$ by constraint $\tv{e}_1 \lessdot \tv{x}$ and lemma \ref{lemma:unifySoundness}.
The body of the let statement will only use the free variables provided by $\Delta$ and $\Delta'$.
We can prove this by lemma \ref{lemma:tvsNoFV} and the fact that the wildcard placeholders used generated the body of the let statement are not used outside of it.
Therefore we can say $\Delta,\Delta' | \Gamma, \expr{x}:\type{N} \vdash \expr{t}_2 : \sigma(\tv{e}_2)$ by assumption
and $\Delta, \Delta' \vdash \sigma(\tv{e}_2) <: \sigma(\tv{a})$ by lemma \ref{lemma:unifySoundness}
given the constraint $\tv{e}_2 \lessdot \tv{a}$.
\item[$\expr{v}.\texttt{f}$] \item[$\expr{v}.\texttt{f}$]
We are alowwed to use capture conversion for $\expr{v}$ here. We are alowwed to use capture conversion for $\expr{v}$ here.
$\Delta \vdash \expr{v} : \sigma(\tv{a})$ by assumption.
\item[$\texttt{let}\ \texttt{x} = \texttt{e} \ \texttt{in} \ \texttt{x}.\texttt{f}$] $\Delta \vdash \sigma(\tv{a}) <: \sigma(\exptype{C}{\ol{\wtv{a}}})$ and
$\Delta|\Gamma \vdash \expr{e}: \type{T}$ by assumption. $\Delta \vdash \type{U}_i <: \sigma(\tv{a})$,
$\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ by lemma \ref{lemma:wildcardWellFormedness}. because of the constraints $[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a}$, $\tv{r} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$ and lemma \ref{lemma:unifySoundness}.
$\Delta, \Delta' | \Gamma, \expr{x} : \type{T} \vdash \texttt{x}.\texttt{f}$ $\textit{fields}(\sigma(\exptype{C}{\overline{\wtv{a}}})) = \sigma([\overline{\wtv{a}}/\ol{X}]\type{T})$.
\item[$\texttt{e}.\texttt{f}$] Let $\sigma(\tv{r}) = \wcNtype{\Delta_c}{N}$, % \item[$\texttt{let}\ \texttt{x} = \texttt{e} \ \texttt{in} \ \texttt{x}.\texttt{f}$]
then $\Delta|\Gamma \vdash \texttt{e} : \wcNtype{\Delta_c}{N}$ by assumption. % $\Delta|\Gamma \vdash \expr{e}: \type{T}$ by assumption.
$\Delta', \Delta, \Delta_c \vdash \type{N} <: \sigma(\exptype{C}{\overline{\wtv{a}}})$ by premise. % $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ by lemma \ref{lemma:wildcardWellFormedness}.
%Let $\sigma(\tv{r}) = \wcNtype{\Delta'}{N}$. % $\Delta, \Delta' | \Gamma, \expr{x} : \type{T} \vdash \texttt{x}.\texttt{f}$
%Let $\sigma([\ol{\wtv{a}}/\ol{X}]\type{T}) = \wcNtype{\Delta_t}{N_t}$. % \item[$\texttt{e}.\texttt{f}$] Let $\sigma(\tv{r}) = \wcNtype{\Delta_c}{N}$,
% then $\Delta|\Gamma \vdash \texttt{e} : \wcNtype{\Delta_c}{N}$ by assumption.
% $\Delta', \Delta, \Delta_c \vdash \type{N} <: \sigma(\exptype{C}{\overline{\wtv{a}}})$ by premise.
% %Let $\sigma(\tv{r}) = \wcNtype{\Delta'}{N}$.
% %Let $\sigma([\ol{\wtv{a}}/\ol{X}]\type{T}) = \wcNtype{\Delta_t}{N_t}$.
The completion of $|\texttt{e}.\texttt{f}|$ is $\texttt{let}\ \texttt{x} = \texttt{e} : \wcNtype{\Delta_c}{N}\ \texttt{in} \ \texttt{x}.\texttt{f}$ % The completion of $|\texttt{e}.\texttt{f}|$ is $\texttt{let}\ \texttt{x} = \texttt{e} : \wcNtype{\Delta_c}{N}\ \texttt{in} \ \texttt{x}.\texttt{f}$
We now show % We now show
$\Delta|\Gamma \vdash \texttt{let}\ \texttt{x} = \texttt{e} : \wcNtype{\Delta_c}{N}\ \texttt{in} \ \texttt{x}.\texttt{f} : \sigma(a)$ % $\Delta|\Gamma \vdash \texttt{let}\ \texttt{x} = \texttt{e} : \wcNtype{\Delta_c}{N}\ \texttt{in} \ \texttt{x}.\texttt{f} : \sigma(a)$
by the T-Field rule. % by the T-Field rule.
$\Delta \vdash \wcNtype{\Delta_c}{N} <: \wcNtype{\Delta_c}{N}$ by S-Refl. % $\Delta \vdash \wcNtype{\Delta_c}{N} <: \wcNtype{\Delta_c}{N}$ by S-Refl.
$\Delta, \Delta_c \vdash \type{U}_i <: \sigma(\tv{a})$, % $\Delta, \Delta_c \vdash \type{U}_i <: \sigma(\tv{a})$,
because of the constraint $[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a}$ and lemma \ref{lemma:unifySoundness}. % because of the constraint $[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a}$ and lemma \ref{lemma:unifySoundness}.
$\textit{fields}(\sigma(\exptype{C}{\overline{\wtv{a}}})) = \sigma([\overline{\wtv{a}}/\ol{X}]\type{T})$ % $\textit{fields}(\sigma(\exptype{C}{\overline{\wtv{a}}})) = \sigma([\overline{\wtv{a}}/\ol{X}]\type{T})$
and $\text{fv}(\type{U}_i) \subseteq \text{fv}(\type{N})$ by definition of $\textit{fields}$. % and $\text{fv}(\type{U}_i) \subseteq \text{fv}(\type{N})$ by definition of $\textit{fields}$.
$\text{dom}(\Delta_c) \subseteq \text{fv}{\type{N}}$ by lemma \ref{lemma:tvsNoFV}. % $\text{dom}(\Delta_c) \subseteq \text{fv}{\type{N}}$ by lemma \ref{lemma:tvsNoFV}.
% X.List<X> <. List<a?> % X.List<X> <. List<a?>
% $\sigma(\ol{\tv{r}}) = \overline{\wcNtype{\Delta}{N}}$, % $\sigma(\ol{\tv{r}}) = \overline{\wcNtype{\Delta}{N}}$,
@ -183,55 +194,65 @@ By structural induction over the expression $\texttt{e}$.
% %Easy, because unify only generates substitutions for normal type placeholders which are OK % %Easy, because unify only generates substitutions for normal type placeholders which are OK
\item[$\texttt{e}.\texttt{m}(\ol{e})$] \item[$\texttt{e}.\texttt{m}(\ol{e})$]
Lets have a look at the case where the receiver and parameter types are all named types. Proof is analog to field access, except the $\Delta \vdash \ol{S}\ \ok$ premise.
So $\sigma(\ol{\tv{r}}) = \ol{T} = \ol{\wcNtype{\Delta_u}{N}}$ and $\sigma(\tv{r}) = \type{T}_r = \wcNtype{\Delta_u}{N}$ We know that $\unify{}(\Delta, [\overline{\wtv{b}}/\ol{Y}]\set{
and a $\Delta'$, $\overline{\Delta}$ where $\Delta' \subseteq \Delta_u$, $\overline{\Delta \subseteq \Delta_u}$ \ol{\tv{e}} \lessdotCC \ol{T}, \type{T} \lessdot \tv{a},
and $\text{dom}(\Delta') = (\text{fv}(\type{N})/\Delta)$, $\overline{\text{dom}(\Delta) = (\text{fv}(\type{N})/\Delta)}$ in \ol{Y} \lessdot \ol{N} } \cup C) = (\Delta', \sigma)$
and if we assume $\sigma(\ol{\tv{e}}) = \ol{\wcNtype{\Delta}{N'}}$
then the call to $\unify{}(\Delta \cup \overline{\Delta}, [\overline{\ntv{b}}/\ol{Y}]\set{
\ol{N'} \lessdot \ol{T}, \type{T} \lessdot \tv{a},
\ol{Y} \lessdot \ol{N} } \cup C)$ succeeds with $\overline{\ntv{b}}$ being normal placeholders this time,
which proofs $\Delta \vdash \ol{S}\ \ok$ via lemma \ref{lemma:unifyWellFormedness}.
%TODO: why does this call succeed?
% Lets have a look at the case where the receiver and parameter types are all named types.
% So $\sigma(\ol{\tv{r}}) = \ol{T} = \ol{\wcNtype{\Delta_u}{N}}$ and $\sigma(\tv{r}) = \type{T}_r = \wcNtype{\Delta_u}{N}$
% and a $\Delta'$, $\overline{\Delta}$ where $\Delta' \subseteq \Delta_u$, $\overline{\Delta \subseteq \Delta_u}$
% and $\text{dom}(\Delta') = (\text{fv}(\type{N})/\Delta)$, $\overline{\text{dom}(\Delta) = (\text{fv}(\type{N})/\Delta)}$ in
$\texttt{let}\ \texttt{x} : \wcNtype{\Delta'}{N} = \texttt{e} \ \texttt{in}\ % $\texttt{let}\ \texttt{x} : \wcNtype{\Delta'}{N} = \texttt{e} \ \texttt{in}\
\texttt{let}\ \ol{x} : \overline{\wcNtype{\Delta'}{N}} = \ol{e} \ \texttt{in}\ \texttt{x}.\texttt{m}(\ol{x})$ % \texttt{let}\ \ol{x} : \overline{\wcNtype{\Delta'}{N}} = \ol{e} \ \texttt{in}\ \texttt{x}.\texttt{m}(\ol{x})$
%TODO: show that this type exists \wcNtype{\Delta'}{N} (a \Delta' which only contains free variables of the type N) % %TODO: show that this type exists \wcNtype{\Delta'}{N} (a \Delta' which only contains free variables of the type N)
% and which is a supertype of T_r (so no free variables in T_r) % % and which is a supertype of T_r (so no free variables in T_r)
% Solution: Make this a lemma and guarantee that Unify does only create types Delta.T with \Delta subset fv(T) % % Solution: Make this a lemma and guarantee that Unify does only create types Delta.T with \Delta subset fv(T)
% This is possible because free variables (except those in \Delta_in) are never used in wildcard environments % % This is possible because free variables (except those in \Delta_in) are never used in wildcard environments
%By lemma \ref{lemma:unifyWeakening} % %By lemma \ref{lemma:unifyWeakening}
We know that % We know that
$\unify{}(\Delta, [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}/\ol{Y}]\set{ \overline{\wcNtype{\Delta}{N}} \lessdotCC \ol{T}, \wcNtype{\Delta'}{N} \lessdotCC \exptype{C}{\ol{X}}})$ % $\unify{}(\Delta, [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}/\ol{Y}]\set{ \overline{\wcNtype{\Delta}{N}} \lessdotCC \ol{T}, \wcNtype{\Delta'}{N} \lessdotCC \exptype{C}{\ol{X}}})$
has a solution. % has a solution.
Also $\overline{\wcNtype{\Delta}{N}} \lessdot \ol{T}$ and $\wcNtype{\Delta'}{N} \lessdotCC \exptype{C}{\ol{X}}$ will be converted to % Also $\overline{\wcNtype{\Delta}{N}} \lessdot \ol{T}$ and $\wcNtype{\Delta'}{N} \lessdotCC \exptype{C}{\ol{X}}$ will be converted to
$\ol{N} \lessdot \ol{T}$ and $\type{N} \lessdot \exptype{C}{\ol{X}}$ by the \rulename{Capture} rule. % $\ol{N} \lessdot \ol{T}$ and $\type{N} \lessdot \exptype{C}{\ol{X}}$ by the \rulename{Capture} rule.
Which then results in the same as calling $\unify{}((\Delta, \Delta', \overline{\Delta}), [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}/\ol{Y}]\set{\ol{N} \lessdot \ol{T}, \type{N} \lessdot \exptype{C}{\ol{X}}})$, % Which then results in the same as calling $\unify{}((\Delta, \Delta', \overline{\Delta}), [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}/\ol{Y}]\set{\ol{N} \lessdot \ol{T}, \type{N} \lessdot \exptype{C}{\ol{X}}})$,
which shows $\Delta, \Delta', \overline{\Delta} \vdash \overline{N} <: [\ol{S}/\ol{X}]\overline{U}$. % which shows $\Delta, \Delta', \overline{\Delta} \vdash \overline{N} <: [\ol{S}/\ol{X}]\overline{U}$.
This implies $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ and $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ % This implies $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ and $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$
$\Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T}$, % $\Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T}$,
$\Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U}$, % $\Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U}$,
and $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}$ % and $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}$
are guaranteed by the generated constraints and lemma \ref{lemma:unifySoundness}.% and \ref{lemma:unifyCC}. % are guaranteed by the generated constraints and lemma \ref{lemma:unifySoundness}.% and \ref{lemma:unifyCC}.
$\Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}$ due to $\ol{T} = \ol{\wcNtype{\Delta}{N}}$ and S-Refl. $\Delta, \Delta' \vdash \type{T}_r <: \wcNtype{\Delta'}{N}$ accordingly. % $\Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}$ due to $\ol{T} = \ol{\wcNtype{\Delta}{N}}$ and S-Refl. $\Delta, \Delta' \vdash \type{T}_r <: \wcNtype{\Delta'}{N}$ accordingly.
$\Delta|\Gamma \vdash \texttt{t}_r : \type{T}_r$ and $\Delta|\Gamma \vdash \ol{t} : \ol{T}_r$ by assumption. % $\Delta|\Gamma \vdash \texttt{t}_r : \type{T}_r$ and $\Delta|\Gamma \vdash \ol{t} : \ol{T}_r$ by assumption.
$\Delta, \Delta' \vdash \ol{\wcNtype{\Delta}{N}} \ \ok$ by lemma \ref{lemma:unifyWellFormedness}, % $\Delta, \Delta' \vdash \ol{\wcNtype{\Delta}{N}} \ \ok$ by lemma \ref{lemma:unifyWellFormedness},
therefore $\Delta, \Delta', \overline{\Delta} \vdash \ol{N} \ \ok$, which implies $\Delta, \Delta', \overline{\Delta} \vdash \ol{U} \ \ok$ % therefore $\Delta, \Delta', \overline{\Delta} \vdash \ol{N} \ \ok$, which implies $\Delta, \Delta', \overline{\Delta} \vdash \ol{U} \ \ok$
%by lemma \ref{lemma:wfHereditary} % %by lemma \ref{lemma:wfHereditary}
and $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok $ by premise of WF-Class. % and $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok $ by premise of WF-Class.
The same goes for $\wcNtype{\Delta'}{N}$. % The same goes for $\wcNtype{\Delta'}{N}$.
% \begin{gather} % % \begin{gather}
% \label{sp:0} % % \label{sp:0}
% \Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T} \\ % % \Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T} \\
% \label{sp:1} % % \label{sp:1}
% \Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U} \\ % % \Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U} \\
% \label{sp:2} % % \label{sp:2}
% \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'} \\ % % \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'} \\
% \label{sp:3} % % \label{sp:3}
% \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \\ % % \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \\
% \label{sp:4} % % \label{sp:4}
% \Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}} % % \Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}
% \end{gather} % % \end{gather}
Method calls generate multiple constraints that share the same wildcard placeholders ($\ol{\wtv{a}}$, $\ol{\wtv{b}}$). % Method calls generate multiple constraints that share the same wildcard placeholders ($\ol{\wtv{a}}$, $\ol{\wtv{b}}$).
\end{description} \end{description}
@ -333,15 +354,14 @@ Trivial. \unify{} fails when a constraint $\tv{a} \doteq \rwildcard{X}$ arises.
% Delta |- N <. T % Delta |- N <. T
% \end{lemma} % \end{lemma}
\begin{lemma}\label{lemma:wildcardsStayInScope} % \begin{lemma}\label{lemma:wildcardsStayInScope}
Free variables can only hop to another constraint if they share the same wildcard placeholder. % Free variables can only hop to another constraint if they share the same wildcard placeholder.
\begin{description} % \begin{description}
\item[If] $(\sigma, \Delta) = \unify{} (\Delta', C \cup \set{\wcNtype{\Delta'}{N} \lessdot \tv{a}})$ % \item[If] $(\sigma, \Delta) = \unify{} (\Delta', C \cup \set{\wcNtype{\Delta'}{N} \lessdot \tv{a}})$
\item[and] $\tv{a}$ being a type placeholders used in $C$ % \item[and] $\tv{a}$ being a type placeholders used in $C$
\item[then] $\text{fv}(\sigma(\tv{a})) \subseteq \Delta, \Delta'$ % \item[then] $\text{fv}(\sigma(\tv{a})) \subseteq \Delta, \Delta'$
\end{description} % \end{description}
If $\wcNtype{\Delta'}{N} \lessdot \tv{a}$ % \end{lemma}
\end{lemma}