From 444af3d5b15dfe86456de4a651a3f3f9098ca350 Mon Sep 17 00:00:00 2001
From: Robin <robin@robin.town>
Date: Mon, 4 Sep 2023 16:31:27 -0400
Subject: [PATCH] Fix some binding unification bugs

---
 src/semantics/denote.ts     | 21 +++++++++--------
 src/semantics/operations.ts | 46 ++++++++++++++++++++++++-------------
 2 files changed, 41 insertions(+), 26 deletions(-)

diff --git a/src/semantics/denote.ts b/src/semantics/denote.ts
index 83d945c..dbd89e2 100644
--- a/src/semantics/denote.ts
+++ b/src/semantics/denote.ts
@@ -582,16 +582,17 @@ function functionalApplication_(
 	} else if (argument.denotation === null) {
 		({ denotation, bindings } = fn);
 	} else {
-		const [f, a, b] = unifyDenotations(
-			fn,
-			typesEqual(
-				(fn.denotation.type as [ExprType, ExprType])[0],
-				argument.denotation.type,
-			)
-				? argument
-				: makeWorldExplicit(argument),
-		);
-		denotation = reduce(app(f, a));
+		const compatibleArgument = typesEqual(
+			(fn.denotation.type as [ExprType, ExprType])[0],
+			argument.denotation.type,
+		)
+			? argument
+			: makeWorldExplicit(argument);
+		const [l, r, b] =
+			fn === left
+				? unifyDenotations(fn, compatibleArgument)
+				: unifyDenotations(compatibleArgument, fn);
+		denotation = reduce(fn === left ? app(l, r) : app(r, l));
 		bindings = b;
 	}
 
diff --git a/src/semantics/operations.ts b/src/semantics/operations.ts
index 7379b3d..0f241d7 100644
--- a/src/semantics/operations.ts
+++ b/src/semantics/operations.ts
@@ -340,23 +340,37 @@ export function unifyDenotations(
 
 	// For each binding referenced in the right subtree
 	forEachBinding(right.bindings, (rb, getter, setter) => {
-		// If there is a matching binding in the left subtree
-		const lb = getter(left.bindings);
-		if (lb !== undefined) {
-			// Then unify the variables
-			setter(bindings, {
-				index: lb.index,
-				subordinate: lb.subordinate && rb.subordinate,
-			});
-			rightMapping[rb.index] = lb.index;
+		// If this variable has already been resolved
+		const resolvedIndex = rightMapping[rb.index];
+		if (resolvedIndex !== undefined) {
+			// Then, as long as no bindings from the left subtree override this binding,
+			// keep it
+			const b = getter(bindings);
+			if (b === undefined || b.index === resolvedIndex) {
+				setter(bindings, {
+					index: resolvedIndex,
+					subordinate: (b?.subordinate ?? true) && rb.subordinate,
+				});
+			}
 		} else {
-			// Otherwise, create a new variable
-			setter(bindings, {
-				index: context.length,
-				subordinate: rightSubordinate || rb.subordinate,
-			});
-			rightMapping[rb.index] = context.length;
-			context.push(right.denotation!.context[rb.index]);
+			// Otherwise, if there is a matching binding in the left subtree
+			const lb = getter(left.bindings);
+			if (lb !== undefined) {
+				// Then unify the variables
+				setter(bindings, {
+					index: lb.index,
+					subordinate: lb.subordinate && rb.subordinate,
+				});
+				rightMapping[rb.index] = lb.index;
+			} else {
+				// Otherwise, create a new variable
+				setter(bindings, {
+					index: context.length,
+					subordinate: rightSubordinate || rb.subordinate,
+				});
+				rightMapping[rb.index] = context.length;
+				context.push(right.denotation!.context[rb.index]);
+			}
 		}
 	});