diff --git a/crates/erg_compiler/ty/mod.rs b/crates/erg_compiler/ty/mod.rs
index bd24bd125..bc8afae4e 100644
--- a/crates/erg_compiler/ty/mod.rs
+++ b/crates/erg_compiler/ty/mod.rs
@@ -4530,20 +4530,37 @@ impl Type {
                         return tv;
                     }
                 }
-                let fv_clone = fv.deep_clone();
                 if let Some((sub, sup)) = fv.get_subsup() {
                     fv.dummy_link();
-                    let sub = f(sub);
-                    let sup = f(sup);
+                    let new_sub = f(sub.clone());
+                    let new_sup = f(sup.clone());
                     fv.undo();
-                    fv_clone.update_constraint(Constraint::new_sandwiched(sub, sup), true);
+                    if new_sub != sub || new_sup != sup {
+                        let fv_clone = fv.deep_clone();
+                        fv_clone
+                            .update_constraint(Constraint::new_sandwiched(new_sub, new_sup), true);
+                        if let Some(name) = fv.unbound_name() {
+                            tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
+                        }
+                        Self::FreeVar(fv_clone)
+                    } else {
+                        Self::FreeVar(fv)
+                    }
                 } else if let Some(ty) = fv.get_type() {
-                    fv_clone.update_constraint(Constraint::new_type_of(f(ty)), true);
-                }
-                if let Some(name) = fv.unbound_name() {
-                    tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
+                    let new_ty = f(ty.clone());
+                    if new_ty != ty {
+                        let fv_clone = fv.deep_clone();
+                        fv_clone.update_constraint(Constraint::new_type_of(new_ty), true);
+                        if let Some(name) = fv.unbound_name() {
+                            tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
+                        }
+                        Self::FreeVar(fv_clone)
+                    } else {
+                        Self::FreeVar(fv)
+                    }
+                } else {
+                    Self::FreeVar(fv)
                 }
