From f0e9af1cf57b009857da24eaf6a34920fba97adb Mon Sep 17 00:00:00 2001
From: James Shubin <james@shubin.ca>
Date: Sun, 20 Aug 2023 20:29:24 -0400
Subject: [PATCH] lang: unification: Add partial knowledge to solved

When we were running our partial unification to compare similar looking
function invariants, we would sometimes learn new information, even if
it didn't entirely solve that invariant. When this new information was
learned, it's important that we globally mark it as solved so that
others can use it to complete their invariants. When it was a critical
piece of information, this would result in new information, which would
eventually lead to that original partial invariant that we learned that
information from to becoming solved.
---
 lang/unification/simplesolver.go | 40 ++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)

diff --git a/lang/unification/simplesolver.go b/lang/unification/simplesolver.go
index 7a4e5f6f..98b8bc2f 100644
--- a/lang/unification/simplesolver.go
+++ b/lang/unification/simplesolver.go
@@ -636,6 +636,16 @@ Loop:
 							typ, exists := funcPartials[eq.Expr1][rhsExpr]
 							if !exists {
 								funcPartials[eq.Expr1][rhsExpr] = lhsTyp // learn!
+
+								// Even though this is only a partial learn, we should still add it to the solved information!
+								if newTyp, exists := solved[rhsExpr]; !exists {
+									solved[rhsExpr] = lhsTyp // yay, we learned something!
+									//used = append(used, i) // mark equality as used up when complete!
+									logf("%s: solved partial rhs func arg equality", Name)
+								} else if err := newTyp.Cmp(lhsTyp); err != nil {
+									return nil, errwrap.Wrapf(err, "can't unify, invariant illogicality with partial rhs func arg equality")
+								}
+
 								continue
 							}
 							if err := typ.Cmp(lhsTyp); err != nil {
@@ -646,6 +656,16 @@ Loop:
 							typ, exists := funcPartials[eq.Expr1][lhsExpr]
 							if !exists {
 								funcPartials[eq.Expr1][lhsExpr] = rhsTyp // learn!
+
+								// Even though this is only a partial learn, we should still add it to the solved information!
+								if newTyp, exists := solved[lhsExpr]; !exists {
+									solved[lhsExpr] = rhsTyp // yay, we learned something!
+									//used = append(used, i) // mark equality as used up when complete!
+									logf("%s: solved partial lhs func arg equality", Name)
+								} else if err := newTyp.Cmp(rhsTyp); err != nil {
+									return nil, errwrap.Wrapf(err, "can't unify, invariant illogicality with partial lhs func arg equality")
+								}
+
 								continue
 							}
 							if err := typ.Cmp(rhsTyp); err != nil {
@@ -665,6 +685,16 @@ Loop:
 						typ, exists := funcPartials[eq.Expr1][rhsExpr]
 						if !exists {
 							funcPartials[eq.Expr1][rhsExpr] = lhsTyp // learn!
+
+							// Even though this is only a partial learn, we should still add it to the solved information!
+							if newTyp, exists := solved[rhsExpr]; !exists {
+								solved[rhsExpr] = lhsTyp // yay, we learned something!
+								//used = append(used, i) // mark equality as used up when complete!
+								logf("%s: solved partial rhs func return equality", Name)
+							} else if err := newTyp.Cmp(lhsTyp); err != nil {
+								return nil, errwrap.Wrapf(err, "can't unify, invariant illogicality with partial rhs func return equality")
+							}
+
 							continue
 						}
 						if err := typ.Cmp(lhsTyp); err != nil {
@@ -675,6 +705,16 @@ Loop:
 						typ, exists := funcPartials[eq.Expr1][lhsExpr]
 						if !exists {
 							funcPartials[eq.Expr1][lhsExpr] = rhsTyp // learn!
+
+							// Even though this is only a partial learn, we should still add it to the solved information!
+							if newTyp, exists := solved[lhsExpr]; !exists {
+								solved[lhsExpr] = rhsTyp // yay, we learned something!
+								//used = append(used, i) // mark equality as used up when complete!
+								logf("%s: solved partial lhs func return equality", Name)
+							} else if err := newTyp.Cmp(rhsTyp); err != nil {
+								return nil, errwrap.Wrapf(err, "can't unify, invariant illogicality with partial lhs func return equality")
+							}
+
 							continue
 						}
 						if err := typ.Cmp(rhsTyp); err != nil {