fix: unify infix expressions by isolating unbound type variables

compiler/noirc_frontend/src/hir_def/types.rs

@@ -1983,13 +1983,16 @@
 
                     if lhs_result.is_ok() && rhs_result.is_ok() {
                         *bindings = new_bindings;
-                        Ok(())
+                        return Ok(());
                     } else {
-                        lhs.try_unify_by_moving_constant_terms(&rhs, bindings)
+                        let result = lhs.try_unify_by_moving_constant_terms(&rhs, bindings);
+                        if result.is_ok() {
+                            return Ok(());
+                        }
                     }
-                } else {
-                    Err(UnificationError)
                 }
+
+                lhs.try_unify_by_isolating_an_unbound_type_variable(&rhs, bindings)
             }
 
             (Constant(value, kind), other) | (other, Constant(value, kind)) => {
@@ -2437,7 +2440,7 @@
         }
 
         let recur_on_binding = |id, replacement: &Type| {
             // Prevent recuring forever if there's a `T := T` binding
             if replacement.type_variable_id() == Some(id) {
                 replacement.clone()
             } else {
@@ -2523,7 +2526,7 @@
                 Type::Tuple(fields)
             }
             Type::Forall(typevars, typ) => {
                 // Trying to substitute_helper a variable de, substitute_bound_typevarsfined within a nested Forall
                 // is usually impossible and indicative of an error in the type checker somewhere.
                 for var in typevars {
                     assert!(!type_bindings.contains_key(&var.id()));
@@ -2690,7 +2693,7 @@
         }
     }
 
     /// Follow bindings if this is a type variable or generic to the first non-typevariable
     /// type. Unlike `follow_bindings`, this won't recursively follow any bindings on any
     /// fields or arguments of this type.
     pub fn follow_bindings_shallow(&self) -> Cow<Type> {
@@ -2715,7 +2718,7 @@
 
     /// Replace any `Type::NamedGeneric` in this type with a `Type::TypeVariable`
     /// using to the same inner `TypeVariable`. This is used during monomorphization
     /// to bind to named generics since they are unbindable during type checking.
     pub fn replace_named_generics_with_type_variables(&mut self) {
         match self {
             Type::FieldElement
@@ -3265,7 +3268,7 @@
                 len.hash(state);
                 env.hash(state);
             }
             Type::Tuple(elems) => elems.hash(state),
             Type::DataType(def, args) => {
                 def.hash(state);
                 args.hash(state);

compiler/noirc_frontend/src/hir_def/types/arithmetic.rs

@@ -374,6 +374,99 @@ impl Type {
 
         Err(UnificationError)
     }
+
+    /// Try to unify the following equations:
+    /// - `A + rhs = other` -> `A = other - rhs`
+    /// - `A - rhs = other` -> `A = other + rhs`
+    /// - `lhs + B = other` -> `B = other - lhs`
+    /// - `lhs - B = other` -> `B = lhs - other`
+    /// - `other = A + rhs` -> `A = other - rhs`
+    /// - `other = A - rhs` -> `A = other + rhs`
+    /// - `other = lhs + B` -> `B = other - lhs`
+    /// - `other = lhs - B` -> `B = lhs - other`
+    pub(super) fn try_unify_by_isolating_an_unbound_type_variable(
+        &self,
+        other: &Type,
+        bindings: &mut TypeBindings,
+    ) -> Result<(), UnificationError> {
+        self.try_unify_by_isolating_an_unbound_type_variable_in_self(other, bindings).or_else(
+            |_| other.try_unify_by_isolating_an_unbound_type_variable_in_self(self, bindings),
+        )
+    }
+
+    /// Try to unify the following equations:
+    /// - `A + rhs = other` -> `A = other - rhs`
+    /// - `A - rhs = other` -> `A = other + rhs`
+    /// - `lhs + B = other` -> `B = other - lhs`
+    /// - `lhs - B = other` -> `B = lhs - other`
+    fn try_unify_by_isolating_an_unbound_type_variable_in_self(
+        &self,
+        other: &Type,
+        bindings: &mut TypeBindings,
+    ) -> Result<(), UnificationError> {
+        if let Type::InfixExpr(lhs_lhs, lhs_op, lhs_rhs, _) = self {
+            let lhs_op_inverse = lhs_op.inverse();
+
+            // Check if it's `A + rhs = other` or `A - rhs = other`
+            if let (Some(op_a_inverse), Type::TypeVariable(lhs_lhs_var)) =
+                (lhs_op_inverse, lhs_lhs.as_ref())
+            {
+                if lhs_lhs_var.1.borrow().is_unbound() {
+                    // We can say that `A = other - rhs` or `A = other + rhs` respectively
+                    let new_rhs =
+                        Type::infix_expr(Box::new(other.clone()), op_a_inverse, lhs_rhs.clone());
+
+                    let mut tmp_bindings = bindings.clone();
+                    if lhs_lhs.try_unify(&new_rhs, &mut tmp_bindings).is_ok() {
+                        *bindings = tmp_bindings;
+                        return Ok(());
+                    }
+                }
+            }
+
+            // Check if it's `lhs + B = other`
+            if let (BinaryTypeOperator::Addition, Type::TypeVariable(lhs_rhs_var)) =
+                (lhs_op, lhs_rhs.as_ref())
+            {
+                if lhs_rhs_var.1.borrow().is_unbound() {
+                    // We can say that `B = other - lhs`
+                    let new_rhs = Type::infix_expr(
+                        Box::new(other.clone()),
+                        BinaryTypeOperator::Subtraction,
+                        lhs_lhs.clone(),
+                    );
+
+                    let mut tmp_bindings = bindings.clone();
+                    if lhs_rhs.try_unify(&new_rhs, &mut tmp_bindings).is_ok() {
+                        *bindings = tmp_bindings;
+                        return Ok(());
+                    }
+                }
+            }
+
+            // Check if it's `lhs - B = other`
+            if let (BinaryTypeOperator::Subtraction, Type::TypeVariable(lhs_rhs_var)) =
+                (lhs_op, lhs_rhs.as_ref())
+            {
+                if lhs_rhs_var.1.borrow().is_unbound() {
+                    // We can say that `B = lhs - other`
+                    let new_rhs = Type::infix_expr(
+                        lhs_lhs.clone(),
+                        BinaryTypeOperator::Subtraction,
+                        Box::new(other.clone()),
+                    );
+
+                    let mut tmp_bindings = bindings.clone();
+                    if lhs_rhs.try_unify(&new_rhs, &mut tmp_bindings).is_ok() {
+                        *bindings = tmp_bindings;
+                        return Ok(());
+                    }
+                }
+            }
+        }
+
+        Err(UnificationError)
+    }
 }
 
 #[cfg(test)]

compiler/noirc_frontend/src/tests/traits.rs

@@ -1633,7 +1633,8 @@ fn accesses_associated_type_inside_trait_using_self() {
 #[test]
 fn serialize_test_with_a_previous_unrelated_definition() {
     let src = r#"
-    // If you remove this Trait definition, the code compiles fine. That's the bug.
+    // There used to be a bug where this unrelated definition would cause compilation to fail
+    // with a "No impl found" error.
     pub trait Trait {}
 
     trait Serialize {
@@ -1651,8 +1652,6 @@ fn serialize_test_with_a_previous_unrelated_definition() {
 
         fn serialize(self: Self) {
             self.0.serialize();
-            ^^^^^^^^^^^^^^^^ No matching impl found for `(Field, Field): Serialize<Size = (3 - _)>`
-            ~~~~~~~~~~~~~~~~ No impl for `(Field, Field): Serialize<Size = (3 - _)>`
         }
     }
 
@@ -1667,8 +1666,5 @@ fn serialize_test_with_a_previous_unrelated_definition() {
         x.serialize();
     }
     "#;
-
-    // In reality there should be no error here, so any error squiggles should be removed.
-    // See https://github.com/noir-lang/noir/issues/8780
     check_monomorphization_error!(&src);
 }

test_programs/compile_failure/noirc_frontend_tests_traits_serialize_test_with_a_previous_unrelated_definition/src/main.nr → test_programs/compile_success_no_bug/noirc_frontend_tests_traits_serialize_test_with_a_previous_unrelated_definition/src/main.nr

@@ -1,5 +1,6 @@
 
-    // If you remove this Trait definition, the code compiles fine. That's the bug.
+    // There used to be a bug where this unrelated definition would cause compilation to fail
+    // with a "No impl found" error.
     pub trait Trait {}
 
     trait Serialize {

test_programs/compile_success_no_bug/noirc_frontend_tests_traits_serialize_test_with_a_previous_unrelated_definition/src_hash.txt

@@ -0,0 +1 @@
+2680920423078649375