-                Self::FreeVar(fv_clone)
             }
             Self::Refinement(mut refine) => {
                 refine.t = Box::new(f(*refine.t));
@@ -4616,6 +4633,7 @@ impl Type {
         self.map(&mut |t| t._replace(target, to, tvs), tvs)
     }
 
+    /// `?T(<: Int).replace(Int, Nat) == ?T'(<: Nat)`
     fn _replace_tp(self, target: &TyParam, to: &TyParam, tvs: &SharedFrees) -> Type {
         match self {
             Self::FreeVar(fv) if fv.is_linked() => fv.unwrap_linked()._replace_tp(target, to, tvs),
@@ -4625,23 +4643,37 @@ impl Type {
                         return tv;
                     }
                 }
-                let fv_clone = fv.deep_clone();
                 if let Some((sub, sup)) = fv.get_subsup() {
                     fv.dummy_link();
-                    let sub = sub._replace_tp(target, to, tvs);
-                    let sup = sup._replace_tp(target, to, tvs);
+                    let new_sub = sub.clone()._replace_tp(target, to, tvs);
+                    let new_sup = sup.clone()._replace_tp(target, to, tvs);
                     fv.undo();
-                    fv_clone.update_constraint(Constraint::new_sandwiched(sub, sup), true);
+                    if new_sub != sub || new_sup != sup {
+                        let fv_clone = fv.deep_clone();
+                        fv_clone
+                            .update_constraint(Constraint::new_sandwiched(new_sub, new_sup), true);
+                        if let Some(name) = fv.unbound_name() {
+                            tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
+                        }
+                        Self::FreeVar(fv_clone)
+                    } else {
+                        Self::FreeVar(fv)
+                    }
                 } else if let Some(ty) = fv.get_type() {
-                    fv_clone.update_constraint(
-                        Constraint::new_type_of(ty._replace_tp(target, to, tvs)),
-                        true,
-                    );
-                }
-                if let Some(name) = fv.unbound_name() {
-                    tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
+                    let new_ty = ty.clone()._replace_tp(target, to, tvs);
+                    if new_ty != ty {
+                        let fv_clone = fv.deep_clone();
+                        fv_clone.update_constraint(Constraint::new_type_of(new_ty), true);
+                        if let Some(name) = fv.unbound_name() {
+                            tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
+                        }
+                        Self::FreeVar(fv_clone)
+                    } else {
+                        Self::FreeVar(fv)
+                    }
+                } else {
+                    Self::FreeVar(fv)
                 }
-                Self::FreeVar(fv_clone)
             }
             Self::Refinement(mut refine) => {
                 refine.t = Box::new(refine.t._replace_tp(target, to, tvs));
@@ -4729,20 +4761,37 @@ impl Type {
                         return tv;
                     }
                 }
-                let fv_clone = fv.deep_clone();
                 if let Some((sub, sup)) = fv.get_subsup() {
                     fv.dummy_link();
-                    let sub = sub.map_tp(f, tvs);
-                    let sup = sup.map_tp(f, tvs);
+                    let new_sub = sub.clone().map_tp(f, tvs);
+                    let new_sup = sup.clone().map_tp(f, tvs);
                     fv.undo();
-                    fv_clone.update_constraint(Constraint::new_sandwiched(sub, sup), true);
+                    if new_sub != sub || new_sup != sup {
+                        let fv_clone = fv.deep_clone();
+                        fv_clone
+                            .update_constraint(Constraint::new_sandwiched(new_sub, new_sup), true);
+                        if let Some(name) = fv.unbound_name() {
+                            tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
+                        }
+                        Self::FreeVar(fv_clone)
+                    } else {
+                        Self::FreeVar(fv)
+                    }
                 } else if let Some(ty) = fv.get_type() {
-                    fv_clone.update_constraint(Constraint::new_type_of(ty.map_tp(f, tvs)), true);
-                }
-                if let Some(name) = fv.unbound_name() {
-                    tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
+                    let new_ty = ty.clone().map_tp(f, tvs);
+                    if new_ty != ty {
+                        let fv_clone = fv.deep_clone();
+                        fv_clone.update_constraint(Constraint::new_type_of(new_ty), true);
+                        if let Some(name) = fv.unbound_name() {
+                            tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
+                        }
+                        Self::FreeVar(fv_clone)
+                    } else {
+                        Self::FreeVar(fv)
+                    }
+                } else {
+                    Self::FreeVar(fv)
                 }
-                Self::FreeVar(fv_clone)
             }
             Self::Refinement(mut refine) => {
                 refine.t = Box::new(refine.t.map_tp(f, tvs));
@@ -4818,21 +4867,37 @@ impl Type {
                         return Ok(tv);
                     }
                 }
-                let fv_clone = fv.deep_clone();
                 if let Some((sub, sup)) = fv.get_subsup() {
                     fv.dummy_link();
-                    let sub = sub.try_map_tp(f, tvs)?;
-                    let sup = sup.try_map_tp(f, tvs)?;
+                    let new_sub = sub.clone().try_map_tp(f, tvs)?;
+                    let new_sup = sup.clone().try_map_tp(f, tvs)?;
                     fv.undo();
-                    fv_clone.update_constraint(Constraint::new_sandwiched(sub, sup), true);
+                    if new_sub != sub || new_sup != sup {
+                        let fv_clone = fv.deep_clone();
+                        fv_clone
+                            .update_constraint(Constraint::new_sandwiched(new_sub, new_sup), true);
+                        if let Some(name) = fv.unbound_name() {
+                            tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
+                        }
+                        Ok(Self::FreeVar(fv_clone))
+                    } else {
+                        Ok(Self::FreeVar(fv))
+                    }
                 } else if let Some(ty) = fv.get_type() {
-                    fv_clone
-                        .update_constraint(Constraint::new_type_of(ty.try_map_tp(f, tvs)?), true);
-                }
-                if let Some(name) = fv.unbound_name() {
-                    tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
+                    let new_ty = ty.clone().try_map_tp(f, tvs)?;
+                    if new_ty != ty {
+                        let fv_clone = fv.deep_clone();
+                        fv_clone.update_constraint(Constraint::new_type_of(new_ty), true);
+                        if let Some(name) = fv.unbound_name() {
+                            tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
+                        }
+                        Ok(Self::FreeVar(fv_clone))
+                    } else {
+                        Ok(Self::FreeVar(fv))
+                    }
+                } else {
+                    Ok(Self::FreeVar(fv))
                 }
