diff --git a/crates/erg_compiler/context/unify.rs b/crates/erg_compiler/context/unify.rs
index cd800639..3e91b8ca 100644
--- a/crates/erg_compiler/context/unify.rs
+++ b/crates/erg_compiler/context/unify.rs
@@ -113,7 +113,7 @@ impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
                 self.occur(&lhs.return_t, &rhs.return_t)?;
                 Ok(())
             }
-            (Poly { params, .. }, FreeVar(fv)) if fv.is_unbound() => {
+            /*(Poly { params, .. }, FreeVar(fv)) if fv.is_unbound() => {
                 for param in params.iter().filter_map(|tp| {
                     if let TyParam::Type(t) = tp {
                         Some(t)
@@ -124,7 +124,7 @@ impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
                     self.occur_inner(param, maybe_sup)?;
                 }
                 Ok(())
-            }
+            }*/
             (FreeVar(fv), Poly { params, .. }) if fv.is_unbound() => {
                 for param in params.iter().filter_map(|tp| {
                     if let TyParam::Type(t) = tp {
diff --git a/crates/erg_compiler/tests/infer.er b/crates/erg_compiler/tests/infer.er
index cdf93b07..d80ad709 100644
--- a/crates/erg_compiler/tests/infer.er
+++ b/crates/erg_compiler/tests/infer.er
@@ -15,3 +15,11 @@ norm x = x.norm()
 a = [1, 2] + [3, 4]
 
 abc = ["c"] + ["a", "b"][1..1000]
+
+f! t =
+    arr = ![]
+    result = ![]
+    result.push! t
+    for! arr, t =>
+        result.extend! f! t
+    result
diff --git a/crates/erg_compiler/tests/test.rs b/crates/erg_compiler/tests/test.rs
index 45a2cf5a..e4f1cb7e 100644
--- a/crates/erg_compiler/tests/test.rs
+++ b/crates/erg_compiler/tests/test.rs
@@ -11,7 +11,7 @@ use erg_compiler::lower::ASTLowerer;
 
 use erg_compiler::ty::constructors::{
     array_t, func0, func1, func2, kw, mono, nd_func, nd_proc, or, poly, proc1, subtype_q, ty_tp,
-    type_q, unknown_len_array_t, v_enum,
+    type_q, unknown_len_array_mut, unknown_len_array_t, v_enum,
 };
 use erg_compiler::ty::Type::*;
 
@@ -73,6 +73,9 @@ fn _test_infer_types() -> Result<(), ()> {
     module.context.assert_var_type("a", &a_t)?;
     let abc_t = unknown_len_array_t(v_enum(set! {"a".into(), "b".into(), "c".into()}));
     module.context.assert_var_type("abc", &abc_t)?;
+    let t = type_q("T");
+    let f_t = proc1(t.clone(), unknown_len_array_mut(t)).quantify();
+    module.context.assert_var_type("f!", &f_t)?;
     Ok(())
 }
 
diff --git a/crates/erg_compiler/ty/constructors.rs b/crates/erg_compiler/ty/constructors.rs
index b169e57f..c5ddb766 100644
--- a/crates/erg_compiler/ty/constructors.rs
+++ b/crates/erg_compiler/ty/constructors.rs
@@ -51,6 +51,10 @@ pub fn unknown_len_array_t(elem_t: Type) -> Type {
     array_t(elem_t, TyParam::erased(Type::Nat))
 }
 
+pub fn unknown_len_array_mut(elem_t: Type) -> Type {
+    array_mut(elem_t, TyParam::erased(Type::Nat))
+}
+
 pub fn tuple_t(args: Vec<Type>) -> Type {
     poly(
         "Tuple",