diff --git a/sway-core/src/language/ty/expression/expression.rs b/sway-core/src/language/ty/expression/expression.rs
index b442e0ba0cd..14a2da461d6 100644
--- a/sway-core/src/language/ty/expression/expression.rs
+++ b/sway-core/src/language/ty/expression/expression.rs
@@ -136,14 +136,20 @@ impl TypeCheckAnalysis for TyExpression {
                         unify::unifier::UnifyKind::Default,
                     );
                     for element in contents {
-                        let element_type = ctx.engines.te().get(*elem_type);
+                        let element_type = ctx.engines.te().get(element.return_type);
 
                         // If the element is never, we do not need to check
                         if matches!(&*element_type, TypeInfo::Never) {
                             continue;
                         }
 
-                        unify.unify(handler, element.return_type, *elem_type, &element.span)
+                        unify.unify(
+                            handler,
+                            element.return_type,
+                            *elem_type,
+                            &element.span,
+                            true,
+                        )
                     }
                 }
             }
diff --git a/sway-core/src/semantic_analysis/ast_node/code_block.rs b/sway-core/src/semantic_analysis/ast_node/code_block.rs
index 41fa19bb75a..623b5e40b3a 100644
--- a/sway-core/src/semantic_analysis/ast_node/code_block.rs
+++ b/sway-core/src/semantic_analysis/ast_node/code_block.rs
@@ -23,10 +23,44 @@ impl ty::TyCodeBlock {
 
     pub(crate) fn type_check(
         handler: &Handler,
-        ctx: TypeCheckContext,
+        mut ctx: TypeCheckContext,
         code_block: &CodeBlock,
+        is_root: bool,
     ) -> Result<Self, ErrorEmitted> {
-        ctx.scoped(|mut ctx| {
+        if !is_root {
+            let code_block_result = ctx.by_ref().scoped(|mut ctx| {
+                let evaluated_contents = code_block
+                    .contents
+                    .iter()
+                    .filter_map(|node| ty::TyAstNode::type_check(handler, ctx.by_ref(), node).ok())
+                    .collect::<Vec<ty::TyAstNode>>();
+                Ok(ty::TyCodeBlock {
+                    contents: evaluated_contents,
+                    whole_block_span: code_block.whole_block_span.clone(),
+                })
+            })?;
+
+            return Ok(code_block_result);
+        }
+
+        ctx.engines.te().clear_unifications();
+
+        // We are typechecking the code block AST nodes twice.
+        // The first pass does all the unifications to the variables types.
+        // In the second pass we use the previous_namespace on variable declaration to unify directly with the result of the first pass.
+        // This is required to fix the test case numeric_type_propagation and issue #6371
+        ctx.by_ref()
+            .with_collecting_unifications()
+            .scoped(|mut ctx| {
+                code_block.contents.iter().for_each(|node| {
+                    ty::TyAstNode::type_check(&Handler::default(), ctx.by_ref(), node).ok();
+                });
+                Ok(())
+            })?;
+
+        ctx.engines.te().reapply_unifications(ctx.engines());
+
+        ctx.by_ref().scoped(|mut ctx| {
             let evaluated_contents = code_block
                 .contents
                 .iter()
diff --git a/sway-core/src/semantic_analysis/ast_node/declaration/declaration.rs b/sway-core/src/semantic_analysis/ast_node/declaration/declaration.rs
index 3f37865215a..a0e77e643bf 100644
--- a/sway-core/src/semantic_analysis/ast_node/declaration/declaration.rs
+++ b/sway-core/src/semantic_analysis/ast_node/declaration/declaration.rs
@@ -11,7 +11,7 @@ use crate::{
         ty::{self, FunctionDecl, TyCodeBlock, TyDecl, TyStorageField},
         CallPath,
     },
-    namespace::{IsExtendingExistingImpl, IsImplSelf},
+    namespace::{IsExtendingExistingImpl, IsImplSelf, ResolvedDeclaration},
     semantic_analysis::{
         symbol_collection_context::SymbolCollectionContext,
         type_check_context::EnforceTypeArguments, ConstShadowingMode, GenericShadowingMode,
@@ -162,6 +162,30 @@ impl TyDecl {
                     },
                 };
 
+                if !ctx.collecting_unifications() {
+                    let previous_symbol = ctx
+                        .namespace()
+                        .module(engines)
+                        .current_items()
+                        .check_symbol_unique(&var_decl.name.clone())
+                        .ok();
+
+                    if let Some(ResolvedDeclaration::Typed(ty::TyDecl::VariableDecl(
+                        variable_decl,
+                    ))) = previous_symbol
+                    {
+                        type_engine.unify(
+                            handler,
+                            engines,
+                            body.return_type,
+                            variable_decl.body.return_type,
+                            &decl.span(engines),
+                            "",
+                            None,
+                        );
+                    }
+                }
+
                 let typed_var_decl = ty::TyDecl::VariableDecl(Box::new(ty::TyVariableDecl {
                     name: var_decl.name.clone(),
                     body,
@@ -359,6 +383,7 @@ impl TyDecl {
                     for i in &impl_trait.items {
                         if let ty::TyTraitItem::Fn(f) = i {
                             let decl = engines.de().get(f.id());
+                            let collecting_unifications = ctx.collecting_unifications();
                             let _ = ctx.namespace.module_mut(ctx.engines()).write(engines, |m| {
                                 m.current_items_mut().insert_typed_symbol(
                                     handler,
@@ -370,6 +395,7 @@ impl TyDecl {
                                     TyDecl::FunctionDecl(FunctionDecl { decl_id: *f.id() }),
                                     ConstShadowingMode::ItemStyle,
                                     GenericShadowingMode::Allow,
+                                    collecting_unifications,
                                 )
                             });
                         }
diff --git a/sway-core/src/semantic_analysis/ast_node/declaration/function.rs b/sway-core/src/semantic_analysis/ast_node/declaration/function.rs
index f5b9b8bb00e..6582c0d3c87 100644
--- a/sway-core/src/semantic_analysis/ast_node/declaration/function.rs
+++ b/sway-core/src/semantic_analysis/ast_node/declaration/function.rs
@@ -215,7 +215,7 @@ impl ty::TyFunctionDecl {
                     .with_type_annotation(return_type.type_id)
                     .with_function_type_annotation(return_type.type_id);
 
-                let body = ty::TyCodeBlock::type_check(handler, ctx.by_ref(), body)
+                let body = ty::TyCodeBlock::type_check(handler, ctx.by_ref(), body, true)
                     .unwrap_or_else(|_err| ty::TyCodeBlock::default());
 
                 ty_fn_decl.body = body;
diff --git a/sway-core/src/semantic_analysis/ast_node/expression/typed_expression.rs b/sway-core/src/semantic_analysis/ast_node/expression/typed_expression.rs
index 26c862b21a1..69824b6a02f 100644
--- a/sway-core/src/semantic_analysis/ast_node/expression/typed_expression.rs
+++ b/sway-core/src/semantic_analysis/ast_node/expression/typed_expression.rs
@@ -635,7 +635,7 @@ impl ty::TyExpression {
         let engines = ctx.engines();
 
         let (typed_block, block_return_type) =
-            match ty::TyCodeBlock::type_check(handler, ctx.by_ref(), contents) {
+            match ty::TyCodeBlock::type_check(handler, ctx.by_ref(), contents, false) {
                 Ok(res) => {
                     let (block_type, _span) = TyCodeBlock::compute_return_type_and_span(&ctx, &res);
                     (res, block_type)
@@ -1840,7 +1840,12 @@ impl ty::TyExpression {
         // from the elements
         let initial_type = match &*ctx.engines().te().get(ctx.type_annotation()) {
             TypeInfo::Array(element_type, _) => {
-                (*ctx.engines().te().get(element_type.type_id)).clone()
+                let element_type = (*ctx.engines().te().get(element_type.type_id)).clone();
+                if matches!(element_type, TypeInfo::Never) {
+                    TypeInfo::Unknown //Even if array element type is Never other elements may not be of type Never.
+                } else {
+                    element_type
+                }
             }
             _ => TypeInfo::Unknown,
         };
@@ -2008,7 +2013,7 @@ impl ty::TyExpression {
                  assigning it to a mutable variable declared outside of the loop \
                  instead.",
         );
-        let typed_body = ty::TyCodeBlock::type_check(handler, ctx.by_ref(), body)?;
+        let typed_body = ty::TyCodeBlock::type_check(handler, ctx.by_ref(), body, false)?;
 
         let exp = ty::TyExpression {
             expression: ty::TyExpressionVariant::WhileLoop {
diff --git a/sway-core/src/semantic_analysis/ast_node/expression/typed_expression/function_application.rs b/sway-core/src/semantic_analysis/ast_node/expression/typed_expression/function_application.rs
index cf39c305572..3ffabc5fbed 100644
--- a/sway-core/src/semantic_analysis/ast_node/expression/typed_expression/function_application.rs
+++ b/sway-core/src/semantic_analysis/ast_node/expression/typed_expression/function_application.rs
@@ -100,7 +100,8 @@ pub(crate) fn instantiate_function_application(
             )
             .with_parent(decl_engine, (*function_decl_ref.id()).into());
 
-        if method_sig.is_concrete(engines)
+        if !ctx.collecting_unifications()
+            && method_sig.is_concrete(engines)
             && function_is_type_check_finalized
             && !function_is_trait_method_dummy
         {
diff --git a/sway-core/src/semantic_analysis/ast_node/expression/typed_expression/method_application.rs b/sway-core/src/semantic_analysis/ast_node/expression/typed_expression/method_application.rs
index ea83cd08847..ec4b5b9529e 100644
--- a/sway-core/src/semantic_analysis/ast_node/expression/typed_expression/method_application.rs
+++ b/sway-core/src/semantic_analysis/ast_node/expression/typed_expression/method_application.rs
@@ -697,7 +697,8 @@ pub(crate) fn type_check_method_application(
         method_return_type_id = method.return_type.type_id;
         decl_engine.replace(*fn_ref.id(), method.clone());
 
-        if method_sig.is_concrete(engines)
+        if !ctx.collecting_unifications()
+            && method_sig.is_concrete(engines)
             && method.is_type_check_finalized
             && !method.is_trait_method_dummy
         {
diff --git a/sway-core/src/semantic_analysis/namespace/lexical_scope.rs b/sway-core/src/semantic_analysis/namespace/lexical_scope.rs
index f327269eee2..ee117bd6e73 100644
--- a/sway-core/src/semantic_analysis/namespace/lexical_scope.rs
+++ b/sway-core/src/semantic_analysis/namespace/lexical_scope.rs
@@ -13,11 +13,12 @@ use crate::{
 
 use super::{root::ResolvedDeclaration, TraitMap};
 
+use parking_lot::RwLock;
 use sway_error::{
     error::{CompileError, ShadowingSource, StructFieldUsageContext},
     handler::{ErrorEmitted, Handler},
 };
-use sway_types::{span::Span, Spanned};
+use sway_types::{span::Span, IdentUnique, Spanned};
 
 use std::sync::Arc;
 
@@ -36,6 +37,7 @@ impl ResolvedFunctionDecl {
 }
 
 pub(super) type SymbolMap = im::OrdMap<Ident, ResolvedDeclaration>;
+pub(super) type SymbolUniqueMap = im::OrdMap<IdentUnique, ResolvedDeclaration>;
 
 type SourceIdent = Ident;
 
@@ -76,6 +78,13 @@ pub struct LexicalScope {
 pub struct Items {
     /// An ordered map from `Ident`s to their associated declarations.
     pub(crate) symbols: SymbolMap,
+
+    /// An ordered map from `IdentUnique`s to their associated declarations.
+    /// This uses an Arc<RwLock<SymbolUniqueMap>> so it is shared between all
+    /// Items clones. This is intended so we can keep the symbols of previous
+    /// lexical scopes while collecting_unifications scopes.
+    pub(crate) symbols_unique_while_collecting_unifications: Arc<RwLock<SymbolUniqueMap>>,
+
     pub(crate) implemented_traits: TraitMap,
     /// Contains symbols imported using star imports (`use foo::*`.).
     ///
@@ -163,9 +172,11 @@ impl Items {
             ResolvedDeclaration::Parsed(item),
             const_shadowing_mode,
             generic_shadowing_mode,
+            false,
         )
     }
 
+    #[allow(clippy::too_many_arguments)]
     pub(crate) fn insert_typed_symbol(
         &mut self,
         handler: &Handler,
@@ -174,6 +185,7 @@ impl Items {
         item: ty::TyDecl,
         const_shadowing_mode: ConstShadowingMode,
         generic_shadowing_mode: GenericShadowingMode,
+        collecting_unifications: bool,
     ) -> Result<(), ErrorEmitted> {
         self.insert_symbol(
             handler,
@@ -182,9 +194,11 @@ impl Items {
             ResolvedDeclaration::Typed(item),
             const_shadowing_mode,
             generic_shadowing_mode,
+            collecting_unifications,
         )
     }
 
+    #[allow(clippy::too_many_arguments)]
     pub(crate) fn insert_symbol(
         &mut self,
         handler: &Handler,
@@ -193,6 +207,7 @@ impl Items {
         item: ResolvedDeclaration,
         const_shadowing_mode: ConstShadowingMode,
         generic_shadowing_mode: GenericShadowingMode,
+        collecting_unifications: bool,
     ) -> Result<(), ErrorEmitted> {
         let parsed_decl_engine = engines.pe();
         let decl_engine = engines.de();
@@ -629,6 +644,11 @@ impl Items {
             );
         }
 
+        if collecting_unifications {
+            self.symbols_unique_while_collecting_unifications
+                .write()
+                .insert(name.clone().into(), item.clone());
+        }
         self.symbols.insert(name, item);
 
         Ok(())
@@ -684,6 +704,20 @@ impl Items {
             })
     }
 
+    pub(crate) fn check_symbol_unique(
+        &self,
+        name: &Ident,
+    ) -> Result<ResolvedDeclaration, CompileError> {
+        self.symbols_unique_while_collecting_unifications
+            .read()
+            .get(&name.into())
+            .cloned()
+            .ok_or_else(|| CompileError::SymbolNotFound {
+                name: name.clone(),
+                span: name.span(),
+            })
+    }
+
     pub fn get_items_for_type(
         &self,
         engines: &Engines,
diff --git a/sway-core/src/semantic_analysis/type_check_context.rs b/sway-core/src/semantic_analysis/type_check_context.rs
index b0a5029d4f2..336554e479d 100644
--- a/sway-core/src/semantic_analysis/type_check_context.rs
+++ b/sway-core/src/semantic_analysis/type_check_context.rs
@@ -94,6 +94,8 @@ pub struct TypeCheckContext<'a> {
 
     /// Indicates when semantic analysis is type checking storage declaration.
     storage_declaration: bool,
+
+    collecting_unifications: bool,
 }
 
 impl<'a> TypeCheckContext<'a> {
@@ -119,6 +121,7 @@ impl<'a> TypeCheckContext<'a> {
             disallow_functions: false,
             storage_declaration: false,
             experimental,
+            collecting_unifications: false,
         }
     }
 
@@ -158,6 +161,7 @@ impl<'a> TypeCheckContext<'a> {
             disallow_functions: false,
             storage_declaration: false,
             experimental,
+            collecting_unifications: false,
         }
     }
 
@@ -186,6 +190,7 @@ impl<'a> TypeCheckContext<'a> {
             disallow_functions: self.disallow_functions,
             storage_declaration: self.storage_declaration,
             experimental: self.experimental,
+            collecting_unifications: self.collecting_unifications,
         }
     }
 
@@ -211,6 +216,7 @@ impl<'a> TypeCheckContext<'a> {
             disallow_functions: self.disallow_functions,
             storage_declaration: self.storage_declaration,
             experimental: self.experimental,
+            collecting_unifications: self.collecting_unifications,
         };
         with_scoped_ctx(ctx)
     }
@@ -237,6 +243,7 @@ impl<'a> TypeCheckContext<'a> {
             disallow_functions: self.disallow_functions,
             storage_declaration: self.storage_declaration,
             experimental: self.experimental,
+            collecting_unifications: self.collecting_unifications,
         };
         Ok((with_scoped_ctx(ctx)?, namespace))
     }
@@ -348,6 +355,13 @@ impl<'a> TypeCheckContext<'a> {
         Self { self_type, ..self }
     }
 
+    pub(crate) fn with_collecting_unifications(self) -> Self {
+        Self {
+            collecting_unifications: true,
+            ..self
+        }
+    }
+
     /// Map this `TypeCheckContext` instance to a new one with
     /// `disallow_functions` set to `true`.
     pub(crate) fn disallow_functions(self) -> Self {
@@ -419,6 +433,10 @@ impl<'a> TypeCheckContext<'a> {
         self.storage_declaration
     }
 
+    pub(crate) fn collecting_unifications(&self) -> bool {
+        self.collecting_unifications
+    }
+
     // Provide some convenience functions around the inner context.
 
     /// Short-hand for calling the `monomorphize` function in the type engine
@@ -480,6 +498,7 @@ impl<'a> TypeCheckContext<'a> {
     ) -> Result<(), ErrorEmitted> {
         let const_shadowing_mode = self.const_shadowing_mode;
         let generic_shadowing_mode = self.generic_shadowing_mode;
+        let collecting_unifications = self.collecting_unifications;
         let engines = self.engines();
         self.namespace_mut()
             .module_mut(engines)
@@ -491,6 +510,7 @@ impl<'a> TypeCheckContext<'a> {
                 ResolvedDeclaration::Typed(item),
                 const_shadowing_mode,
                 generic_shadowing_mode,
+                collecting_unifications,
             )
     }
 
@@ -1111,6 +1131,14 @@ impl<'a> TypeCheckContext<'a> {
 
         // default numeric types to u64
         if type_engine.contains_numeric(decl_engine, type_id) {
+            // While collecting unification we don't decay numeric and will ignore this error.
+            if self.collecting_unifications {
+                return Err(handler.emit_err(CompileError::MethodNotFound {
+                    method_name: method_name.clone(),
+                    type_name: self.engines.help_out(type_id).to_string(),
+                    span: method_name.span(),
+                }));
+            }
             type_engine.decay_numeric(handler, self.engines, type_id, &method_name.span())?;
         }
 
diff --git a/sway-core/src/transform/to_parsed_lang/context.rs b/sway-core/src/transform/to_parsed_lang/context.rs
index dcd661a685b..f450eb5257f 100644
--- a/sway-core/src/transform/to_parsed_lang/context.rs
+++ b/sway-core/src/transform/to_parsed_lang/context.rs
@@ -20,6 +20,9 @@ pub struct Context {
     /// that store values matched in match expressions.
     match_expression_matched_value_unique_suffix: usize,
 
+    /// Unique suffix used to generate unique names for for loops.
+    for_unique_suffix: usize,
+
     /// The build target.
     build_target: BuildTarget,
 
@@ -40,6 +43,7 @@ impl Context {
             destructured_struct_unique_suffix: std::default::Default::default(),
             destructured_tuple_unique_suffix: std::default::Default::default(),
             match_expression_matched_value_unique_suffix: std::default::Default::default(),
+            for_unique_suffix: std::default::Default::default(),
             program_type: std::default::Default::default(),
             implementing_type: None,
         }
@@ -74,6 +78,12 @@ impl Context {
         self.match_expression_matched_value_unique_suffix
     }
 
+    /// Returns a unique suffix used to generate a unique name for a destructured struct.
+    pub fn next_for_unique_suffix(&mut self) -> usize {
+        self.for_unique_suffix += 1;
+        self.for_unique_suffix
+    }
+
     /// Returns the build target.
     pub fn build_target(&self) -> BuildTarget {
         self.build_target
diff --git a/sway-core/src/transform/to_parsed_lang/convert_parse_tree.rs b/sway-core/src/transform/to_parsed_lang/convert_parse_tree.rs
index 4ed2e8799ab..642badfeadf 100644
--- a/sway-core/src/transform/to_parsed_lang/convert_parse_tree.rs
+++ b/sway-core/src/transform/to_parsed_lang/convert_parse_tree.rs
@@ -3110,13 +3110,19 @@ fn for_expr_to_expression(
     //        let value = value_opt.unwrap();
     //        code_block
     //    }
-    let value_opt_ident = Ident::new_no_span("__for_value_opt".into());
+    let value_opt_ident = Ident::new_no_span(format!(
+        "__for_value_opt_{}",
+        context.next_for_unique_suffix()
+    ));
     let value_opt_expr = Expression {
         kind: ExpressionKind::Variable(value_opt_ident.clone()),
         span: Span::dummy(),
     };
 
-    let iterable_ident = Ident::new_no_span("__for_iterable".into());
+    let iterable_ident = Ident::new_no_span(format!(
+        "__for_iterable_{}",
+        context.next_for_unique_suffix()
+    ));
     let iterable_expr = Expression {
         kind: ExpressionKind::Variable(iterable_ident.clone()),
         span: Span::dummy(),
@@ -3801,7 +3807,11 @@ fn statement_let_to_ast_nodes_unfold(
                     mutable,
                     name,
                 } => (reference, mutable, name),
-                Pattern::Wildcard { .. } => (None, None, Ident::new_no_span("_".into())),
+                Pattern::Wildcard { underscore_token } => (
+                    None,
+                    None,
+                    Ident::new_with_override("_".to_string(), underscore_token.span()),
+                ),
                 Pattern::AmbiguousSingleIdent(ident) => (None, None, ident),
                 _ => unreachable!(),
             };
@@ -3946,7 +3956,7 @@ fn statement_let_to_ast_nodes_unfold(
             let tuple_name =
                 generate_tuple_var_name(context.next_destructured_tuple_unique_suffix());
 
-            let tuple_name = Ident::new_with_override(tuple_name, span.clone());
+            let tuple_name = Ident::new_with_override(tuple_name, pat_tuple.span().clone());
 
             // Acript a second declaration to a tuple of placeholders to check that the tuple
             // is properly sized to the pattern
@@ -3958,13 +3968,16 @@ fn statement_let_to_ast_nodes_unfold(
                             .clone()
                             .into_inner()
                             .into_iter()
-                            .map(|_| {
+                            .map(|pat| {
                                 let initial_type_id =
                                     engines.te().insert(engines, TypeInfo::Unknown, None);
                                 let dummy_type_param = TypeParameter {
                                     type_id: initial_type_id,
                                     initial_type_id,
-                                    name_ident: Ident::new_with_override("_".into(), span.clone()),
+                                    name_ident: Ident::new_with_override(
+                                        "_".into(),
+                                        pat.span().clone(),
+                                    ),
                                     trait_constraints: vec![],
                                     trait_constraints_span: Span::dummy(),
                                     is_from_parent: false,
diff --git a/sway-core/src/type_system/ast_elements/type_parameter.rs b/sway-core/src/type_system/ast_elements/type_parameter.rs
index 13b8b69b77f..4372388c00d 100644
--- a/sway-core/src/type_system/ast_elements/type_parameter.rs
+++ b/sway-core/src/type_system/ast_elements/type_parameter.rs
@@ -352,6 +352,7 @@ impl TypeParameter {
 
         // Trait constraints mutate so we replace the previous type id associated TypeInfo.
         type_engine.replace(
+            ctx.engines(),
             type_parameter.type_id,
             TypeSourceInfo {
                 type_info: TypeInfo::UnknownGeneric {
@@ -441,6 +442,7 @@ impl TypeParameter {
                         }
 
                         ctx.engines.te().replace(
+                            ctx.engines(),
                             *type_id,
                             TypeSourceInfo {
                                 type_info: TypeInfo::UnknownGeneric {
@@ -499,22 +501,24 @@ impl TypeParameter {
                     ..
                 } = type_param;
 
-                // Check to see if the trait constraints are satisfied.
-                match ctx
-                    .namespace_mut()
-                    .module_mut(engines)
-                    .current_items_mut()
-                    .implemented_traits
-                    .check_if_trait_constraints_are_satisfied_for_type(
-                        handler,
-                        *type_id,
-                        trait_constraints,
-                        access_span,
-                        engines,
-                        TryInsertingTraitImplOnFailure::Yes,
-                    ) {
-                    Ok(res) => res,
-                    Err(_) => continue,
+                if !ctx.collecting_unifications() {
+                    // Check to see if the trait constraints are satisfied.
+                    match ctx
+                        .namespace_mut()
+                        .module_mut(engines)
+                        .current_items_mut()
+                        .implemented_traits
+                        .check_if_trait_constraints_are_satisfied_for_type(
+                            handler,
+                            *type_id,
+                            trait_constraints,
+                            access_span,
+                            engines,
+                            TryInsertingTraitImplOnFailure::Yes,
+                        ) {
+                        Ok(res) => res,
+                        Err(_) => continue,
+                    }
                 }
 
                 for trait_constraint in trait_constraints {
diff --git a/sway-core/src/type_system/engine.rs b/sway-core/src/type_system/engine.rs
index 206bed81bb2..86ed395e243 100644
--- a/sway-core/src/type_system/engine.rs
+++ b/sway-core/src/type_system/engine.rs
@@ -7,7 +7,7 @@ use crate::{
 use core::fmt::Write;
 use hashbrown::{hash_map::RawEntryMut, HashMap};
 use parking_lot::RwLock;
-use std::sync::Arc;
+use std::{sync::Arc, time::Instant};
 use sway_error::{
     error::CompileError,
     handler::{ErrorEmitted, Handler},
@@ -17,10 +17,32 @@ use sway_types::{integer_bits::IntegerBits, span::Span, ProgramId, SourceId};
 
 use super::unify::unifier::UnifyKind;
 
-#[derive(Debug, Default)]
+#[derive(Debug)]
 pub struct TypeEngine {
     slab: ConcurrentSlab<TypeSourceInfo>,
     id_map: RwLock<HashMap<TypeSourceInfo, TypeId>>,
+    unifications: ConcurrentSlab<Unification>,
+    last_replace: RwLock<Instant>,
+}
+
+#[derive(Debug, Clone)]
+pub(crate) struct Unification {
+    pub received: TypeId,
+    pub expected: TypeId,
+    pub span: Span,
+    pub help_text: String,
+    pub unify_kind: UnifyKind,
+}
+
+impl Default for TypeEngine {
+    fn default() -> Self {
+        TypeEngine {
+            slab: Default::default(),
+            id_map: Default::default(),
+            unifications: Default::default(),
+            last_replace: RwLock::new(Instant::now()),
+        }
+    }
 }
 
 impl Clone for TypeEngine {
@@ -28,6 +50,8 @@ impl Clone for TypeEngine {
         TypeEngine {
             slab: self.slab.clone(),
             id_map: RwLock::new(self.id_map.read().clone()),
+            unifications: self.unifications.clone(),
+            last_replace: RwLock::new(*self.last_replace.read()),
         }
     }
 }
@@ -88,7 +112,11 @@ impl TypeEngine {
         self.clear_items(|id| id != source_id);
     }
 
-    pub fn replace(&self, id: TypeId, new_value: TypeSourceInfo) {
+    pub fn replace(&self, engines: &Engines, id: TypeId, new_value: TypeSourceInfo) {
+        if !(*self.slab.get(id.index())).eq(&new_value, &PartialEqWithEnginesContext::new(engines))
+        {
+            self.touch_last_replace();
+        }
         self.slab.replace(id.index(), new_value);
     }
 
@@ -146,6 +174,7 @@ impl TypeEngine {
             help_text,
             err_override,
             UnifyKind::Default,
+            true,
         );
     }
 
@@ -176,6 +205,7 @@ impl TypeEngine {
             help_text,
             err_override,
             UnifyKind::WithSelf,
+            true,
         );
     }
 
@@ -206,9 +236,15 @@ impl TypeEngine {
             help_text,
             err_override,
             UnifyKind::WithGeneric,
+            true,
         );
     }
 
+    fn touch_last_replace(&self) {
+        let mut write_last_change = self.last_replace.write();
+        *write_last_change = Instant::now();
+    }
+
     #[allow(clippy::too_many_arguments)]
     fn unify_helper(
         handler: &Handler,
@@ -219,6 +255,7 @@ impl TypeEngine {
         help_text: &str,
         err_override: Option<CompileError>,
         unify_kind: UnifyKind,
+        push_unification: bool,
     ) {
         if !UnifyCheck::coercion(engines).check(received, expected) {
             // create a "mismatched type" error unless the `err_override`
@@ -241,7 +278,7 @@ impl TypeEngine {
 
         let h = Handler::default();
         let unifier = Unifier::new(engines, help_text, unify_kind);
-        unifier.unify(handler, received, expected, span);
+        unifier.unify(handler, received, expected, span, push_unification);
 
         match err_override {
             Some(err_override) if h.has_errors() => {
@@ -253,6 +290,34 @@ impl TypeEngine {
         }
     }
 
+    pub(crate) fn push_unification(&self, unification: Unification) {
+        self.unifications.insert(unification);
+    }
+
+    pub(crate) fn clear_unifications(&self) {
+        self.unifications.clear();
+    }
+
+    pub(crate) fn reapply_unifications(&self, engines: &Engines) {
+        let current_last_replace = *self.last_replace.read();
+        for unification in self.unifications.values() {
+            Self::unify_helper(
+                &Handler::default(),
+                engines,
+                unification.received,
+                unification.expected,
+                &unification.span,
+                &unification.help_text,
+                None,
+                unification.unify_kind.clone(),
+                false,
+            )
+        }
+        if *self.last_replace.read() > current_last_replace {
+            self.reapply_unifications(engines);
+        }
+    }
+
     pub(crate) fn to_typeinfo(&self, id: TypeId, error_span: &Span) -> Result<TypeInfo, TypeError> {
         match &*self.get(id) {
             TypeInfo::Unknown => Err(TypeError::UnknownType {
diff --git a/sway-core/src/type_system/id.rs b/sway-core/src/type_system/id.rs
index 9410fd2d6ac..4e523804df4 100644
--- a/sway-core/src/type_system/id.rs
+++ b/sway-core/src/type_system/id.rs
@@ -511,6 +511,10 @@ impl TypeId {
         span: &Span,
         type_param: Option<TypeParameter>,
     ) -> Result<(), ErrorEmitted> {
+        if ctx.collecting_unifications() {
+            return Ok(());
+        }
+
         let engines = ctx.engines();
 
         let mut structure_generics = self.extract_inner_types_with_trait_constraints(engines);
diff --git a/sway-core/src/type_system/unify/unifier.rs b/sway-core/src/type_system/unify/unifier.rs
index c23bb0c3dd2..41b72802602 100644
--- a/sway-core/src/type_system/unify/unifier.rs
+++ b/sway-core/src/type_system/unify/unifier.rs
@@ -6,11 +6,12 @@ use sway_types::Span;
 use crate::{
     engine_threading::{Engines, PartialEqWithEngines, PartialEqWithEnginesContext, WithEngines},
     language::{ty, CallPath},
-    type_system::priv_prelude::*,
+    type_system::{engine::Unification, priv_prelude::*},
 };
 
 use super::occurs_check::OccursCheck;
 
+#[derive(Debug, Clone)]
 pub(crate) enum UnifyKind {
     /// Make the types of `received` and `expected` equivalent (or produce an
     /// error if there is a conflict between them).
@@ -63,6 +64,7 @@ impl<'a> Unifier<'a> {
         let type_engine = self.engines.te();
         let source_id = span.source_id().copied();
         type_engine.replace(
+            self.engines,
             received,
             TypeSourceInfo {
                 type_info: expected_type_info.clone().into(),
@@ -81,6 +83,7 @@ impl<'a> Unifier<'a> {
         let type_engine = self.engines.te();
         let source_id = span.source_id().copied();
         type_engine.replace(
+            self.engines,
             expected,
             TypeSourceInfo {
                 type_info: received_type_info.clone().into(),
@@ -90,7 +93,26 @@ impl<'a> Unifier<'a> {
     }
 
     /// Performs type unification with `received` and `expected`.
-    pub(crate) fn unify(&self, handler: &Handler, received: TypeId, expected: TypeId, span: &Span) {
+    pub(crate) fn unify(
+        &self,
+        handler: &Handler,
+        received: TypeId,
+        expected: TypeId,
+        span: &Span,
+        push_unification: bool,
+    ) {
+        if push_unification {
+            let unification = Unification {
+                received,
+                expected,
+                span: span.clone(),
+                help_text: self.help_text.clone(),
+                unify_kind: self.unify_kind.clone(),
+            };
+
+            self.engines.te().push_unification(unification);
+        }
+
         use TypeInfo::{
             Alias, Array, Boolean, Contract, Enum, Never, Numeric, Placeholder, RawUntypedPtr,
             RawUntypedSlice, Ref, Slice, StringArray, StringSlice, Struct, Tuple, Unknown,
@@ -224,8 +246,8 @@ impl<'a> Unifier<'a> {
             (Never, _) => {}
 
             // Type aliases and the types they encapsulate coerce to each other.
-            (Alias { ty, .. }, _) => self.unify(handler, ty.type_id, expected, span),
-            (_, Alias { ty, .. }) => self.unify(handler, received, ty.type_id, span),
+            (Alias { ty, .. }, _) => self.unify(handler, ty.type_id, expected, span, false),
+            (_, Alias { ty, .. }) => self.unify(handler, received, ty.type_id, span, false),
 
             (Enum(r_decl_ref), Enum(e_decl_ref)) => {
                 let r_decl = self.engines.de().get_enum(r_decl_ref);
@@ -363,7 +385,7 @@ impl<'a> Unifier<'a> {
 
     fn unify_tuples(&self, handler: &Handler, rfs: &[TypeArgument], efs: &[TypeArgument]) {
         for (rf, ef) in rfs.iter().zip(efs.iter()) {
-            self.unify(handler, rf.type_id, ef.type_id, &rf.span);
+            self.unify(handler, rf.type_id, ef.type_id, &rf.span, false);
         }
     }
 
@@ -385,10 +407,11 @@ impl<'a> Unifier<'a> {
                     rf.type_argument.type_id,
                     ef.type_argument.type_id,
                     span,
+                    false,
                 );
             });
             rtps.iter().zip(etps.iter()).for_each(|(rtp, etp)| {
-                self.unify(handler, rtp.type_id, etp.type_id, span);
+                self.unify(handler, rtp.type_id, etp.type_id, span, false);
             });
         } else {
             let (received, expected) = self.assign_args(received, expected);
@@ -422,10 +445,11 @@ impl<'a> Unifier<'a> {
                     rv.type_argument.type_id,
                     ev.type_argument.type_id,
                     span,
+                    false,
                 );
             });
             rtps.iter().zip(etps.iter()).for_each(|(rtp, etp)| {
-                self.unify(handler, rtp.type_id, etp.type_id, span);
+                self.unify(handler, rtp.type_id, etp.type_id, span, false);
             });
         } else {
             let (received, expected) = self.assign_args(received, expected);
@@ -460,6 +484,7 @@ impl<'a> Unifier<'a> {
             received_type_argument.type_id,
             expected_type_argument.type_id,
             span,
+            false,
         );
         let (new_errors, warnings) = h.consume();
 
diff --git a/sway-types/src/ident.rs b/sway-types/src/ident.rs
index 3f1dd1fe575..f4aa577bc5d 100644
--- a/sway-types/src/ident.rs
+++ b/sway-types/src/ident.rs
@@ -180,18 +180,22 @@ impl From<&IdentUnique> for Ident {
 impl Hash for IdentUnique {
     fn hash<H: Hasher>(&self, state: &mut H) {
         self.0.span().hash(state);
+        self.0.as_str().hash(state);
     }
 }
 
 impl PartialEq for IdentUnique {
     fn eq(&self, other: &Self) -> bool {
-        self.0.span() == other.0.span()
+        self.0.as_str() == other.0.as_str() && self.0.span() == other.0.span()
     }
 }
 
 impl Ord for IdentUnique {
     fn cmp(&self, other: &Self) -> Ordering {
-        self.0.span().cmp(&other.0.span())
+        self.0
+            .span()
+            .cmp(&other.0.span())
+            .then(self.0.as_str().cmp(other.0.as_str()))
     }
 }
 
diff --git a/test/src/e2e_vm_tests/test_programs/should_fail/struct_instantiation_type_mismatch/src/main.sw b/test/src/e2e_vm_tests/test_programs/should_fail/struct_instantiation_type_mismatch/src/main.sw
index 7ab423a42ba..c501dc4a681 100644
--- a/test/src/e2e_vm_tests/test_programs/should_fail/struct_instantiation_type_mismatch/src/main.sw
+++ b/test/src/e2e_vm_tests/test_programs/should_fail/struct_instantiation_type_mismatch/src/main.sw
@@ -84,9 +84,6 @@ fn main() {
         _ => false,
     };
 
-    // TODO: Unfortunately, at the moment we do not provide a help message here that
-    // the error is coming from the enum declaration and not variable annotation.
-    // This will wait until we introduce a separate type inference step.
     let s: GenericStruct<_, bool> = GenericStruct::<u8, _> { a: 123u64, b: true };
     let _ = s.a == 123u8; // No error here.
     let _ = s.b == true; // No error here.
diff --git a/test/src/e2e_vm_tests/test_programs/should_fail/struct_instantiation_type_mismatch/test.toml b/test/src/e2e_vm_tests/test_programs/should_fail/struct_instantiation_type_mismatch/test.toml
index b66666a14eb..5e7ddbbb42e 100644
--- a/test/src/e2e_vm_tests/test_programs/should_fail/struct_instantiation_type_mismatch/test.toml
+++ b/test/src/e2e_vm_tests/test_programs/should_fail/struct_instantiation_type_mismatch/test.toml
@@ -132,7 +132,7 @@ category = "fail"
 #nextln: $()Mismatched types.
 #nextln: $()expected: u8
 #nextln: $()found:    u64.
-#nextln: $()Variable declaration's type annotation does not match up with the assigned expression's type.
+#nextln: $()Struct field's type must match the type specified in its declaration.
 #nextln: $()let _ = s.a == 123u8; // No error here.
 #nextln: $()let _ = s.b == true; // No error here.
 
diff --git a/test/src/e2e_vm_tests/test_programs/should_fail/type_check_analyze_errors/test.toml b/test/src/e2e_vm_tests/test_programs/should_fail/type_check_analyze_errors/test.toml
index 65ba3c1072b..1c6df70f7ee 100644
--- a/test/src/e2e_vm_tests/test_programs/should_fail/type_check_analyze_errors/test.toml
+++ b/test/src/e2e_vm_tests/test_programs/should_fail/type_check_analyze_errors/test.toml
@@ -1,5 +1,10 @@
 category = "fail"
 
+# check: $()let a = [1, 2, "hello"];
+# nextln: $()Mismatched types
+# nextln: $()expected: numeric
+# nextln: $()found:    str
+
 # check: $()let _a = 0x100;
 # nextln: $()Literal would overflow because its value does not fit into "u8"
 
@@ -8,8 +13,3 @@ category = "fail"
 
 # check: $()let _a = 0x100000000;
 # nextln: $()Literal would overflow because its value does not fit into "u32"
-
-# check: $()let a = [1, 2, "hello"];
-# nextln: $()Mismatched types
-# nextln: $()expected: numeric
-# nextln: $()found:    str
diff --git a/test/src/e2e_vm_tests/test_programs/should_pass/language/numeric_type_propagation/Forc.lock b/test/src/e2e_vm_tests/test_programs/should_pass/language/numeric_type_propagation/Forc.lock
new file mode 100644
index 00000000000..c8d0134a5c1
--- /dev/null
+++ b/test/src/e2e_vm_tests/test_programs/should_pass/language/numeric_type_propagation/Forc.lock
@@ -0,0 +1,13 @@
+[[package]]
+name = "core"
+source = "path+from-root-A2943394F152C9BB"
+
+[[package]]
+name = "numeric_type_propagation"
+source = "member"
+dependencies = ["std"]
+
+[[package]]
+name = "std"
+source = "path+from-root-A2943394F152C9BB"
+dependencies = ["core"]
diff --git a/test/src/e2e_vm_tests/test_programs/should_pass/language/numeric_type_propagation/Forc.toml b/test/src/e2e_vm_tests/test_programs/should_pass/language/numeric_type_propagation/Forc.toml
new file mode 100644
index 00000000000..b84f7484a8b
--- /dev/null
+++ b/test/src/e2e_vm_tests/test_programs/should_pass/language/numeric_type_propagation/Forc.toml
@@ -0,0 +1,9 @@
+[project]
+authors = ["Fuel Labs <contact@fuel.sh>"]
+entry = "main.sw"
+implicit-std = false
+license = "Apache-2.0"
+name = "numeric_type_propagation"
+
+[dependencies]
+std = { path = "../../../../../../../sway-lib-std" }
diff --git a/test/src/e2e_vm_tests/test_programs/should_pass/language/numeric_type_propagation/src/main.sw b/test/src/e2e_vm_tests/test_programs/should_pass/language/numeric_type_propagation/src/main.sw
new file mode 100644
index 00000000000..9dac838621b
--- /dev/null
+++ b/test/src/e2e_vm_tests/test_programs/should_pass/language/numeric_type_propagation/src/main.sw
@@ -0,0 +1,74 @@
+script;
+
+trait MyTrait{
+    fn foo(ref mut self) -> u64;
+}
+
+impl MyTrait for u64 {
+    fn foo(ref mut self) -> u64 {
+        64
+    }
+}
+impl MyTrait for u32 {
+    fn foo(ref mut self) -> u64 {
+        32
+    }
+}
+
+impl u64 {
+    fn baz(self) -> u64 {
+        64
+    }
+}
+impl u32 {
+    fn baz(self) -> u64{
+        32
+    }
+}
+
+fn bar<T>(ref mut x: T) -> u64 where T: MyTrait {
+    x.foo()
+}
+
+fn main() -> bool {
+    let mut a = 0; // depth 1 type propagation
+    let mut b = 0; // depth 2 type propagation
+    let mut c = 0; // depth 3 type propagation
+    assert_eq(bar(a), 32);
+    assert_eq(bar(b), 32);
+    assert_eq(bar(c), 32);
+    {
+        c = b;
+    }
+    {
+        b = a;
+    }
+    {
+        let _: &u32 = &a;
+    }
+    assert_eq(a.baz(), 32);
+    assert_eq(b.baz(), 32);
+    assert_eq(c.baz(), 32);
+    {   // Test inside nested code block
+        let mut a = 0; // depth 1 type propagation
+        let mut b = 0; // depth 2 type propagation
+        let mut c = 0; // depth 3 type propagation
+        assert_eq(bar(a), 32);
+        assert_eq(bar(b), 32);
+        assert_eq(bar(c), 32);
+        {
+            c = b;
+        }
+        {
+            b = a;
+        }
+        {
+            let _: &u32 = &a;
+        }
+        assert_eq(a.baz(), 32);
+        assert_eq(b.baz(), 32);
+        assert_eq(c.baz(), 32);
+    }
+
+    true
+}
\ No newline at end of file
diff --git a/test/src/e2e_vm_tests/test_programs/should_pass/language/numeric_type_propagation/test.toml b/test/src/e2e_vm_tests/test_programs/should_pass/language/numeric_type_propagation/test.toml
new file mode 100644
index 00000000000..28fb5e56e0c
--- /dev/null
+++ b/test/src/e2e_vm_tests/test_programs/should_pass/language/numeric_type_propagation/test.toml
@@ -0,0 +1,4 @@
+category = "run"
+expected_result = { action = "return", value = 1 }
+expected_result_new_encoding = { action = "return_data", value = "01" }
+expected_warnings = 5
\ No newline at end of file