From a0d98b9403ea5a455ba6eac89b1d2e09e3aa9290 Mon Sep 17 00:00:00 2001
From: Andreas Stadelmeier <andi@paulus.haus>
Date: Tue, 13 Feb 2024 18:40:39 +0100
Subject: [PATCH] Make match rule remember constraint type

---
 unify.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/unify.tex b/unify.tex
index c648428..797d2a7 100644
--- a/unify.tex
+++ b/unify.tex
@@ -370,16 +370,16 @@ Their upper and lower bounds are fresh type variables.
           \begin{array}[c]{@{}ll}
           \begin{array}[c]{l}
              \wildcardEnv \vdash C \cup \, \set{
-                \tv{a} \lessdot \wctype{\Delta}{D}{\ol{T}}, \tv{a} \lessdot \wctype{\Delta'}{D'}{\ol{T'}} }\\ 
+                \tv{a} \lessdot_1 \wctype{\Delta}{D}{\ol{T}}, \tv{a} \lessdot_2 \wctype{\Delta'}{D'}{\ol{T'}} }\\ 
             \hline
             \vspace*{-0.4cm}\\
 \wildcardEnv \vdash C \cup \, \left\{ \begin{array}[c]{l}
                 \tv{a} \lessdot \wctype{\overline{\wildcard{A}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{A}}},
               \ol{\tv{l}} \lessdot \ol{\tv{u}}, \\
             \wctype{\overline{\wildcard{A}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{A}}}
-                     \lessdot \wctype{\Delta}{D}{\ol{T}}, \\
+                     \lessdot_1 \wctype{\Delta}{D}{\ol{T}}, \\
             \wctype{\overline{\wildcard{A}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{A}}}
-                     \lessdot \wctype{\Delta'}{D'}{\ol{T'}}
+                     \lessdot_2 \wctype{\Delta'}{D'}{\ol{T'}}
 \end{array}
 \right\}
           \end{array}