diff --git a/crates/erg_common/macros.rs b/crates/erg_common/macros.rs
index 07c3958f..51c17d49 100644
--- a/crates/erg_common/macros.rs
+++ b/crates/erg_common/macros.rs
@@ -626,6 +626,7 @@ macro_rules! set_recursion_limit {
 
         let counter = $crate::macros::RecursionCounter::new(&COUNTER);
         if counter.limit_reached() {
+            $crate::log!(err "Recursion limit reached");
             return $returns;
         }
     };
diff --git a/crates/erg_compiler/context/eval.rs b/crates/erg_compiler/context/eval.rs
index 3e2283e4..05d62ade 100644
--- a/crates/erg_compiler/context/eval.rs
+++ b/crates/erg_compiler/context/eval.rs
@@ -406,11 +406,17 @@ impl<'c> Substituter<'c> {
     /// -> Iterable(Int)
     /// ```
     pub(crate) fn substitute_self(qt: &Type, subtype: &Type, ctx: &'c Context) -> Option<Self> {
+        #[allow(clippy::blocks_in_conditions)]
         for t in qt.contained_ts() {
             if t.is_qvar()
                 && &t.qual_name()[..] == "Self"
-                && t.get_super()
-                    .is_some_and(|sup| ctx.supertype_of(&sup, subtype))
+                && t.get_super().is_some_and(|sup| {
+                    let fv = t.as_free().unwrap();
+                    fv.dummy_link();
+                    let res = ctx.supertype_of(&sup, subtype);
+                    fv.undo();
+                    res
+                })
             {
                 let mut _self = Self::new(ctx);
                 t.undoable_link(subtype, &_self.undoable_linked);
diff --git a/crates/erg_compiler/ty/free.rs b/crates/erg_compiler/ty/free.rs
index a6dd1be4..407dbda7 100644
--- a/crates/erg_compiler/ty/free.rs
+++ b/crates/erg_compiler/ty/free.rs
@@ -248,8 +248,8 @@ impl Constraint {
                 } else if sup.addr_eq(target) {
                     Self::new_supertype_of(sub)
                 } else {
-                    let sub = sub.eliminate_sub(target);
-                    let sup = sup.eliminate_sub(target);
+                    let sub = sub.eliminate_subsup(target);
+                    let sup = sup.eliminate_subsup(target);
                     Self::new_sandwiched(sub, sup)
                 }
             }
diff --git a/crates/erg_compiler/ty/mod.rs b/crates/erg_compiler/ty/mod.rs
index 2dfee180..e403ba14 100644
--- a/crates/erg_compiler/ty/mod.rs
+++ b/crates/erg_compiler/ty/mod.rs
@@ -37,7 +37,7 @@ use erg_parser::ast::Expr;
 use erg_parser::token::TokenKind;
 
 pub use const_subr::*;
-use constructors::{dict_t, int_interval, mono};
+use constructors::{callable, dict_t, int_interval, mono};
 use free::{CanbeFree, Constraint, Free, FreeKind, FreeTyVar, HasLevel, Level, GENERIC_LEVEL};
 pub use predicate::Predicate;
 pub use typaram::{IntervalOp, TyParam};
@@ -2007,7 +2007,7 @@ impl HasLevel for Type {
                     Some(min)
                 }
             }
-            _ => None,
+            mono_type_pattern!() => None,
         }
     }
 
@@ -2084,7 +2084,7 @@ impl HasLevel for Type {
                 sub.set_level(level);
                 sup.set_level(level);
             }
-            _ => {}
+            mono_type_pattern!() => {} //_ => {}
         }
     }
 }
@@ -2874,7 +2874,11 @@ impl Type {
                     || after.as_ref().map_or(false, |t| t.contains_tvar(target))
             }
             Self::Bounded { sub, sup } => sub.contains_tvar(target) || sup.contains_tvar(target),
-            _ => false,
+            Self::Callable { param_ts, return_t } => {
+                param_ts.iter().any(|t| t.contains_tvar(target)) || return_t.contains_tvar(target)
+            }
+            Self::Guard(guard) => guard.to.contains_tvar(target),
+            mono_type_pattern!() => false,
         }
     }
 