-                Ok(Self::FreeVar(fv_clone))
             }
             Self::Refinement(mut refine) => {
                 refine.t = Box::new(refine.t.try_map_tp(f, tvs)?);
@@ -6128,4 +6193,20 @@ mod tests {
         assert!(subr.is_recursive());
         assert!(sup.is_recursive());
     }
+
+    #[test]
+    fn test_link() {
+        let t = named_free_var("T".into(), 1, Constraint::new_type_of(Type::Type));
+        let u = free_var(1, Constraint::new_type_of(Type::Type));
+        let v = t.clone();
+        u.link(&unknown_len_list_t(t.clone()), None);
+        t.destructive_link(&Type::Int);
+        assert_eq!(v, Type::Int);
+        assert_eq!(
+            u,
+            unknown_len_list_t(Type::Int),
+            "{u} != {}",
+            unknown_len_list_t(Type::Int)
+        );
+    }
 }
diff --git a/crates/erg_compiler/ty/typaram.rs b/crates/erg_compiler/ty/typaram.rs
index f244329d6..1f94c3bac 100644
--- a/crates/erg_compiler/ty/typaram.rs
+++ b/crates/erg_compiler/ty/typaram.rs
@@ -1571,11 +1571,16 @@ impl TyParam {
                 if let Some(tp) = tvs.get_tp(&name) {
                     return tp;
                 }
-                let typ = fv.get_type().unwrap()._replace(target, to, tvs);
-                let fv_clone = fv.deep_clone();
-                fv_clone.update_type(typ);
-                tvs.insert_tp(name, Self::FreeVar(fv_clone.clone()));
-                Self::FreeVar(fv_clone)
+                let typ = fv.get_type().unwrap();
+                let new_typ = typ.clone()._replace(target, to, tvs);
+                if new_typ != typ {
+                    let fv_clone = fv.deep_clone();
+                    fv_clone.update_type(new_typ);
+                    tvs.insert_tp(name, Self::FreeVar(fv_clone.clone()));
+                    Self::FreeVar(fv_clone)
+                } else {
+                    Self::FreeVar(fv)
+                }
             }
             Self::Type(t) => Self::t(t._replace(target, to, tvs)),
             Self::Erased(t) => Self::erased(t._replace(target, to, tvs)),
@@ -1927,12 +1932,17 @@ impl TyParam {
                     }
                 }
                 let typ = fv.get_type().unwrap();
-                let fv_clone = fv.deep_clone();
-                fv_clone.update_type(typ.map_tp(f, tvs));
-                if let Some(name) = fv_clone.unbound_name() {
-                    tvs.insert_tp(name, TyParam::FreeVar(fv_clone.clone()));
+                let new_typ = typ.clone().map_tp(f, tvs);
+                if typ != new_typ {
+                    let fv_clone = fv.deep_clone();
+                    fv_clone.update_type(new_typ);
+                    if let Some(name) = fv_clone.unbound_name() {
+                        tvs.insert_tp(name, TyParam::FreeVar(fv_clone.clone()));
+                    }
+                    TyParam::FreeVar(fv_clone)
+                } else {
+                    TyParam::FreeVar(fv)
                 }
-                TyParam::FreeVar(fv_clone)
             }
             TyParam::FreeVar(_) => self,
             TyParam::App { name, args } => {
@@ -1996,13 +2006,18 @@ impl TyParam {
                         return tp;
                     }
                 }
-                let fv_clone = fv.deep_clone();
                 let typ = fv.get_type().unwrap();
-                fv_clone.update_type(f(typ));
-                if let Some(name) = fv_clone.unbound_name() {
-                    tvs.insert_tp(name, TyParam::FreeVar(fv_clone.clone()));
+                let new_typ = f(typ.clone());
+                if typ != new_typ {
+                    let fv_clone = fv.deep_clone();
+                    fv_clone.update_type(new_typ);
+                    if let Some(name) = fv_clone.unbound_name() {
+                        tvs.insert_tp(name, TyParam::FreeVar(fv_clone.clone()));
+                    }
+                    TyParam::FreeVar(fv_clone)
+                } else {
+                    TyParam::FreeVar(fv)
                 }
-                TyParam::FreeVar(fv_clone)
             }
             TyParam::FreeVar(_) => self,
             TyParam::App { name, args } => {