Fix some binding unification bugs

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;
 	}
 

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]);
+			}
 		}
 	});