diff --git a/compiler/noirc_frontend/src/hir/def_collector/dc_crate.rs b/compiler/noirc_frontend/src/hir/def_collector/dc_crate.rs
index e87ef34088d..b1e559895b8 100644
--- a/compiler/noirc_frontend/src/hir/def_collector/dc_crate.rs
+++ b/compiler/noirc_frontend/src/hir/def_collector/dc_crate.rs
@@ -474,18 +474,18 @@ pub(crate) fn check_methods_signatures(
     let trait_methods = std::mem::take(&mut the_trait.methods);
 
     for (file_id, func_id) in impl_methods {
-        let impl_method = resolver.interner.function_meta(func_id);
         let func_name = resolver.interner.function_name(func_id).to_owned();
 
-        let mut typecheck_errors = Vec::new();
-
         // This is None in the case where the impl block has a method that's not part of the trait.
         // If that's the case, a `MethodNotInTrait` error has already been thrown, and we can ignore
         // the impl method, since there's nothing in the trait to match its signature against.
         if let Some(trait_method) =
             trait_methods.iter().find(|method| method.name.0.contents == func_name)
         {
-            let impl_function_type = impl_method.typ.instantiate(resolver.interner);
+            let mut typecheck_errors = Vec::new();
+            let impl_method = resolver.interner.function_meta(func_id);
+
+            let (impl_function_type, _) = impl_method.typ.instantiate(resolver.interner);
 
             let impl_method_generic_count =
                 impl_method.typ.generic_count() - trait_impl_generic_count;
@@ -505,7 +505,7 @@ pub(crate) fn check_methods_signatures(
                 errors.push((error.into(), *file_id));
             }
 
-            if let Type::Function(impl_params, _, _) = impl_function_type.0 {
+            if let Type::Function(impl_params, _, _) = impl_function_type {
                 if trait_method.arguments().len() == impl_params.len() {
                     // Check the parameters of the impl method against the parameters of the trait method
                     let args = trait_method.arguments().iter();
diff --git a/compiler/noirc_frontend/src/hir_def/traits.rs b/compiler/noirc_frontend/src/hir_def/traits.rs
index 7bf5870e1f5..bbe4e1743d2 100644
--- a/compiler/noirc_frontend/src/hir_def/traits.rs
+++ b/compiler/noirc_frontend/src/hir_def/traits.rs
@@ -65,6 +65,7 @@ pub struct Trait {
     pub self_type_typevar_id: TypeVariableId,
     pub self_type_typevar: TypeVariable,
 }
+
 #[derive(Debug)]
 pub struct TraitImpl {
     pub ident: Ident,
diff --git a/compiler/noirc_frontend/src/hir_def/types.rs b/compiler/noirc_frontend/src/hir_def/types.rs
index 977293ec678..9a9c0c047d1 100644
--- a/compiler/noirc_frontend/src/hir_def/types.rs
+++ b/compiler/noirc_frontend/src/hir_def/types.rs
@@ -1,4 +1,5 @@
 use std::{
+    borrow::Cow,
     cell::RefCell,
     collections::{BTreeSet, HashMap},
     rc::Rc,
@@ -299,7 +300,7 @@ impl std::fmt::Display for TypeAliasType {
         write!(f, "{}", self.name)?;
 
         if !self.generics.is_empty() {
-            let generics = vecmap(&self.generics, |(_, binding)| binding.0.borrow().to_string());
+            let generics = vecmap(&self.generics, |(_, binding)| binding.borrow().to_string());
             write!(f, "{}", generics.join(", "))?;
         }
 
@@ -415,11 +416,11 @@ pub enum TypeVariableKind {
 /// A TypeVariable is a mutable reference that is either
 /// bound to some type, or unbound with a given TypeVariableId.
 #[derive(Debug, PartialEq, Eq, Clone, Hash)]
-pub struct TypeVariable(Shared<TypeBinding>);
+pub struct TypeVariable(TypeVariableId, Shared<TypeBinding>);
 
 impl TypeVariable {
     pub fn unbound(id: TypeVariableId) -> Self {
-        TypeVariable(Shared::new(TypeBinding::Unbound(id)))
+        TypeVariable(id, Shared::new(TypeBinding::Unbound(id)))
     }
 
     /// Bind this type variable to a value.
@@ -428,7 +429,7 @@ impl TypeVariable {
     /// Also Panics if the ID of this TypeVariable occurs within the given
     /// binding, as that would cause an infinitely recursive type.
     pub fn bind(&self, typ: Type) {
-        let id = match &*self.0.borrow() {
+        let id = match &*self.1.borrow() {
             TypeBinding::Bound(binding) => {
                 unreachable!("TypeVariable::bind, cannot bind bound var {} to {}", binding, typ)
             }
@@ -436,11 +437,11 @@ impl TypeVariable {
         };
 
         assert!(!typ.occurs(id));
-        *self.0.borrow_mut() = TypeBinding::Bound(typ);
+        *self.1.borrow_mut() = TypeBinding::Bound(typ);
     }
 
     pub fn try_bind(&self, binding: Type, span: Span) -> Result<(), TypeCheckError> {
-        let id = match &*self.0.borrow() {
+        let id = match &*self.1.borrow() {
             TypeBinding::Bound(binding) => {
                 unreachable!("Expected unbound, found bound to {binding}")
             }
@@ -450,28 +451,28 @@ impl TypeVariable {
         if binding.occurs(id) {
             Err(TypeCheckError::TypeAnnotationsNeeded { span })
         } else {
-            *self.0.borrow_mut() = TypeBinding::Bound(binding);
+            *self.1.borrow_mut() = TypeBinding::Bound(binding);
             Ok(())
         }
     }
 
     /// Borrows this TypeVariable to (e.g.) manually match on the inner TypeBinding.
     pub fn borrow(&self) -> std::cell::Ref<TypeBinding> {
-        self.0.borrow()
+        self.1.borrow()
     }
 
     /// Unbind this type variable, setting it to Unbound(id).
     ///
     /// This is generally a logic error to use outside of monomorphization.
     pub fn unbind(&self, id: TypeVariableId) {
-        *self.0.borrow_mut() = TypeBinding::Unbound(id);
+        *self.1.borrow_mut() = TypeBinding::Unbound(id);
     }
 
     /// Forcibly bind a type variable to a new type - even if the type
     /// variable is already bound to a different type. This generally
     /// a logic error to use outside of monomorphization.
     pub fn force_bind(&self, typ: Type) {
-        *self.0.borrow_mut() = TypeBinding::Bound(typ);
+        *self.1.borrow_mut() = TypeBinding::Bound(typ);
     }
 }
 
@@ -503,7 +504,7 @@ impl Type {
     }
 
     pub fn type_variable(id: TypeVariableId) -> Type {
-        let var = TypeVariable(Shared::new(TypeBinding::Unbound(id)));
+        let var = TypeVariable::unbound(id);
         Type::TypeVariable(var, TypeVariableKind::Normal)
     }
 
@@ -512,14 +513,14 @@ impl Type {
     pub fn constant_variable(length: u64, interner: &mut NodeInterner) -> Type {
         let id = interner.next_type_variable_id();
         let kind = TypeVariableKind::Constant(length);
-        let var = TypeVariable(Shared::new(TypeBinding::Unbound(id)));
+        let var = TypeVariable::unbound(id);
         Type::TypeVariable(var, kind)
     }
 
     pub fn polymorphic_integer(interner: &mut NodeInterner) -> Type {
         let id = interner.next_type_variable_id();
         let kind = TypeVariableKind::IntegerOrField;
-        let var = TypeVariable(Shared::new(TypeBinding::Unbound(id)));
+        let var = TypeVariable::unbound(id);
         Type::TypeVariable(var, kind)
     }
 
@@ -529,7 +530,7 @@ impl Type {
     /// they shouldn't be bound over until monomorphization.
     pub fn is_bindable(&self) -> bool {
         match self {
-            Type::TypeVariable(binding, _) => match &*binding.0.borrow() {
+            Type::TypeVariable(binding, _) => match &*binding.borrow() {
                 TypeBinding::Bound(binding) => binding.is_bindable(),
                 TypeBinding::Unbound(_) => true,
             },
@@ -553,7 +554,7 @@ impl Type {
         // True if the given type is a NamedGeneric with the target_id
         let named_generic_id_matches_target = |typ: &Type| {
             if let Type::NamedGeneric(type_variable, _) = typ {
-                match &*type_variable.0.borrow() {
+                match &*type_variable.borrow() {
                     TypeBinding::Bound(_) => {
                         unreachable!("Named generics should not be bound until monomorphization")
                     }
@@ -653,7 +654,7 @@ impl Type {
         match self {
             Type::Forall(generics, _) => generics.len(),
             Type::TypeVariable(type_variable, _) | Type::NamedGeneric(type_variable, _) => {
-                match &*type_variable.0.borrow() {
+                match &*type_variable.borrow() {
                     TypeBinding::Bound(binding) => binding.generic_count(),
                     TypeBinding::Unbound(_) => 0,
                 }
@@ -668,6 +669,25 @@ impl Type {
         let polymorphic_type_vars = vecmap(type_bindings, |(id, (type_var, _))| (id, type_var));
         Type::Forall(polymorphic_type_vars, Box::new(self))
     }
+
+    /// Return this type as a monomorphic type - without a `Type::Forall` if there is one.
+    /// This is only a shallow check since Noir's type system prohibits `Type::Forall` anywhere
+    /// inside other types.
+    pub fn as_monotype(&self) -> &Type {
+        match self {
+            Type::Forall(_, typ) => typ.as_ref(),
+            other => other,
+        }
+    }
+
+    /// Return the generics and type within this `Type::Forall`.
+    /// Panics if `self` is not `Type::Forall`
+    pub fn unwrap_forall(&self) -> (Cow<Generics>, &Type) {
+        match self {
+            Type::Forall(generics, typ) => (Cow::Borrowed(generics), typ.as_ref()),
+            other => (Cow::Owned(Generics::new()), other),
+        }
+    }
 }
 
 impl std::fmt::Display for Type {
@@ -687,23 +707,23 @@ impl std::fmt::Display for Type {
                 Signedness::Signed => write!(f, "i{num_bits}"),
                 Signedness::Unsigned => write!(f, "u{num_bits}"),
             },
-            Type::TypeVariable(var, TypeVariableKind::Normal) => write!(f, "{}", var.0.borrow()),
+            Type::TypeVariable(var, TypeVariableKind::Normal) => write!(f, "{}", var.borrow()),
             Type::TypeVariable(binding, TypeVariableKind::IntegerOrField) => {
-                if let TypeBinding::Unbound(_) = &*binding.0.borrow() {
+                if let TypeBinding::Unbound(_) = &*binding.borrow() {
                     // Show a Field by default if this TypeVariableKind::IntegerOrField is unbound, since that is
                     // what they bind to by default anyway. It is less confusing than displaying it
                     // as a generic.
                     write!(f, "Field")
                 } else {
-                    write!(f, "{}", binding.0.borrow())
+                    write!(f, "{}", binding.borrow())
                 }
             }
             Type::TypeVariable(binding, TypeVariableKind::Constant(n)) => {
-                if let TypeBinding::Unbound(_) = &*binding.0.borrow() {
+                if let TypeBinding::Unbound(_) = &*binding.borrow() {
                     // TypeVariableKind::Constant(n) binds to Type::Constant(n) by default, so just show that.
                     write!(f, "{n}")
                 } else {
-                    write!(f, "{}", binding.0.borrow())
+                    write!(f, "{}", binding.borrow())
                 }
             }
             Type::Struct(s, args) => {
@@ -728,7 +748,7 @@ impl std::fmt::Display for Type {
             }
             Type::Unit => write!(f, "()"),
             Type::Error => write!(f, "error"),
-            Type::NamedGeneric(binding, name) => match &*binding.0.borrow() {
+            Type::NamedGeneric(binding, name) => match &*binding.borrow() {
                 TypeBinding::Bound(binding) => binding.fmt(f),
                 TypeBinding::Unbound(_) if name.is_empty() => write!(f, "_"),
                 TypeBinding::Unbound(_) => write!(f, "{name}"),
@@ -795,7 +815,7 @@ impl Type {
         target_length: u64,
         bindings: &mut TypeBindings,
     ) -> Result<(), UnificationError> {
-        let target_id = match &*var.0.borrow() {
+        let target_id = match &*var.borrow() {
             TypeBinding::Bound(_) => unreachable!(),
             TypeBinding::Unbound(id) => *id,
         };
@@ -814,7 +834,7 @@ impl Type {
             // A TypeVariable is less specific than a MaybeConstant, so we bind
             // to the other type variable instead.
             Type::TypeVariable(new_var, kind) => {
-                let borrow = new_var.0.borrow();
+                let borrow = new_var.borrow();
                 match &*borrow {
                     TypeBinding::Bound(typ) => {
                         typ.try_bind_to_maybe_constant(var, target_length, bindings)
@@ -862,7 +882,7 @@ impl Type {
         var: &TypeVariable,
         bindings: &mut TypeBindings,
     ) -> Result<(), UnificationError> {
-        let target_id = match &*var.0.borrow() {
+        let target_id = match &*var.borrow() {
             TypeBinding::Bound(_) => unreachable!(),
             TypeBinding::Unbound(id) => *id,
         };
@@ -875,7 +895,7 @@ impl Type {
                 Ok(())
             }
             Type::TypeVariable(self_var, TypeVariableKind::IntegerOrField) => {
-                let borrow = self_var.0.borrow();
+                let borrow = self_var.borrow();
                 match &*borrow {
                     TypeBinding::Bound(typ) => typ.try_bind_to_polymorphic_int(var, bindings),
                     // Avoid infinitely recursive bindings
@@ -887,7 +907,7 @@ impl Type {
                 }
             }
             Type::TypeVariable(binding, TypeVariableKind::Normal) => {
-                let borrow = binding.0.borrow();
+                let borrow = binding.borrow();
                 match &*borrow {
                     TypeBinding::Bound(typ) => typ.try_bind_to_polymorphic_int(var, bindings),
                     // Avoid infinitely recursive bindings
@@ -917,7 +937,7 @@ impl Type {
         var: &TypeVariable,
         bindings: &mut TypeBindings,
     ) -> Result<(), UnificationError> {
-        let target_id = match &*var.0.borrow() {
+        let target_id = match &*var.borrow() {
             TypeBinding::Bound(_) => unreachable!(),
             TypeBinding::Unbound(id) => *id,
         };
@@ -945,7 +965,7 @@ impl Type {
 
     fn get_inner_type_variable(&self) -> Option<Shared<TypeBinding>> {
         match self {
-            Type::TypeVariable(var, _) | Type::NamedGeneric(var, _) => Some(var.0.clone()),
+            Type::TypeVariable(var, _) | Type::NamedGeneric(var, _) => Some(var.1.clone()),
             _ => None,
         }
     }
@@ -1041,9 +1061,9 @@ impl Type {
             }
 
             (NamedGeneric(binding, _), other) | (other, NamedGeneric(binding, _))
-                if !binding.0.borrow().is_unbound() =>
+                if !binding.borrow().is_unbound() =>
             {
-                if let TypeBinding::Bound(link) = &*binding.0.borrow() {
+                if let TypeBinding::Bound(link) = &*binding.borrow() {
                     link.try_unify(other, bindings)
                 } else {
                     unreachable!("If guard ensures binding is bound")
@@ -1052,8 +1072,8 @@ impl Type {
 
             (NamedGeneric(binding_a, name_a), NamedGeneric(binding_b, name_b)) => {
                 // Bound NamedGenerics are caught by the check above
-                assert!(binding_a.0.borrow().is_unbound());
-                assert!(binding_b.0.borrow().is_unbound());
+                assert!(binding_a.borrow().is_unbound());
+                assert!(binding_b.borrow().is_unbound());
 
                 if name_a == name_b {
                     Ok(())
@@ -1101,7 +1121,7 @@ impl Type {
         // bind to the given type or not.
         bind_variable: impl FnOnce(&mut TypeBindings) -> Result<(), UnificationError>,
     ) -> Result<(), UnificationError> {
-        match &*type_variable.0.borrow() {
+        match &*type_variable.borrow() {
             // If it is already bound, unify against what it is bound to
             TypeBinding::Bound(link) => link.try_unify(self, bindings),
             TypeBinding::Unbound(id) => {
@@ -1245,7 +1265,7 @@ impl Type {
                     })
                     .collect();
 
-                let instantiated = typ.substitute(&replacements);
+                let instantiated = typ.force_substitute(&replacements);
                 (instantiated, replacements)
             }
             other => (other.clone(), HashMap::new()),
@@ -1314,7 +1334,7 @@ impl Type {
             }
             Type::Forall(_, typ) => typ.find_all_unbound_type_variables(type_variables),
             Type::TypeVariable(type_variable, _) | Type::NamedGeneric(type_variable, _) => {
-                match &*type_variable.0.borrow() {
+                match &*type_variable.borrow() {
                     TypeBinding::Bound(binding) => {
                         binding.find_all_unbound_type_variables(type_variables);
                     }
@@ -1332,64 +1352,106 @@ impl Type {
     /// given bindings if found. If a type variable is not found within
     /// the given TypeBindings, it is unchanged.
     pub fn substitute(&self, type_bindings: &TypeBindings) -> Type {
+        self.substitute_helper(type_bindings, false)
+    }
+
+    /// Forcibly substitute any type variables found within this type with the
+    /// given bindings if found. If a type variable is not found within
+    /// the given TypeBindings, it is unchanged.
+    ///
+    /// Compared to `substitute`, this function will also substitute any type variables
+    /// from type_bindings, even if they are bound in `self`. Since this can undo previous
+    /// bindings, this function should be avoided unless necessary. Currently, it is only
+    /// needed when handling bindings between trait methods and their corresponding impl
+    /// method during monomorphization.
+    pub fn force_substitute(&self, type_bindings: &TypeBindings) -> Type {
+        self.substitute_helper(type_bindings, true)
+    }
+
+    /// This helper function only differs in the additional parameter which, if set,
+    /// allows substitutions on already-bound type variables. This should be `false`
+    /// for most uses, but is currently needed during monomorphization when instantiating
+    /// trait functions to shed any previous bindings from recursive parent calls to the
+    /// same trait.
+    fn substitute_helper(
+        &self,
+        type_bindings: &TypeBindings,
+        substitute_bound_typevars: bool,
+    ) -> Type {
         if type_bindings.is_empty() {
             return self.clone();
         }
 
-        let substitute_binding = |binding: &TypeVariable| match &*binding.0.borrow() {
-            TypeBinding::Bound(binding) => binding.substitute(type_bindings),
-            TypeBinding::Unbound(id) => match type_bindings.get(id) {
-                Some((_, binding)) => binding.clone(),
-                None => self.clone(),
-            },
+        let substitute_binding = |binding: &TypeVariable| {
+            // Check the id first to allow substituting to
+            // type variables that have already been bound over.
+            // This is neede for monomorphizing trait impl methods.
+            match type_bindings.get(&binding.0) {
+                Some((_, binding)) if substitute_bound_typevars => binding.clone(),
+                _ => match &*binding.borrow() {
+                    TypeBinding::Bound(binding) => {
+                        binding.substitute_helper(type_bindings, substitute_bound_typevars)
+                    }
+                    TypeBinding::Unbound(id) => match type_bindings.get(id) {
+                        Some((_, binding)) => binding.clone(),
+                        None => self.clone(),
+                    },
+                },
+            }
         };
 
         match self {
             Type::Array(size, element) => {
-                let size = Box::new(size.substitute(type_bindings));
-                let element = Box::new(element.substitute(type_bindings));
-                Type::Array(size, element)
+                let size = size.substitute_helper(type_bindings, substitute_bound_typevars);
+                let element = element.substitute_helper(type_bindings, substitute_bound_typevars);
+                Type::Array(Box::new(size), Box::new(element))
             }
             Type::String(size) => {
-                let size = Box::new(size.substitute(type_bindings));
-                Type::String(size)
+                let size = size.substitute_helper(type_bindings, substitute_bound_typevars);
+                Type::String(Box::new(size))
             }
             Type::FmtString(size, fields) => {
-                let size = Box::new(size.substitute(type_bindings));
-                let fields = Box::new(fields.substitute(type_bindings));
-                Type::FmtString(size, fields)
+                let size = size.substitute_helper(type_bindings, substitute_bound_typevars);
+                let fields = fields.substitute_helper(type_bindings, substitute_bound_typevars);
+                Type::FmtString(Box::new(size), Box::new(fields))
             }
             Type::NamedGeneric(binding, _) | Type::TypeVariable(binding, _) => {
                 substitute_binding(binding)
             }
-            // Do not substitute fields, it can lead to infinite recursion
+            // Do not substitute_helper fields, it ca, substitute_bound_typevarsn lead to infinite recursion
             // and we should not match fields when type checking anyway.
             Type::Struct(fields, args) => {
-                let args = vecmap(args, |arg| arg.substitute(type_bindings));
+                let args = vecmap(args, |arg| {
+                    arg.substitute_helper(type_bindings, substitute_bound_typevars)
+                });
                 Type::Struct(fields.clone(), args)
             }
             Type::Tuple(fields) => {
-                let fields = vecmap(fields, |field| field.substitute(type_bindings));
+                let fields = vecmap(fields, |field| {
+                    field.substitute_helper(type_bindings, substitute_bound_typevars)
+                });
                 Type::Tuple(fields)
             }
             Type::Forall(typevars, typ) => {
-                // Trying to substitute a variable defined within a nested Forall
+                // 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));
                 }
-                let typ = Box::new(typ.substitute(type_bindings));
+                let typ = Box::new(typ.substitute_helper(type_bindings, substitute_bound_typevars));
                 Type::Forall(typevars.clone(), typ)
             }
             Type::Function(args, ret, env) => {
-                let args = vecmap(args, |arg| arg.substitute(type_bindings));
-                let ret = Box::new(ret.substitute(type_bindings));
-                let env = Box::new(env.substitute(type_bindings));
+                let args = vecmap(args, |arg| {
+                    arg.substitute_helper(type_bindings, substitute_bound_typevars)
+                });
+                let ret = Box::new(ret.substitute_helper(type_bindings, substitute_bound_typevars));
+                let env = Box::new(env.substitute_helper(type_bindings, substitute_bound_typevars));
                 Type::Function(args, ret, env)
             }
-            Type::MutableReference(element) => {
-                Type::MutableReference(Box::new(element.substitute(type_bindings)))
-            }
+            Type::MutableReference(element) => Type::MutableReference(Box::new(
+                element.substitute_helper(type_bindings, substitute_bound_typevars),
+            )),
 
             Type::FieldElement
             | Type::Integer(_, _)
@@ -1415,7 +1477,7 @@ impl Type {
             Type::Struct(_, generic_args) => generic_args.iter().any(|arg| arg.occurs(target_id)),
             Type::Tuple(fields) => fields.iter().any(|field| field.occurs(target_id)),
             Type::NamedGeneric(binding, _) | Type::TypeVariable(binding, _) => {
-                match &*binding.0.borrow() {
+                match &*binding.borrow() {
                     TypeBinding::Bound(binding) => binding.occurs(target_id),
                     TypeBinding::Unbound(id) => *id == target_id,
                 }
@@ -1465,7 +1527,7 @@ impl Type {
             }
             Tuple(args) => Tuple(vecmap(args, |arg| arg.follow_bindings())),
             TypeVariable(var, _) | NamedGeneric(var, _) => {
-                if let TypeBinding::Bound(typ) = &*var.0.borrow() {
+                if let TypeBinding::Bound(typ) = &*var.borrow() {
                     return typ.follow_bindings();
                 }
                 self.clone()
@@ -1570,7 +1632,7 @@ impl From<&Type> for PrintableType {
                 Signedness::Signed => PrintableType::SignedInteger { width: *bit_width },
             },
             Type::TypeVariable(binding, TypeVariableKind::IntegerOrField) => {
-                match &*binding.0.borrow() {
+                match &*binding.borrow() {
                     TypeBinding::Bound(typ) => typ.into(),
                     TypeBinding::Unbound(_) => Type::default_int_type().into(),
                 }
diff --git a/compiler/noirc_frontend/src/monomorphization/mod.rs b/compiler/noirc_frontend/src/monomorphization/mod.rs
index c24a2290011..3510475e881 100644
--- a/compiler/noirc_frontend/src/monomorphization/mod.rs
+++ b/compiler/noirc_frontend/src/monomorphization/mod.rs
@@ -26,8 +26,8 @@ use crate::{
     },
     node_interner::{self, DefinitionKind, NodeInterner, StmtId, TraitImplKind, TraitMethodId},
     token::FunctionAttribute,
-    ContractFunctionType, FunctionKind, Type, TypeBinding, TypeBindings, TypeVariableKind, UnaryOp,
-    Visibility,
+    ContractFunctionType, FunctionKind, Type, TypeBinding, TypeBindings, TypeVariable,
+    TypeVariableId, TypeVariableKind, UnaryOp, Visibility,
 };
 
 use self::ast::{Definition, FuncId, Function, LocalId, Program};
@@ -58,8 +58,9 @@ struct Monomorphizer<'interner> {
     /// confuse users.
     locals: HashMap<node_interner::DefinitionId, LocalId>,
 
-    /// Queue of functions to monomorphize next
-    queue: VecDeque<(node_interner::FuncId, FuncId, TypeBindings)>,
+    /// Queue of functions to monomorphize next each item in the queue is a tuple of:
+    /// (old_id, new_monomorphized_id, any type bindings to apply, the trait method if old_id is from a trait impl)
+    queue: VecDeque<(node_interner::FuncId, FuncId, TypeBindings, Option<TraitMethodId>)>,
 
     /// When a function finishes being monomorphized, the monomorphized ast::Function is
     /// stored here along with its FuncId.
@@ -97,11 +98,13 @@ pub fn monomorphize(main: node_interner::FuncId, interner: &NodeInterner) -> Pro
     let function_sig = monomorphizer.compile_main(main);
 
     while !monomorphizer.queue.is_empty() {
-        let (next_fn_id, new_id, bindings) = monomorphizer.queue.pop_front().unwrap();
+        let (next_fn_id, new_id, bindings, trait_method) = monomorphizer.queue.pop_front().unwrap();
         monomorphizer.locals.clear();
 
         perform_instantiation_bindings(&bindings);
+        let impl_bindings = monomorphizer.perform_impl_bindings(trait_method, next_fn_id);
         monomorphizer.function(next_fn_id, new_id);
+        undo_instantiation_bindings(impl_bindings);
         undo_instantiation_bindings(bindings);
     }
 
@@ -154,6 +157,7 @@ impl<'interner> Monomorphizer<'interner> {
         id: node_interner::FuncId,
         expr_id: node_interner::ExprId,
         typ: &HirType,
+        trait_method: Option<TraitMethodId>,
     ) -> Definition {
         let typ = typ.follow_bindings();
         match self.globals.get(&id).and_then(|inner_map| inner_map.get(&typ)) {
@@ -177,7 +181,7 @@ impl<'interner> Monomorphizer<'interner> {
                         Definition::Builtin(opcode)
                     }
                     FunctionKind::Normal => {
-                        let id = self.queue_function(id, expr_id, typ);
+                        let id = self.queue_function(id, expr_id, typ, trait_method);
                         Definition::Function(id)
                     }
                     FunctionKind::Oracle => {
@@ -685,7 +689,7 @@ impl<'interner> Monomorphizer<'interner> {
                 let location = Some(ident.location);
                 let name = definition.name.clone();
                 let typ = self.interner.id_type(expr_id);
-                let definition = self.lookup_function(*func_id, expr_id, &typ);
+                let definition = self.lookup_function(*func_id, expr_id, &typ, None);
                 let typ = self.convert_type(&typ);
                 let ident = ast::Ident { location, mutable, definition, name, typ: typ.clone() };
                 let ident_expression = ast::Expression::Ident(ident);
@@ -857,7 +861,7 @@ impl<'interner> Monomorphizer<'interner> {
             .get_selected_impl_for_expression(expr_id)
             .expect("ICE: missing trait impl - should be caught during type checking");
 
-        let hir_func_id = match trait_impl {
+        let func_id = match trait_impl {
             node_interner::TraitImplKind::Normal(impl_id) => {
                 self.interner.get_trait_implementation(impl_id).borrow().methods
                     [method.method_index]
@@ -885,7 +889,7 @@ impl<'interner> Monomorphizer<'interner> {
             }
         };
 
-        let func_def = self.lookup_function(hir_func_id, expr_id, &function_type);
+        let func_def = self.lookup_function(func_id, expr_id, &function_type, Some(method));
         let func_id = match func_def {
             Definition::Function(func_id) => func_id,
             _ => unreachable!(),
@@ -1107,14 +1111,14 @@ impl<'interner> Monomorphizer<'interner> {
         id: node_interner::FuncId,
         expr_id: node_interner::ExprId,
         function_type: HirType,
+        trait_method: Option<TraitMethodId>,
     ) -> FuncId {
         let new_id = self.next_function_id();
         self.define_global(id, function_type.clone(), new_id);
 
         let bindings = self.interner.get_instantiation_bindings(expr_id);
         let bindings = self.follow_bindings(bindings);
-
-        self.queue.push_back((id, new_id, bindings));
+        self.queue.push_back((id, new_id, bindings, trait_method));
         new_id
     }
 
@@ -1503,6 +1507,46 @@ impl<'interner> Monomorphizer<'interner> {
 
         result
     }
+
+    /// Call sites are instantiated against the trait method, but when an impl is later selected,
+    /// the corresponding method in the impl will have a different set of generics. `perform_impl_bindings`
+    /// is needed to apply the generics from the trait method to the impl method. Without this,
+    /// static method references to generic impls (e.g. `Eq::eq` for `[T; N]`) will fail to re-apply
+    /// the correct type bindings during monomorphization.
+    fn perform_impl_bindings(
+        &self,
+        trait_method: Option<TraitMethodId>,
+        impl_method: node_interner::FuncId,
+    ) -> TypeBindings {
+        let mut bindings = TypeBindings::new();
+
+        if let Some(trait_method) = trait_method {
+            let the_trait = self.interner.get_trait(trait_method.trait_id);
+
+            let trait_method_type = the_trait.methods[trait_method.method_index].typ.as_monotype();
+
+            // Make each NamedGeneric in this type bindable by replacing it with a TypeVariable
+            // with the same internal id and binding.
+            let (generics, impl_method_type) =
+                self.interner.function_meta(&impl_method).typ.unwrap_forall();
+
+            let replace_type_variable = |(id, var): &(TypeVariableId, TypeVariable)| {
+                (*id, (var.clone(), Type::TypeVariable(var.clone(), TypeVariableKind::Normal)))
+            };
+
+            // Replace each NamedGeneric with a TypeVariable containing the same internal type variable
+            let type_bindings = generics.iter().map(replace_type_variable).collect();
+            let impl_method_type = impl_method_type.force_substitute(&type_bindings);
+
+            trait_method_type.try_unify(&impl_method_type, &mut bindings).unwrap_or_else(|_| {
+                unreachable!("Impl method type {} does not unify with trait method type {} during monomorphization", impl_method_type, trait_method_type)
+            });
+
+            perform_instantiation_bindings(&bindings);
+        }
+
+        bindings
+    }
 }
 
 fn unwrap_tuple_type(typ: &HirType) -> Vec<HirType> {
diff --git a/compiler/noirc_frontend/src/node_interner.rs b/compiler/noirc_frontend/src/node_interner.rs
index 9d310b595de..e0170ec914f 100644
--- a/compiler/noirc_frontend/src/node_interner.rs
+++ b/compiler/noirc_frontend/src/node_interner.rs
@@ -1104,7 +1104,10 @@ impl NodeInterner {
         recursion_limit: u32,
     ) -> Result<(), Vec<TraitConstraint>> {
         for constraint in where_clause {
-            let constraint_type = constraint.typ.substitute(instantiation_bindings);
+            // Instantiation bindings are generally safe to force substitute into the same type.
+            // This is needed here to undo any bindings done to trait methods by monomorphization.
+            // Otherwise, an impl for (A, B) could get narrowed to only an impl for e.g. (u8, u16).
+            let constraint_type = constraint.typ.force_substitute(instantiation_bindings);
             let constraint_type = constraint_type.substitute(type_bindings);
 
             self.lookup_trait_implementation_helper(
diff --git a/test_programs/compile_success_empty/regression_3964/Nargo.toml b/test_programs/compile_success_empty/regression_3964/Nargo.toml
new file mode 100644
index 00000000000..a3fd040bcc2
--- /dev/null
+++ b/test_programs/compile_success_empty/regression_3964/Nargo.toml
@@ -0,0 +1,7 @@
+[package]
+name = "regression_3964"
+type = "bin"
+authors = [""]
+compiler_version = ">=0.20.0"
+
+[dependencies]
diff --git a/test_programs/compile_success_empty/regression_3964/src/main.nr b/test_programs/compile_success_empty/regression_3964/src/main.nr
new file mode 100644
index 00000000000..0600a4281a0
--- /dev/null
+++ b/test_programs/compile_success_empty/regression_3964/src/main.nr
@@ -0,0 +1,5 @@
+fn main() {
+    let one: u8 = 1;
+    let p = ((one, 2), (3, 4));
+    assert(p == p);
+}