@@ -2937,7 +2941,11 @@ impl Type {
                     || after.as_ref().map_or(false, |t| t.contains_type(target))
             }
             Self::Bounded { sub, sup } => sub.contains_type(target) || sup.contains_type(target),
-            _ => false,
+            Self::Callable { param_ts, return_t } => {
+                param_ts.iter().any(|t| t.contains_type(target)) || return_t.contains_type(target)
+            }
+            Self::Guard(guard) => guard.to.contains_type(target),
+            mono_type_pattern!() => false,
         }
     }
 
@@ -2971,13 +2979,18 @@ impl Type {
                     || after.as_ref().map_or(false, |t| t.contains_tp(target))
             }
             Self::Bounded { sub, sup } => sub.contains_tp(target) || sup.contains_tp(target),
-            _ => false,
+            Self::Callable { param_ts, return_t } => {
+                param_ts.iter().any(|t| t.contains_tp(target)) || return_t.contains_tp(target)
+            }
+            Self::Guard(guard) => guard.to.contains_tp(target),
+            mono_type_pattern!() => false,
         }
     }
 
     pub fn contains_value(&self, target: &ValueObj) -> bool {
         match self {
             Self::FreeVar(fv) if fv.is_linked() => fv.crack().contains_value(target),
+            Self::FreeVar(_) => false,
             Self::Record(rec) => rec.iter().any(|(_, t)| t.contains_value(target)),
             Self::NamedTuple(rec) => rec.iter().any(|(_, t)| t.contains_value(target)),
             Self::Poly { params, .. } => params.iter().any(|tp| tp.contains_value(target)),
@@ -3000,7 +3013,11 @@ impl Type {
                     || after.as_ref().map_or(false, |t| t.contains_value(target))
             }
             Self::Bounded { sub, sup } => sub.contains_value(target) || sup.contains_value(target),
-            _ => false,
+            Self::Callable { param_ts, return_t } => {
+                param_ts.iter().any(|t| t.contains_value(target)) || return_t.contains_value(target)
+            }
+            Self::Guard(guard) => guard.to.contains_value(target),
+            mono_type_pattern!() => false,
         }
     }
 
@@ -3039,7 +3056,11 @@ impl Type {
                     || after.as_ref().map_or(false, |t| t.contains_type(self))
             }
             Self::Bounded { sub, sup } => sub.contains_type(self) || sup.contains_type(self),
-            _ => false,
+            Self::Callable { param_ts, return_t } => {
+                param_ts.iter().any(|t| t.contains_type(self)) || return_t.contains_type(self)
+            }
+            Self::Guard(guard) => guard.to.contains_type(self),
+            mono_type_pattern!() => false,
         }
     }
 
@@ -3518,6 +3539,7 @@ impl Type {
                     base
                 }
             }
+            Self::FreeVar(_) => set! {},
             Self::Ref(ty) => ty.qvars_inner(),
             Self::RefMut { before, after } => before.qvars_inner().concat(
                 after
@@ -3541,6 +3563,7 @@ impl Type {
             Self::Refinement(refine) => refine.t.qvars_inner().concat(refine.pred.qvars()),
             // ((|T| T -> T) and U).qvars() == U.qvars()
             // Self::Quantified(quant) => quant.qvars(),
+            Self::Quantified(_) => set! {},
             Self::Poly { params, .. } => params
                 .iter()
                 .fold(set! {}, |acc, tp| acc.concat(tp.qvars())),
@@ -3551,7 +3574,7 @@ impl Type {
             Self::Structural(ty) => ty.qvars_inner(),
             Self::Guard(guard) => guard.to.qvars_inner(),
             Self::Bounded { sub, sup } => sub.qvars_inner().concat(sup.qvars_inner()),
-            _ => set! {},
+            mono_type_pattern!() => set! {},
         }
     }
 
@@ -3598,6 +3621,7 @@ impl Type {
                 param_ts.iter().any(|t| t.has_qvar()) || return_t.has_qvar()
             }
             Self::Subr(subr) => subr.has_qvar(),
+            Self::Quantified(_) => false,
             // Self::Quantified(quant) => quant.has_qvar(),
             Self::Record(r) => r.values().any(|t| t.has_qvar()),
             Self::NamedTuple(r) => r.iter().any(|(_, t)| t.has_qvar()),
@@ -3610,7 +3634,7 @@ impl Type {
             Self::Structural(ty) => ty.has_qvar(),
             Self::Guard(guard) => guard.to.has_qvar(),
             Self::Bounded { sub, sup } => sub.has_qvar() || sup.has_qvar(),
-            _ => false,
+            mono_type_pattern!() => false,
         }
     }
 
@@ -3669,7 +3693,7 @@ impl Type {
             Self::Bounded { sub, sup } => {
                 sub.has_undoable_linked_var() || sup.has_undoable_linked_var()
             }
-            _ => false,
+            mono_type_pattern!() => false,
         }
     }
 
@@ -3719,7 +3743,7 @@ impl Type {
             Self::Structural(ty) => ty.has_unbound_var(),
             Self::Guard(guard) => guard.to.has_unbound_var(),
             Self::Bounded { sub, sup } => sub.has_unbound_var() || sup.has_unbound_var(),
-            _ => false,
+            mono_type_pattern!() => false,
         }
     }
 
@@ -4065,41 +4089,41 @@ impl Type {
             }
             Self::Subr(subr) => Self::Subr(subr.derefine()),
             Self::Quantified(quant) => quant.derefine().quantify(),
-            other => other.clone(),
+            mono_type_pattern!() => self.clone(),
         }
     }
 
     /// ```erg
-    /// (T or U).eliminate_sub(T) == U
-    /// ?X(<: T or U).eliminate_sub(T) == ?X(<: U)
+    /// (T or U).eliminate_subsup(T) == U
+    /// ?X(<: T or U).eliminate_subsup(T) == ?X(<: U)
     /// ```
-    pub fn eliminate_sub(self, target: &Type) -> Self {
+    pub fn eliminate_subsup(self, target: &Type) -> Self {
         match self {
-            Self::FreeVar(fv) if fv.is_linked() => fv.unwrap_linked().eliminate_sub(target),
+            Self::FreeVar(fv) if fv.is_linked() => fv.unwrap_linked().eliminate_subsup(target),
             Self::FreeVar(ref fv) if fv.constraint_is_sandwiched() => {
                 let (sub, sup) = fv.get_subsup().unwrap();
                 fv.do_avoiding_recursion(|| {
-                    let sub = sub.eliminate_sub(target);
-                    let sup = sup.eliminate_sub(target);
+                    let sub = sub.eliminate_subsup(target);
+                    let sup = sup.eliminate_subsup(target);
                     self.update_tyvar(sub, sup, None, false);
                 });
                 self
             }
             Self::And(l, r) => {
                 if l.addr_eq(target) {
-                    return r.eliminate_sub(target);
+                    return r.eliminate_subsup(target);
                 } else if r.addr_eq(target) {
-                    return l.eliminate_sub(target);
+                    return l.eliminate_subsup(target);
                 }
-                l.eliminate_sub(target) & r.eliminate_sub(target)
+                l.eliminate_subsup(target) & r.eliminate_subsup(target)
             }
             Self::Or(l, r) => {
                 if l.addr_eq(target) {
-                    return r.eliminate_sub(target);
+                    return r.eliminate_subsup(target);
                 } else if r.addr_eq(target) {
-                    return l.eliminate_sub(target);
+                    return l.eliminate_subsup(target);
                 }
-                l.eliminate_sub(target) | r.eliminate_sub(target)
+                l.eliminate_subsup(target) | r.eliminate_subsup(target)
             }
             other => other,
         }
@@ -4115,6 +4139,7 @@ impl Type {
         }
         match self {
             Self::FreeVar(fv) if fv.is_linked() => fv.unwrap_linked().eliminate_recursion(target),
+            Self::FreeVar(_) => self,
             Self::Refinement(mut refine) => {
                 refine.t = Box::new(refine.t.eliminate_recursion(target));
                 refine.pred = Box::new(refine.pred.map_t(&mut |t| t.eliminate_recursion(target)));
@@ -4176,7 +4201,7 @@ impl Type {
                 sub: Box::new(sub.eliminate_recursion(target)),
                 sup: Box::new(sup.eliminate_recursion(target)),
             },
-            other => other,
+            mono_type_pattern!() => self,
         }
     }
 
@@ -4344,7 +4369,7 @@ impl Type {
                 sub: Box::new(sub._replace(target, to)),
                 sup: Box::new(sup._replace(target, to)),
             },
-            other => other,
+            mono_type_pattern!() => self,
         }
     }
 
@@ -4430,7 +4455,7 @@ impl Type {
                 sub: Box::new(sub._replace_tp(target, to)),
                 sup: Box::new(sup._replace_tp(target, to)),
             },
-            other => other,
+            mono_type_pattern!() => self,
         }
     }
 
@@ -4507,7 +4532,7 @@ impl Type {
                 sub: Box::new(sub.map_tp(f)),
                 sup: Box::new(sup.map_tp(f)),
             },
-            other => other,
+            mono_type_pattern!() => self,
         }
     }
 
@@ -4629,6 +4654,7 @@ impl Type {
     pub fn normalize(self) -> Self {
         match self {
             Self::FreeVar(fv) if fv.is_linked() => fv.unwrap_linked().normalize(),
+            Self::FreeVar(_) => self,
             Self::Poly { name, params } => {
                 let params = params.into_iter().map(|tp| tp.normalize()).collect();
                 Self::Poly { name, params }
@@ -4684,6 +4710,7 @@ impl Type {
             Self::Or(l, r) => l.normalize() | r.normalize(),
             Self::Not(ty) => !ty.normalize(),
             Self::Structural(ty) => ty.normalize().structuralize(),
+            Self::Quantified(quant) => quant.normalize().quantify(),
             Self::Guard(guard) => Self::Guard(GuardType::new(
                 guard.namespace,
                 guard.target,
@@ -4693,7 +4720,12 @@ impl Type {
                 sub: Box::new(sub.normalize()),
                 sup: Box::new(sup.normalize()),
             },
-            other => other,
+            Self::Callable { param_ts, return_t } => {
+                let param_ts = param_ts.into_iter().map(|t| t.normalize()).collect();
+                let return_t = return_t.normalize();
+                callable(param_ts, return_t)
+            }
+            mono_type_pattern!() => self,
         }
     }
 
@@ -4735,10 +4767,12 @@ impl Type {
             }*/
             return;
         }
-        let to = to.clone().eliminate_sub(self).eliminate_recursion(self);
         match self {
-            Self::FreeVar(fv) => fv.link(&to),
-            Self::Refinement(refine) => refine.t.destructive_link(&to),
+            Self::FreeVar(fv) => {
+                let to = to.clone().eliminate_subsup(self).eliminate_recursion(self);
+                fv.link(&to);
+            }
+            Self::Refinement(refine) => refine.t.destructive_link(to),
             _ => {
                 if DEBUG_MODE {
                     panic!("{self} is not a free variable");
@@ -4756,10 +4790,12 @@ impl Type {
             self.inc_undo_count();
             return;
         }
-        let to = to.clone().eliminate_sub(self);
         match self {
-            Self::FreeVar(fv) => fv.undoable_link(&to),
-            Self::Refinement(refine) => refine.t.undoable_link(&to, list),
+            Self::FreeVar(fv) => {
+                let to = to.clone().eliminate_subsup(self);
+                fv.undoable_link(&to);
+            }
+            Self::Refinement(refine) => refine.t.undoable_link(to, list),
             _ => {
                 if DEBUG_MODE {
                     panic!("{self} is not a free variable")
@@ -4903,6 +4939,7 @@ impl Type {
                         .union(&sup.contained_ts())
                 })
             }
+            Self::FreeVar(_) => set! { self.clone() },
             Self::Refinement(refine) => refine.t.contained_ts(),
             Self::Ref(t) => t.contained_ts(),
             Self::RefMut { before, .. } => before.contained_ts(),
@@ -4944,7 +4981,8 @@ impl Type {
                 ts.extend(params.iter().flat_map(|tp| tp.contained_ts()));
                 ts
             }
-            _ => set! { self.clone() },
+            Self::Guard(guard) => guard.to.contained_ts(),
+            mono_type_pattern!() => set! { self.clone() },
         }
     }
 
@@ -4958,6 +4996,7 @@ impl Type {
             Self::FreeVar(fv) if fv.is_generalized() => {
                 fv.update_init();
             }
+            Self::FreeVar(_) => {}
             // TODO: T(:> X, <: Y).dereference()
             Self::Refinement(refine) => {
                 refine.t.dereference();
@@ -5034,7 +5073,7 @@ impl Type {
             Self::Guard(guard) => {
                 guard.to.dereference();
             }
-            _ => {}
+            mono_type_pattern!() => {}
         }
     }
 
diff --git a/crates/erg_compiler/ty/typaram.rs b/crates/erg_compiler/ty/typaram.rs
index 42a9bfa2..448aec4b 100644
--- a/crates/erg_compiler/ty/typaram.rs
+++ b/crates/erg_compiler/ty/typaram.rs
@@ -1125,11 +1125,16 @@ impl TyParam {
                     base
                 }
             }
+            Self::FreeVar(_) => set! {},
             Self::Type(t) => t.qvars(),
             Self::Proj { obj, .. } => obj.qvars(),
+            Self::ProjCall { obj, args, .. } => args
+                .iter()
+                .fold(obj.qvars(), |acc, arg| acc.concat(arg.qvars())),
             Self::List(ts) | Self::Tuple(ts) => {
                 ts.iter().fold(set! {}, |acc, t| acc.concat(t.qvars()))
             }
+            Self::UnsizedList(elem) => elem.qvars(),
             Self::Set(ts) => ts.iter().fold(set! {}, |acc, t| acc.concat(t.qvars())),
             Self::Dict(ts) => ts.iter().fold(set! {}, |acc, (k, v)| {
                 acc.concat(k.qvars().concat(v.qvars()))
@@ -1146,7 +1151,7 @@ impl TyParam {
             Self::App { args, .. } => args.iter().fold(set! {}, |acc, p| acc.concat(p.qvars())),
             Self::Erased(t) => t.qvars(),
             Self::Value(val) => val.qvars(),
-            _ => set! {},
+            Self::Mono(_) | Self::Failure => set! {},
         }
     }
 
@@ -1154,9 +1159,12 @@ impl TyParam {
         match self {
             Self::FreeVar(fv) if fv.is_unbound() && fv.is_generalized() => true,
             Self::FreeVar(fv) if fv.is_linked() => fv.crack().has_qvar(),
+            Self::FreeVar(_) => false,
             Self::Type(t) => t.has_qvar(),
             Self::Proj { obj, .. } => obj.has_qvar(),
+            Self::ProjCall { obj, args, .. } => obj.has_qvar() || args.iter().any(|t| t.has_qvar()),
             Self::List(tps) | Self::Tuple(tps) => tps.iter().any(|tp| tp.has_qvar()),
+            Self::UnsizedList(elem) => elem.has_qvar(),
             Self::Set(tps) => tps.iter().any(|tp| tp.has_qvar()),
             Self::Dict(tps) => tps.iter().any(|(k, v)| k.has_qvar() || v.has_qvar()),
             Self::Record(rec) | Self::DataClass { fields: rec, .. } => {
@@ -1168,7 +1176,7 @@ impl TyParam {
             Self::App { args, .. } => args.iter().any(|p| p.has_qvar()),
             Self::Erased(t) => t.has_qvar(),
             Self::Value(val) => val.has_qvar(),
-            _ => false,
+            Self::Mono(_) | Self::Failure => false,
         }
     }
 
@@ -1178,7 +1186,11 @@ impl TyParam {
             Self::Type(t) => t.contains_tvar(target),
             Self::Erased(t) => t.contains_tvar(target),
             Self::Proj { obj, .. } => obj.contains_tvar(target),
+            Self::ProjCall { obj, args, .. } => {
+                obj.contains_tvar(target) || args.iter().any(|t| t.contains_tvar(target))
+            }
             Self::List(ts) | Self::Tuple(ts) => ts.iter().any(|t| t.contains_tvar(target)),
+            Self::UnsizedList(elem) => elem.contains_tvar(target),
             Self::Set(ts) => ts.iter().any(|t| t.contains_tvar(target)),
             Self::Dict(ts) => ts
                 .iter()
@@ -1528,8 +1540,12 @@ impl TyParam {
         }
         match self {
             Self::FreeVar(fv) => {
-                let to = to.clone().eliminate_recursion(self);
-                fv.link(&to);
+                if to.contains_tp(self) {
+                    let to = to.clone().eliminate_recursion(self);
+                    fv.link(&to);
+                } else {
+                    fv.link(to);
+                }
             }
             Self::Type(t) => {
                 if let Ok(to) = <&Type>::try_from(to) {
@@ -1558,8 +1574,12 @@ impl TyParam {
         }
         match self {
             Self::FreeVar(fv) => {
-                let to = to.clone().eliminate_recursion(self);
-                fv.undoable_link(&to);
+                if to.contains_tp(self) {
+                    let to = to.clone().eliminate_recursion(self);
+                    fv.undoable_link(&to);
+                } else {
+                    fv.undoable_link(to);
+                }
             }
             Self::Type(t) => {
                 if let Ok(to) = <&Type>::try_from(to) {
@@ -1672,6 +1692,7 @@ impl TyParam {
             Self::FreeVar(fv) if fv.is_generalized() => {
                 fv.update_init();
             }
+            Self::FreeVar(_) => {}
             Self::Type(t) => t.dereference(),
             Self::Value(val) => val.dereference(),
             Self::App { args, .. } => {
@@ -1729,7 +1750,7 @@ impl TyParam {
                 rhs.dereference();
             }
             Self::Erased(t) => t.dereference(),
-            _ => {}
+            Self::Mono(_) | Self::Failure => {}
         }
     }
 
@@ -1756,6 +1777,7 @@ impl TyParam {
         match self {
             Self::FreeVar(fv) if fv.is_linked() => fv.crack().variables(),
             Self::FreeVar(fv) if fv.get_type().is_some() => fv.get_type().unwrap().variables(),
+            Self::FreeVar(_) => set! {},
             Self::Mono(name) => set! { name.clone() },
             Self::App { name, args } => {
                 let mut set = set! { name.clone() };
@@ -1791,7 +1813,7 @@ impl TyParam {
             }
             Self::Type(t) | Self::Erased(t) => t.variables(),
             Self::Value(val) => val.variables(),
-            _ => set! {},
+            Self::Failure => set! {},
         }
     }
 
@@ -1799,6 +1821,12 @@ impl TyParam {
     pub fn map(self, f: &mut impl FnMut(TyParam) -> TyParam) -> TyParam {
         match self {
             TyParam::FreeVar(fv) if fv.is_linked() => f(fv.unwrap_linked()),
+            TyParam::FreeVar(fv) if fv.get_type().is_some() => {
+                let typ = fv.get_type().unwrap();
+                fv.update_type(typ.map_tp(f));
+                TyParam::FreeVar(fv)
+            }
+            TyParam::FreeVar(_) => self,
             TyParam::App { name, args } => {
                 let new_args = args.into_iter().map(f).collect::<Vec<_>>();
                 TyParam::app(name, new_args)
@@ -1845,13 +1873,21 @@ impl TyParam {
                 args: args.into_iter().map(f).collect::<Vec<_>>(),
             },
             TyParam::Value(val) => TyParam::Value(val.map_tp(f)),
-            self_ => self_,
+            TyParam::Type(t) => TyParam::t(t.map_tp(f)),
+            TyParam::Erased(t) => TyParam::erased(t.map_tp(f)),
+            TyParam::Mono(_) | TyParam::Failure => self,
         }
     }
 
     pub fn map_t(self, f: &mut impl FnMut(Type) -> Type) -> TyParam {
         match self {
             TyParam::FreeVar(fv) if fv.is_linked() => fv.unwrap_linked().map_t(f),
+            TyParam::FreeVar(fv) if fv.get_type().is_some() => {
+                let typ = fv.get_type().unwrap();
+                fv.update_type(f(typ));
+                TyParam::FreeVar(fv)
+            }
+            TyParam::FreeVar(_) => self,
             TyParam::App { name, args } => {
                 let new_args = args.into_iter().map(|tp| tp.map_t(f)).collect::<Vec<_>>();
                 TyParam::app(name, new_args)
@@ -1900,7 +1936,9 @@ impl TyParam {
                 }
             }
             TyParam::Value(val) => TyParam::Value(val.map_t(f)),
-            self_ => self_,
+            TyParam::Type(t) => TyParam::t(f(*t)),
+            TyParam::Erased(t) => TyParam::erased(f(*t)),
+            TyParam::Mono(_) | TyParam::Failure => self,
         }
     }